Library list_extensions.more_list

Some additional properties for the Coq lists.





Set Implicit Arguments.




Require Import Bool.

Require Import List.

Require Import Arith.




Lemma tail_prop : forall A :  Type, forall (P : A -> Prop), forall a, forall l, 

  (forall b, In b (a::l) -> P b) -> (forall b, In b l -> P b).

Proof.

intros Ar P a l H b In_b; apply H; right; trivial.

Qed.




Lemma tail_set : forall A : Set, forall (P : A -> Set), forall a, forall l, 

  (forall b, In b (a::l) -> P b) -> (forall b, In b l -> P b).

Proof.

intros Ar P a l H b In_b; apply H; right; trivial.

Qed.

Relations between length, map, append, In and nth.





Definition length_app := app_length.

Definition length_map := map_length.




Lemma nth_error_map :

  forall (A B : Set) (f : A -> B) (l : list A) i,

  match nth_error (map f l) i with

  | Some f_li => 

           match nth_error l i with

            | Some li => f_li = f li

            | None => False

            end

  | None =>

            match nth_error l i with

            | Some li => False

            | None => True

            end

end.

Proof.

induction l as [ | a l ]; 

intro i; destruct i as [ | i ]; simpl; trivial.

apply IHl; trivial.

Qed.




Lemma split_list : 

  forall (A : Set) (l1 l2 l3 l4 : list A), l1 ++ l2 = l3 ++ l4 ->

  {l | l1 = l3 ++ l /\ l4 = l ++ l2} + {l | l3 = l1 ++ l /\ l2 = l ++ l4}.

Proof.

intros A l1; induction l1 as [ | a1 l1].

right; exists l3; split; trivial.

intros l2 [ | a3 l3] l4 H.

left; exists (a1 :: l1); split; trivial.

rewrite H; trivial.

injection H; clear H; intros H a1_eq_a3; subst a3.

destruct (IHl1 _ _ _ H) as [H' | H'].

destruct H' as [l [H1 H2]]; subst l1 l4.

left; exists l; split; trivial.

destruct H' as [l [H1 H2]]; subst l2 l3.

right; exists l; split; trivial.

Qed.




Lemma map_id : forall (A : Set) l, map (fun t : A => t) l = l.

Proof.

intros A l; induction l as [ | t l]; simpl; trivial.

rewrite IHl; trivial.

Qed.




Lemma map_eq : forall (A B : Set) (f g : A -> B) l, (forall a, In a l -> f a = g a) -> map f l = map g l.

Proof.

intros A B f g l; induction l as [ | a l]; intros H; trivial.

simpl; rewrite (H a).

rewrite IHl; trivial.

intros; apply H; right; trivial.

left; trivial.

Qed.




Lemma map_duplicate : forall (A : Set) (ll : list (A*A)), 

   map (@fst A A) ll = map (@snd A A) ll ->

   forall a b, In (a,b) ll -> a = b.

Proof.

intros A ll; induction ll as [ | [a1 a2] ll]; intros H a b ab_in_ll.

contradiction.

simpl in H; injection H; clear H; intros H H'; subst a2.

simpl in ab_in_ll; destruct ab_in_ll as [ab_eq_a12 | ab_in_ll].

injection ab_eq_a12; intros; subst a b; trivial.

apply IHll; trivial.

Qed.




Lemma split_map : 

  forall (A B : Set) (f : A -> B) l k1 k2, map f l = k1 ++ k2 ->

  {l1 : list A & {l2 : list A | l = l1 ++ l2 /\ map f l1 = k1 /\ map f l2 = k2}}.

Proof.

intros A B f l; induction l as [ | a l].

intros k1 k2 H; exists (@nil A); exists (@nil A); split; trivial.

simpl in H; destruct k1 as [ | b k1].

simpl in H; subst k2; split; trivial.

discriminate.

intros [ | b k1] k2 H; simpl in H; injection H; clear H; intros; subst.

exists (@nil A);  exists (a :: l); do 2 (split; trivial).

destruct (IHl k1 k2 H) as [l1 [l2 [H1 [H2 H3]]]].

exists (a :: l1); exists l2; subst; do 2 (split; trivial).

Qed.




Lemma length_add : 

  forall (A : Set) (l1 l2 : list A) a, length (l1 ++ a :: l2) = S (length (l1 ++ l2)).

Proof.

intros A l1 l2 a; rewrite app_length; simpl;

rewrite plus_comm; simpl; rewrite plus_comm;

rewrite app_length; trivial.

Qed.

A measure on lists based on a measure on elements.





Fixpoint list_size (A : Set) (size : A -> nat) (l : list A) {struct l} : nat :=

  match l with

  | nil => 0

  | h :: tl => size h + list_size size tl

  end.




Lemma list_size_tl_compat :

  forall (A : Set) (size : A -> nat) a b l, size a < size b -> 

    list_size size (a :: l) < list_size size (b :: l).

Proof.

intros A size a b l H; simpl; apply plus_lt_compat_r; trivial.

Qed.




Lemma list_size_app:

 forall (A : Set) (size : A -> nat) l1 l2,

 list_size size (l1 ++ l2) = list_size size l1 + list_size size l2.

Proof.

induction l1 as [ | a1 l1 ]; trivial.

intros; simpl; rewrite IHl1; auto with arith.

Qed.




Lemma list_size_fold :

  forall (A : Set) (size : A -> nat) l,

  (fix size_list (l0 : list A) : nat :=

   match l0 with

   | nil => 0

   | t :: lt => size t + size_list lt

   end) l = list_size size l.

Proof.

intros A size l; induction l; trivial.

simpl; rewrite IHl; trivial.

Qed.




Lemma list_size_size_eq :

  forall (A : Set) (size1 : A -> nat) (size2 : A -> nat) l,

 (forall a, In a l -> size1 a = size2 a) -> list_size size1 l = list_size size2 l.

Proof.

intros A size1 size2 l; induction l as [ | a l]; simpl; trivial.

intros size1_eq_size2.

rewrite (size1_eq_size2 a (or_introl _ (refl_equal _))).

apply (f_equal (fun n => size2 a + n)); apply IHl;

intros; apply size1_eq_size2; right; trivial.

Qed.

Induction principles for list.

Induction on the length.


Definition list_rec2 :

  forall A, forall P : list A -> Type,

    (forall (n:nat) (l : list A), length l <= n -> P l) -> 

    forall l : list A, P l.

Proof.

intros A P H l; apply (H (length l) l); apply le_n.

Defined.

Induction on the the size.


Definition list_rec3 (A : Set) (size : A -> nat) :

  forall P : list A -> Type,

    (forall (n:nat) (l : list A), list_size size l <= n -> P l) -> 

    forall l : list A, P l.

Proof.

intros A size P H l; apply (H (list_size size l) l); apply le_n.

Defined.

How to remove an element in a list, whenever it is present.





Lemma in_split_set :

  forall (A : Set) 

    (eq_dec : forall a1 a2 : A, {a1 = a2}+{a1 <> a2}) 

   (a : A) (l : list A), In a l -> {l1 : list A & { l2 : list A | l = l1 ++ a :: l2}}.

Proof.

intros A eq_dec a l; induction l as [ | e l].

contradiction.

destruct (eq_dec e a) as [e_eq_a | e_diff_a].

intros _; exists (@nil A); exists l; simpl; subst; trivial.

intro a_in_el; destruct IHl as [l' [l'' H]].

destruct a_in_el as [e_eq_a | a_in_l]; trivial.

absurd (e = a); trivial.

exists (e :: l'); exists l''; subst l; simpl; trivial.

Qed.




Lemma in_in_split_set :

  forall (A : Set) 

   (a b : A) (l1 l2 k1 k2 : list A), l1 ++ a :: l2 = k1 ++ b :: k2 ->

   {l | l1 = k1 ++ b :: l /\ k2 = l ++ a :: l2} +

   {l | k1 = l1 ++ a :: l /\ l2 = l ++ b :: k2} +

   {a = b /\ l1 = k1 /\ l2 = k2}.

Proof.

intros A a b l1; generalize a b; clear a b; induction l1 as [ | a1 l1];

intros a b l2 k1 k2 H; destruct k1 as [ | b1 k1].

simpl in H; injection H; intros l2_eq_k2 a_eq_b; right; repeat split; trivial.

simpl in H; injection H; intros l2_eq_k a_eq_b1; subst; clear H.

left; right; exists k1; repeat split; trivial.

simpl in H; injection H; intros l_eq_k2 a1_eq_b; subst; clear H.

left; left; exists l1; repeat split; trivial.

simpl in H; injection H; intros l_eq_k a1_eq_b1; subst; clear H.

destruct (IHl1 _ _ _ _ _ l_eq_k) as [[H | H] | H].

destruct H as [l [H1 H2]]; subst.

left; left; exists l; repeat split; trivial.

destruct H as [l [H1 H2]]; subst.

left; right; exists l; repeat split; trivial.

destruct H as [a_eq_b [H1 H2]]; subst.

right; repeat split; trivial.

Qed.




Function remove (A : Set) (eqA : A -> A -> Prop)

    (eqA_dec : forall a1 a2 : A, {eqA a1 a2}+{~eqA a1 a2}) 

  (a : A) (l : list A) {struct l} : (option (list A)) :=

  match l with

  | nil => None 

  | h :: tl =>

    if (eqA_dec a h : sumbool _ _)

    then Some tl

    else 

        match @remove A eqA eqA_dec a tl with

        | Some rmv => Some (h :: rmv)

        | None => None 

        end

  end.




Lemma in_remove :

  forall (A : Set) (eqA : A -> A -> Prop)

  (eqA_dec : forall a1 a2 : A, {eqA a1 a2}+{~eqA a1 a2}) a l,  

  match remove eqA eqA_dec a l with

  | None => forall a', eqA a a' -> ~ In a' l

  | Some l' => 

              exists a', exists l', exists l'', 

              eqA a a' /\ l = l' ++ a' :: l'' /\ remove eqA eqA_dec a l = Some (l' ++ l'')

  end.

Proof.

intros A eqA eqA_dec a l; 

functional induction (remove eqA eqA_dec a l) 

     as [ l l_eq_nil
          | l a' l' l_eq_a'_l' a_eq_a' _H 
          | l a' l' l_eq_a'_l' a_diff_a' _H IH rmv H
          | l a' l' l_eq_a'_l' a_diff_a' _H IH H].

auto.

clear _H; exists a'; exists (@nil A); exists l'; intuition.

rewrite H in IH; destruct IH as [a'' [l'' [l''' [H' [H'' H''']]]]].

exists a''; exists (a' :: l''); exists l'''; subst l'; rewrite app_comm_cons; injection H'''; intros; subst.

simpl; intuition.

rewrite H in IH.

intros a'' a_eq_a'' [a''_eq_a' | a''_in_l'].

subst a''; absurd (eqA a a'); trivial.

apply (IH a''); trivial.

Qed.




Lemma in_insert :

forall (A : Set) (l1 l2 : list A) e a, In a (l1 ++ l2) -> In a (l1 ++ e :: l2).

Proof.

intros A l1 l2 e a a_in_l1_l2; 

destruct (in_app_or _ _ _ a_in_l1_l2) as [a_in_l1 | a_in_l2]; 

apply in_or_app; [left | right; right]; trivial.

Qed.




Lemma diff_in_remove :

forall (A : Set) (l1 l2 : list A) e a, a <> e -> In a (l1 ++ e :: l2) -> In a (l1 ++ l2).

Proof.

intros A l1 l2 e a a_diff_e a_in_l1_e_l2; 

destruct (in_app_or _ _ _ a_in_l1_e_l2) as [a_in_l1 | [a_eq_e | a_in_l2]]; 

apply in_or_app; 

[left
| absurd (a=e); subst
| right]; trivial.

Qed.

Iterators.


Lemma fold_left_in_acc : 

  forall (A B : Type) (f : list B -> A -> list B) x l,

  (forall acc x y, In y acc -> In x l -> In y (f acc x)) ->

  forall acc, In x acc -> In x (fold_left f l acc).

Proof.

  intros A B f x l; induction l as [ | a l]; intros Hf acc x_in_acc; simpl; trivial.

  apply IHl.

  intros; apply Hf; [idtac | right]; trivial.

  apply Hf; [idtac | left]; trivial.

Qed.




Lemma fold_left_in_acc_split : 

  forall (A B : Type) (f : A -> list B), 

    let g := fun acc x => (f x) ++ acc in 

      forall  acc1 acc2 x l,

        In x (fold_left g l (acc1 ++ acc2)) <-> In x (fold_left g l acc1) \/ In x acc2.

Proof.

  intros A B f g acc1 acc2 x l.

  revert acc1 acc2;induction l as [ | y l]; simpl.

  split; auto with *.

  intros acc1 acc2; rewrite <- IHl.

  unfold g.

  rewrite ass_app.

  reflexivity.

Qed.




Fixpoint fold_left2 (A B C : Set) (f : A -> B -> C -> A) (a : A) (l1 : list B) (l2 : list C)  

  {struct l1} : option A :=

  match l1, l2 with

  | nil, nil => Some a

  | b :: t1, c :: t2 => fold_left2 f (f a b c) t1 t2

  | _, _ => None

  end.

more properties on the nth element.


Lemma nth_error_nil : forall (A : Set) n, @nth_error A nil n = None.

Proof.

intros A [ | n]; simpl; trivial.

Qed.




Lemma nth_error_ok_in :

  forall (A : Set) n (l : list A) (a : A),

  nth_error l n = Some a -> {l1 : list A & {l2 : list A | length l1 = n /\ l = l1 ++ a :: l2}}.

Proof.

intros A n l; generalize n; clear n; induction l as [ | a' l].

intros n a; rewrite nth_error_nil; intros; discriminate.

intros [ | n] a; simpl; intros H.

injection H; intro; subst a'.

exists (@nil A); exists l; split; trivial.

destruct (IHl n a H) as [l1 [l2 [L H']]].

exists (a' :: l1); exists l2; simpl; split; subst; trivial.

Qed.




Lemma nth_error_at_pos :

  forall (A : Set) l1 a l2, nth_error (l1 ++ a :: l2) (length l1) = @Some A a.

Proof.

intros A l1; induction l1 as [ | a1 l1]; intros a l2; simpl; trivial.

Qed.




Lemma nth_error_remove :

  forall (A : Set) (a : A) k k' n,

    nth_error (k ++ a :: k') (if le_lt_dec (length k) n then S n else n) = 

        nth_error (k ++ k') n.

Proof.

intros A b k; induction k as [ | a k]; intros k' m.

simpl; trivial.

simpl length; simpl app.

destruct m as [ | m].

simpl; trivial.

generalize (IHk k' m);

destruct (le_lt_dec (length k) m) as [k_le_m | k_gt_m];

destruct (le_lt_dec (S (length k)) (S m)) as [k_le_m' | k_gt_m'].

simpl; trivial.

absurd (S m <= m); auto with arith; apply le_trans with (length k); auto with arith.

absurd (S m <= m); auto with arith; apply le_trans with (length k); auto with arith.

simpl; trivial.

Qed.

Association lists.

find.


Function find (A B : Set) (eqA : forall (a1 a2 : A), {a1=a2}+{a1<>a2})

(a : A) (l : list (A * B)) {struct l} : option (B) :=

 match l with

 | nil => None

 | (a1,b1) :: l =>

     if (eqA a a1 : sumbool _ _)

     then Some b1

     else find eqA a l

  end.




Lemma find_diff :

     forall (A B : Set) (eqA : forall (a1 a2 : A), {a1=a2}+{a1<>a2}) a1 a2,

      a1 <> a2 -> forall l1 l2 b, find eqA a2 (l1 ++ (a1,b) :: l2) = find (B:= B) eqA a2 (l1 ++ l2).

Proof.

intros A B eqA a1 a2 a1_diff_a2 l1; induction l1 as [ | [a b] l1]; intros l2 b'; simpl.

destruct (eqA a2 a1) as [a2_eq_a1 | _]; [absurd (a1 = a1); subst | idtac]; trivial.

destruct (eqA a2 a); trivial.

Qed.




Lemma find_mem :

   forall (A B : Set) (eqA : forall (a1 a2 : A), {a1=a2}+{a1<>a2})

  (a : A)  (l : list (A * B)) (b : B),

  find eqA a l = Some b -> {l1 : list (A * B) & {l2 : list (A * B) | l = l1 ++ (a,b) :: l2 } }.

Proof.

intros A B eqA a l b; 

functional induction (find eqA a l)

    as [ A B eqA a l l_eq_nil
          | A B eqA a l a1 b1 l' l_eq_a1_b1_l' a_eq_a1 _
          | A B eqA a l a1 b1 l' l_eq_a1_b1_l' a_diff_a1 _H IH]; intro H.

discriminate.

injection H; clear H; intros; 

exists (@nil (A*B)) ; exists l'; subst; trivial.

destruct (IH b H) as [l1 [l2 H']]; 

exists ((a1,b1) :: l1); exists l2; subst; rewrite app_comm_cons; trivial.

Qed.




Lemma find_not_mem :

  forall (A B : Set) (eqA : forall (a1 a2 : A), {a1=a2}+{a1<>a2})

  (a : A) (b : B) (l : list (A * B)) (dom : list A),

  ~In a dom -> (forall a', In a' dom -> find eqA a' ((a,b) :: l) = find eqA a' l).

Proof.

intros A B eqA a b l dom a_not_in_dom a' a'_in_dom; simpl;

destruct (eqA a' a) as [a'_eq_a | a'_diff_a].

subst a'; absurd (In a dom); trivial.

trivial.

Qed.




Lemma find_not_found : 

  forall (A B : Set) (eqA : forall (a1 a2 : A), {a1=a2}+{a1<>a2})

  (a : A) (b : B) (l : list (A * B)), find eqA a l = None -> ~In (a,b) l.

Proof.

intros A B eqA a b l; induction l as [ | [a1 b1] l].

intros _ ab_in_nil; contradiction.

simpl; destruct (eqA a a1) as [a_eq_a1 | a_diff_a1].

intro; discriminate.

intros H [a1b1_eq_ab | ab_in_l].

apply a_diff_a1; injection a1b1_eq_ab; intros; subst; trivial.

apply (IHl H); trivial.

Qed.




Lemma In_dec_app :

  forall (A : Set) (eqA : forall (a1 a2 : A), {a1=a2}+{a1<>a2}) a 

  (l1 l2 : list A) P Q,

  (if In_dec eqA a (l1 ++ l2) then P else Q) <->  

  (if (In_dec eqA a l1) 

  then P

  else if (In_dec eqA a l2) then P else Q).

Proof.

intros A eqA a l1; induction l1 as [ | a1 l1]; intro l2; simpl.

intuition.

intros P Q; destruct (eqA a1 a) as [a1_eq_a | a1_diff_a].

intuition.

generalize (IHl1 l2 P Q); destruct (In_dec eqA a (l1 ++ l2)).

destruct (In_dec eqA a l1); intuition.

destruct (In_dec eqA a l1); intuition.

Qed.




Lemma find_app :

  forall (A B : Set) (eqA : forall (a1 a2 : A), {a1=a2}+{a1<>a2}) a 

  (l1 l2 : list (A * B)),

  find eqA a (l1 ++ l2) =

     if In_dec eqA a (map (fun st => fst st) l1)

     then find eqA a l1

        else	find eqA a l2.

Proof.

intros A B eqA a l1; induction l1 as [ | [a1 b1] l1]; intro l2; simpl.

trivial.

destruct (eqA a a1) as [a_eq_a1 | a_diff_a1];

destruct (eqA a1 a) as [a1_eq_a | a1_diff_a]; trivial.

subst a1; absurd (a = a); trivial.

subst a1; absurd (a = a); trivial.

rewrite IHl1; 

destruct (In_dec eqA a (map (fun st : A * B => fst st) l1)); trivial.

Qed.




Lemma find_map : 

  forall (A B C : Set) (eqA : forall (a1 a2 : A), {a1=a2}+{a1<>a2}) (f : B -> C),

  forall a l, 

   match find eqA a l with

   | Some b => find eqA a (map (fun xval : A * B => (fst xval, f (snd xval))) l) = Some (f b)

   | None => find eqA a (map (fun xval : A * B => (fst xval, f (snd xval))) l) = None

   end.

Proof.

intros A B C eqA f a l; induction l as [ | [a1 b1] l]; simpl; trivial.

destruct (eqA a a1) as [a_eq_a1 | a_diff_a1]; trivial.

Qed.




Fixpoint merge (A B : Set) (eqA : forall (a1 a2 : A), {a1=a2}+{a1<>a2}) 

                         (eqB : forall (b1 b2 : B), {b1=b2}+{b1<>b2}) 

                        (partial_res l : list (A*B)) {struct l} : option (list (A*B)) :=

  match l with

  | nil => Some partial_res

  | (a,b) :: l => 

       match find eqA a partial_res with

       | Some b' => if eqB b b' then merge eqA eqB partial_res l else None

       | None => merge eqA eqB ((a,b) :: partial_res) l

       end

   end.




Lemma merge_correct :

   forall (A B : Set) eqA eqB (l1 l2 : list (A*B)), 

       (forall a2 b2 c2, In (a2,b2) l2 -> In (a2,c2) l2 -> b2 = c2) ->

       match merge eqA eqB l1 l2 with

       | Some l => (forall a b, find eqA a l1 = Some b -> find eqA a l = Some b) /\

                            (forall a b, find eqA a l2 = Some b -> find eqA a l = Some b) /\

                            (forall a b, find eqA a l = Some b -> (find eqA a l1 = Some b \/

                                                                                       find eqA a l2 = Some b))

        | None => exists a, exists b1, exists b2, 

                                                  find eqA a l1 = Some b1 /\

                                                  find (A:=A) eqA a l2 = Some b2 /\

                                                  (b1 <> b2)

        end.

Proof.

intros A B eqA eqB l1 l2; generalize l1; clear l1;

induction l2 as [ | [a2 b2] l2]; intros l1 Hl2; simpl.

intuition.

discriminate.

case_eq (find eqA a2 l1).

intros b H; destruct (eqB b2 b) as [b2_eq_b | b2_diff_b].

subst b.

assert (H' := IHl2 l1); destruct (merge eqA eqB l1 l2) as [l | ].

destruct H' as [H1 [H2 H3]].

intros a3 b3 c3 H1 H2; apply (Hl2 a3); right; trivial.

split; trivial.

split.

intros a b; destruct (eqA a a2) as [a_eq_a2 | a_diff_a2].

intros H'; injection H'; clear H'; intros; subst a b; apply H1; trivial.

apply H2; trivial.

intros a b H'; destruct (eqA a a2) as [a_eq_a2 | a_diff_a2].

subst a; rewrite (H1 a2 b2 H) in H'.

injection H'; clear H'; intros; subst b.

right; trivial.

apply H3; trivial.

destruct H' as [a [c1 [c2 [H1 [H2 H3]]]]].

intros a3 b3 c3 H1 H2; apply (Hl2 a3); right; trivial.

exists a; exists c1; exists c2; split; trivial.

split; trivial.

destruct (eqA a a2) as [a_eq_a2 | a_diff_a2].

subst a.

rewrite (Hl2 a2 b2 c2); trivial.

left; trivial.

right; destruct (find_mem _ _ _ H2) as [l2' [l2'' H']]; subst.

apply in_or_app; right; left; trivial.

trivial.

exists a2; destruct (eqA a2 a2) as [_ | a2_diff_a2].

exists b; exists b2; split; trivial; split; trivial.

intro; subst b2; absurd (b = b); trivial.

absurd (a2 =a2); trivial.




intro H; 

assert (H' := IHl2 ((a2,b2) :: l1)); destruct (merge eqA eqB ((a2, b2) :: l1) l2) as [l | ].

destruct H' as [H1 [H2 H3]].

intros a3 b3 c3 H1 H2; apply (Hl2 a3); right; trivial.

split.

intros a b H'; apply H1; simpl.

destruct (eqA a a2) as [a_eq_a2 | a_diff_a2]; trivial.

subst a; rewrite H' in H; discriminate.

split.

intros a b; destruct (eqA a a2) as [a_eq_a2 | a_diff_a2].

intros H'; injection H'; clear H'; intros; subst a b; apply H1.

simpl; destruct (eqA a2 a2) as [_ | a2_diff_a2]; trivial.

absurd (a2 =a2); trivial.

apply H2; trivial.

intros a b H'; generalize (H3 a b H'); simpl; destruct (eqA a a2) as [a_eq_a2 | a_diff_a2].

intuition.

right; rewrite (Hl2 a b2 b); trivial.

subst; left; trivial.

destruct (@find_mem A B eqA _ _ _ H4) as [k1 [k2 K]]; subst.

right; apply in_or_app; right; left; trivial.

trivial.

assert (Hl2' : forall (a2 : A) (b2 c2 : B), In (a2, b2) l2 -> In (a2, c2) l2 -> b2 = c2).

intros a3 b3 c3 H1 H2; apply (Hl2 a3); right; trivial.

destruct (H' Hl2') as [a [c1 [c2 [H1 [H2 H3]]]]]; clear H'.

simpl in H1; destruct (eqA a a2) as [a_eq_a2 | a_diff_a2]; trivial.

injection H1; clear H1; intros; subst b2 a2.

absurd (c1 = c2); trivial.

apply (Hl2 a c1 c2).

left; trivial.

right; destruct (find_mem _ _ _ H2) as [k1 [k2 K]]; subst.

apply in_or_app; right; left; trivial.

exists a; exists c1; exists c2; subst; split; trivial; split; trivial.

destruct (eqA a a2) as [a_eq_a2 | _]; trivial.

absurd (a = a2); trivial.

Qed.




Lemma merge_inv :

  forall (A B : Set) eqA eqB (l1 l2 : list (A*B)), 

       (forall a1 b1 c1, In (a1,b1) l1 -> In (a1,c1) l1 -> b1 = c1) ->

       (forall a2 b2 c2, In (a2,b2) l2 -> In (a2,c2) l2 -> b2 = c2) ->

       match merge eqA eqB l1 l2 with

       | Some l => (forall a b c, In (a,b) l -> In (a,c) l -> b = c) 

       | None => True

       end.

Proof.

intros A B eqA eqB l1 l2; generalize l1; clear l1;

induction l2 as [ | [a2 b2] l2]; intros l1 Inv1 Inv2; simpl.

exact Inv1.

case_eq (find eqA a2 l1).

intros b H; destruct (eqB b2 b) as [b2_eq_b | b2_diff_b].

subst b.

assert (H' := IHl2 l1 Inv1); destruct (merge eqA eqB l1 l2) as [l | ].

apply H'.

intros a3 b3 c3 K1 K2; apply (Inv2 a3); right; trivial.

trivial.

trivial.




intro H; 

assert (H' := IHl2 ((a2,b2) :: l1)); 

case_eq (merge eqA eqB ((a2, b2) :: l1) l2).

intros l H''; rewrite H'' in H'; apply H'.

intros a1 b1 c2 [a1b1_eq_a2b2 | a1b1_in_l1] [a1c1_eq_a2b2 | a1c1_in_l1].

injection a1b1_eq_a2b2; clear a1b1_eq_a2b2; intros; subst.

injection a1c1_eq_a2b2; clear a1c1_eq_a2b2; intros; subst; trivial.

injection a1b1_eq_a2b2; clear a1b1_eq_a2b2; intros; subst.

assert False.

apply (find_not_found eqA a1 c2 l1); trivial.

contradiction.

injection a1c1_eq_a2b2; clear a1c1_eq_a2b2; intros; subst.

assert False.

apply (find_not_found eqA a1 b1 l1); trivial.

contradiction.

apply (Inv1 a1); trivial.

intros a3 b3 c3 K1 K2; apply (Inv2 a3); right; trivial.

trivial.

Qed.

number of occurences of the first element of a pair.


Function nb_occ (A B : Set) (eqA : forall (a1 a2 : A), {a1=a2}+{a1<>a2})

  (a : A) (l : list (A * B)) {struct l} : nat :=

  match l with

  | nil => 0

  | (a',_) :: tl =>

     if (eqA a a' : sumbool _ _) then S (nb_occ eqA a tl) else nb_occ eqA a tl

  end.




Lemma nb_occ_app :

  forall (A B : Set) (eqA : forall (a1 a2 : A), {a1=a2}+{a1<>a2})

  a (l1 l2 : list (A * B)), 

  nb_occ eqA a (l1++l2) = nb_occ eqA a l1 + nb_occ eqA a l2.

Proof.

intros A B eqA a l1; induction l1 as [ | [a1 b1] l1]; simpl; trivial.

intro l2; rewrite IHl1; destruct (eqA a a1) as [_ | _]; trivial.

Qed.




Lemma none_nb_occ_O :

  forall (A B : Set) (eqA : forall (a1 a2 : A), {a1=a2}+{a1<>a2})

  (a : A) (l : list (A * B)),

  find eqA a l = None -> nb_occ eqA a l = 0.

Proof.

intros A B eqA a l; 

functional induction (find eqA a l) 

     as [ A B eqA a l l_eq_nil
          | A B eqA a l a1 b1 l' l_eq_a1_b1_l' a_eq_a1 _
          | A B eqA a l a1 b1 l' l_eq_a1_b1_l' a_diff_a1 _H IH].

trivial.

intros; discriminate.

intros; simpl; rewrite _H; apply IH; trivial.

Qed.




Lemma some_nb_occ_Sn :

  forall (A B : Set) (eqA : forall (a1 a2 : A), {a1=a2}+{a1<>a2})

  (a : A) (l : list (A * B)) b,

  find eqA a l = Some b -> 1 <= nb_occ eqA a l.

Proof.

intros A B eqA a l;

functional induction (find eqA a l) 

     as [ A B eqA a l l_eq_nil
          | A B eqA a l a1 b1 l' l_eq_a1_b1_l' a_eq_a1 _H
          | A B eqA a l a1 b1 l' l_eq_a1_b1_l' a_diff_a1 _H IH].

intros; discriminate.

intros; simpl; rewrite _H; auto with arith.

intros; simpl; rewrite _H; apply IH with b; trivial.

Qed.




Lemma reduce_assoc_list :

  forall (A B : Set) (eqA : forall (a1 a2 : A), {a1=a2}+{a1<>a2}),

  forall (l : list (A * B)), exists l', 

 (forall a, nb_occ eqA a l' <= 1) /\ (forall a, find eqA a l = find eqA a l').

Proof.

intros A B eqA l; induction l as [ | [a b] l].

exists (nil : list (A * B)); split; trivial; auto.

destruct IHl as [l' [IH1 IH2]].

assert (H := @f_equal _ _ (fun a => find eqA a l') a); cbv beta in H;

destruct (find eqA a l') as [ b' | ];

generalize (sym_eq (H _ (refl_equal _))); clear H; intro H.

destruct (find_mem eqA a l' H) as [l1 [l2 H'']];

exists ((a,b) :: l1 ++ l2); split.

intro a'; generalize (IH1 a'); subst l'; simpl; do 2 rewrite nb_occ_app; simpl; 

destruct (eqA a' a); [rewrite plus_comm; simpl; rewrite plus_comm | idtac]; trivial.

intro a'; simpl; destruct (eqA a' a); [trivial | rewrite IH2; subst l'].

clear IH1 IH2 H; induction l1 as [ | [a1 b1] l1].

simpl; destruct (eqA a' a) as [a'_eq_a | _]; [absurd (a' = a) | idtac]; trivial.

simpl; rewrite IHl1; trivial.

exists ((a,b) :: l'); split.

intro a'; simpl; destruct (eqA a' a) as [a'_eq_a | _]; [idtac | trivial];

subst a'; rewrite (none_nb_occ_O eqA _ _ H); auto with arith.

intro a'; simpl; rewrite IH2; trivial.

Qed.




Lemma insert_1 :

forall (A : Set) (l1 l2 r1 r2 : list A) (a b : A), l1 ++ l2 = r1 ++ b :: r2 ->

 exists r1', exists r2', l1 ++ a :: l2 = r1' ++ b :: r2'.

Proof.

intros A l1; induction l1 as [ | a1 l1].

simpl; intros l2 r1 r2 a b H; rewrite H; exists (a :: r1); exists r2; simpl; trivial.

intros l2 [ | b1 r1] r2 a b H; simpl in H;

injection H; clear H; intros H a1_eq; subst a1.

exists (@nil A); exists (l1 ++ a :: l2); simpl; trivial.

destruct (IHl1 _ _ _ a _ H) as [r1' [r2' H']]; simpl; rewrite H'.

exists (b1 :: r1'); exists r2'; simpl; trivial.

Qed.




Lemma insert_2 :

forall (A : Set) (l1 l2 r1 r2 r3 : list A) (a b b' : A), 

  l1 ++ l2 = r1 ++ b :: r2 ++ b' :: r3 ->

 exists r1', exists r2', exists r3', l1 ++ a :: l2 = r1' ++ b :: r2' ++ b' :: r3'.

Proof.

intros A l1; induction l1 as [ | a1 l1].

simpl; intros l2 r1 r2 r3 a b b' H; rewrite H; 

exists (a :: r1); exists r2; exists r3; simpl; trivial.

intros l2 [ | b1 r1] r2 r3 a b b' H; simpl in H;

injection H; clear H; intros H a1_eq; subst a1.

destruct (insert_1 l1 l2  r2 r3 a b' H) as [r2' [r3' H']]; simpl; rewrite H'.

exists (@nil A); exists r2'; exists r3'; simpl; trivial.

destruct (IHl1 l2 r1  r2 r3 a b b' H) as [r1' [r2' [r3' H']]]; simpl; rewrite H'.

exists (b1 :: r1'); exists r2'; exists r3'; simpl; trivial.

Qed.




Function list_forall (A : Set) (f : A -> bool) (l : list A) {struct l} : bool :=

  match l with 

  | nil => true

  | a :: l => ifb (f a) (list_forall f l) false

  end.




Lemma list_forall_app :

   forall (A : Set) (f : A -> bool) (l1 l2 : list A),

   list_forall f (l1 ++ l2) = Bool.andb (list_forall f l1) (list_forall f l2).

Proof.

intros A f l1; induction l1 as [ | a1 l1]; simpl; trivial.

intro l2; rewrite (IHl1 l2); destruct (f a1); simpl; trivial.

Qed.




Lemma list_forall_is_sound :

  forall (A : Set) P (P_dec : forall a, {P a}+{~P a}) (l : list A),

  list_forall (fun a => if P_dec a then true else false) l = true <-> 

  (forall a, In a l -> P a).

Proof.

intros A P P_dec l; induction l as [ | a l]; simpl.

intuition.

destruct (P_dec a) as [Pa | not_Pa]; simpl; split; intro H.

intros b [a_eq_b | b_in_l]; [subst | apply ((proj1 IHl) H) ]; trivial.

setoid_rewrite IHl; intros; apply H; right; trivial.

discriminate.

absurd (P a); trivial; apply H; left; trivial.

Qed.




Lemma list_forall_impl :

  forall (A : Set) (f f' : A -> bool) (l : list A), 

  (forall a, In a l -> f a = true -> f' a = true) ->

  (list_forall f l) = true -> (list_forall f' l) = true.

Proof.

intros A f f' l; induction l as [ | a l]; simpl; trivial.

intros Hl; assert (Ha := Hl a (or_introl _ (refl_equal _))).

destruct (f a); simpl.

intro H; rewrite IHl; simpl; trivial.

rewrite (Ha (refl_equal _)); trivial.

intros; apply Hl; trivial; right; trivial.

intro; absurd (false = true); trivial; discriminate.

Qed.




Function list_forall2 (A B : Set) (f : A -> B -> bool) (l : list A) (l' : list B){struct l} : bool :=

  match l, l' with 

  | nil, nil => true

  | (a :: l), (b :: l') => ifb (f a b) (list_forall2 f l l') false

  | _, _ => false

  end.




Lemma list_forall2_is_sound :

  forall (A B : Set) (f : A -> B -> bool) (l : list A) (l' : list B),

  list_forall2 f l l' = true <-> 

  (length l = length l' /\ forall a b, In (a,b) (combine l l') -> f a b = true).

Proof.

intros A B f l; induction l as [ | a l]; destruct l' as [ | b l'].

simpl; intuition.

simpl; intuition; discriminate.

simpl; intuition; discriminate.

simpl; intuition.

destruct (f a b); try discriminate; simpl in H;

destruct (proj1 (IHl l') H) as [H' _]; rewrite H'; trivial.

injection H1; intros; subst a0 b0; 

destruct (f a b); try discriminate; trivial.

destruct (f a b); try discriminate; simpl in H;

destruct (proj1 (IHl l') H) as [_ H']; apply H'; trivial.

rewrite (H1 a b (or_introl _ (refl_equal _))); simpl.

apply (proj2 (IHl l')); split.

injection H0; trivial.

intros; apply H1; right; trivial.

Qed.




Function list_forall_option (A : Set) (f : A -> option bool) (l : list A) 

  {struct l} : option bool :=

  match l with 

  | nil => Some true

  | a :: l => match f a with

                  | None => None

                  | Some true => list_forall_option f l

                  | Some false =>

                         match list_forall_option f l with

                         | None => None

                         | Some _ => Some false

                         end

                  end

 end.




Lemma list_forall_option_is_sound :

  forall (A : Set) f l,

  match @list_forall_option A f l with

  | Some true => forall a, In a l -> f a = Some true

  | Some false => (exists a, In a l /\ f a = Some false) /\ 

                            (forall a, In a l -> f a = None -> False)

  | None => exists a, In a l /\ f a = None

  end.

Proof.

intros A f l; induction l as [ | a l].

simpl; intros; contradiction.

simpl; assert (Fa : forall b, b = a -> f b = f a).

intros; subst; trivial.

destruct (f a) as [ [ | ] | ]; generalize (Fa _ (refl_equal _)); clear Fa; intro Fa.

destruct (list_forall_option f l) as [ [ | ] | ].

intros b [b_eq_a | b_in_l]; [subst; rewrite Fa | rewrite IHl]; trivial.

destruct IHl as [[b [b_in_l fb_eq_false]] IHl].

split.

exists b; split; trivial; right; trivial.

intros c [c_eq_a | c_in_l]; 

[ subst; rewrite Fa; discriminate
| apply IHl; trivial].

destruct IHl as [b [b_in_l fb_eq_none]]; exists b; split; trivial; right; trivial.

destruct (list_forall_option f l) as [ [ | ] | ].

split.

exists a; split; trivial; left; trivial.

intros b [b_eq_a | b_in_l]; 

[ subst; rewrite Fa | rewrite IHl; trivial]; discriminate.

destruct IHl as [[b [b_in_l fb_eq_false]] IHl].

split.

exists a; split; trivial; left; trivial.

intros c [c_eq_a | c_in_l]; 

[ subst; rewrite Fa; discriminate | apply IHl; trivial].

destruct IHl as [b [b_in_l fb_eq_none]]; exists b; split; trivial; right; trivial.

exists a; split; trivial; left; trivial.

Qed.




Lemma list_forall_option_is_complete_true :

  forall (A : Set) f l, (forall a, In a l -> f a = Some true) ->

    @list_forall_option A f l = Some true.

Proof.

intros A f l; induction l as [ | a l].

simpl; intros; trivial.

intro H; simpl; rewrite (H _ (or_introl _ (refl_equal _)));

apply IHl; intros; apply H; right; trivial.

Qed.




Lemma list_forall_option_is_complete_false :

  forall (A : Set) f l, (exists a, In a l /\ f a = Some false) ->

                            (forall a, In a l -> f a = None -> False) ->

    @list_forall_option A f l = Some false.

Proof.

intros A f l; induction l as [ | a l].

intros [a [a_in_nil _]] _; contradiction.

intros [b [[b_eq_a | b_in_l] fb_eq_false]] H; simpl.

subst b; rewrite fb_eq_false.

generalize (list_forall_option_is_sound f l);

destruct (list_forall_option f l) as [ [ | ] | ]; trivial.

intros [c [c_in_l fc_eq_none]].

assert (H' := H c (or_intror _ c_in_l) fc_eq_none); contradiction.

generalize (H a (or_introl _ (refl_equal _))); destruct (f a) as [ [ | ] | ].

intros _; apply IHl.

exists b; split; trivial.

intros c c_in_l; apply H; right; trivial.

intros;

generalize (list_forall_option_is_sound f l);

destruct (list_forall_option f l) as [ [ | ] | ]; trivial.

intros [c [c_in_l fc_eq_none]].

assert (H' := H c (or_intror _ c_in_l) fc_eq_none); contradiction.

intro H'; generalize (H' (refl_equal _)); contradiction.

Qed.




Function list_exists (A : Set) (f : A -> bool) (l : list A) {struct l} : bool :=

  match l with

  | nil => false

  | a :: l => ifb (f a) true (list_exists f l)

  end.




Lemma list_exists_app :

   forall (A : Set) (f : A -> bool) (l1 l2 : list A),

   list_exists f (l1 ++ l2) = Bool.orb (list_exists f l1) (list_exists f l2).

Proof.

intros A f l1; induction l1 as [ | a1 l1]; simpl; trivial.

intro l2; rewrite (IHl1 l2); destruct (f a1); simpl; trivial.

Qed.




Lemma list_exists_is_sound :

  forall (A : Set) (f : A -> bool) (l : list A),

  list_exists f l = true <-> 

  (exists a, In a l /\ f a = true).

Proof.

intros A f l; induction l as [ | a l]; simpl.

split; [intros; discriminate | intros [a [Abs _]]; contradiction].

assert (H: forall a', a' = a -> f a' = f a).

intros; subst; trivial.

destruct (f a) as [fa | not_fa]; simpl; 

generalize (H _ (refl_equal _)); clear H; intro H;

split; intro H'.

exists a; split; trivial; left; trivial.

trivial.

destruct ((proj1 IHl) H') as [a' [a'_in_l fa']]; exists a'; split; trivial; right; trivial.

destruct H' as [a' [[a_eq_a' | a'_in_l] fa']].

subst a'; rewrite H in fa'; absurd (false = true); trivial; discriminate.

apply (proj2 IHl); exists a'; split; trivial.

Qed.




Lemma list_exists_impl :

  forall (A : Set) (f f' : A -> bool) (l : list A), 

  (forall a, In a l -> f a = true -> f' a = true) ->

  (list_exists f l) = true -> (list_exists f' l) = true.

Proof.

intros A f f' l; induction l as [ | a l]; simpl; trivial.

intros Hl; assert (Ha := Hl a (or_introl _ (refl_equal _))).

destruct (f a); simpl.

rewrite (Ha (refl_equal _)); trivial.

intro H; rewrite IHl; simpl; trivial.

destruct (f' a); trivial.

intros; apply Hl; trivial; right; trivial.

Qed.




Function list_exists_option (A : Set) (f : A -> option bool) (l : list A) 

 {struct l} : option bool :=

  match l with

  | nil => Some false

  | a :: l => match f a with

                  | Some true => Some true

                  | Some false => (list_exists_option f l)

                  | None => 

                         match list_exists_option f l with

                         | Some true => Some true

                         | _ => None

                         end

                 end

 end.




Lemma list_exists_option_is_sound :

  forall (A : Set) f l,

  match @list_exists_option A f l with

  | Some true => exists a, In a l /\ f a = Some true

  | Some false => forall a, In a l -> f a = Some false

  | None => (exists a, In a l /\ f a = None) /\ 

                   (forall a, In a l -> f a = Some true -> False)

  end.

Proof.

intros A f l; induction l as [ | a l].

simpl; intros; contradiction.

simpl; assert (Fa : forall b, b = a -> f b = f a).

intros; subst; trivial.

destruct (f a) as [ [ | ] | ]; generalize (Fa _ (refl_equal _)); clear Fa; intro Fa.

destruct (list_exists_option f l) as [ [ | ] | ];

exists a; split; trivial; left; trivial.

destruct (list_exists_option f l) as [ [ | ] | ].

destruct IHl as [b [b_in_l fb_eq_true]]; exists b; split; trivial; right; trivial.

intros b [b_eq_a | b_in_l]; [subst; rewrite Fa | rewrite IHl]; trivial.

destruct IHl as [ [b [b_in_l fb_eq_none]] IHl]; split.

exists b; split; trivial; right; trivial.

intros c [c_eq_a | c_in_l]; 

[ subst; rewrite Fa; discriminate | apply IHl; trivial].

destruct (list_exists_option f l) as [ [ | ] | ].

destruct IHl as [b [b_in_l fb_eq_true]]; exists b; split; trivial; right; trivial.

split.

exists a; split; trivial; left; trivial.

intros b [b_eq_a | b_in_l]; 

[ subst; rewrite Fa | rewrite IHl; trivial]; discriminate.

split.

exists a; split; trivial; left; trivial.

destruct IHl as [ _ IHl]; intros b [b_eq_a | b_in_l]; 

[ subst; rewrite Fa; discriminate | apply IHl; trivial].

Qed.




Lemma list_exists_option_is_complete_true :

  forall (A : Set) f l, (exists a, In a l /\ f a = Some true) ->

                       @list_exists_option A f l = Some true.

Proof.

intros A f l; induction l as [ | a l].

simpl; intros [a [a_in_nil fa_eq_true]]; contradiction.

intros [b [[b_eq_a | b_in_l] fb_eq_true]]; simpl.

subst b; rewrite fb_eq_true; trivial.

destruct (f a) as [ [ | ] | ]; trivial.

rewrite IHl; trivial; exists b; split; trivial.

rewrite IHl; trivial; exists b; split; trivial.

Qed.




Lemma list_exists_option_is_complete_false :

  forall (A : Set) f l, (forall a, In a l -> f a = Some false) ->

                       @list_exists_option A f l = Some false.

Proof.

intros A f l; induction l as [ | a l].

intros; simpl; trivial.

intros H; simpl.

rewrite (H _ (or_introl _ (refl_equal _))); 

apply IHl; intros; apply H; right; trivial.

Qed.




Lemma list_exists_option_is_complete_none :

 forall A f l, (exists a, In a l /\ f a = None) ->

                   (forall a, In a l -> f a = Some true -> False) ->

                       @list_exists_option A f l = None.

Proof.

intros A f l; induction l as [ | t l].

intros [a [a_in_nil _]]; contradiction.

simpl; intros [a [[a_eq_t | a_in_l] fa_eq_none]] H.

subst a; rewrite fa_eq_none.

generalize (list_exists_option_is_sound f l);

destruct (list_exists_option f l) as [ [ | ] | ]; trivial.

intros [a [a_in_l fa_eq_true]]; 

assert False; [idtac | contradiction].

apply (H a); trivial; right; trivial.

generalize (H t (or_introl _ (refl_equal _))); destruct (f t) as [ [ | ] | ].

intro H'; assert (H'' := H' (refl_equal _)); contradiction.

intros _; apply IHl.

exists a; split; trivial.

intros b b_in_l; apply H; right; trivial.

intros _; generalize (list_exists_option_is_sound f l);

destruct (list_exists_option f l) as [ [ | ] | ].

intros [b [b_in_l fb_eq_true]]; 

assert False; [idtac | contradiction].

apply (H b); trivial; right; trivial.

trivial.

trivial.

Qed.




Definition list_exists_rest (A : Set) (P : A -> Prop) l 

(P_dec : forall a, In a l -> {P a}+{~P a}) : bool.

Proof.

intros A P l; induction l as [ | a l]; intro P_dec.

exact false.

case (P_dec a (or_introl _ (refl_equal _))).

intros; exact true.

intros; assert (P_dec' : forall a : A, In a l -> {P a} + {~ P a}).

intros; apply P_dec; right; trivial.

exact (IHl P_dec').

Defined.




Lemma list_exists_rest_is_sound :

  forall (A : Set) (P : A -> Prop) l P_dec,

  list_exists_rest P l P_dec= true <->  (exists a, In a l /\ P a).

Proof.

intros A P l; induction l as [ | a l]; intros P_dec; simpl.

split; [intros; discriminate | intros [a [Abs _]]; contradiction].

destruct (P_dec a) as [Pa | not_Pa].

split; trivial.

intros _; exists a; split; trivial; left; trivial.

split.

intro H; setoid_rewrite IHl in H.

destruct H as [b [b_in_l Pb]]; exists b; split; trivial; right; trivial.

intro H; destruct H as [b [[b_eq_a | b_in_l] Pb]].

subst b; absurd (P a); trivial.

setoid_rewrite IHl; exists b; split; trivial.

Qed.




Fixpoint mapi (A : Set) (f : A -> A) (l : list A) {struct l} : list (list A) :=

  match l  with

  | nil => nil

  | a :: l => ((f a) :: l) :: (map (fun k => a :: k) (mapi f l))

  end.




Lemma mapi_spec :

  forall (A : Set) (f : A -> A) l l',

  (In l' (mapi f l) <-> exists l1, exists a, exists l2, l = l1 ++ a :: l2 /\ l' = l1 ++ (f a) :: l2).

Proof.

intros A f l; induction l as [ | a l]; intros l'; split; intro H.

contradiction.

destruct H as [[ | a1 l1] [a [l2 [H _]]]]; discriminate.

simpl in H; destruct H as [H | H].

exists (@nil A); exists a; exists l; split; subst; trivial.

setoid_rewrite in_map_iff in H; destruct H as [l'' [H1 H2]].

setoid_rewrite (IHl l'') in H2.

destruct H2 as [l1 [b [l2 [K K']]]].

exists (a :: l1); exists b; exists l2; subst; split; trivial.

destruct H as [l1 [b [l2 [K K']]]]; subst.

destruct l1 as [ | a1 l1]; simpl in K; injection K; clear K; intros; subst.

simpl; left; trivial.

right; simpl; setoid_rewrite in_map_iff.

exists (l1 ++ f b :: l2); split; trivial.

setoid_rewrite IHl.

exists l1; exists b; exists l2; split; trivial.

Qed.




Fixpoint mapii (A : Set) (f : A -> list A) (l : list A) {struct l} : list (list A) :=

  match l  with

  | nil => nil

  | a :: l => (map (fun b => b :: l) (f a)) ++ (map (fun k => a :: k) (mapii f l))

  end.




Lemma mapii_spec :

  forall (A : Set) (f : A -> list A) l l',

  (In l' (mapii f l) <-> exists l1, exists a, exists b, exists l2, 

                                  In b (f a) /\ l = l1 ++ a :: l2 /\ l' = l1 ++ b :: l2).

Proof.

intros A f l; induction l as [ | a l]; intros l'; split; intro H.

contradiction.

destruct H as [[ | a1 l1] [a [b [l2 [_ [H _]]]]]]; discriminate.

simpl in H; destruct (in_app_or _ _ _ H) as [H' | H']; clear H; rename H' into H.

setoid_rewrite in_map_iff in H; destruct H as [b [H1 H2]].

exists (@nil A); exists a; exists b; exists l; subst; repeat split; trivial.

setoid_rewrite in_map_iff in H; destruct H as [l'' [H1 H2]].

setoid_rewrite (IHl l'') in H2.

destruct H2 as [l1 [a' [b [l2 [K [K' K'']]]]]].

exists (a :: l1); exists a'; exists b; exists l2; subst; repeat split; trivial.

destruct H as [l1 [a' [b [l2 [K [K' K'']]]]]]; subst.

destruct l1 as [ | a1 l1]; simpl in K'; injection K'; clear K'; intros; subst.

simpl; apply in_or_app; left; setoid_rewrite in_map_iff; exists b; split; trivial.

simpl; apply in_or_app; right; simpl; setoid_rewrite in_map_iff.

exists (l1 ++ b :: l2); split; trivial.

setoid_rewrite IHl.

exists l1; exists a'; exists b; exists l2; repeat split; trivial.

Qed.




Section DepFun.

Variable A : Set.




Inductive dep_fun : Set :=

  | Dep_fun : forall (l : list A) (f : forall t, In t l -> list A), dep_fun.




Definition o_length (lf1 lf2: dep_fun) := 

  match lf1, lf2 with

  | Dep_fun l1 _, Dep_fun l2 _ => length l1 < length l2

  end.




Lemma wf_length : well_founded o_length.

Proof.

unfold well_founded, o_length.

intros [l f]; apply Acc_intro.

generalize (length l); clear f l.

intro n; induction n as [ | n].

intros [y f] Abs; absurd (length y < 0); auto with arith.

intros [y f] Sy; inversion Sy; subst.

apply Acc_intro; intros x Sx; apply IHn; trivial.

apply IHn; trivial.

Defined.




Definition dep_fun_tail (a : A) (l : list A) (f : forall t, In t (a :: l) -> list A) : dep_fun.

intros a l f.

assert (f' : forall t, In t l -> list A).

intros t t_in_l; exact (f t (or_intror _ t_in_l)).

exact (Dep_fun l f').

Defined.




Lemma map_dep_call :

  forall a l f, o_length (dep_fun_tail f) (Dep_fun (a :: l) f).

Proof.

intros a f l; simpl; auto with arith.

Qed.




Definition F_mapii: 

    forall (lf : dep_fun) (mrec : forall lf', o_length lf' lf -> list (list A)), list (list A).

Proof.

intros [l f] mrec; destruct l as [ | a l].

exact nil.

exact (map (fun b => b :: l) (f a (or_introl _ (refl_equal _))) ++ 

          (map (fun k => a :: k) (mrec (dep_fun_tail f) (map_dep_call f)))).

Defined.




Definition mapii_dep : dep_fun -> list (list A) :=

Fix wf_length (fun lf => list (list A)) F_mapii.




Lemma mapii_dep_unfold : 

  forall lf : dep_fun, mapii_dep lf = @F_mapii lf (fun y _ => mapii_dep y).

Proof.

intros lf; unfold mapii_dep.

refine (Fix_eq _ _ _ _ lf).

clear lf; intros [l f] F G H.

unfold F_mapii; destruct l as [ | a l]; simpl; auto.

rewrite H; trivial.

Qed.




Lemma mapii_dep_spec :

  (forall a1 a2 : A, {a1 = a2}+{a1 <> a2}) -> forall l f l',

  (forall a a_in_l a_in_l', f a a_in_l = f a a_in_l') ->

  (In l' (mapii_dep (Dep_fun l f)) <-> exists l1, exists a, exists a_in_l, exists b, exists l2,  

                                  In b (f a a_in_l) /\ l = l1 ++ a :: l2 /\ l' = l1 ++ b :: l2).

Proof.

intros eqA l; induction l as [ | a l]; intros f l' proof_ir; split; intro H.

contradiction.

destruct H as [[ | a1 l1] [a [a_in_l [b [l2 [_ [H _]]]]]]]; discriminate.

rewrite mapii_dep_unfold in H; simpl in H.

destruct (in_app_or _ _ _ H) as [H' | H']; clear H; rename H' into H.

setoid_rewrite in_map_iff in H; destruct H as [b [H1 H2]].

exists (@nil A); exists a; 

exists (or_introl

             ((fix In (a : A) (l : list A) {struct l} : Prop :=

                 match l with

                 | nil => False

                 | b :: m => b = a \/ In a m

                 end) a l) (refl_equal a));

exists b; exists l; subst; repeat split; trivial.

setoid_rewrite in_map_iff in H; destruct H as [l'' [H1 H2]].

unfold dep_fun_tail in H2.

setoid_rewrite IHl in H2.

destruct H2 as [l1 [a' [a'_in_l [b [l2 [K [K' K'']]]]]]].

exists (a :: l1); exists a'; exists (or_intror (a = a') a'_in_l);

exists b; exists l2; subst; repeat split; trivial.

intros; apply proof_ir; right; trivial.

destruct H as [l1 [a' [a'_in_l [b [l2 [K [K' K'']]]]]]]; subst.

destruct l1 as [ | a1 l1]; simpl in K'; injection K'; clear K'; intros.

subst l2 a'.

simpl; rewrite mapii_dep_unfold; simpl.

apply in_or_app; left; setoid_rewrite in_map_iff; exists b; split; trivial.

simpl; rewrite <- (proof_ir a a'_in_l); trivial.

rewrite mapii_dep_unfold; simpl.

apply in_or_app; right; simpl; setoid_rewrite in_map_iff.

exists (l1 ++ b :: l2); split; subst a1; trivial.

unfold dep_fun_tail.

setoid_rewrite IHl.

intros; apply proof_ir; right; trivial.

destruct (eqA a a') as [a_eq_a' | a_diff_a'].

subst a'.

assert (a_in_l : In a l).

clear K; subst l; apply in_or_app; right; left; trivial.

exists l1; exists a; exists a_in_l; exists b; exists l2; repeat split; trivial.

rewrite <- (proof_ir a a'_in_l); trivial.

assert (a'_in_l' : In a' l).

clear K; destruct a'_in_l as [a'_eq_a | a'_in_l]; trivial.

absurd (a = a'); trivial.

exists l1; exists a'; exists a'_in_l'; exists b; exists l2; repeat split; trivial.

rewrite <- (proof_ir a' a'_in_l); trivial.

Qed.




Lemma mapii_dep_eq :

  forall l f g, (forall t (t_in_l : In t l), f t t_in_l = g t t_in_l) -> 

  mapii_dep (Dep_fun l f) = mapii_dep (Dep_fun l g).

Proof.

intro l; induction l as [ | a l]; intros f g H; do 2 rewrite mapii_dep_unfold; simpl; trivial.

rewrite (H a).

apply (f_equal (fun ll =>

 map (fun b : A => b :: l)

  (g a

     (or_introl

        ((fix In (a0 : A) (l0 : list A) {struct l0} : Prop :=

            match l0 with

            | nil => False

            | b :: m => b = a0 \/ In a0 m

            end) a l) (refl_equal a))) ++

   map (fun k : list A => a :: k) ll)).

unfold dep_fun_tail.

apply IHl.

intros; apply H; right; trivial.

Qed.

End DepFun.

map_without_repetition applies a function to the elements of a list, but only a single time when there are several consecutive occurences of the same element. Moreover, the function is supposed to return an option as a result, in order to simulate exceptions, and the abnormal results are discarted.





Function map_without_repetition (A B : Set) 

  (eqA : forall (a1 a2 : A), {a1=a2}+{a1<>a2}) 

  (f : A -> option B) (l : list A) {struct l} : list B :=

    match l with

    | nil => (nil : list B)

    | a1 :: l1 =>

           match l1 with

           | nil =>

              match f a1 with

              | None => nil

              | Some b1 => b1 :: nil

              end

           | a2 :: _ =>

              if (eqA a1 a2 : sumbool _ _)

              then map_without_repetition eqA f l1

              else 

                 match f a1 with

                 | None => map_without_repetition eqA f l1

                 | Some b1 => b1 :: (map_without_repetition eqA f l1)

                 end

           end

      end.




Lemma prop_map_without_repetition :

 forall (A B : Set) (eqA : forall (a1 a2 : A), {a1=a2}+{a1<>a2}) 

  (P : B -> Prop) f l,

  (forall a, In a l -> 

   match f a with 

   | None => True 

   | Some f_a => P f_a

   end) ->

   (forall b, In b (map_without_repetition eqA f l) -> P b).

Proof.

intros A B eqA P f l H; 

functional induction (map_without_repetition eqA f l)

     as [ (* Case 1 *) A B eqA f
          | (* Case 2 *) A B eqA f l a1 l1 l_eq_a1_l1 l1_eq_nil fa1_eq_none 
          | (* Case 3 *) A B eqA f l a1 l1 l_eq_a1_l1 l1_eq_nil b1 fa1_eq_b1 
          | (* Case 4 *) A B eqA f l a1 l1 l_eq_a1_l1 a2 l2 l1_eq_a2_l2 a1_eq_a2 _ IH 
          | (* Case 5 *) A B eqA f l a1 l1 l_eq_a1_l1 a2 l2 l1_eq_a2_l2 a1_diff_a2 _ fa1_eq_none IH 
          | (* Case 6 *) A B eqA f l a1 l1 l_eq_a1_l1 a2 l2 l1_eq_a2_l2 a1_diff_a2 _ b1 fa1_eq_b1 IH H1 H2 H3 H4 H5].

contradiction.

contradiction.

intros b [b_eq_b1 | b_in_nil]; 

[subst b; generalize (H a1 (or_introl _ (refl_equal _))); rewrite fa1_eq_b1; trivial
| contradiction].

apply IH; intros; apply H; right; trivial.

apply IH; intros; apply H; right; trivial.

intros b [b_eq_b1 | b_in_map_l1];

[subst b; generalize (H a1 (or_introl _ (refl_equal _))); rewrite fa1_eq_b1; trivial
| apply IH; trivial; intros; apply H; right; trivial ].

Qed.




Lemma exists_map_without_repetition :

  forall (A B : Set) (eqA : forall (a1 a2 : A), {a1=a2}+{a1<>a2}) 

  (P : B -> Prop) f l,

  (exists a,  In a l /\ match f a with 

                        | None => False

                        | Some b => P b

                        end) ->

  (exists b, In b (map_without_repetition eqA f l) /\ P b).

Proof.

intros A B eqA P f l [a [a_in_l P_fa]]; 

functional induction (map_without_repetition eqA f l)

     as [ A B eqA f l l_eq_nil
          | A B eqA f l a1 l1 l_eq_a1_l1 l1_eq_nil fa1_eq_none 
          | A B eqA f l a1 l1 l_eq_a1_l1 l1_eq_nil b1 fa1_eq_b1 
          | A B eqA f l a1 l1 l_eq_a1_l1 a2 l2 l1_eq_a2_l2 a1_eq_a2 _ IH 
          | A B eqA f l a1 l1 l_eq_a1_l1 a2 l2 l1_eq_a2_l2 a1_diff_a2 _ fa1_eq_none IH 
          | A B eqA f l a1 l1 l_eq_a1_l1 a2 l2 l1_eq_a2_l2 a1_diff_a2 _ b1 fa1_eq_b1 IH].

contradiction.

destruct a_in_l as [a_eq_a1 | a_in_nil];

[subst a; rewrite fa1_eq_none in P_fa | idtac]; contradiction.

destruct a_in_l as [a_eq_a1 | a_in_nil];

[subst a; exists b1; split; [ left | rewrite fa1_eq_b1 in P_fa]; trivial | contradiction].

apply (IH P a); 

[destruct a_in_l as [a_eq_a2 | a_in_l1] ; [left | idtac]

| idtac ]; trivial.

apply (IH P a);

[ destruct a_in_l as [a_eq_a1 | a_in_l1]; 

                  [subst a; rewrite fa1_eq_none in P_fa; contradiction | trivial]

| trivial].

destruct a_in_l as [a_eq_a1 | a_in_l1].

exists b1; split; [left | subst a; rewrite fa1_eq_b1 in P_fa]; trivial.

destruct (IH P a a_in_l1 P_fa) as [b [H1 H2]]; 

exists b; split; [right | idtac]; trivial.

Qed.

map12_without_repetition is similar to map_without_repetition, but the applied function returns two optional results instead of one.





Function map12_without_repetition (A B : Set) 

  (eqA : forall (a1 a2 : A), {a1=a2}+{a1<>a2}) 

  (f : A -> option B * option B) (l : list A) {struct l} : list B :=

   match l with

    | nil => (nil : list B)

    | a1 :: l1 =>

           match l1 with

           | nil =>

              match f a1 with

              | (None, None) => nil

              | (Some b1, None) => b1 :: nil

              | (None, Some c1) => c1 :: nil

              | (Some b1, Some c1) => b1 :: c1 :: nil

              end

           | a2 :: _ =>

              if (eqA a1 a2 : sumbool _ _)

              then map12_without_repetition eqA f l1

              else 

                 match f a1 with

                 | (None, None) => map12_without_repetition eqA f l1

                 | (Some b1, None) => b1 :: map12_without_repetition eqA f l1

                 | (None, Some c1) => c1 :: map12_without_repetition eqA f l1

                 | (Some b1, Some c1) => b1 :: c1 :: map12_without_repetition eqA f l1

                  end

           end

      end.




Lemma prop_map12_without_repetition :

  forall (A B : Set) (eqA : forall (a1 a2 : A), {a1=a2}+{a1<>a2}) 

  (P : B -> Prop) f l,

  (forall a, In a l -> 

   match f a with 

   | (None, None) => True 

   | (Some b, None) => P b

   | (None, Some c) => P c

   | (Some b, Some c) => P b /\ P c

   end) ->

 (forall d, In d (map12_without_repetition eqA f l) -> P d).

Proof.

intros A B eqA P f l H;

functional induction (map12_without_repetition eqA f l)

     as [ (* Case 1 *) A B eqA f l l_eq_nil 
          | (* Case 2 *) A B eqA f l a1 l1 l_eq_a1_l1 l1_eq_nil fa1_eq_none 
          | (* Case 3 *) A B eqA f l a1 l1 l_eq_a1_l1 l1_eq_nil b1 fa1_eq_b1 
          | (* Case 4 *) A B eqA f l a1 l1 l_eq_a1_l1 l1_eq_nil c1 fa1_eq_c1 
          | (* Case 5 *) A B eqA f l a1 l1 l_eq_a1_l1 l1_eq_nil b1 c1 fa1_eq_b1_c1 
          | (* Case 6 *) A B eqA f l a1 l1 l_eq_a1_l1 a2 l2 l1_eq_a2_l2 a1_eq_a2 _ IH 
          | (* Case 7 *) A B eqA f l a1 l1 l_eq_a1_l1 a2 l2 l1_eq_a2_l2 a1_diff_a2 _ fa1_eq_none IH 
          | (* Case 8 *) A B eqA f l a1 l1 l_eq_a1_l1 a2 l2 l1_eq_a2_l2 a1_diff_a2 _ b1 fa1_eq_b1 IH 
          | (* Case 9 *) A B eqA f l a1 l1 l_eq_a1_l1 a2 l2 l1_eq_a2_l2 a1_diff_a2 _ c1 fa1_eq_c1 IH 
          | (* Case 10 *) A B eqA f l a1 l1 l_eq_a1_l1 a2 l2 l1_eq_a2_l2 a1_diff_a2 _ b1 c1 fa1_eq_b1_c1 IH].

contradiction.

contradiction.

intros d [d_eq_b1 | d_in_nil]; 

[ subst d; generalize (H a1 (or_introl _ (refl_equal _))); rewrite  fa1_eq_b1; trivial
| contradiction].

intros d [d_eq_c1 | d_in_nil]; 

[ subst d; generalize (H a1 (or_introl _ (refl_equal _))); rewrite  fa1_eq_c1; trivial
| contradiction].

intros d [d_eq_b1 | [d_eq_c1 | d_in_nil]]; 

[ subst d; generalize (H a1 (or_introl _ (refl_equal _))); rewrite  fa1_eq_b1_c1; intuition
| subst d; generalize (H a1 (or_introl _ (refl_equal _))); rewrite  fa1_eq_b1_c1; intuition
| contradiction].

apply (IH P); intros; apply H; right; subst; trivial.

apply (IH P); intros; apply H; right; subst; trivial.

intros d [d_eq_b1 | d_in_map_l1];

[ subst d; generalize (H _ (or_introl _ (refl_equal _))); rewrite fa1_eq_b1
| apply IH; trivial; intros; apply H; right]; trivial.

intros d [d_eq_c1 | d_in_map_l1];

[ subst d; generalize (H _ (or_introl _ (refl_equal _))); rewrite fa1_eq_c1
| apply IH; trivial; intros; apply H; right ]; trivial.

intros d [d_eq_b1 | [d_eq_c1 | d_in_map_l1]];

[ subst d; generalize (H _ (or_introl _ (refl_equal _))); rewrite fa1_eq_b1_c1
| subst d; generalize (H _ (or_introl _ (refl_equal _))); rewrite fa1_eq_b1_c1
| apply IH; trivial; intros; apply H; right ]; intuition.

Qed.




Lemma exists_map12_without_repetition :

  forall (A B : Set) (eqA : forall (a1 a2 : A), {a1=a2}+{a1<>a2}) 

  (P : B -> Prop) f l,

  ((exists a, In a l /\ match f a with 

                        | (None, None) => False

                        | (Some b, None) => P b

                        | (None, Some c) => P c

                        | (Some b, Some c) => P b \/ P c

                        end) ->

  (exists d, In d (map12_without_repetition eqA f l) /\ P d)).

Proof.

intros A B eqA P f l [a [a_in_l P_fa]];

functional induction (map12_without_repetition eqA f l)

     as [ (* Case 1 *) A B eqA f l l_eq_nil 
          | (* Case 2 *) A B eqA f l a1 l1 l_eq_a1_l1 l1_eq_nil fa1_eq_none 
          | (* Case 3 *) A B eqA f l a1 l1 l_eq_a1_l1 l1_eq_nil b1 fa1_eq_b1 
          | (* Case 4 *) A B eqA f l a1 l1 l_eq_a1_l1 l1_eq_nil c1 fa1_eq_c1 
          | (* Case 5 *) A B eqA f l a1 l1 l_eq_a1_l1 l1_eq_nil b1 c1 fa1_eq_b1_c1 
          | (* Case 6 *) A B eqA f l a1 l1 l_eq_a1_l1 a2 l2 l1_eq_a2_l2 a1_eq_a2 _ IH 
          | (* Case 7 *) A B eqA f l a1 l1 l_eq_a1_l1 a2 l2 l1_eq_a2_l2 a1_diff_a2 _ fa1_eq_none IH 
          | (* Case 8 *) A B eqA f l a1 l1 l_eq_a1_l1 a2 l2 l1_eq_a2_l2 a1_diff_a2 _ b1 fa1_eq_b1 IH 
          | (* Case 9 *) A B eqA f l a1 l1 l_eq_a1_l1 a2 l2 l1_eq_a2_l2 a1_diff_a2 _ c1 fa1_eq_c1 IH 
          | (* Case 10 *) A B eqA f l a1 l1 l_eq_a1_l1 a2 l2 l1_eq_a2_l2 a1_diff_a2 _ b1 c1 fa1_eq_b1_c1 IH].

contradiction.

destruct a_in_l as [a_eq_a1 | a_in_nil];

[subst a; rewrite fa1_eq_none in P_fa | idtac]; contradiction.

destruct a_in_l as [a_eq_a1 | a_in_nil];

[subst a; exists b1; split; [ left | rewrite fa1_eq_b1 in P_fa]; trivial | contradiction].

destruct a_in_l as [a_eq_a1 | a_in_nil];

[subst a; exists c1; split; [ left | rewrite fa1_eq_c1 in P_fa]; trivial | contradiction].

destruct a_in_l as [a_eq_a1 | a_in_nil].

subst a; rewrite fa1_eq_b1_c1 in P_fa; destruct P_fa as [P_b1 | P_c1];

[ exists b1; split; [left | idtac]

| exists c1; split; [right; left | idtac]]; trivial.

contradiction.

apply (IH P a); 

[ destruct a_in_l as [a_eq_a2 | a_in_l1] ; [left | idtac]

| idtac ]; trivial.

apply (IH P a);

[ destruct a_in_l as [a1_eq_a | a_in_l1];

   [ subst a1; rewrite fa1_eq_none in P_fa; contradiction | trivial]

| trivial].

destruct a_in_l as [a_eq_a1 | a_in_l1].

exists b1; split; [left | subst a; rewrite fa1_eq_b1 in P_fa]; trivial.

destruct (IH P a a_in_l1 P_fa) as [b [H1 H2]]; 

exists b; split; [right | idtac]; trivial.

destruct a_in_l as [a_eq_a1 | a_in_l1].

exists c1; split; [left | subst a; rewrite fa1_eq_c1 in P_fa]; trivial.

destruct (IH P a a_in_l1 P_fa) as [b [H1 H2]]; 

exists b; split; [right | idtac]; trivial.

destruct a_in_l as [a_eq_a1 | a_in_l1].

subst a1; rewrite fa1_eq_b1_c1 in P_fa; destruct P_fa as [P_b1 | P_c1].

exists b1; split; [left | idtac]; trivial.

exists c1; split; [right; left | idtac]; trivial.

destruct (IH P a a_in_l1 P_fa) as [b [H1 H2]]; 

exists b; split; [right; right | idtac]; trivial.

Qed.




Section S.

Variable A:Set.

Variable A_dec : forall x y:A, {x=y}+{~x=y}.

Fixpoint mem (x:A) (l:list A) : bool := 

  match l with 

    | nil => false 

    | y::l => if (A_dec x y) then true else mem x l

  end.

Lemma In_mem : forall x l, mem x l = true -> In x l.

Proof.

  intros x.

  fix 1.

  intros l;case l.

  intro abs;discriminate abs.

  intros y l'.

  unfold mem.

  case (A_dec x y).

  intros Heq _;left;symmetry;exact Heq.

  intros.

  right.

  apply In_mem.

  exact H.

Defined.




Fixpoint included_list (l1 l2:list A) {struct l1} : bool :=

  match l1 with 

    | nil => true

    | x::l1 => andb (mem x l2) (included_list l1 l2)

  end.




Lemma included_list_sound : 

  forall l1 l2, (included_list l1 l2 = true) -> forall x, In x l1 -> In x l2.

Proof.

  fix 1.

  intros l1 l2;case l1.




  intros _ x abs;elim abs.

  simpl.

  intros a l H x H0.

  case H0.

  intros Heq;rewrite <- Heq.

  apply In_mem.

  case (andb_prop _ _ H );auto.

  apply included_list_sound.

  case (andb_prop _ _ H );auto.




Qed.




End S.