D5c: Predykaty na listach


From Typonomikon Require Export D5b D1g.

Proste predykaty

elem

Zdefiniuj induktywny predykat elem. elem x l jest spełniony, gdy x jest elementem listy l.


Lemma elem_not_nil :
  forall (A : Type) (x : A), ~ elem x [].

Lemma elem_not_cons :
  forall (A : Type) (x h : A) (t : list A),
    ~ elem x (h :: t) -> x <> h /\ ~ elem x t.

Lemma elem_cons' :
  forall (A : Type) (x h : A) (t : list A),
    elem x (h :: t) <-> x = h \/ elem x t.

Lemma elem_snoc :
  forall (A : Type) (x y : A) (l : list A),
    elem x (snoc y l) <-> elem x l \/ x = y.

Lemma elem_app_l :
  forall (A : Type) (x : A) (l1 l2 : list A),
    elem x l1 -> elem x (l1 ++ l2).

Lemma elem_app_r :
  forall (A : Type) (x : A) (l1 l2 : list A),
    elem x l2 -> elem x (l1 ++ l2).

Lemma elem_or_app :
  forall (A : Type) (x : A) (l1 l2 : list A),
    elem x l1 \/ elem x l2 -> elem x (l1 ++ l2).

Lemma elem_app_or :
  forall (A : Type) (x : A) (l1 l2 : list A),
    elem x (l1 ++ l2) -> elem x l1 \/ elem x l2.

Lemma elem_app :
  forall (A : Type) (x : A) (l1 l2 : list A),
    elem x (l1 ++ l2) <-> elem x l1 \/ elem x l2.

Lemma elem_spec :
  forall (A : Type) (x : A) (l : list A),
    elem x l <-> exists l1 l2 : list A, l = l1 ++ x :: l2.

Lemma elem_map :
  forall (A B : Type) (f : A -> B) (l : list A) (x : A),
    elem x l -> elem (f x) (map f l).

Lemma elem_map_conv :
  forall (A B : Type) (f : A -> B) (l : list A) (y : B),
    elem y (map f l) <-> exists x : A, f x = y /\ elem x l.

Lemma elem_map_conv' :
  forall (A B : Type) (f : A -> B) (l : list A) (x : A),
    (forall x y : A, f x = f y -> x = y) ->
      elem (f x) (map f l) -> elem x l.

Lemma map_ext_elem :
  forall (A B : Type) (f g : A -> B) (l : list A),
    (forall x : A, elem x l -> f x = g x) -> map f l = map g l.

Lemma elem_join :
  forall (A : Type) (x : A) (ll : list (list A)),
    elem x (join ll) <-> exists l : list A, elem x l /\ elem l ll.

Lemma elem_replicate :
  forall (A : Type) (n : nat) (x y : A),
    elem y (replicate n x) <-> n <> 0 /\ x = y.

Lemma nth_elem :
  forall (A : Type) (l : list A) (n : nat),
    n < length l -> exists x : A, nth n l = Some x /\ elem x l.

(* TOOD: ulepszyć? *) Lemma iff_elem_nth :
  forall (A : Type) (x : A) (l : list A),
    elem x l <-> exists n : nat, nth n l = Some x.

Lemma elem_rev_aux :
  forall (A : Type) (x : A) (l : list A),
    elem x l -> elem x (rev l).

Lemma elem_rev :
  forall (A : Type) (x : A) (l : list A),
    elem x (rev l) <-> elem x l.

Lemma elem_remove_nth :
  forall (A : Type) (x : A) (l : list A) (n : nat),
    elem x l -> nth n l <> Some x ->
    match remove n l with
    | None => True
    | Some (_, l') => elem x l'
    end.

Lemma elem_take :
  forall (A : Type) (l : list A) (n : nat) (x : A),
    elem x (take n l) -> elem x l.

Lemma elem_drop :
  forall (A : Type) (l : list A) (n : nat) (x : A),
    elem x (drop n l) -> elem x l.

Lemma elem_splitAt' :
  forall (A : Type) (l l1 l2 : list A) (n : nat) (x y : A),
    splitAt n l = Some (l1, y, l2) ->
      elem x l <-> x = y \/ elem x l1 \/ elem x l2.

Lemma elem_insert :
  forall (A : Type) (l : list A) (n : nat) (x y : A),
    elem y (insert l n x) <-> x = y \/ elem y l.

Lemma elem_replace :
  forall (A : Type) (l l' : list A) (n : nat) (x y : A),
    replace l n x = Some l' ->
      elem y l' <-> elem y (take n l) \/ x = y \/ elem y (drop (S n) l).

Lemma elem_filter :
  forall (A : Type) (p : A -> bool) (l : list A) (x : A),
    elem x (filter p l) <-> p x = true /\ elem x l.

Lemma elem_filter_conv :
  forall (A : Type) (p : A -> bool) (x : A) (l : list A),
    elem x l <->
    elem x (filter p l) /\ p x = true \/
    elem x (filter (fun x : A => negb (p x)) l) /\ p x = false.

Lemma elem_partition :
  forall (A : Type) (p : A -> bool) (x : A) (l l1 l2 : list A),
    partition p l = (l1, l2) ->
      elem x l <->
      (elem x l1 /\ p x = true) \/ (elem x l2 /\ p x = false).

Lemma elem_takeWhile :
  forall (A : Type) (p : A -> bool) (l : list A) (x : A),
    elem x (takeWhile p l) -> elem x l /\ p x = true.

Lemma elem_dropWhile :
  forall (A : Type) (p : A -> bool) (l : list A) (x : A),
    elem x (dropWhile p l) -> elem x l.

Lemma elem_takeWhile_dropWhile :
  forall (A : Type) (p : A -> bool) (l : list A) (x : A),
    elem x l <-> elem x (takeWhile p l) \/ elem x (dropWhile p l).

Lemma elem_dropWhile_conv :
  forall (A : Type) (p : A -> bool) (l : list A) (x : A),
    elem x l -> ~ elem x (dropWhile p l) -> p x = true.


Lemma span_spec' :
  forall (A : Type) (p : A -> bool) (l : list A),
    match span p l with
    | None => forall x : A, elem x l -> p x = false
    | Some (b, x, e) =>
        b = takeWhile (fun x : A => negb (p x)) l /\
        Some x = find p l /\
        x :: e = dropWhile (fun x : A => negb (p x)) l /\
        Some (x, b ++ e) = removeFirst p l
    end.

Lemma elem_span_None :
  forall (A : Type) (p : A -> bool) (l : list A),
    span p l = None -> forall x : A, elem x l -> p x = false.

Lemma elem_span_Some :
  forall (A : Type) (p : A -> bool) (x : A) (l b e : list A),
    span p l = Some (b, x, e) ->
      forall y : A, elem y l <-> elem y b \/ y = x \/ elem y e.

Lemma elem_span :
  forall (A : Type) (p : A -> bool) (l : list A),
    match span p l with
    | None => forall x : A, elem x l -> p x = false
    | Some (b, x, e) =>
        forall y : A, elem y l <-> elem y b \/ y = x \/ elem y e
    end.

Lemma elem_removeFirst_None :
  forall (A : Type) (p : A -> bool) (l : list A),
    removeFirst p l = None ->
      forall x : A, elem x l -> p x = false.

Lemma elem_zip :
  forall (A B : Type) (a : A) (b : B) (la : list A) (lb : list B),
    elem (a, b) (zip la lb) -> elem a la /\ elem b lb.

Lemma zip_not_elem :
  exists (A B : Type) (a : A) (b : B) (la : list A) (lb : list B),
    elem a la /\ elem b lb /\ ~ elem (a, b) (zip la lb).

Lemma elem_findIndices :
  forall (A : Type) (p : A -> bool) (l : list A) (n : nat),
    elem n (findIndices p l) ->
      exists x : A, nth n l = Some x /\ p x = true.

Lemma isEmpty_bind :
  forall (A B : Type) (f : A -> list B) (l : list A),
    isEmpty (bind f l) = true <->
    l = [] \/ l <> [] /\ forall x : A, elem x l -> f x = [].

Lemma elem_pmap :
  forall (A B : Type) (f : A -> option B) (l : list A) (a : A) (b : B),
    f a = Some b -> elem a l -> elem b (pmap f l).

Lemma elem_pmap' :
  forall (A B : Type) (f : A -> option B) (l : list A) (b : B),
    (exists a : A, elem a l /\ f a = Some b) -> elem b (pmap f l).

Lemma elem_pmap_conv :
  forall (A B : Type) (f : A -> option B) (l : list A) (b : B),
    elem b (pmap f l) -> exists a : A, elem a l /\ f a = Some b.

Lemma elem_intersperse :
  forall (A : Type) (x y : A) (l : list A),
    elem x (intersperse y l) <-> elem x l \/ (x = y /\ 2 <= length l).

Lemma elem_interleave :
  forall {A : Type} (x : A) (l1 l2 : list A),
    elem x (interleave l1 l2) <->
    elem x l1 \/ elem x l2.

Lemma groupBy_elem :
  forall (A : Type) (p : A -> A -> bool) (x : A) (l : list A),
    elem x l -> exists g : list A, elem x g /\ elem g (groupBy p l).

Lemma groupBy_elem_nil :
  forall (A : Type) (p : A -> A -> bool) (l : list A),
    ~ elem [] (groupBy p l).

Lemma elem_insert_before_in :
  forall (A : Type) (x : A) (l1 l2 : list A) (n : nat),
    elem x (insertBefore.insertBefore n l1 l2) <->
    elem x l1 \/ elem x l2.

In

Gratuluję, udało ci się zdefiniować predykat elem i dowieść wszystkich jego właściwości. To jednak nie koniec zabawy, gdyż predykaty możemy definiować nie tylko przez indukcję, ale także przez rekursję. Być może taki sposób definiowania jest nawet lepszy? Przyjrzyjmy się poniższej definicji — tak właśnie "bycie elementem" jest zdefiniowane w bibliotece standardowej.

Fixpoint In {A : Type} (x : A) (l : list A) : Prop :=
match l with
| [] => False
| h :: t => x = h \/ In x t
end.

Powyższa definicja jest bardzo podobna do tej induktywnej. In x dla listy pustej redukuje się do False, co oznacza, że w pustej liście nic nie ma, zaś dla listy mającej głowę i ogon redukuje się do zdania "x jest głową lub jest elementem ogona".
Definicja taka ma swoje wady i zalety. Największą moim zdaniem wadą jest to, że nie możemy robić indukcji po dowodzie, gdyż dowód faktu In x l nie jest induktywny. Największą zaletą zaś jest fakt, że nie możemy robić indukcji po dowodzie — im mniej potencjalnych rzeczy, po których można robić indukcję, tym mniej zastanawiania się. Przekonajmy się zatem na własnej skórze, która definicja jest "lepsza".

Lemma In_elem :
  forall (A : Type) (x : A) (l : list A),
    In x l <-> elem x l.

Lemma In_not_nil :
  forall (A : Type) (x : A), ~ In x [].

Lemma In_not_cons :
  forall (A : Type) (x h : A) (t : list A),
    ~ In x (h :: t) -> x <> h /\ ~ In x t.

Lemma In_cons :
  forall (A : Type) (x h : A) (t : list A),
    In x (h :: t) <-> x = h \/ In x t.

Lemma In_snoc :
  forall (A : Type) (x y : A) (l : list A),
    In x (snoc y l) <-> In x l \/ x = y.

Lemma In_app_l :
  forall (A : Type) (x : A) (l1 l2 : list A),
    In x l1 -> In x (l1 ++ l2).

Lemma In_app_r :
  forall (A : Type) (x : A) (l1 l2 : list A),
    In x l2 -> In x (l1 ++ l2).

Lemma In_or_app :
  forall (A : Type) (x : A) (l1 l2 : list A),
    In x l1 \/ In x l2 -> In x (l1 ++ l2).

Lemma In_app_or :
  forall (A : Type) (x : A) (l1 l2 : list A),
    In x (l1 ++ l2) -> In x l1 \/ In x l2.

Lemma In_app :
  forall (A : Type) (x : A) (l1 l2 : list A),
    In x (l1 ++ l2) <-> In x l1 \/ In x l2.

Lemma In_spec :
  forall (A : Type) (x : A) (l : list A),
    In x l <-> exists l1 l2 : list A, l = l1 ++ x :: l2.

Lemma In_map :
  forall (A B : Type) (f : A -> B) (l : list A) (x : A),
    In x l -> In (f x) (map f l).

Lemma In_map_conv :
  forall (A B : Type) (f : A -> B) (l : list A) (y : B),
    In y (map f l) <-> exists x : A, f x = y /\ In x l.

Lemma In_map_conv' :
  forall (A B : Type) (f : A -> B) (l : list A) (x : A),
    (forall x y : A, f x = f y -> x = y) ->
      In (f x) (map f l) -> In x l.

Lemma map_ext_In :
  forall (A B : Type) (f g : A -> B) (l : list A),
    (forall x : A, In x l -> f x = g x) -> map f l = map g l.

Lemma In_join :
  forall (A : Type) (x : A) (ll : list (list A)),
    In x (join ll) <->
    exists l : list A, In x l /\ In l ll.

Lemma In_replicate :
  forall (A : Type) (n : nat) (x y : A),
    In y (replicate n x) <-> n <> 0 /\ x = y.

Lemma In_iterate :
  forall (A : Type) (f : A -> A) (n : nat) (x y : A),
    In y (iterate f n x) <-> exists k : nat, k < n /\ y = iter f k x.

Lemma nth_In :
  forall (A : Type) (l : list A) (n : nat),
    n < length l -> exists x : A, nth n l = Some x /\ In x l.

Lemma iff_In_nth :
  forall (A : Type) (x : A) (l : list A),
    In x l <-> exists n : nat, nth n l = Some x.

Lemma In_rev :
  forall (A : Type) (x : A) (l : list A),
    In x (rev l) <-> In x l.

Lemma In_take :
  forall (A : Type) (l : list A) (n : nat) (x : A),
    In x (take n l) -> In x l.

Lemma In_drop :
  forall (A : Type) (l : list A) (n : nat) (x : A),
    In x (drop n l) -> In x l.

Lemma In_splitAt :
  forall (A : Type) (l b e : list A) (n : nat) (x y : A),
    splitAt n l = Some (b, x, e) ->
      In y l <-> In y b \/ x = y \/ In y e.

Lemma In_insert :
  forall (A : Type) (l : list A) (n : nat) (x y : A),
    In y (insert l n x) <-> x = y \/ In y l.

Lemma In_replace :
  forall (A : Type) (l l' : list A) (n : nat) (x y : A),
    replace l n x = Some l' ->
      In y l' <-> In y (take n l) \/ x = y \/ In y (drop (S n) l).

Lemma In_filter :
  forall (A : Type) (p : A -> bool) (l : list A) (x : A),
    In x (filter p l) <-> p x = true /\ In x l.

Lemma In_filter_conv :
  forall (A : Type) (p : A -> bool) (x : A) (l : list A),
    In x l <->
    In x (filter p l) /\ p x = true \/
    In x (filter (fun x : A => negb (p x)) l) /\ p x = false.

Lemma In_partition :
  forall (A : Type) (p : A -> bool) (x : A) (l l1 l2 : list A),
    partition p l = (l1, l2) ->
      In x l <->
      (In x l1 /\ p x = true) \/ (In x l2 /\ p x = false).

Lemma In_takeWhile :
  forall (A : Type) (p : A -> bool) (l : list A) (x : A),
    In x (takeWhile p l) -> In x l /\ p x = true.

Lemma In_dropWhile :
  forall (A : Type) (p : A -> bool) (l : list A) (x : A),
    In x (dropWhile p l) -> In x l.

Lemma In_takeWhile_dropWhile :
  forall (A : Type) (p : A -> bool) (l : list A) (x : A),
    In x l ->
      In x (takeWhile p l) \/
      In x (dropWhile p l).

Lemma In_dropWhile_conv :
  forall (A : Type) (p : A -> bool) (l : list A) (x : A),
    In x l -> ~ In x (dropWhile p l) -> p x = true.

Lemma In_span :
  forall (A : Type) (p : A -> bool) (x y : A) (l b e : list A),
    span p l = Some (b, x, e) ->
      In y l <-> In y b \/ y = x \/ In y e.

Lemma In_zip :
  forall (A B : Type) (a : A) (b : B) (la : list A) (lb : list B),
    In (a, b) (zip la lb) -> In a la /\ In b lb.

Lemma zip_not_In :
  exists (A B : Type) (a : A) (b : B) (la : list A) (lb : list B),
    In a la /\ In b lb /\ ~ In (a, b) (zip la lb).

Lemma In_intersperse :
  forall (A : Type) (x y : A) (l : list A),
    In x (intersperse y l) <->
    In x l \/ (x = y /\ 2 <= length l).

Lemma In_insert_before_in :
  forall (A : Type) (x : A) (l1 l2 : list A) (n : nat),
    In x (insertBefore.insertBefore n l1 l2) <->
    In x l1 \/ In x l2.

NoDup

Zdefiniuj induktywny predykat NoDup. Zdanie NoDup l jest prawdziwe, gdy w l nie ma powtarzających się elementów. Udowodnij, że zdefiniowany przez ciebie predykat posiada pożądane właściwości.


Lemma NoDup_singl :
  forall (A : Type) (x : A), NoDup [x].

Lemma NoDup_cons_inv :
  forall (A : Type) (h : A) (t : list A),
    NoDup (h :: t) -> NoDup t.

Lemma NoDup_length :
  forall (A : Type) (l : list A),
    ~ NoDup l -> 2 <= length l.

Lemma NoDup_snoc :
  forall (A : Type) (x : A) (l : list A),
    NoDup (snoc x l) <-> NoDup l /\ ~ elem x l.

Lemma NoDup_app :
  forall (A : Type) (l1 l2 : list A),
    NoDup (l1 ++ l2) <->
    NoDup l1 /\
    NoDup l2 /\
    (forall x : A, elem x l1 -> ~ elem x l2) /\
    (forall x : A, elem x l2 -> ~ elem x l1).

Lemma NoDup_app_comm :
  forall (A : Type) (l1 l2 : list A),
    NoDup (l1 ++ l2) <-> NoDup (l2 ++ l1).

Lemma NoDup_rev :
  forall (A : Type) (l : list A),
    NoDup (rev l) <-> NoDup l.

Lemma NoDup_map :
  forall (A B : Type) (f : A -> B) (l : list A),
    NoDup (map f l) -> NoDup l.

Lemma NoDup_map_inj :
  forall (A B : Type) (f : A -> B) (l : list A),
    (forall x y : A, f x = f y -> x = y) ->
      NoDup l -> NoDup (map f l).

Lemma NoDup_replicate :
  forall (A : Type) (n : nat) (x : A),
    NoDup (replicate n x) <-> n = 0 \/ n = 1.

Lemma NoDup_take :
  forall (A : Type) (l : list A) (n : nat),
    NoDup l -> NoDup (take n l).

Lemma NoDup_drop :
  forall (A : Type) (l : list A) (n : nat),
    NoDup l -> NoDup (drop n l).

Lemma NoDup_filter :
  forall (A : Type) (p : A -> bool) (l : list A),
    NoDup l -> NoDup (filter p l).

Lemma NoDup_partition :
  forall (A : Type) (p : A -> bool) (l l1 l2 : list A),
    partition p l = (l1, l2) -> NoDup l <-> NoDup l1 /\ NoDup l2.

Lemma NoDup_takeWhile :
  forall (A : Type) (p : A -> bool) (l : list A),
    NoDup l -> NoDup (takeWhile p l).

Lemma NoDup_dropWhile :
  forall (A : Type) (p : A -> bool) (l : list A),
    NoDup l -> NoDup (dropWhile p l).

Lemma NoDup_zip :
  forall (A B : Type) (la : list A) (lb : list B),
    NoDup la /\ NoDup lb -> NoDup (zip la lb).

Lemma NoDup_zip_conv :
  exists (A B : Type) (la : list A) (lb : list B),
    NoDup (zip la lb) /\ ~ NoDup la /\ ~ NoDup lb.

Lemma NoDup_pmap :
  exists (A B : Type) (f : A -> option B) (l : list A),
    NoDup l /\ ~ NoDup (pmap f l).

Lemma NoDup_intersperse :
  forall (A : Type) (x : A) (l : list A),
    NoDup (intersperse x l) -> length l <= 2.

Lemma NoDup_spec :
  forall (A : Type) (l : list A),
    ~ NoDup l <->
    exists (x : A) (l1 l2 l3 : list A),
      l = l1 ++ x :: l2 ++ x :: l3.

Dup

Powodem problemów z predykatem NoDup jest fakt, że jest on w pewnym sensie niekonstruktywny. Wynika to wprost z jego definicji: NoDup l zachodzi, gdy w l nie ma duplikatów. Parafrazując: NoDup l zachodzi, gdy nieprawda, że w l są duplikaty.
Jak widać, w naszej definicji implicite występuje negacja. Wobec tego jeżeli spróbujemy za pomocą NoDup wyrazić zdanie "na liście l są duplikaty", to tak naprawdę dostaniemy zdanie "nieprawda, że nieprawda, że l ma duplikaty".
Dostaliśmy więc po głowie nagłym atakiem podwójnej negacji. Nie ma się co dziwić w takiej sytuacji, że nasza "negatywna" definicja predykatu NoDup jest nazbyt klasyczna. Możemy jednak uratować sytuację, jeżeli zdefiniujemy predykat Dup i zanegujemy go.
Zdefiniuj predykat Dup, który jest spełniony, gdy na liście występują duplikaty.


Lemma Dup_nil :
  forall A : Type, ~ Dup (@nil A).

Lemma Dup_cons :
  forall (A : Type) (x : A) (l : list A),
    Dup (x :: l) <-> elem x l \/ Dup l.

Lemma Dup_singl :
  forall (A : Type) (x : A), ~ Dup [x].

Lemma Dup_cons_inv :
  forall (A : Type) (h : A) (t : list A),
    ~ Dup (h :: t) -> ~ elem h t /\ ~ Dup t.

Lemma Dup_spec :
  forall (A : Type) (l : list A),
    Dup l <->
    exists (x : A) (l1 l2 l3 : list A),
      l = l1 ++ x :: l2 ++ x :: l3.

Lemma Dup_NoDup :
  forall (A : Type) (l : list A),
    ~ Dup l <-> NoDup l.

Lemma Dup_length :
  forall (A : Type) (l : list A),
    Dup l -> 2 <= length l.

Lemma Dup_snoc :
  forall (A : Type) (x : A) (l : list A),
    Dup (snoc x l) <-> Dup l \/ elem x l.

Lemma Dup_app_l :
  forall (A : Type) (l1 l2 : list A),
    Dup l1 -> Dup (l1 ++ l2).

Lemma Dup_app_r :
  forall (A : Type) (l1 l2 : list A),
    Dup l2 -> Dup (l1 ++ l2).

Lemma Dup_app_both :
  forall (A : Type) (x : A) (l1 l2 : list A),
    elem x l1 -> elem x l2 -> Dup (l1 ++ l2).

Lemma Dup_app :
  forall (A : Type) (l1 l2 : list A),
    Dup (l1 ++ l2) <->
    Dup l1 \/ Dup l2 \/ exists x : A, elem x l1 /\ elem x l2.

Lemma Dup_rev :
  forall (A : Type) (l : list A),
    Dup (rev l) <-> Dup l.

Lemma Dup_map :
  forall (A B : Type) (f : A -> B) (l : list A),
    Dup l -> Dup (map f l).

Lemma Dup_map_conv :
  forall (A B : Type) (f : A -> B) (l : list A),
    (forall x y : A, f x = f y -> x = y) ->
      Dup (map f l) -> Dup l.

Lemma Dup_join :
  forall (A : Type) (ll : list (list A)),
    Dup (join ll) ->
    (exists l : list A, elem l ll /\ Dup l) \/
    (exists (x : A) (l1 l2 : list A),
      elem x l1 /\ elem x l2 /\ elem l1 ll /\ elem l2 ll).

Lemma Dup_replicate :
  forall (A : Type) (n : nat) (x : A),
    Dup (replicate n x) -> 2 <= n.

Lemma Dup_nth :
  forall (A : Type) (l : list A),
    Dup l <->
    exists (x : A) (n1 n2 : nat),
      n1 < n2 /\ nth n1 l = Some x /\ nth n2 l = Some x.

Lemma Dup_take :
  forall (A : Type) (l : list A) (n : nat),
    Dup (take n l) -> Dup l.

Lemma Dup_drop :
  forall (A : Type) (l : list A) (n : nat),
    Dup (drop n l) -> Dup l.


Lemma Dup_filter :
  forall (A : Type) (p : A -> bool) (l : list A),
    Dup (filter p l) -> Dup l.

Lemma Dup_filter_conv :
  forall (A : Type) (p : A -> bool) (l : list A),
    Dup l ->
      Dup (filter p l) \/
      Dup (filter (fun x : A => negb (p x)) l).

Lemma Dup_partition :
  forall (A : Type) (p : A -> bool) (l l1 l2 : list A),
    partition p l = (l1, l2) -> Dup l <-> Dup l1 \/ Dup l2.

Lemma Dup_takeWhile :
  forall (A : Type) (p : A -> bool) (l : list A),
    Dup (takeWhile p l) -> Dup l.

Lemma Dup_dropWhile :
  forall (A : Type) (p : A -> bool) (l : list A),
    Dup (dropWhile p l) -> Dup l.

Lemma Dup_takeWhile_dropWhile_conv :
  forall (A : Type) (p : A -> bool) (l : list A),
    Dup l ->
      Dup (takeWhile p l) \/
      Dup (dropWhile p l) \/
      exists x : A,
        elem x (takeWhile p l) /\ elem x (dropWhile p l).

Lemma Dup_span :
  forall (A : Type) (p : A -> bool) (x : A) (l b e : list A),
    span p l = Some (b, x, e) ->
      Dup l <-> Dup b \/ Dup e \/ elem x b \/ elem x e \/
        exists y : A, elem y b /\ elem y e.


Lemma Dup_zip :
  forall (A B : Type) (la : list A) (lb : list B),
    Dup (zip la lb) -> Dup la /\ Dup lb.

Lemma Dup_zip_conv :
  forall (A B : Type) (la : list A) (lb : list B),
    ~ Dup la /\ ~ Dup lb -> ~ Dup (zip la lb).

Lemma Dup_pmap :
  exists (A B : Type) (f : A -> option B) (l : list A),
    Dup l /\ ~ Dup (pmap f l).

Lemma Dup_intersperse :
  forall (A : Type) (x : A) (l : list A),
    Dup (intersperse x l) -> 2 <= length l.

Lemma Dup_interleave :
  forall {A : Type} (l1 l2 : list A),
    Dup (interleave l1 l2) <->
    Dup l1 \/ Dup l2 \/ exists x : A, elem x l1 /\ elem x l2.

Rep

Jeżeli zastanowimy się chwilę, to dojdziemy do wniosku, że Dup l znaczy "istnieje x, który występuje na liście l co najmniej dwa razy". Widać więc, że Dup jest jedynie specjalnym przypadkiem pewngo bardziej ogólnego predykatu Rep x n dla dowolnego x oraz n = 2. Zdefiniuj relację Rep. Zdanie Rep x n l zachodzi, gdy element x występuje na liście l co najmnej n razy.
Zastanów się, czy lepsza będzie definicja induktywna, czy rekurencyjna. Jeżeli nie masz nic lepszego do roboty, zaimplementuj obie wersje i porównaj je pod względem łatwości w użyciu.


Lemma Rep_S_cons :
  forall (A : Type) (x y : A) (n : nat) (l : list A),
    Rep x (S n) (y :: l) <-> (x = y /\ Rep x n l) \/ Rep x (S n) l.

Lemma Rep_cons :
  forall (A : Type) (x y : A) (n : nat) (l : list A),
    Rep x n (y :: l) <-> (x = y /\ Rep x (n - 1) l) \/ Rep x n l.

Lemma elem_Rep :
  forall (A : Type) (x : A) (l : list A),
    elem x l -> Rep x 1 l.

Lemma Rep_elem :
  forall (A : Type) (x : A) (n : nat) (l : list A),
    1 <= n -> Rep x n l -> elem x l.

Lemma Dup_Rep :
  forall (A : Type) (l : list A),
    Dup l -> exists x : A, Rep x 2 l.

Lemma Rep_Dup :
  forall (A : Type) (x : A) (n : nat) (l : list A),
    2 <= n -> Rep x n l -> Dup l.

Lemma Rep_le :
  forall (A : Type) (x : A) (n m : nat) (l : list A),
    n <= m -> Rep x m l -> Rep x n l.

Lemma Rep_S_inv :
  forall (A : Type) (x : A) (n : nat) (l : list A),
    Rep x (S n) l -> Rep x n l.

Lemma Rep_length :
  forall (A : Type) (x : A) (n : nat) (l : list A),
    Rep x n l -> n <= length l.

Lemma Rep_S_snoc :
  forall (A : Type) (x : A) (n : nat) (l : list A),
    Rep x n l -> Rep x (S n) (snoc x l).

Lemma Rep_snoc :
  forall (A : Type) (x y : A) (n : nat) (l : list A),
    Rep x n l -> Rep x n (snoc y l).

Lemma Rep_app_l :
  forall (A : Type) (x : A) (n : nat) (l1 l2 : list A),
    Rep x n l1 -> Rep x n (l1 ++ l2).

Lemma Rep_app_r :
  forall (A : Type) (x : A) (n : nat) (l1 l2 : list A),
    Rep x n l2 -> Rep x n (l1 ++ l2).

Lemma Rep_app :
  forall (A : Type) (x : A) (n1 n2 : nat) (l1 l2 : list A),
    Rep x n1 l1 -> Rep x n2 l2 -> Rep x (n1 + n2) (l1 ++ l2).

Lemma Rep_app_conv :
  forall (A : Type) (x : A) (n : nat) (l1 l2 : list A),
    Rep x n (l1 ++ l2) <->
      exists n1 n2 : nat,
        Rep x n1 l1 /\ Rep x n2 l2 /\ n = n1 + n2.

Lemma Rep_rev :
  forall (A : Type) (x : A) (n : nat) (l : list A),
    Rep x n (rev l) <-> Rep x n l.

Lemma Rep_map :
  forall (A B : Type) (f : A -> B) (x : A) (n : nat) (l : list A),
    Rep x n l -> Rep (f x) n (map f l).

Lemma Rep_map_conv :
  forall (A B : Type) (f : A -> B) (x : A) (n : nat) (l : list A),
    (forall x y : A, f x = f y -> x = y) ->
      Rep (f x) n (map f l) -> Rep x n l.

Lemma Rep_replicate :
  forall (A : Type) (x : A) (n : nat),
    Rep x n (replicate n x).

Lemma Rep_replicate_general :
  forall (A : Type) (x : A) (n m : nat),
    n <= m -> Rep x n (replicate m x).

Lemma Rep_take :
  forall (A : Type) (x : A) (l : list A) (n m : nat),
    Rep x n (take m l) -> Rep x n l.

Lemma Rep_drop :
  forall (A : Type) (x : A) (l : list A) (n m : nat),
    Rep x n (drop m l) -> Rep x n l.

Lemma Rep_filter :
  forall (A : Type) (p : A -> bool) (x : A) (n : nat) (l : list A),
    Rep x n (filter p l) -> Rep x n l.

Lemma Rep_filter_true :
  forall (A : Type) (p : A -> bool) (x : A) (n : nat) (l : list A),
    p x = true -> Rep x n l -> Rep x n (filter p l).

Lemma Rep_filter_false :
  forall (A : Type) (p : A -> bool) (x : A) (l : list A) (n : nat),
    p x = false -> Rep x n (filter p l) -> n = 0.

Lemma Rep_takeWhile :
  forall (A : Type) (p : A -> bool) (x : A) (l : list A) (n : nat),
    Rep x n (takeWhile p l) -> Rep x n l.

Lemma Rep_dropWhile :
  forall (A : Type) (p : A -> bool) (x : A) (l : list A) (n : nat),
    Rep x n (dropWhile p l) -> Rep x n l.

Lemma Rep_zip :
  forall (A B : Type) (a : A) (b : B) (la : list A) (lb : list B) (n : nat),
    Rep (a, b) n (zip la lb) -> Rep a n la /\ Rep b n lb.

#[global] Hint Constructors Rep : core.

Lemma Rep_intersperse :
  forall (A : Type) (x y : A) (n : nat) (l : list A),
    Rep x n (intersperse y l) <->
    Rep x n l \/ x = y /\ Rep x (S n - length l) l.

Exists

Zaimplementuj induktywny predykat Exists. Exists P l zachodzi, gdy lista l zawiera taki element, który spełnia predykat P.


Lemma Exists_spec :
  forall (A : Type) (P : A -> Prop) (l : list A),
    Exists P l <-> exists x : A, elem x l /\ P x.

Lemma elem_Exists :
  forall {A : Type} {x : A} {l : list A},
    elem x l <-> Exists (fun y => x = y) l.

Lemma Exists_nil :
  forall (A : Type) (P : A -> Prop),
    Exists P [] <-> False.

Lemma Exists_cons :
  forall (A : Type) (P : A -> Prop) (h : A) (t : list A),
    Exists P (h :: t) <-> P h \/ Exists P t.

Lemma Exists_length :
  forall (A : Type) (P : A -> Prop) (l : list A),
    Exists P l -> 1 <= length l.

Lemma Exists_snoc :
  forall (A : Type) (P : A -> Prop) (x : A) (l : list A),
    Exists P (snoc x l) <-> Exists P l \/ P x.

Lemma Exists_app :
  forall (A : Type) (P : A -> Prop) (l1 l2 : list A),
    Exists P (l1 ++ l2) <-> Exists P l1 \/ Exists P l2.

Lemma Exists_rev :
  forall (A : Type) (P : A -> Prop) (l : list A),
    Exists P (rev l) <-> Exists P l.

Lemma Exists_map :
  forall (A B : Type) (P : B -> Prop) (f : A -> B) (l : list A),
    Exists P (map f l) -> Exists (fun x : A => P (f x)) l.

Lemma Exists_join :
  forall (A : Type) (P : A -> Prop) (ll : list (list A)),
    Exists P (join ll) <->
    Exists (fun l : list A => Exists P l) ll.

Lemma Exists_replicate :
  forall (A : Type) (P : A -> Prop) (n : nat) (x : A),
    Exists P (replicate n x) <-> 1 <= n /\ P x.

Lemma Exists_nth :
  forall (A : Type) (P : A -> Prop) (l : list A),
    Exists P l <->
    exists (n : nat) (x : A), nth n l = Some x /\ P x.

Lemma Exists_remove :
  forall (A : Type) (P : A -> Prop) (l : list A) (n : nat),
    Exists P l ->
    match remove n l with
    | None => True
    | Some (x, l') => ~ P x -> Exists P l'
    end.

Lemma Exists_take :
  forall (A : Type) (P : A -> Prop) (l : list A) (n : nat),
    Exists P (take n l) -> Exists P l.

Lemma Exists_drop :
  forall (A : Type) (P : A -> Prop) (l : list A) (n : nat),
    Exists P (drop n l) -> Exists P l.

Lemma Exists_take_drop :
  forall (A : Type) (P : A -> Prop) (l : list A) (n : nat),
    Exists P l -> Exists P (take n l) \/ Exists P (drop n l).

Lemma Exists_cycle :
  forall (A : Type) (P : A -> Prop) (n : nat) (l : list A),
    Exists P (cycle n l) <-> Exists P l.

Lemma Exists_splitAt :
  forall (A : Type) (P : A -> Prop) (l l1 l2 : list A) (n : nat) (x : A),
    splitAt n l = Some (l1, x, l2) ->
      Exists P l <-> P x \/ Exists P l1 \/ Exists P l2.

Lemma Exists_insert :
  forall (A : Type) (P : A -> Prop) (l : list A) (n : nat) (x : A),
    Exists P (insert l n x) <-> P x \/ Exists P l.

Lemma Exists_replace :
  forall (A : Type) (P : A -> Prop) (l l' : list A) (n : nat) (x : A),
    replace l n x = Some l' ->
      Exists P l' <->
      Exists P (take n l) \/ P x \/ Exists P (drop (S n) l).

Lemma Exists_filter :
  forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
    Exists P (filter p l) -> Exists P l.

Lemma Exists_filter_conv :
  forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
    Exists P l ->
      Exists P (filter p l) \/
      Exists P (filter (fun x : A => negb (p x)) l).

Lemma Exists_filter_compat :
  forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
    (forall x : A, P x <-> p x = false) -> ~ Exists P (filter p l).

Lemma Exists_partition :
  forall (A : Type) (P : A -> Prop) (p : A -> bool) (l l1 l2 : list A),
    partition p l = (l1, l2) ->
      Exists P l <-> Exists P l1 \/ Exists P l2.

Lemma Exists_takeWhile :
  forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
    Exists P (takeWhile p l) -> Exists P l.

Lemma Exists_takeWhile_compat :
  forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
    (forall x : A, P x <-> p x = false) -> ~ Exists P (takeWhile p l).

Lemma Exists_dropWhile :
  forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
    Exists P (dropWhile p l) -> Exists P l.

Lemma Exists_takeWhile_dropWhile :
  forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
    Exists P l -> Exists P (takeWhile p l) \/ Exists P (dropWhile p l).

Lemma Exists_span :
  forall
    (A : Type) (P : A -> Prop) (p : A -> bool) (x : A) (l b e : list A),
      (forall x : A, P x <-> p x = true) ->
      span p l = Some (b, x, e) ->
        Exists P l <-> Exists P b \/ P x \/ Exists P e.

Lemma Exists_interesting :
  forall (A B : Type) (P : A * B -> Prop) (la : list A) (hb : B) (tb : list B),
    Exists (fun a : A => Exists (fun b : B => P (a, b)) tb) la ->
    Exists (fun a : A => Exists (fun b : B => P (a, b)) (hb :: tb)) la.

Lemma Exists_zip :
  forall (A B : Type) (P : A * B -> Prop) (la : list A) (lb : list B),
    Exists P (zip la lb) ->
      Exists (fun a : A => Exists (fun b : B => P (a, b)) lb) la.

Lemma Exists_pmap :
  forall (A B : Type) (f : A -> option B) (P : B -> Prop) (l : list A),
    Exists P (pmap f l) <->
      Exists (fun x : A => match f x with | Some b => P b | _ => False end) l.

Lemma Exists_intersperse :
  forall (A : Type) (P : A -> Prop) (x : A) (l : list A),
    Exists P (intersperse x l) <->
    Exists P l \/ (P x /\ 2 <= length l).

Lemma Exists_interleave :
  forall {A : Type} (P : A -> Prop) (l1 l2 : list A),
    Exists P (interleave l1 l2) <->
    Exists P l1 \/ Exists P l2.

Lemma Exists_insert_before_in :
  forall (A : Type) (P : A -> Prop) (l1 l2 : list A) (n : nat),
    Exists P (insertBefore.insertBefore n l1 l2) <->
    Exists P l1 \/ Exists P l2.

Forall

Zaimplementuj induktywny predykat Forall. Forall P l jest spełniony, gdy każdy element listy l spełnia predykat P.


Lemma Forall_spec :
  forall (A : Type) (P : A -> Prop) (l : list A),
    Forall P l <-> forall x : A, elem x l -> P x.

Lemma Forall_nil :
  forall (A : Type) (P : A -> Prop),
    Forall P [] <-> True.

Lemma Forall_cons :
  forall (A : Type) (P : A -> Prop) (h : A) (t : list A),
    Forall P (h :: t) <-> P h /\ Forall P t.

Lemma Forall_snoc :
  forall (A : Type) (P : A -> Prop) (x : A) (l : list A),
    Forall P (snoc x l) <-> Forall P l /\ P x.

Lemma Forall_app :
  forall (A : Type) (P : A -> Prop) (l1 l2 : list A),
    Forall P (l1 ++ l2) <-> Forall P l1 /\ Forall P l2.

Lemma Forall_rev :
  forall (A : Type) (P : A -> Prop) (l : list A),
    Forall P (rev l) <-> Forall P l.

Lemma Forall_map :
  forall (A B : Type) (P : B -> Prop) (f : A -> B) (l : list A),
    Forall P (map f l) -> Forall (fun x : A => P (f x)) l.

Lemma Forall_join :
  forall (A : Type) (P : A -> Prop) (ll : list (list A)),
    Forall P (join ll) <-> Forall (fun l : list A => Forall P l) ll.

Lemma Forall_replicate :
  forall (A : Type) (P : A -> Prop) (n : nat) (x : A),
    Forall P (replicate n x) <-> n = 0 \/ P x.

Lemma Forall_nth :
  forall (A : Type) (P : A -> Prop) (l : list A),
    Forall P l <-> forall n : nat, n < length l ->
      exists x : A, nth n l = Some x /\ P x.

Lemma Forall_remove :
  forall (A : Type) (P : A -> Prop) (l : list A) (n : nat),
    Forall P l ->
    match remove n l with
    | None => True
    | Some (x, l') => Forall P l'
    end.

Lemma Forall_take :
  forall (A : Type) (P : A -> Prop) (l : list A) (n : nat),
    Forall P l -> Forall P (take n l).

Lemma Forall_drop :
  forall (A : Type) (P : A -> Prop) (l : list A) (n : nat),
    Forall P l -> Forall P (drop n l).

Lemma Forall_take_drop :
  forall (A : Type) (P : A -> Prop) (l : list A) (n : nat),
    Forall P (take n l) -> Forall P (drop n l) -> Forall P l.

Lemma Forall_splitAt :
  forall (A : Type) (P : A -> Prop) (l l1 l2 : list A) (n : nat) (x : A),
    splitAt n l = Some (l1, x, l2) ->
      Forall P l <-> P x /\ Forall P l1 /\ Forall P l2.

Lemma Forall_insert :
  forall (A : Type) (P : A -> Prop) (l : list A) (n : nat) (x : A),
      Forall P (insert l n x) <-> P x /\ Forall P l.

Lemma Forall_replace :
  forall (A : Type) (P : A -> Prop) (l l' : list A) (n : nat) (x : A),
    replace l n x = Some l' ->
      Forall P l' <->
      Forall P (take n l) /\ P x /\ Forall P (drop (S n) l).

Lemma Forall_filter :
  forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
    Forall P l -> Forall P (filter p l).

Lemma Forall_filter_conv :
  forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
    Forall P (filter p l) ->
    Forall P (filter (fun x : A => negb (p x)) l) ->
      Forall P l.

Lemma Forall_filter_compat :
  forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
    (forall x : A, P x <-> p x = true) -> Forall P (filter p l).

Lemma Forall_partition :
  forall (A : Type) (P : A -> Prop) (p : A -> bool) (l l1 l2 : list A),
    partition p l = (l1, l2) ->
      Forall P l <-> Forall P l1 /\ Forall P l2.

Lemma Forall_takeWhile :
  forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
    Forall P l -> Forall P (takeWhile p l).

Lemma Forall_takeWhile_compat :
  forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
    (forall x : A, P x <-> p x = true) -> Forall P (takeWhile p l).

Lemma Forall_dropWhile :
  forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
    Forall P l -> Forall P (dropWhile p l).

Lemma Forall_takeWhile_dropWhile :
  forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
    Forall P (takeWhile p l) -> Forall P (dropWhile p l) -> Forall P l.

Lemma Forall_span :
  forall
    (A : Type) (P : A -> Prop) (p : A -> bool) (x : A) (l b e : list A),
      (forall x : A, P x <-> p x = true) ->
      span p l = Some (b, x, e) ->
        Forall P l <-> Forall P b /\ P x /\ Forall P e.

Lemma Forall_zip :
  forall (A B : Type) (PA : A -> Prop) (PB : B -> Prop)
  (la : list A) (lb : list B),
    Forall PA la -> Forall PB lb ->
      Forall (fun '(a, b) => PA a /\ PB b) (zip la lb).

Lemma Forall_pmap :
  forall (A B : Type) (f : A -> option B) (P : B -> Prop) (l : list A),
    Forall (fun x : A => match f x with | Some b => P b | _ => False end) l ->
      Forall P (pmap f l).

Lemma Forall_intersperse :
  forall (A : Type) (P : A -> Prop) (x : A) (l : list A),
    Forall P (intersperse x l) <->
    Forall P l /\ (2 <= length l -> P x).

Lemma Forall_interleave :
  forall {A : Type} (P : A -> Prop) (l1 l2 : list A),
    Forall P (interleave l1 l2) <->
    Forall P l1 /\ Forall P l2.

Lemma Forall_insert_before_in :
  forall (A : Type) (P : A -> Prop) (l1 l2 : list A) (n : nat),
    Forall P (insertBefore.insertBefore n l1 l2) <->
    Forall P l1 /\ Forall P l2.

Lemma Forall_impl :
  forall (A : Type) (P Q : A -> Prop) (l : list A),
    (forall x : A , P x -> Q x) ->
      Forall P l -> Forall Q l.

Lemma Forall_Exists :
  forall (A : Type) (P : A -> Prop) (l : list A),
    Forall P l -> ~ Exists (fun x : A => ~ P x) l.

Lemma Exists_Forall :
  forall (A : Type) (P : A -> Prop) (l : list A),
    Exists P l -> ~ Forall (fun x : A => ~ P x) l.

AtLeast

Czas uogólnić relację Rep oraz predykaty Exists i Forall. Zdefiniuj w tym celu relację AtLeast. Zdanie AtLeast P n l zachodzi, gdy na liście l jest co najmniej n elementów spełniających predykat P.


Lemma AtLeast_cons :
  forall (A : Type) (P : A -> Prop) (n : nat) (h : A) (t : list A),
    AtLeast P n (h :: t) <->
    AtLeast P n t \/ P h /\ AtLeast P (n - 1) t.

Lemma AtLeast_cons' :
  forall (A : Type) (P : A -> Prop) (n : nat) (h : A) (t : list A),
    AtLeast P (S n) (h :: t) -> AtLeast P n t.

Lemma AtLeast_length :
  forall (A : Type) (P : A -> Prop) (n : nat) (l : list A),
    AtLeast P n l -> n <= length l.

Lemma AtLeast_snoc :
  forall (A : Type) (P : A -> Prop) (n : nat) (x : A) (l : list A),
    AtLeast P n l -> AtLeast P n (snoc x l).

Lemma AtLeast_S_snoc :
  forall (A : Type) (P : A -> Prop) (n : nat) (x : A) (l : list A),
    AtLeast P n l -> P x -> AtLeast P (S n) (snoc x l).

Lemma AtLeast_Exists :
  forall (A : Type) (P : A -> Prop) (l : list A),
    AtLeast P 1 l <-> Exists P l.

Lemma AtLeast_Forall :
  forall (A : Type) (P : A -> Prop) (l : list A),
    AtLeast P (length l) l <-> Forall P l.

Lemma AtLeast_Rep :
  forall (A : Type) (x : A) (n : nat) (l : list A),
    AtLeast (fun y : A => x = y) n l <-> Rep x n l.

Lemma AtLeast_app_l :
  forall (A : Type) (P : A -> Prop) (n : nat) (l1 l2 : list A),
    AtLeast P n l1 -> AtLeast P n (l1 ++ l2).

Lemma AtLeast_app_r :
  forall (A : Type) (P : A -> Prop) (n : nat) (l1 l2 : list A),
    AtLeast P n l2 -> AtLeast P n (l1 ++ l2).

Lemma AtLeast_plus_app :
  forall (A : Type) (P : A -> Prop) (n1 n2 : nat) (l1 l2 : list A),
    AtLeast P n1 l1 -> AtLeast P n2 l2 ->
      AtLeast P (n1 + n2) (l1 ++ l2).

Lemma AtLeast_app_conv :
  forall (A : Type) (P : A -> Prop) (n : nat) (l1 l2 : list A),
    AtLeast P n (l1 ++ l2) ->
      exists n1 n2 : nat, AtLeast P n1 l1 /\ AtLeast P n2 l2 /\ n = n1 + n2.

Lemma AtLeast_app :
  forall (A : Type) (P : A -> Prop) (n : nat) (l1 l2 : list A),
    AtLeast P n (l1 ++ l2) <->
    exists n1 n2 : nat,
      AtLeast P n1 l1 /\ AtLeast P n2 l2 /\ n = n1 + n2.

Lemma AtLeast_app_comm :
  forall (A : Type) (P : A -> Prop) (n : nat) (l1 l2 : list A),
    AtLeast P n (l1 ++ l2) -> AtLeast P n (l2 ++ l1).

Lemma AtLeast_rev :
  forall (A : Type) (P : A -> Prop) (n : nat) (l : list A),
    AtLeast P n (rev l) <-> AtLeast P n l.

Lemma AtLeast_map :
  forall (A B : Type) (P : B -> Prop) (f : A -> B) (n : nat) (l : list A),
    AtLeast (fun x : A => P (f x)) n l ->
      AtLeast P n (map f l).

Lemma AtLeast_map_conv :
  forall (A B : Type) (P : B -> Prop) (f : A -> B) (n : nat) (l : list A),
    (forall x y : A, f x = f y -> x = y) -> AtLeast P n (map f l) ->
      AtLeast (fun x : A => P (f x)) n l.

Lemma AtLeast_replicate :
  forall (A : Type) (P : A -> Prop) (n : nat) (x : A),
    n <> 0 -> P x -> AtLeast P n (replicate n x).

Lemma AtLeast_replicate_conv :
  forall (A : Type) (P : A -> Prop) (n m : nat) (x : A),
    AtLeast P m (replicate n x) -> m = 0 \/ m <= n /\ P x.

Lemma AtLeast_remove :
  forall (A : Type) (P : A -> Prop) (l : list A) (m : nat),
    AtLeast P m l -> forall n : nat,
      match remove n l with
      | None => True
      | Some (_, l') => AtLeast P (m - 1) l'
      end.

Lemma AtLeast_take :
  forall (A : Type) (P : A -> Prop) (l : list A) (n m : nat),
    AtLeast P m (take n l) -> AtLeast P m l.

Lemma AtLeast_drop :
  forall (A : Type) (P : A -> Prop) (l : list A) (n m : nat),
    AtLeast P m (drop n l) -> AtLeast P m l.

Lemma AtLeast_take_drop :
  forall (A : Type) (P : A -> Prop) (n m : nat) (l : list A),
    AtLeast P n l ->
    exists n1 n2 : nat,
      AtLeast P n1 (take m l) /\ AtLeast P n2 (drop m l) /\ n = n1 + n2.

Lemma AtLeast_splitAt :
  forall (A : Type) (P : A -> Prop) (l l1 l2 : list A) (n : nat) (x : A),
    splitAt n l = Some (l1, x, l2) ->
      forall m : nat,
        AtLeast P m l ->
        exists m1 mx m2 : nat,
          AtLeast P m1 l1 /\ AtLeast P mx [x] /\ AtLeast P m2 l2 /\
          m1 + mx + m2 = m.

Lemma AtLeast_insert :
  forall (A : Type) (P : A -> Prop) (l : list A) (n : nat),
    AtLeast P n l -> forall (m : nat) (x : A),
      AtLeast P n (insert l m x).

Lemma AtLeast_replace :
  forall (A : Type) (P : A -> Prop) (l l' : list A) (n m : nat) (x : A),
    replace l n x = Some l' -> AtLeast P m l ->
      AtLeast P (m - 1) l'.

Lemma AtLeast_replace' :
  forall (A : Type) (P : A -> Prop) (l l' : list A) (n m : nat) (x : A),
    replace l n x = Some l' -> AtLeast P m l -> P x ->
      AtLeast P m l'.

Lemma AtLeast_replace_conv :
  forall (A : Type) (P : A -> Prop) (l l' : list A) (n m : nat) (x : A),
    replace l n x = Some l' -> AtLeast P m l' -> AtLeast P (m - 1) l.

Lemma AtLeast_replace_conv' :
  forall (A : Type) (P : A -> Prop) (l l' : list A) (n m : nat) (x y : A),
    replace l n x = Some l' -> nth n l = Some y -> P y ->
      AtLeast P m l' -> AtLeast P m l.


Lemma AtLeast_filter :
  forall (A : Type) (P : A -> Prop) (p : A -> bool) (n : nat) (l : list A),
    AtLeast P n (filter p l) -> AtLeast P n l.

Lemma AtLeast_filter_compat_true :
  forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
    (forall x : A, P x <-> p x = true) ->
      AtLeast P (length (filter p l)) (filter p l).

Lemma AtLeast_filter_compat_false :
  forall (A : Type) (P : A -> Prop) (p : A -> bool) (n : nat) (l : list A),
    (forall x : A, P x <-> p x = false) ->
      AtLeast P n (filter p l) -> n = 0.

Lemma AtLeast_takeWhile :
  forall (A : Type) (P : A -> Prop) (p : A -> bool) (n : nat) (l : list A),
    AtLeast P n (takeWhile p l) -> AtLeast P n l.

Lemma AtLeast_dropWhile :
  forall (A : Type) (P : A -> Prop) (p : A -> bool) (n : nat) (l : list A),
    AtLeast P n (dropWhile p l) -> AtLeast P n l.

Lemma AtLeast_takeWhile_true :
  forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
    (forall x : A, P x <-> p x = true) ->
      AtLeast P (length (takeWhile p l)) (takeWhile p l).

Lemma AtLeast_takeWhile_false :
  forall (A : Type) (P : A -> Prop) (p : A -> bool) (n : nat) (l : list A),
    (forall x : A, P x <-> p x = false) ->
      AtLeast P n (takeWhile p l) -> n = 0.

Lemma AtLeast_dropWhile_true :
  forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A) (n : nat),
    (forall x : A, P x <-> p x = true) ->
      AtLeast P n l -> AtLeast P (n - length (takeWhile p l)) (dropWhile p l).

Lemma AtLeast_dropWhile_false :
  forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A) (n : nat),
    (forall x : A, P x <-> p x = false) ->
      AtLeast P n l -> AtLeast P n (dropWhile p l).

Lemma AtLeast_zip :
  forall (A B : Type) (PA : A -> Prop) (PB : B -> Prop)
  (la : list A) (lb : list B) (n : nat),
    AtLeast (fun '(a, b) => PA a /\ PB b) n (zip la lb) ->
      AtLeast PA n la /\ AtLeast PB n lb.

Lemma AtLeast_findIndices :
  forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A) (n : nat),
    (forall x : A, P x <-> p x = true) ->
      AtLeast P n l -> n <= length (findIndices p l).

Lemma AtLeast_1_elem :
  forall (A : Type) (P : A -> Prop) (l : list A),
    AtLeast P 1 l <-> exists x : A, elem x l /\ P x.

Lemma AtLeast_intersperse :
  forall (A : Type) (P : A -> Prop) (x : A) (l : list A),
    P x -> AtLeast P (length l - 1) (intersperse x l).

Lemma AtLeast_intersperse' :
  forall (A : Type) (P : A -> Prop) (x : A) (n : nat) (l : list A),
    AtLeast P n l -> P x ->
      AtLeast P (n + (length l - 1)) (intersperse x l).

Lemma AtLeast_intersperse'' :
  forall (A : Type) (P : A -> Prop) (x : A) (n : nat) (l : list A),
    AtLeast P n l -> ~ P x -> AtLeast P n (intersperse x l).

Lemma AtLeast_insert_before_in :
  forall (A : Type) (P : A -> Prop) (l1 l2 : list A) (n m : nat),
    AtLeast P m (insertBefore.insertBefore n l1 l2) <->
    (exists m1 m2 : nat,
      AtLeast P m1 l1 /\ AtLeast P m2 l2 /\ m = m1 + m2).

Exactly

Zdefiniuj predykat Exactly. Zdanie Exactly P n l zachodzi, gdy na liście l występuje dokładnie n elementów spełniających predykat P.


Lemma Exactly_0_cons :
  forall (A : Type) (P : A -> Prop) (x : A) (l : list A),
    Exactly P 0 (x :: l) <-> ~ P x /\ Exactly P 0 l.

Lemma Exactly_S_cons :
  forall (A : Type) (P : A -> Prop) (n : nat) (x : A) (l : list A),
    Exactly P (S n) (x :: l) <->
    P x /\ Exactly P n l \/ ~ P x /\ Exactly P (S n) l.

Lemma Exactly_AtLeast :
  forall (A : Type) (P : A -> Prop) (n : nat) (l : list A),
    Exactly P n l -> AtLeast P n l.

Lemma Exactly_eq :
  forall (A : Type) (P : A -> Prop) (n m : nat) (l : list A),
    Exactly P n l -> Exactly P m l -> n = m.

Lemma Exactly_length :
  forall (A : Type) (P : A -> Prop) (n : nat) (l : list A),
    Exactly P n l -> n <= length l.

Lemma Exactly_snoc :
  forall (A : Type) (P : A -> Prop) (n : nat) (x : A) (l : list A),
    Exactly P n l -> ~ P x -> Exactly P n (snoc x l).

Lemma Exactly_S_snoc :
  forall (A : Type) (P : A -> Prop) (n : nat) (x : A) (l : list A),
    Exactly P n l -> P x -> Exactly P (S n) (snoc x l).

Lemma Exactly_app :
  forall (A : Type) (P : A -> Prop) (n1 n2 : nat) (l1 l2 : list A),
    Exactly P n1 l1 -> Exactly P n2 l2 -> Exactly P (n1 + n2) (l1 ++ l2).

Lemma Exactly_app_conv :
  forall (A : Type) (P : A -> Prop) (n : nat) (l1 l2 : list A),
    Exactly P n (l1 ++ l2) ->
      exists n1 n2 : nat,
        Exactly P n1 l1 /\ Exactly P n2 l2 /\ n = n1 + n2.

Lemma Exactly_app_comm :
  forall (A : Type) (P : A -> Prop) (n : nat) (l1 l2 : list A),
    Exactly P n (l1 ++ l2) -> Exactly P n (l2 ++ l1).

Lemma Exactly_rev :
  forall (A : Type) (P : A -> Prop) (n : nat) (l : list A),
    Exactly P n (rev l) <-> Exactly P n l.

Lemma Exactly_map :
  forall (A B : Type) (P : B -> Prop) (f : A -> B) (n : nat) (l : list A),
    (forall x y : A, f x = f y -> x = y) ->
    Exactly (fun x : A => P (f x)) n l <->
      Exactly P n (map f l).

Lemma Exactly_replicate :
  forall (A : Type) (P : A -> Prop) (n : nat) (x : A),
    P x -> Exactly P n (replicate n x).

Lemma Exactly_replicate_conv :
  forall (A : Type) (P : A -> Prop) (n : nat) (x : A),
    Exactly P n (replicate n x) -> n = 0 \/ P x.

Lemma Exactly_replicate' :
  forall (A : Type) (P : A -> Prop) (n m : nat) (x : A),
    Exactly P n (replicate m x) <->
    n = 0 /\ m = 0 \/
    n = 0 /\ ~ P x \/
    n = m /\ P x.

Lemma Exactly_take :
  forall (A : Type) (P : A -> Prop) (l : list A) (n m1 m2 : nat),
    Exactly P m1 (take n l) -> Exactly P m2 l -> m1 <= m2.

Lemma Exactly_drop :
  forall (A : Type) (P : A -> Prop) (l : list A) (n m1 m2 : nat),
    Exactly P m1 (drop n l) -> Exactly P m2 l -> m1 <= m2.

Lemma Exactly_take_drop :
  forall (A : Type) (P : A -> Prop) (l : list A) (n m : nat),
    Exactly P n l -> exists n1 n2 : nat,
      n = n1 + n2 /\ Exactly P n1 (take m l) /\ Exactly P n2 (drop m l).

Lemma Exactly_splitAt :
  forall (A : Type) (P : A -> Prop) (l l1 l2 : list A) (n : nat) (x : A),
    splitAt n l = Some (l1, x, l2) ->
      forall m : nat,
        Exactly P m l <->
        exists m1 mx m2 : nat,
          Exactly P m1 l1 /\ Exactly P mx [x] /\ Exactly P m2 l2 /\
          m1 + mx + m2 = m.

Lemma Exactly_filter :
  forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
    (forall x : A, P x <-> p x = true) ->
      Exactly P (length (filter p l)) (filter p l).

Lemma Exactly_takeWhile :
  forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
    (forall x : A, P x <-> p x = true) ->
      Exactly P (length (takeWhile p l)) (takeWhile p l).

Lemma Exactly_dropWhile :
  forall (A : Type) (P : A -> Prop) (p : A -> bool) (n : nat) (l : list A),
    (forall x : A, P x <-> p x = true) ->
    Exactly P n l ->
      Exactly P (n - length (takeWhile p l)) (dropWhile p l).

Lemma Exactly_span :
  forall
    (A : Type) (P : A -> Prop) (p : A -> bool)
    (n : nat)(x : A) (l b e : list A),
      (forall x : A, P x <-> p x = true) ->
      span p l = Some (b, x, e) ->
        Exactly P n l <->
        exists n1 n2 : nat,
          Exactly P n1 b /\ Exactly P n2 e /\
          if p x then S (n1 + n2) = n else n1 + n2 = n.


Lemma Exactly_intersperse :
  forall (A : Type) (P : A -> Prop) (x : A) (n : nat) (l : list A),
    Exactly P n l -> P x ->
      Exactly P (n + (length l - 1)) (intersperse x l).

Lemma Exactly_intersperse' :
  forall (A : Type) (P : A -> Prop) (x : A) (n : nat) (l : list A),
    Exactly P n l -> ~ P x ->
      Exactly P n (intersperse x l).

AtMost

Zdefiniuj relację AtMost. Zdanie AtMost P n l zachodzi, gdy na liście l występuje co najwyżej n elementów spełniających predykat P.
Przykład:
AtMost (fun n => n = 0) 3 [0; 1; 2; 3; 0] zachodzi.
AtMost (fun n => n < 5) 5 [1; 2; 3; 4; 5; 6; 7] nie zachodzi.


Lemma AtMost_0 :
  forall (A : Type) (P : A -> Prop) (x : A) (l : list A),
    AtMost P 0 (x :: l) <-> ~ P x /\ AtMost P 0 l.

Lemma AtMost_nil :
  forall (A : Type) (P : A -> Prop) (n : nat),
    AtMost P n [] <-> True.

Lemma AtMost_le :
  forall (A : Type) (P : A -> Prop) (n : nat) (l : list A),
    AtMost P n l -> forall m : nat, n <= m -> AtMost P m l.

Lemma AtMost_S_cons :
  forall (A : Type) (P : A -> Prop) (n : nat) (x : A) (l : list A),
    AtMost P (S n) (x :: l) <->
    (~ P x /\ AtMost P (S n) l) \/ AtMost P n l.

Lemma AtMost_S_snoc :
  forall (A : Type) (P : A -> Prop) (n : nat) (x : A) (l : list A),
    AtMost P n l -> AtMost P (S n) (snoc x l).

Lemma AtMost_snoc :
  forall (A : Type) (P : A -> Prop) (n : nat) (x : A) (l : list A),
    AtMost P n l -> ~ P x -> AtMost P n (snoc x l).

Lemma AtMost_S :
  forall (A : Type) (P : A -> Prop) (n : nat) (l : list A),
    AtMost P n l -> AtMost P (S n) l.

Palindromy

Palindrom to słowo, które czyta się tak samo od przodu jak i od tyłu.
Zdefiniuj induktywny predykat Palindrome, które odpowiada powyższemu pojęciu palindromu, ale dla list elementów dowolnego typu, a nie tylko słów.



Lemma Palindrome_inv :
  forall (A : Type) (x : A) (l : list A),
    Palindrome (x :: l ++ [x]) -> Palindrome l.

Lemma Palindrome_inv_2 :
  forall (A : Type) (x y : A),
    Palindrome [x; y] -> x = y.

Lemma Palindrome_inv_3 :
  forall (A : Type) (x y : A) (l : list A),
    Palindrome (x :: l ++ [y]) -> x = y.

Lemma Palindrome_length :
  forall (A : Type) (x : A) (n : nat),
    exists l : list A, Palindrome l /\ n <= length l.

Lemma Palindrome_cons_snoc :
  forall (A : Type) (x : A) (l : list A),
    Palindrome l -> Palindrome (x :: snoc x l).

Lemma Palindrome_app :
  forall (A : Type) (l1 l2 : list A),
    Palindrome l1 -> Palindrome l2 -> Palindrome (l1 ++ l2 ++ rev l1).

Lemma Palindrome_app' :
  forall (A : Type) (l1 l2 : list A),
    Palindrome l2 -> Palindrome (l1 ++ l2 ++ rev l1).

Lemma Palindrome_rev :
  forall (A : Type) (l : list A),
    Palindrome l <-> Palindrome (rev l).

(* Palindromowa indukcja *)
Lemma list_palindrome_ind :
  forall (A : Type) (P : list A -> Prop),
    P [] ->
    (forall x : A, P [x]) ->
    (forall (x y : A) (l : list A), P l -> P (x :: snoc y l)) ->
      forall l : list A, P l.

Lemma Palindrome_spec :
  forall (A : Type) (l : list A),
    Palindrome l <-> l = rev l.

Lemma Palindrome_spec' :
  forall (A : Type) (l : list A),
    Palindrome l -> exists l1 l2 : list A,
      l = l1 ++ l2 ++ rev l1 /\ length l2 <= 1.

Lemma Palindrome_map :
  forall (A B : Type) (f : A -> B) (l : list A),
    Palindrome l -> Palindrome (map f l).

Lemma replicate_S :
  forall (A : Type) (n : nat) (x : A),
    replicate (S n) x = x :: replicate n x.

Lemma Palindrome_replicate :
  forall (A : Type) (n : nat) (x : A),
    Palindrome (replicate n x).

Lemma Palindrome_cons_replicate :
  forall (A : Type) (n : nat) (x y : A),
    Palindrome (x :: replicate n y) -> n = 0 \/ x = y.

Lemma Palindrome_iterate :
  forall (A : Type) (f : A -> A),
    (forall (n : nat) (x : A), Palindrome (iterate f n x)) ->
      forall x : A, f x = x.

Lemma Palindrome_nth :
  forall (A : Type) (l : list A),
    Palindrome l -> forall n : nat,
      n < length l -> nth n l = nth (length l - S n) l.

Lemma Palindrome_drop :
  forall (A : Type) (l : list A),
    (forall n : nat, Palindrome (drop n l)) ->
      l = [] \/ exists (n : nat) (x : A), l = replicate n x.

Lemma Palindrome_take :
  forall (A : Type) (l : list A),
    (forall n : nat, Palindrome (take n l)) ->
      l = [] \/ exists (n : nat) (x : A), l = replicate n x.

Lemma replace_Palindrome :
  forall (A : Type) (l l' : list A) (n : nat) (x : A),
    replace l n x = Some l' -> Palindrome l ->
      Palindrome l' <-> length l = 1 /\ n = 0 \/ nth n l = Some x.

Lemma Palindrome_zip :
  exists (A B : Type) (la : list A) (lb : list B),
    Palindrome la /\ Palindrome lb /\ ~ Palindrome (zip la lb).


Lemma Palindrome_findLast_rev :
  forall (A : Type) (p : A -> bool) (l : list A),
    Palindrome l -> find p l = findLast p l.

Lemma Palindrome_pmap :
  forall (A B : Type) (f : A -> option B) (l : list A),
    Palindrome l -> Palindrome (pmap f l).

Lemma Palindrome_intersperse :
  forall (A : Type) (x : A) (l : list A),
    Palindrome l -> Palindrome (intersperse x l).


Lemma Palindrome_Dup :
  forall (A : Type) (l : list A),
    Palindrome l -> length l <= 1 \/ Dup l.

Rozstrzyganie predykatów na listach (TODO)


Definition elem_dec
  {A : Type} (eq_dec : A -> A -> bool) (x : A) (l : list A) : bool :=
    any (eq_dec x) l.

Lemma elem_dec_spec :
  forall
    {A : Type} {eq_dec : A -> A -> bool}
    (eq_dec_spec : forall x y : A, reflect (x = y) (eq_dec x y))
    (x : A) (l : list A),
      reflect (elem x l) (elem_dec eq_dec x l).

Lemma In_dec_spec :
  forall
    {A : Type} {eq_dec : A -> A -> bool}
    (eq_dec_spec : forall x y : A, reflect (x = y) (eq_dec x y))
    (x : A) (l : list A),
      reflect (In x l) (elem_dec eq_dec x l).

Fixpoint Dup_dec
  {A : Type} (eq_dec : A -> A -> bool) (l : list A) : bool :=
match l with
| [] => false
| h :: t => elem_dec eq_dec h t || Dup_dec eq_dec t
end.

Lemma Dup_dec_spec :
  forall
    (A : Type) (eq_dec : A -> A -> bool)
    (eq_dec_spec : forall x y : A, reflect (x = y) (eq_dec x y))
    (l : list A),
      reflect (Dup l) (Dup_dec eq_dec l).

Lemma Exists_dec_spec :
  forall
    {A : Type} {P : A -> Prop} {p : A -> bool}
    (P_dec_spec : forall x : A, reflect (P x) (p x))
    (l : list A),
      reflect (Exists P l) (any p l).

Lemma Forall_dec_spec :
  forall
    {A : Type} {P : A -> Prop} {p : A -> bool}
    (P_dec_spec : forall x : A, reflect (P x) (p x))
    (l : list A),
      reflect (Forall P l) (all p l).

Definition Exactly_dec
  {A : Type} (p : A -> bool) (n : nat) (l : list A) : bool :=
    count p l =? n.

Lemma Exactly_dec_spec :
  forall
    {A : Type} {P : A -> Prop} {p : A -> bool}
    (P_dec_spec : forall x : A, reflect (P x) (p x))
    (l : list A) (n : nat),
      reflect (Exactly P n l) (Exactly_dec p n l).

Definition AtLeast_dec
  {A : Type} (p : A -> bool) (n : nat) (l : list A) : bool :=
    n <=? count p l.

Lemma AtLeast_dec_spec :
  forall
    {A : Type} {P : A -> Prop} {p : A -> bool}
    (P_dec_spec : forall x : A, reflect (P x) (p x))
    (l : list A) (n : nat),
      reflect (AtLeast P n l) (AtLeast_dec p n l).

Definition AtMost_dec
  {A : Type} (p : A -> bool) (n : nat) (l : list A) : bool :=
    count p l <=? n.

Lemma AtMost_dec_spec :
  forall
    {A : Type} {P : A -> Prop} {p : A -> bool}
    (P_dec_spec : forall x : A, reflect (P x) (p x))
    (l : list A) (n : nat),
      reflect (AtMost P n l) (AtMost_dec p n l).

Predykaty na listach - rekurencyjnie (TODO)


Module Recursives.

Można zadać sobie pytanie: skoro predykaty takie jak elem czy exists można zdefiniować zarówno induktywnie jak i przez rekursję, który sposób jest lepszy?
Odpowiedź jest prosta: jeżeli możesz użyć rekursji, zrób to.

Fixpoint elem {A : Type} (x : A) (l : list A) : Prop :=
match l with
| [] => False
| h :: t => x = h \/ elem x t
end.

Fixpoint all {A : Type} (P : A -> Prop) (l : list A) : Prop :=
match l with
| [] => True
| h :: t => P h /\ all P t
end.

Lemma all_spec :
  forall (A : Type) (P : A -> Prop) (l : list A),
    all P l <-> Forall P l.

Fixpoint exactly
  {A : Type} (P : A -> Prop) (n : nat) (l : list A) : Prop :=
match l, n with
| [], 0 => True
| [], _ => False
| h :: t, 0 => ~ P h /\ exactly P 0 t
| h :: t, S n' =>
    (P h /\ exactly P n' t) \/ (~ P h /\ exactly P n t)
end.

Lemma exactly_spec :
  forall (A : Type) (P : A -> Prop) (n : nat) (l : list A),
    exactly P n l <-> Exactly P n l.

exists



Lemma ex_spec :
  forall (A : Type) (P : A -> Prop) (l : list A),
    ex P l <-> exists x : A, elem x l /\ P x.

Lemma ex_nil :
  forall (A : Type) (P : A -> Prop),
    ex P [] <-> False.

Lemma ex_cons :
  forall (A : Type) (P : A -> Prop) (h : A) (t : list A),
    ex P (h :: t) <-> P h \/ ex P t.

Lemma ex_length :
  forall (A : Type) (P : A -> Prop) (l : list A),
    ex P l -> 1 <= length l.

Lemma ex_snoc :
  forall (A : Type) (P : A -> Prop) (x : A) (l : list A),
    ex P (snoc x l) <-> ex P l \/ P x.

Lemma ex_app :
  forall (A : Type) (P : A -> Prop) (l1 l2 : list A),
    ex P (l1 ++ l2) <-> ex P l1 \/ ex P l2.

Lemma ex_rev :
  forall (A : Type) (P : A -> Prop) (l : list A),
    ex P (rev l) <-> ex P l.

Lemma ex_map :
  forall (A B : Type) (P : B -> Prop) (f : A -> B) (l : list A),
    ex P (map f l) -> ex (fun x : A => P (f x)) l.

Lemma ex_join :
  forall (A : Type) (P : A -> Prop) (ll : list (list A)),
    ex P (join ll) <->
    ex (fun l : list A => ex P l) ll.

Lemma ex_replicate :
  forall (A : Type) (P : A -> Prop) (n : nat) (x : A),
    ex P (replicate n x) <-> 1 <= n /\ P x.

Lemma ex_nth :
  forall (A : Type) (P : A -> Prop) (l : list A),
    ex P l <->
    exists (n : nat) (x : A), nth n l = Some x /\ P x.

Lemma ex_remove :
  forall (A : Type) (P : A -> Prop) (l : list A) (n : nat),
    ex P l ->
    match remove n l with
    | None => True
    | Some (x, l') => ~ P x -> ex P l'
    end.

Lemma ex_take :
  forall (A : Type) (P : A -> Prop) (l : list A) (n : nat),
    ex P (take n l) -> ex P l.

Lemma ex_drop :
  forall (A : Type) (P : A -> Prop) (l : list A) (n : nat),
    ex P (drop n l) -> ex P l.

Lemma ex_take_drop :
  forall (A : Type) (P : A -> Prop) (l : list A) (n : nat),
    ex P l -> ex P (take n l) \/ ex P (drop n l).

Lemma ex_splitAt :
  forall (A : Type) (P : A -> Prop) (l l1 l2 : list A) (n : nat) (x : A),
    splitAt n l = Some (l1, x, l2) ->
      ex P l <-> P x \/ ex P l1 \/ ex P l2.

Lemma ex_insert :
  forall (A : Type) (P : A -> Prop) (l : list A) (n : nat) (x : A),
    ex P (insert l n x) <-> P x \/ ex P l.

Lemma ex_replace :
  forall (A : Type) (P : A -> Prop) (l l' : list A) (n : nat) (x : A),
    replace l n x = Some l' ->
      ex P l' <->
      ex P (take n l) \/ P x \/ ex P (drop (S n) l).

Lemma ex_filter :
  forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
    ex P (filter p l) -> ex P l.

Lemma ex_filter_conv :
  forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
    ex P l ->
      ex P (filter p l) \/
      ex P (filter (fun x : A => negb (p x)) l).

Lemma ex_filter_compat :
  forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
    (forall x : A, P x <-> p x = false) -> ~ ex P (filter p l).

Lemma ex_partition :
  forall (A : Type) (P : A -> Prop) (p : A -> bool) (l l1 l2 : list A),
    partition p l = (l1, l2) ->
      ex P l <-> ex P l1 \/ ex P l2.

Lemma ex_takeWhile :
  forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
    ex P (takeWhile p l) -> ex P l.

Lemma ex_takeWhile_compat :
  forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
    (forall x : A, P x <-> p x = false) -> ~ ex P (takeWhile p l).

Lemma ex_dropWhile :
  forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
    ex P (dropWhile p l) -> ex P l.

Lemma ex_takeWhile_dropWhile :
  forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
    ex P l -> ex P (takeWhile p l) \/ ex P (dropWhile p l).

Lemma ex_span :
  forall
    (A : Type) (P : A -> Prop) (p : A -> bool) (x : A) (l b e : list A),
      (forall x : A, P x <-> p x = true) ->
      span p l = Some (b, x, e) ->
        ex P l <-> ex P b \/ P x \/ ex P e.

Lemma ex_interesting :
  forall (A B : Type) (P : A * B -> Prop) (la : list A) (hb : B) (tb : list B),
    ex (fun a : A => ex (fun b : B => P (a, b)) tb) la ->
    ex (fun a : A => ex (fun b : B => P (a, b)) (hb :: tb)) la.

Lemma ex_zip :
  forall (A B : Type) (P : A * B -> Prop) (la : list A) (lb : list B),
    ex P (zip la lb) ->
      ex (fun a : A => ex (fun b : B => P (a, b)) lb) la.

Lemma ex_pmap :
  forall (A B : Type) (f : A -> option B) (P : B -> Prop) (l : list A),
    ex P (pmap f l) <->
      ex (fun x : A => match f x with | Some b => P b | _ => False end) l.

Lemma ex_intersperse :
  forall (A : Type) (P : A -> Prop) (x : A) (l : list A),
    ex P (intersperse x l) <->
    ex P l \/ (P x /\ 2 <= length l).

End Recursives.