Module CommonList

From Coq Require Import List.
From Coq Require Import Lists.SetoidList.
From Coq Require Import Permutation.
From Coq Require Import Decidable.
From Coq Require Import Relations.
From Coq Require Import Morphisms.
From Coq Require Import Classes.EquivDec.
From Coq Require Import Omega.

From Velus Require Import CommonTactics.

Import List.ListNotations.
Open Scope list_scope.

Section Extra.

  Context {A: Type}.

  Lemma List_shift_first:
    forall ll (x : A) lr,
      ll ++ (x :: lr) = (ll ++ [x]) ++ lr.

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

  Corollary in_app_weak :
    forall (x : A) l l',
      In x l -> In x (l ++ l').

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

  Lemma app_last_app:
    forall xs xs' (x: A),
      (xs ++ [x]) ++ xs' = xs ++ x :: xs'.

  Lemma cons_is_app:
    forall (x: A) xs,
      x :: xs = [x] ++ xs.

  Remark Forall_hd:
    forall (A : Type) (P : A -> Prop) (x : A) (l : list A),
      Forall P (x :: l) -> P x.

  Remark Forall_tl:
    forall (A : Type) (P : A -> Prop) (x : A) (l : list A),
      Forall P (x :: l) -> Forall P l.

  Remark Forall_hd_tl:
    forall (A : Type) (P : A -> Prop) (x : A) (l : list A),
      Forall P (x :: l) -> P x /\ Forall P l.

  Lemma not_in_cons (x a : A) (l : list A):
    ~ In x (a :: l) <-> x <> a /\ ~ In x l.

  Lemma fold_left_map:
    forall {B C} (l: list A) (f: C -> B -> C) (g: A -> B) a,
      fold_left f (map g l) a = fold_left (fun a x => f a (g x)) l a.

  Lemma fold_left_map_fst:
    forall {B C} f xs (acc : C),
      fold_left (fun acc xy => f acc (fst xy)) xs acc
      = fold_left f (map (@fst A B) xs) acc.

  Remark not_In2_app:
    forall (x: A) l1 l2,
      ~ In x l2 ->
      In x (l1 ++ l2) ->
      In x l1.

  Lemma not_In_app:
    forall xs ys (x : A),
      ~In x (xs ++ ys) <-> (~In x xs /\ ~In x ys).

  Lemma partition_switch:
    forall f g,
      (forall x:A, f x = g x) ->
      forall xs, partition f xs = partition g xs.

  Lemma filter_app:
    forall (p:A->bool) xs ys,
      filter p xs ++ filter p ys = filter p (xs ++ ys).

  Remark split_map:
    forall {B C} (xs: list C) (l: list A) (l': list B) f f',
      split (map (fun x => (f x, f' x)) xs) = (l, l') ->
      l = map f xs /\ l' = map f' xs.

  Remark In_singleton:
    forall (y x: A),
      In y [x] <-> y = x.

  Lemma In_weaken_cons:
    forall {A} (y x:A) xs,
      In x (y::xs) ->
      x <> y ->
      In x xs.

  Lemma in_filter:
    forall f x (l: list A), In x (filter f l) -> In x l.

  Lemma Forall_not_In_singleton:
    forall (x: A) ys,
      ~ In x ys ->
      Forall (fun y => ~ In y [x]) ys.

  Global Add Parametric Morphism {A} : (@length A)
      with signature @Permutation.Permutation A ==> eq
        as length_permutation.

  Lemma split_last:
    forall {B} (x: A * B) xs,
      split (xs ++ [x]) =
      let (g, d) := split xs in
      (g ++ [fst x], d ++ [snd x]).

  Lemma nth_seq:
    forall {A} n' n (xs: list A) x,
      n' < length xs - n ->
      nth n' (seq n (length xs - n)) x = n' + n.

  Lemma seq_cons:
    forall k m,
      m < k ->
      seq m (k - m) = m :: seq (S m) (k - S m).

  Lemma length_hd_error:
    forall (l: list A),
      0 < length l ->
      exists x, hd_error l = Some x.

  Fact hd_error_Some_In:
    forall (xs: list A) x,
      hd_error xs = Some x ->
      In x xs.

  Fact hd_error_Some_hd:
    forall d (xs: list A) x,
      hd_error xs = Some x ->
      hd d xs = x.

  Lemma hd_error_In:
    forall xs (x : A),
      hd_error xs = Some x -> In x xs.

  Lemma split_map_fst {B} : forall (l : list (A * B)),
      fst (split l) = map fst l.

  Lemma split_map_snd {B} : forall (l : list (A * B)),
      snd (split l) = map snd l.

  Lemma map_ext_in' {B C} : forall (f : A -> C) (g : B -> C) l1 l2,
      length l1 = length l2 ->
      (forall a b, In (a, b) (combine l1 l2) -> f a = g b) ->
      map f l1 = map g l2.

  Remark map_cons'':
    forall {A B : Type} l y ys (f : A -> B),
      map f l = y :: ys ->
      exists x xs, l = x :: xs /\ y = f x /\ ys = map f xs.
End Extra.

Section find.

  Context {A: Type} (f: A -> bool).

  Lemma find_Exists:
    forall xs,
      find f xs <> None <-> Exists (fun x => f x = true) xs.

  Lemma find_split:
    forall xs x,
      find f xs = Some x ->
      exists bxs axs, xs = bxs ++ x :: axs.

  Lemma find_weak_spec:
    forall (xs: list A),
      find f xs = None ->
      Forall (fun x => f x = false) xs.
End find.

Section split.
  Context {A B : Type}.

  Lemma split_fst_snd : forall (xs : list (A * B)),
      split xs = (map fst xs, map snd xs).

  Corollary combine_fst_snd : forall (xs : list (A * B)),
      xs = combine (map fst xs) (map snd xs).
End split.

Section Map.

  Context {A B: Type}.
  Variable f: A -> B.

  Remark map_cons':
    forall l y ys,
      map f l = y :: ys ->
      exists x xs, l = x :: xs /\ y = f x /\ ys = map f xs.

  Remark map_app':
    forall l1 l l2,
      map f l = l1 ++ l2 ->
      exists k1 k2, l = k1 ++ k2 /\ l1 = map f k1 /\ l2 = map f k2.

  Lemma map_nth':
    forall (l : list A) (d: B) (d' : A) (n : nat),
      n < length l ->
      nth n (List.map f l) d = f (nth n l d').

End Map.

Section Incl.

  Context {A: Type}.

  Lemma incl_cons':
    forall (x: A) xs ys,
      incl (x :: xs) ys -> In x ys /\ incl xs ys.

  Lemma incl_tl': forall (x : A) xs ys,
      incl xs ys -> incl (x::xs) (x::ys).

  Lemma incl_nil:
    forall (xs: list A),
      incl xs [] -> xs = [].

  Lemma incl_nil': forall (xs : list A),
      incl [] xs.

  Lemma Forall_incl:
    forall (l l': list A) P,
      Forall P l ->
      incl l' l ->
      Forall P l'.

  Lemma incl_map {B} : forall (l l' : list A) (f : A -> B),
      incl l l' -> incl (map f l) (map f l').

  Lemma incl_appl' : forall (l n m : list A),
      incl n m ->
      incl (n ++ l) (m ++ l).

  Lemma incl_appr' : forall (l n m : list A),
      incl n m ->
      incl (l ++ n) (l ++ m).

  Lemma incl_filter : forall (f : A -> bool) xs ys,
      incl xs ys ->
      incl (filter f xs) (filter f ys).

  Lemma incl_concat_map {B} : forall (f : A -> list B) x xs,
      In x xs ->
      incl (f x) (concat (map f xs)).

  Global Instance incl_refl : Reflexive (@incl A).

  Global Instance incl_trans : Transitive (@incl A).

End Incl.

Section Nodup.

  Context {A: Type}.

  Lemma NoDup_cons':
    forall (x:A) xs,
      NoDup (x::xs) <-> ~In x xs /\ NoDup xs.

  Lemma NoDup_map_inv {B} (f: A -> B) l : NoDup (map f l) -> NoDup l.

  Lemma NoDup_app_weaken:
    forall (xs: list A) ys,
      NoDup (xs ++ ys) ->
      NoDup xs.

  Lemma NoDup_app_l : forall (xs : list A) ys,
      NoDup (xs ++ ys) ->
      NoDup xs.

  Lemma NoDup_app_r : forall (xs : list A) ys,
      NoDup (xs ++ ys) ->
      NoDup ys.

  Lemma NoDup_app_cons:
    forall ws (x: A) xs,
      NoDup (ws ++ x :: xs)
      <-> ~In x (ws ++ xs) /\ NoDup (ws ++ xs).

  Lemma NoDup_app_In:
    forall (x: A) xs ws,
      NoDup (xs ++ ws) ->
      In x xs ->
      ~In x ws.

  Lemma NoDup_app':
    forall (xs ws: list A),
      NoDup xs ->
      NoDup ws ->
      Forall (fun x => ~ In x ws) xs ->
      NoDup (xs ++ ws).

  Lemma NoDup_app'_iff:
    forall (xs ws: list A),
      NoDup (xs ++ ws) <->
       (NoDup xs
      /\ NoDup ws
      /\ Forall (fun x => ~ In x ws) xs).

  Lemma NoDup_swap:
    forall (x y z: list A),
      NoDup (x ++ y ++ z) <->
      NoDup (y ++ x ++ z).

  Lemma nodup_filter:
    forall f (l: list A),
      NoDup l -> NoDup (filter f l).

  Lemma NoDup_Permutation_ter: forall (l l' : list A),
      NoDup l ->
      incl l l' ->
      length l = length l' ->
      Permutation l l'.

  Corollary NoDup_length_incl': forall (l l' : list A),
      NoDup l ->
      incl l l' ->
      length l = length l' ->
      NoDup l'.

End Nodup.

Lemma concat_length:
  forall {A} (l: list (list A)),
    length (concat l) = fold_left (fun s x => s + length x) l 0.

Section ConcatMap.

  Context {A B: Type}.

  Lemma flat_map_length:
    forall l (f : A -> list B),
      length (flat_map f l) = fold_left (fun s x => s + length (f x)) l 0.

  Lemma length_flat_map:
    forall (f: B -> list A) x xs,
      length (flat_map f (x :: xs)) = length (f x) + length (flat_map f xs).

  Lemma flat_map_app:
    forall (f : A -> list B) xs ys,
      flat_map f xs ++ flat_map f ys = flat_map f (xs ++ ys).

  Lemma Permutation_cons_1:
    forall {A} (x : A) xs ys,
      Permutation (x::xs) ys
      <-> exists zs, Permutation xs zs /\ Permutation ys (x::zs).

  Lemma flat_map_ExistsIn:
    forall (f : A -> list B) xs y ys,
      flat_map f xs = y :: ys ->
      exists x ys', In x xs /\ f x = y :: ys'.

  Lemma In_flat_map:
    forall (f : A -> list B) xss v,
      In v (flat_map f xss) ->
      exists xs,
        In xs xss /\ In v (f xs).

  Fact in_flat_map' : forall (f : A -> list B) (l : list A) (y : B),
      In y (flat_map f l) <-> Exists (fun x => In y (f x)) l.

  Remark in_concat_cons:
    forall l' (l: list A) x xs,
      In x l ->
      In (xs :: l) l' ->
      In x (concat l').

  Remark in_concat':
    forall l' (l: list A) x,
      In x l ->
      In l l' ->
      In x (concat l').

  Lemma in_concat:
    forall (ls : list (list A)) (y : A),
      In y (concat ls) <-> (exists l : list A, In y l /\ In l ls).

  Lemma concat_Forall :
    forall (l' : list (list A)) (l : list A) (P : A -> Prop),
      Forall P (concat l') ->
      In l l' ->
      Forall P l.

  Lemma Forall_concat : forall (l : list (list A)) P,
      Forall (fun l => Forall P l) l -> Forall P (concat l).

  Lemma concat_length_1 : forall (f : A -> list B) (l : list A),
      Forall (fun x => length (f x) = 1) l ->
      length (concat (map f l)) = length l.

  Lemma concat_length_eq : forall (l1 : list (list A)) (l2 : list (list B)),
      Forall2 (fun l1 l2 => length l1 = length l2) l1 l2 ->
      length (concat l1) = length (concat l2).

  Lemma concat_length_map_nth : forall (f : A -> list B) (l : list A) n da db,
      n < length l ->
      Forall (fun x => length (f x) = 1) l ->
      f (nth n l da) = [nth n (concat (map f l)) db].

  Fact concat_map_singl1 : forall (l : list A),
    (concat (map (fun x => [x]) l)) = l.

  Fact concat_map_singl2 : forall (l : list (list A)),
    (concat (concat (List.map (fun x => List.map (fun x => [x]) x) l))) = (concat l).

  Lemma concat_eq_nil : forall (l : list (list A)),
      concat l = [] <-> Forall (fun l => l = nil) l.

End ConcatMap.

Section FoldLeft2.

  Context {A B C : Type}.

  Variable (f : A -> B -> C -> A).

  Fixpoint fold_left2 (xs : list B) (ys : list C) (a : A) : A :=
    match xs, ys with
    | x::xs', y::ys' => fold_left2 xs' ys' (f a x y)
    | _, _ => a
    end.


End FoldLeft2.

Section Permutation.

  Context {A: Type}.

  Lemma Permutation_incl1:
    forall (ws: list A) xs ys,
      Permutation xs ys ->
      (incl xs ws <-> incl ys ws).

  Global Instance Permutation_incl_Proper:
    Proper (@Permutation A ==> @Permutation A ==> iff) (@incl A).

  Global Instance NoDup_Permutation_Proper:
    Proper (Permutation (A:=A) ==> iff) (@NoDup A).

  Lemma Permutation_app_assoc:
    forall (ws: list A) xs ys,
      Permutation ((ws ++ xs) ++ ys) (ws ++ xs ++ ys).

  Global Instance Permutation_app_Proper2 (xs: list A):
    Proper (Permutation (A:=A) ==> Permutation (A:=A))
           (app (A:=A) xs).

  Global Instance Permutation_app_Proper3:
    Proper (Permutation (A:=A) ==> (@eq (list A)) ==> Permutation (A:=A))
           (app (A:=A)).

  Global Instance Permutation_concat_Proper:
    Proper (Permutation (A:=list A) ==> Permutation (A:=A))
           (@concat A).

  Lemma Permutation_rev_append:
    forall {A} (xs zs : list A),
      Permutation (rev_append zs xs) (zs ++ xs).

  Definition notb (f: A -> bool) (x: A) := negb (f x).

  Lemma filter_notb_app:
    forall (p: A -> bool) xs,
      Permutation (filter p xs ++ filter (notb p) xs) xs.

  Global Instance Permutation_filter_Proper (p:A->bool):
    Proper (@Permutation A ==> @Permutation A) (filter p).

  Lemma permutation_partition:
    forall p (l: list A),
      Permutation l (fst (partition p l) ++ snd (partition p l)).

  Lemma fst_partition_filter:
    forall P (xs: list A),
      Permutation (fst (partition P xs)) (filter P xs).

  Lemma snd_partition_filter:
    forall P (xs: list A),
      Permutation (snd (partition P xs)) (filter (fun x => negb (P x)) xs).

  Global Instance Permutation_map_Proper {B}:
    Proper ((@eq (A -> B)) ==> Permutation (A:=A) ==> (Permutation (A:=B)))
           (@map A B).

  Lemma Permutation_swap:
    forall (xs ys zs: list A),
      Permutation (xs ++ ys ++ zs) (ys ++ xs ++ zs).

End Permutation.

Section Pointwise.

  Context {A: Type}.

  Global Instance pointwise_filter_Proper:
    Proper (pointwise_relation A eq ==> @eq (list A) ==> @eq (list A))
           (@filter A).

  Global Instance pointwise_partition_Proper:
    Proper (pointwise_relation A eq ==> @eq (list A) ==> @eq (list A * list A))
           (@partition A).

  Global Instance Forall_Permutation_Proper:
    Proper (pointwise_relation A iff ==> Permutation (A:=A) ==> iff) (@Forall A).

  Global Instance Exists_Permutation_Proper:
    Proper (pointwise_relation A iff ==> Permutation (A:=A) ==> iff) (@Exists A).

  Global Instance Permutation_map_Proper2 {A B}:
    Proper (pointwise_relation A eq ==> Permutation.Permutation (A:=A)
                               ==> (Permutation.Permutation (A:=B)))
           (@map A B).

  Global Instance Permutation_flat_map_Proper :
    forall A B f,
      Proper (Permutation (A:=A) ==> Permutation (A:=B))
             (flat_map (A:=A) (B:=B) f).

End Pointwise.

Section ForallExists.

  Context {A: Type}.

  Lemma Forall_map:
    forall {B} P (f: A -> B) xs,
      Forall P (map f xs) <-> Forall (fun x => P (f x)) xs.

  Variable P: A -> Prop.

  Lemma Forall_cons2:
    forall x l,
      Forall P (x :: l) <-> P x /\ Forall P l.

  Lemma Forall_app:
    forall ll rr,
      Forall P (ll ++ rr) <-> (Forall P ll /\ Forall P rr).

  Lemma Exists_app:
    forall ll rr,
      Exists P rr ->
      Exists P (ll ++ rr).

  Lemma Exists_app':
    forall (l l': list A),
      Exists P (l ++ l') <-> Exists P l \/ Exists P l'.

  Lemma Forall_Forall:
    forall Q xs,
      Forall P xs -> Forall Q xs -> Forall (fun x=>P x /\ Q x) xs.

  Lemma Exists_dec_In:
    forall xs,
      (forall x, In x xs -> {P x} + {~P x}) ->
      {Exists P xs} + {~Exists P xs}.

  Lemma Forall_Exists:
    forall Q xs,
      Forall P xs ->
      Exists Q xs ->
      Exists (fun x=>P x /\ Q x) xs.

  Lemma decidable_Exists:
    forall xs,
      (forall x, In x xs -> decidable (P x)) ->
      decidable (Exists P xs).

  Lemma decidable_Exists_not_Forall:
    forall xs,
      (forall x, In x xs -> decidable (P x)) ->
      (Exists P xs <-> ~Forall (fun x => ~(P x)) xs).

  Lemma Exists_map:
    forall {B} P (f : A -> B) xs,
      Exists P (map f xs) <-> Exists (fun x => P (f x)) xs.

  Lemma Exists_Exists:
    forall (Q : A -> Prop) xs,
    (forall x, P x -> Q x) ->
    Exists P xs -> Exists Q xs.

  Lemma Permutation_Forall:
    forall l l',
      Permutation l l' ->
      Forall P l ->
      Forall P l'.

  Lemma Forall_app_weaken:
    forall xs ys,
      Forall P (xs ++ ys) ->
      Forall P ys.

  Lemma Forall_impl_In :
    forall (Q : A -> Prop) l,
      (forall a, In a l -> P a -> Q a) ->
      Forall P l -> Forall Q l.

  Lemma Forall_Forall':
    forall (Q : A -> Prop) (xs : list A),
      Forall P xs /\ Forall Q xs <-> Forall (fun x : A => P x /\ Q x) xs.

  Lemma Forall_singl:
    forall (x : A),
      Forall P [x] -> P x.

  Lemma Forall_not_In_app:
    forall (zs xs ys: list A),
      Forall (fun z => ~ In z xs) zs ->
      Forall (fun z => ~ In z ys) zs ->
      Forall (fun z => ~ In z (xs ++ ys)) zs.

  Lemma Exists_concat : forall xs,
      Exists P (concat xs) <-> Exists (Exists P) xs.

  Lemma Exists_concat_nth : forall xs n d,
      n < length xs ->
      Exists P (nth n xs d) -> Exists P (concat xs).

  Lemma Exists_concat_nth' : forall xs d,
      Exists P (concat xs) ->
      exists n, (n < length xs /\ Exists P (nth n xs d)).

  Lemma Exists_combine_l {B} : forall xs (ys : list B),
      length xs = length ys ->
      Exists P xs <-> Exists (fun '(x, _) => P x) (combine xs ys).

  Lemma Exists_combine_r {B} : forall xs (ys : list B),
      length xs = length ys ->
      Exists P xs <-> Exists (fun '(_, x) => P x) (combine ys xs).

  Lemma Exists_singl : forall (x : A),
      Exists P [x] ->
      P x.

End ForallExists.

Lemma Forall_iff_insideout:
  forall {A} (P Q : A -> Prop) xs,
    (Forall (fun x => P x <-> Q x) xs) ->
    (Forall P xs <-> Forall Q xs).

Section ForallExistsB.

  Context {A: Type}.
  Variable p: A -> bool.

  Lemma Exists_existsb:
    forall xs P,
      (forall x, P x <-> p x = true) ->
      (Exists P xs <-> existsb p xs = true).

  Lemma forallb_exists:
    forall (l: list A),
      forallb p l = false <-> (exists x : A, In x l /\ p x = false).

  Lemma existsb_Forall:
    forall xs,
      existsb p xs = false <->
      forallb (fun x => negb (p x)) xs = true.

  Lemma existsb_Forall_neg:
    forall xs,
      existsb (fun x => negb (p x)) xs = false <->
      forallb p xs = true.

  Lemma forallb_Forall:
    forall xs,
      forallb p xs = true <-> Forall (fun x => p x = true) xs.

End ForallExistsB.

Section ExistsB.
  Context {A B: Type}.
  Variable p q : B -> bool.
  Variable f : A -> B.

  Lemma existsb_map: forall xs,
      existsb p (map f xs) = existsb (fun a => p (f a)) xs.

  Lemma existsb_ext : forall xs,
      (forall x, p x = q x) ->
      existsb p xs = existsb q xs.
End ExistsB.

Section list_ind2.
  Context {A B : Type}.
  Variable P : list A -> list B -> Prop.

  Hypothesis Hnil : P nil nil.
  Hypothesis Hcons : forall a l1 b l2,
      P l1 l2 -> P (a::l1) (b::l2).

  Fixpoint list_ind2 l1 l2 : length l1 = length l2 -> P l1 l2.
End list_ind2.

Section Combine.

  Context {A B C: Type}.

  Lemma combine_map_fst:
    forall (f: A -> B) xs (ys: list C),
      combine (map f xs) ys = map (fun x=>(f (fst x), snd x)) (combine xs ys).

  Lemma combine_map_fst':
    forall (xs : list A) (ys : list B),
      length xs = length ys -> map fst (combine xs ys) = xs.

  Lemma combine_map_snd:
    forall (f: C -> B) (xs: list A) ys,
      combine xs (map f ys) = map (fun x=>(fst x, f (snd x))) (combine xs ys).

  Lemma combine_map_snd':
    forall (xs : list A) (ys : list B),
      length xs = length ys -> map snd (combine xs ys) = ys.

  Lemma combine_same : forall (xs : list A),
      combine xs xs = map (fun x => (x, x)) xs.

  Lemma combine_nil_l:
    forall (xs: list B),
      combine (@nil A) xs = [].

  Lemma combine_nil_r:
    forall (xs: list A),
      combine xs (@nil B) = [].

  Lemma combine_app_l:
    forall (xs xs': list A) (ys: list B),
      combine (xs ++ xs') ys = combine xs (firstn (length xs) ys)
                                       ++ combine xs' (skipn (length xs) ys).

  Lemma combine_app_r:
    forall (xs: list A) (ys ys': list B),
      combine xs (ys ++ ys') = combine (firstn (length ys) xs) ys
                                       ++ combine (skipn (length ys) xs) ys'.

  Lemma NotIn_combine:
    forall (xs: list A) (ys: list B) x y,
      ~In x xs ->
      ~In (x, y) (combine xs ys).

  Lemma In_combine_f:
    forall (f1 : A -> B) (f2 : A -> C) xs x1 x2,
      In (x1, x2) (combine (map f1 xs) (map f2 xs)) ->
      exists x,
        In x xs /\ x1 = f1 x /\ x2 = f2 x.

  Lemma map_snd_combine:
    forall (l: list A) (l': list B),
      length l = length l' ->
      map (@snd A B) (combine l l') = l'.

  Lemma combine_length_l:
    forall (l : list A) (l' : list B),
      length (combine l l') = length l ->
      length l <= length l'.

  Lemma combine_length_r:
    forall (l : list A) (l' : list B),
      length (combine l l') = length l' ->
      length l >= length l'.

  Lemma combine_nth_l:
    forall (l : list A) (l': list B) n d1 d2,
      length l <= length l' ->
      exists d, nth n (combine l l') (d1, d2) = (nth n l d1, d).

  Lemma combine_nth_r:
    forall (l : list A) (l': list B) n d1 d2,
      length l >= length l' ->
      exists d, nth n (combine l l') (d1, d2) = (d, nth n l' d2).

  Lemma in_combine_nodup :
    forall {A B} xs ys (x : A) (y : B) y',
      NoDup xs ->
      In (x, y) (combine xs ys) ->
      In (x, y') (combine xs ys) ->
      y = y'.

End Combine.

Lemma In_combine_f_left:
  forall {A B} (f1 : A -> B) xs x x1,
    In (x1, x) (combine (map f1 xs) xs) ->
    In x xs /\ x1 = f1 x.

Lemma In_combine_f_right:
  forall {A B} (f2 : A -> B) xs x x2,
    In (x, x2) (combine xs (map f2 xs)) ->
    In x xs /\ x2 = f2 x.

Lemma combine_map_both:
  forall {A B C D} (f: A -> B) (g: C -> D) xs ys,
    combine (map f xs) (map g ys)
    = map (fun x => (f (fst x), g (snd x))) (combine xs ys).

Section SkipnDropn.

  Context {A : Type}.

  Lemma skipn_app:
    forall (xs: list A) ys n,
      n = length xs ->
      skipn n (xs ++ ys) = ys.

  Lemma skipn_nil:
    forall n,
      skipn n (@nil A) = @nil A.

  Lemma firstn_nil:
    forall n,
      firstn n (@nil A) = @nil A.

  Lemma firstn_app:
    forall (xs: list A) ys n,
      n = length xs ->
      firstn n (xs ++ ys) = xs.

  Lemma In_skipn:
    forall (xs: list A) n x,
      In x (skipn n xs) ->
      In x xs.

  Lemma In_firstn:
    forall (xs: list A) n x,
      In x (firstn n xs) ->
      In x xs.

  Lemma Forall_skipn:
    forall P (xs: list A) n,
      Forall P xs ->
      Forall P (skipn n xs).

  Lemma skipn_cons:
    forall n (xs: list A) x,
      n > 0 ->
      skipn n (x :: xs) = skipn(n - 1) xs.

  Lemma skipn_length:
    forall n (l: list A),
      length (skipn n l) = length l - n.

  Lemma nth_skipn:
    forall (xs: list A) n' n x_d,
      nth n' (skipn n xs) x_d = nth (n' + n) xs x_d.

  Lemma nth_firstn_1: forall (xs: list A) n' n x_d,
      n' < n ->
      nth n' (firstn n xs) x_d = nth n' xs x_d.

End SkipnDropn.

Section AppLength.
  Context {A B : Type}.

  Lemma app_length_impl :
    forall (l1 l'1 : list A) (l2 l'2 : list B),
      length l'1 = length l'2 ->
      length (l'1 ++ l1) = length (l'2 ++ l2) ->
      length l1 = length l2.

  Lemma length_app :
    forall (l : list A) (l1 l2 : list B),
      (length l = length (l1 ++ l2)) ->
      (exists l1' l2', l = l1' ++ l2'
                  /\ length l1' = length l1
                  /\ length l2' = length l2).

  Lemma app_length_inv1 :
    forall (l1 l1' l2 l2' : list A),
      l1 ++ l2 = l1' ++ l2' ->
      length l1 = length l1' ->
      l1 = l1'.

  Lemma app_length_inv2:
    forall (l1 l1' l2 l2' : list A),
      l1 ++ l2 = l1' ++ l2' ->
      length l1 = length l1' ->
      l2 = l2'.
End AppLength.

Section Forall2.

  Context {A B C : Type}.

  Open Scope bool_scope.

  Fixpoint forall2b (f : A -> B -> bool) l1 l2 :=
    match l1, l2 with
    | nil, nil => true
    | e1 :: l1, e2 :: l2 => f e1 e2 && forall2b f l1 l2
    | _, _ => false
    end.

  Lemma forall2b_Forall2:
    forall (p : A -> B -> bool) (xs : list A) (ys : list B),
      forall2b p xs ys = true <-> Forall2 (fun x y => p x y = true) xs ys.

  Lemma Forall2_forall2_eq:
    forall (eq_A: A -> A -> Prop) (eq_B: B -> B -> Prop)
      (eq_A_refl: reflexive A eq_A)
      (eq_B_refl: reflexive B eq_B)
      (P: A -> B -> Prop)
      (P_compat: Proper (eq_A ==> eq_B ==> Basics.impl) P)
      (l1: list A) (l2: list B),
      Forall2 P l1 l2
      <-> length l1 = length l2
        /\ forall a b n x1 x2,
          n < length l1 ->
          eq_A (nth n l1 a) x1 ->
          eq_B (nth n l2 b) x2 ->
          P x1 x2.

  Lemma Forall2_forall2 :
    forall P l1 l2,
      Forall2 P l1 l2
      <-> length l1 = length l2
          /\ forall (a : A) (b : B) n x1 x2,
          n < length l1 ->
          nth n l1 a = x1 ->
          nth n l2 b = x2 ->
          P x1 x2.

  Lemma Forall2_ignore2:
    forall {A B} (P : A -> B -> Prop) xs ys,
      Forall2 P xs ys ->
      Forall (fun x => exists y, In y ys /\ P x y) xs.

  Lemma Forall2_ignore2': forall (P : A -> Prop) xs (ys : list B),
      length xs = length ys ->
      Forall P xs ->
      Forall2 (fun x _ => P x) xs ys.

  Lemma Forall2_ignore1:
    forall {A B} (P : A -> B -> Prop) xs ys,
      Forall2 P xs ys ->
      Forall (fun y => exists x, In x xs /\ P x y) ys.

  Lemma Forall2_ignore1': forall (P : B -> Prop) (xs : list A) ys,
      length ys = length xs ->
      Forall P ys ->
      Forall2 (fun _ y => P y) xs ys.

  Lemma Forall2_cons':
    forall P (x : A) (y : B) l l',
      (P x y /\ Forall2 P l l') <-> Forall2 P (x::l) (y::l').

  Lemma Forall2_det : forall (R : A -> B -> Prop),
      (forall x y1 y2, R x y1 -> R x y2 -> y1 = y2) ->
      forall xs ys1 ys2, Forall2 R xs ys1 -> Forall2 R xs ys2 -> ys1 = ys2.

  Remark Forall2_hd:
    forall (A B : Type) (P : A -> B -> Prop)
      (x : A) (l : list A) (x' : B) (l' : list B),
      Forall2 P (x :: l) (x' :: l') -> P x x'.

  Remark Forall2_tl:
    forall (A B : Type) (P : A -> B -> Prop)
      (x : A) (l : list A) (x' : B) (l' : list B),
      Forall2 P (x :: l) (x' :: l') -> Forall2 P l l'.

  Lemma Forall2_combine:
    forall P (xs: list A) (ys: list B),
      Forall2 P xs ys -> Forall (fun x => P (fst x) (snd x)) (combine xs ys).

  Lemma Forall2_combine':
    forall P (xs : list A) (ys : list B),
      Forall2 (fun x y => P (x, y)) xs ys -> Forall P (combine xs ys).

  Lemma Forall2_combine'':
    forall P (xs : list A) (ys : list B),
      length xs = length ys ->
      Forall (fun '(x, y) => P x y) (combine xs ys) ->
      Forall2 P xs ys.

  Lemma Forall2_combine_ll: forall P (xs : list A) (ys : list B) (zs : list C),
      Forall2 P xs ys ->
      length zs = length xs ->
      Forall2 (fun '(_, x) y => P x y) (combine zs xs) ys.

  Lemma Forall2_combine_lr: forall P (xs : list A) (ys : list B) (zs : list C),
      Forall2 P xs ys ->
      length zs = length xs ->
      Forall2 (fun '(x, _) y => P x y) (combine xs zs) ys.

  Lemma Forall2_same:
    forall P (xs: list A),
      Forall (fun x => P x x) xs <-> Forall2 P xs xs.

  Lemma Forall2_eq_refl:
    forall (x: list A), Forall2 eq x x.

  Lemma Forall2_in_left:
    forall P (xs: list A) (ys: list B) x,
      Forall2 P xs ys ->
      In x xs ->
      exists y, In y ys /\ P x y.

  Lemma Forall2_in_right:
    forall P (xs: list A) (ys: list B) y,
      Forall2 P xs ys ->
      In y ys ->
      exists x, In x xs /\ P x y.

  Lemma Forall2_chain_In':
    forall {C} P Q (xs: list A) (ys: list B) (zs: list C) x z,
      Forall2 P xs ys ->
      Forall2 Q ys zs ->
      In (x, z) (combine xs zs) ->
      exists y, P x y /\ Q y z /\ In (x, y) (combine xs ys)
                               /\ In (y, z) (combine ys zs).

  Lemma Forall2_chain_In:
    forall {C} P Q (xs: list A) (ys: list B) (zs: list C) x z,
      Forall2 P xs ys ->
      Forall2 Q ys zs ->
      In (x, z) (combine xs zs) ->
      exists y, P x y /\ Q y z.

  Lemma all_In_Forall2:
    forall (P: A -> B -> Prop) xs vs,
      length xs = length vs ->
      (forall x v, In (x, v) (combine xs vs) -> P x v) ->
      Forall2 P xs vs.

  Lemma Forall2_impl_In:
    forall (P Q: A -> B -> Prop) (l1: list A) (l2: list B),
      (forall (a: A) (b: B), In a l1 -> In b l2 -> P a b -> Q a b) ->
      Forall2 P l1 l2 ->
      Forall2 Q l1 l2.

  Global Instance Forall2_Proper:
    Proper (pointwise_relation A (pointwise_relation B iff)
                               ==> eq ==> eq ==> iff) (@Forall2 A B).

  Lemma Forall2_swap_args:
    forall (P: A -> B -> Prop) (xs: list A) (ys: list B),
      Forall2 P xs ys <-> Forall2 (fun y x => P x y) ys xs.

  Lemma Forall2_Forall2:
    forall (P1: A -> B -> Prop) P2 xs ys,
      Forall2 P1 xs ys ->
      Forall2 P2 xs ys ->
      Forall2 (fun x y => P1 x y /\ P2 x y) xs ys.

  Lemma Forall2_length :
    forall (P : A -> B -> Prop) l1 l2,
      Forall2 P l1 l2 -> length l1 = length l2.

  Lemma Forall2_forall:
    forall (P: A -> B -> Prop) xs ys,
      ((forall x y, In (x, y) (combine xs ys) -> P x y)
       /\ length xs = length ys)
      <->
      Forall2 P xs ys.

  Lemma Forall2_eq:
    forall (xs: list A) ys,
      Forall2 eq xs ys <-> xs = ys.

  Lemma Forall2_In:
    forall x v xs vs (P : A -> B -> Prop) ,
      In (x, v) (combine xs vs) ->
      Forall2 P xs vs ->
      P x v.

  Lemma Forall2_left_cons:
    forall P (x:A) xs (ys : list B),
      Forall2 P (x::xs) ys ->
      exists y ys', ys = y::ys' /\ P x y /\ Forall2 P xs ys'.

  Lemma Forall2_right_cons:
    forall P (xs: list A) (y: B) ys,
      Forall2 P xs (y::ys) ->
      exists x xs', xs = x::xs' /\ P x y /\ Forall2 P xs' ys.

  Lemma Forall2_Forall2_exists:
    forall {C} P Q (xs: list A) (ys: list B),
      Forall2 (fun x y=> exists z, P x z /\ Q y z) xs ys ->
      exists (zs: list C), Forall2 P xs zs /\ Forall2 Q ys zs.

  Lemma Forall2_map_1:
    forall {C} P (f: A -> C) (xs: list A) (ys: list B),
      Forall2 P (map f xs) ys <-> Forall2 (fun x=>P (f x)) xs ys.

  Lemma Forall2_in_left_combine:
    forall (l: list A) (l': list B) P x,
      Forall2 P l l' ->
      In x l ->
      exists y, In (x, y) (combine l l') /\ P x y.

  Lemma Forall2_app_split :
    forall (P : A -> B -> Prop) l1 l1' l2 l2',
      Forall2 P (l1 ++ l2) (l1' ++ l2') ->
      length l1 = length l1' ->
      Forall2 P l1 l1' /\ Forall2 P l2 l2'.

  Lemma Forall2_Permutation_1 : forall (P : A -> B -> Prop) l1 l1' l2,
      Permutation l1 l1' ->
      Forall2 P l1 l2 ->
      exists l2', Permutation l2 l2' /\ Forall2 P l1' l2'.


  Lemma Forall2_const_map :
    forall (P : A -> B -> Prop) (e : A) (l : list C) (l' : list B),
      Forall (fun y => P e y) l' ->
      length l = length l' ->
      Forall2 (fun x y => P x y) (map (fun _ => e) l) l'.

  Lemma Forall2_singl : forall (P : A -> B -> Prop) x y,
      Forall2 P [x] [y] -> P x y.
End Forall2.

Hint Resolve (proj2 (Forall2_eq _ _)).

Lemma Forall2_trans_ex:
  forall {A B C} (P: A -> B -> Prop) Q xs ys (zs: list C),
    Forall2 P xs ys ->
    Forall2 Q ys zs ->
    Forall2 (fun x z => exists y, In y ys /\ P x y /\ Q y z) xs zs.

Lemma Forall2_map_2:
  forall {A B C} P (f: B -> C) (xs: list A) (ys: list B),
    Forall2 P xs (map f ys) <-> Forall2 (fun x y=>P x (f y)) xs ys.

Lemma forall2_right:
  forall {A B : Type} (P : list A -> list B -> Prop),
    P [] [] ->
    (forall x y xs' ys',
        P xs' ys' ->
        P (x::xs') (y::ys')) ->
    forall xs ys,
      length xs = length ys ->
      P xs ys.

Fact nth_concat2 {A B} : forall (x1 : A) (x2 : B) l1 l2 a b n,
    length l1 = length l2 ->
    Forall2 (fun l1 l2 => length l1 = length l2) l1 l2 ->
    n < length (concat l1) ->
    x1 = nth n (concat l1) a ->
    x2 = nth n (concat l2) b ->
    exists n', exists n'', (n' < length l1 /\
                  n'' < length (nth n' l1 [a]) /\
                  x1 = nth n'' (nth n' l1 [a]) a /\
                  x2 = nth n'' (nth n' l2 [b]) b).

Lemma Forall2_concat {A B} : forall (P : A -> B -> Prop) l1 l2,
    Forall2 (fun l1 l2 => Forall2 P l1 l2) l1 l2 ->
    Forall2 P (concat l1) (concat l2).

Section Forall3.

  Context {A B C : Type}.
  Variable R : A -> B -> C -> Prop.

  Inductive Forall3 : list A -> list B -> list C -> Prop :=
  | Forall3_nil : Forall3 [] [] []
  | Forall3_cons : forall (x : A) (y : B) (z: C)
                          (l0 : list A) (l1 : list B) (l2 : list C),
      R x y z ->
      Forall3 l0 l1 l2 ->
      Forall3 (x :: l0) (y :: l1) (z :: l2).

  Lemma Forall3_length :
    forall (l1 : list A) (l2 : list B) (l3 : list C),
      Forall3 l1 l2 l3 ->
      length l1 = length l2
      /\ length l2 = length l3.

  Lemma Forall3_in_right:
    forall (xs : list A)
      (ys : list B) (zs : list C) (z : C),
      Forall3 xs ys zs ->
      In z zs -> exists (x : A) (y : B), In x xs /\ In y ys /\ R x y z.

  Remark Forall3_tl:
    forall (x : A)
      (y : B) (z : C) (l0 : list A) (l1 : list B) (l2 : list C),
      Forall3 (x :: l0) (y :: l1) (z :: l2) -> Forall3 l0 l1 l2.

  Fixpoint forall3b (f : A -> B -> C -> bool) l1 l2 l3 :=
    match l1, l2, l3 with
    | nil, nil, nil => true
    | e1 :: l1, e2 :: l2, e3 :: l3 => andb (f e1 e2 e3) (forall3b f l1 l2 l3)
    | _, _, _ => false
    end.

  Lemma Forall3_ignore23:
    forall xs ys zs,
      Forall3 xs ys zs ->
      Forall (fun x => exists y z, R x y z) xs.

  Lemma Forall3_ignore13:
    forall xs ys zs,
      Forall3 xs ys zs ->
      Forall (fun y => exists x z, R x y z) ys.

  Lemma Forall3_ignore12:
    forall xs ys zs,
      Forall3 xs ys zs ->
      Forall (fun z => exists x y, R x y z) zs.

  Lemma Forall3_ignore2:
    forall xs ys zs,
      Forall3 xs ys zs ->
      Forall2 (fun x z => exists y, R x y z) xs zs.

  Lemma Forall3_ignore3:
    forall xs ys zs,
      Forall3 xs ys zs ->
      Forall2 (fun x y => exists z, R x y z) xs ys.
End Forall3.

Lemma Forall3_forall3 {A B C}:
  forall P l1 l2 l3,
    Forall3 P l1 l2 l3
    <-> length l1 = length l2
      /\ length l1 = length l3
      /\ forall (a : A) (b : B) (c : C) n x1 x2 x3,
          n < length l1 ->
          nth n l1 a = x1 ->
          nth n l2 b = x2 ->
          nth n l3 c = x3 ->
          P x1 x2 x3.

Lemma forall3b_Forall3:
  forall {A B C} (p : A -> B -> C -> bool) xs ys zs,
    (forall3b p xs ys zs = true) <-> (Forall3 (fun x y z => p x y z = true) xs ys zs).

Lemma Forall3_impl_In:
  forall {A B C} (P Q : A -> B -> C -> Prop) xs ys zs,
    (forall x y z, In x xs -> In y ys -> In z zs -> P x y z -> Q x y z) ->
    Forall3 P xs ys zs -> Forall3 Q xs ys zs.


Lemma Forall3_Forall3 {A B C}: forall (P Q : A -> B -> C -> Prop) xs ys zs,
    Forall3 P xs ys zs ->
    Forall3 Q xs ys zs ->
    Forall3 (fun x y z => P x y z /\ Q x y z) xs ys zs.

Lemma Forall3_combine'1 {A B C} : forall (P : (A * B) -> C -> Prop) xs ys zs,
    Forall3 (fun x y z => P (x, y) z) xs ys zs ->
    Forall2 P (combine xs ys) zs.

Lemma Forall3_ignore1' {A B C} : forall P (xs : list A) (ys : list B) (zs : list C),
    length xs = length ys ->
    Forall2 P ys zs ->
    Forall3 (fun _ y z => P y z) xs ys zs.

Lemma Forall3_ignore2' {A B C} : forall P (xs : list A) (ys : list B) (zs : list C),
    length ys = length xs ->
    Forall2 P xs zs ->
    Forall3 (fun x _ z => P x z) xs ys zs.

Lemma Forall3_ignore3' {A B C} : forall P (xs : list A) (ys : list B) (zs : list C),
    length zs = length xs ->
    Forall2 P xs ys ->
    Forall3 (fun x y _ => P x y) xs ys zs.

Global Instance Forall3_Proper' {A B C}:
  Proper (pointwise_relation A (pointwise_relation B (pointwise_relation C Basics.impl))
                             ==> eq ==> eq ==> eq ==> Basics.impl) (@Forall3 A B C).

Global Instance Forall3_Proper {A B C}:
  Proper (pointwise_relation A (pointwise_relation B (pointwise_relation C iff))
                             ==> eq ==> eq ==> eq ==> iff) (@Forall3 A B C).

Section InMembers.
  Context {A B: Type}.

  Fixpoint InMembers (a:A) (l:list (A * B)) : Prop :=
    match l with
    | nil => False
    | (a', _) :: m => a' = a \/ InMembers a m
    end.

  Inductive NoDupMembers: list (A * B) -> Prop :=
  | NoDupMembers_nil:
      NoDupMembers nil
  | NoDupMembers_cons: forall a b l,
      ~ InMembers a l ->
      NoDupMembers l ->
      NoDupMembers ((a, b)::l).

  Lemma inmembers_eq:
    forall a b l, InMembers a ((a, b) :: l).

  Lemma inmembers_cons:
    forall a a' l, InMembers a l -> InMembers a (a' :: l).

  Lemma In_InMembers:
    forall a b xs,
      In (a, b) xs -> InMembers a xs.

  Lemma InMembers_In:
    forall a xs,
      InMembers a xs -> exists b, In (a, b) xs.

  Lemma nodupmembers_cons:
    forall id ty xs,
      NoDupMembers ((id, ty) :: xs) <->
      ~InMembers id xs /\ NoDupMembers xs.

  Lemma NotInMembers_NotIn:
    forall a b xs, ~ InMembers a xs -> ~ In (a, b) xs.

  Lemma NotIn_NotInMembers:
    forall a xs, (forall b, ~ In (a, b) xs) -> ~ InMembers a xs.

  Lemma NotInMembers_cons:
    forall xs x y,
      ~InMembers y (x::xs) <-> ~InMembers y xs /\ y <> fst x.

  Lemma InMembers_app:
    forall y ws xs,
      InMembers y (ws ++ xs) <-> (InMembers y ws) \/ (InMembers y xs).

  Global Instance InMembers_Permutation_Proper:
    Proper (eq ==> (@Permutation (A*B)) ==> iff) InMembers.

  Lemma NotInMembers_app:
    forall y ws xs,
      ~InMembers y (ws ++ xs) <-> (~InMembers y xs /\ ~InMembers y ws).

  Lemma InMembers_dec:
    forall (x : A) (xs : list (A * B)),
      (forall (x y: A), {x = y} + {x <> y}) ->
      { InMembers x xs } + { ~InMembers x xs }.

  Lemma inmembers_skipn:
    forall x (xs: list (A * B)) n,
      InMembers x (skipn n xs) ->
      InMembers x xs.

  Lemma inmembers_firstn:
    forall x (xs: list (A * B)) n,
      InMembers x (firstn n xs) ->
      InMembers x xs.

  Lemma InMembers_skipn_firstn:
    forall x (xs: list (A * B)) n,
      InMembers x (skipn n xs) ->
      NoDupMembers xs ->
      ~InMembers x (firstn n xs).

  Lemma InMembers_firstn_skipn:
    forall (xs: list (A * B)) n x,
      InMembers x (firstn n xs) ->
      NoDupMembers xs ->
      ~InMembers x (skipn n xs).

  Lemma NoDupMembers_NoDup:
    forall xs, NoDupMembers xs -> NoDup xs.

  Lemma NoDupMembers_app_cons:
    forall ws x y xs,
      NoDupMembers (ws ++ (x, y) :: xs)
      <-> ~InMembers x (ws ++ xs) /\ NoDupMembers (ws ++ xs).

  Lemma NoDupMembers_remove_1:
    forall ws x xs,
      NoDupMembers (ws ++ x :: xs) -> NoDupMembers (ws ++ xs).

  Lemma NoDupMembers_app_r:
    forall ws xs,
      NoDupMembers (ws ++ xs) -> NoDupMembers xs.

  Global Instance NoDupMembers_Permutation_Proper:
    Proper (Permutation (A:=A * B) ==> iff) NoDupMembers.

  Lemma NoDupMembers_app_l:
    forall ws xs,
      NoDupMembers (ws ++ xs) -> NoDupMembers ws.

  Lemma NoDupMembers_app_InMembers:
    forall x xs ws,
      NoDupMembers (xs ++ ws) ->
      InMembers x xs ->
      ~InMembers x ws.

  Lemma NoDupMembers_app_InMembers_l:
    forall x xs ws,
      NoDupMembers (xs ++ ws) ->
      InMembers x ws ->
      ~InMembers x xs.

  Lemma NoDupMembers_det:
    forall x t t' xs,
      NoDupMembers xs ->
      In (x, t) xs ->
      In (x, t') xs ->
      t = t'.

  Lemma NoDupMembers_firstn:
    forall (xs: list (A * B)) n,
      NoDupMembers xs ->
      NoDupMembers (firstn n xs).

  Lemma InMembers_neq:
    forall x y xs,
      InMembers x xs ->
      ~ InMembers y xs ->
      x <> y.

  Remark fst_InMembers:
    forall x xs,
      InMembers x xs <-> In x (map (@fst A B) xs).

  Remark fst_NoDupMembers:
    forall xs,
      NoDupMembers xs <-> NoDup (map (@fst A B) xs).

  Lemma InMembers_In_combine:
    forall x (xs: list A) (ys: list B),
      InMembers x (combine xs ys) ->
      In x xs.

  Lemma In_InMembers_combine:
    forall x (xs: list A) (ys: list B),
      length xs = length ys ->
      (In x xs <-> InMembers x (combine xs ys)).

  Lemma NoDup_NoDupMembers_combine:
    forall (xs: list A) (ys: list B),
    NoDup xs -> NoDupMembers (combine xs ys).

  Lemma NoDupMembers_combine_NoDup:
    forall (xs: list A) (ys: list B),
      length xs = length ys ->
      NoDupMembers (combine xs ys) -> NoDup xs.

  Remark InMembers_snd_In:
    forall {C} y l,
      InMembers y (map (@snd C (A * B)) l) ->
      exists x z, In (x, (y, z)) l.

  Remark In_InMembers_snd:
    forall {C} x y z l,
      In (x, (y, z)) l ->
      InMembers y (map (@snd C (A * B)) l).

  Lemma NoDupMembers_app:
    forall (ws xs : list (A * B)),
      NoDupMembers ws ->
      NoDupMembers xs ->
      (forall x, InMembers x ws -> ~InMembers x xs) ->
      NoDupMembers (ws ++ xs).

  Lemma NoDup_NoDupA:
    forall (xs: list A),
      NoDup xs <-> SetoidList.NoDupA eq xs.

  Lemma NoDup_skipn:
    forall (xs: list A) n,
      NoDup xs -> NoDup (skipn n xs).

  Lemma NoDupMembers_skipn:
    forall (xs: list (A * B)) n,
      NoDupMembers xs -> NoDupMembers (skipn n xs).

  Lemma InMembers_Forall:
    forall P (xs : list (A * B)) x,
      Forall P (map (@fst A B) xs) ->
      InMembers x xs ->
      P x.

  Lemma NoDupMembers_app':
    forall (xs ys : list (A * B)),
      NoDupMembers (xs++ys) ->
      NoDupMembers xs /\ NoDupMembers ys.

  Lemma InMembers_incl : forall x (xs ys : list (A * B)),
      incl xs ys ->
      InMembers x xs ->
      InMembers x ys.

  Fact incl_NoDup_In : forall (l1 l2 : list (A * B)) x y,
      incl l1 l2 ->
      NoDupMembers l2 ->
      InMembers x l1 ->
      In (x, y) l2 ->
      In (x, y) l1.
End InMembers.

Fact find_some' : forall {A} (xs : list (positive * A)) x v ,
    NoDupMembers xs ->
    In (x, v) xs ->
    find (fun xtc => (fst xtc =? x)%positive) xs = Some (x, v).

Section OptionLists.

  Context {A : Type}.

  Fixpoint LiftO (d : Prop) (P : A -> Prop) (x : option A) : Prop :=
    match x with None => d | Some x => P x end.

  Fixpoint Ino (a : A) (l : list (option A)) : Prop :=
    match l with
    | [] => False
    | b :: m => LiftO False (eq a) b \/ Ino a m
    end.


  Inductive NoDupo : list (option A) -> Prop :=
    NoDupo_nil : NoDupo []
  | NoDupo_conss : forall x l, ~ Ino x l -> NoDupo l -> NoDupo (Some x :: l)
  | NoDupo_consn : forall l, NoDupo l -> NoDupo (None :: l).

  Definition assert_singleton (xs : option (list A)) : option A :=
    match xs with Some [x] => Some x | _ => None end.

  Lemma assert_singleton_spec:
    forall e (v : A),
      assert_singleton e = Some v ->
      e = Some [v].

  Lemma Ino_In :
    forall (x : A) xs, Ino x xs <-> In (Some x) xs.

  Lemma ino_app_iff :
    forall (l l' : list (option A)) (a : A),
      Ino a (l ++ l') <-> Ino a l \/ Ino a l'.

  Lemma ino_dec:
    forall (x : A) xos,
      (forall x y : A, {x = y} + {x <> y}) ->
      Ino x xos \/ ~Ino x xos.

  Lemma NoDupo_app':
    forall (xs ws : list (option A)),
      NoDupo xs ->
      NoDupo ws ->
      (forall x : A, Ino x xs -> ~ Ino x ws) ->
      NoDupo (xs ++ ws).

  Lemma Ino_Forall:
    forall (x : A) (xs : list (option A)) (P : option A -> Prop),
      Forall P xs -> Ino x xs -> P (Some x).

  Lemma NoDupo_NoDup: forall (xs : list A),
      NoDupo (map Some xs) <-> NoDup xs.

End OptionLists.

Ltac app_NoDupMembers_det :=
  match goal with
  | H: NoDupMembers ?xs,
         H1: In (?x, ?t1) ?xs,
             H2: In (?x, ?t2) ?xs |- _ =>
      assert (t1 = t2) by (eapply NoDupMembers_det; eauto); subst t2; clear H2
    end.


Definition same_elements {A} : relation (list A) :=
  fun xs ys => forall x, In x xs <-> In x ys.

Lemma same_elements_refl {A} : reflexive _ (@same_elements A).

Lemma same_elements_sym {A} : symmetric _ (@same_elements A).

Lemma same_elements_trans {A} : transitive _ (@same_elements A).

Add Parametric Relation {A} : (list A) same_elements
    reflexivity proved by same_elements_refl
    symmetry proved by same_elements_sym
    transitivity proved by same_elements_trans
      as same_relation_rel.

Section Nub.
  Context {A : Type} (DA : forall x y : A, {x = y} + {x <> y}).

  Fixpoint nub (xs : list A) : list A :=
    match xs with
    | [] => []
    | x::xs => if in_dec DA x xs then nub xs else x :: nub xs end.

  Lemma In_nub:
    forall xs x,
      In x xs <-> In x (nub xs).

  Lemma nub_same_elements:
    forall xs, same_elements (nub xs) xs.

  Lemma NoDup_nub:
    forall xs, NoDup (nub xs).

  Lemma uniquify_list:
    forall (xs : list A), exists ys, (forall x, In x xs <-> In x ys) /\ NoDup ys.

End Nub.

Add Parametric Morphism {A} : (@List.In A)
    with signature (eq ==> same_elements ==> iff)
      as In_same_elements.


Section LL.

  Context {A : Type}.

  Definition ll (ls1 ls2 : list A) :=
    length ls1 < length ls2.

  Lemma ll_wf':
    forall ls, Acc ll ls.

  Theorem ll_wf:
    well_founded ll.

End LL.

Section ListSuffix.

  Context {A : Type}.

  Definition ltsuffix (ls1 ls2 : list A) :=
    exists ls1', ls2 = ls1' ++ ls1 /\ ls1' <> nil.

  Lemma ltsuffix_wf:
    well_founded ltsuffix.

End ListSuffix.

Section Wf_Prod.

  Context {A B : Type}
          (R1 : A -> A -> Prop)
          (R2 : B -> B -> Prop).

  Hypothesis R1_wf : well_founded R1.
  Hypothesis R2_wf : well_founded R2.

  Definition rr xx yy :=
    R1 (fst xx) (fst yy) /\ R2 (snd xx) (snd yy).

  Lemma rr_wf: well_founded rr.

End Wf_Prod.

Section Ltsuffix2.

  Context {A B : Type}.

  Definition ltsuffix2 := rr (@ltsuffix A) (@ltsuffix B).

  Lemma ltsuffix2_wf : well_founded ltsuffix2.
  Proof rr_wf (@ltsuffix A) (@ltsuffix B) ltsuffix_wf ltsuffix_wf.

End Ltsuffix2.

Set Implicit Arguments.

Section Well_founded_FixPoint.

  Variable A : Type.
  Variable R : A -> A -> Prop.

  Hypothesis Rwf : well_founded R.

  Variable F : forall x:A, (forall y:A, R y x -> Prop) -> Prop.

  Local Notation Fix_F := (@Fix_F A R (fun _ => Prop) F).
  Local Notation Acc := (@Acc A R).

  Definition PFix (x:A) := Fix_F (Rwf x).

  Hypothesis
    F_ext :
    forall (x:A) (f g:forall y:A, R y x -> Prop),
      (forall (y:A) (p:R y x), f y p <-> g y p) -> (F f <-> F g).

  Lemma Fix_F_inv : forall (x:A) (r s:Acc x), Fix_F r <-> Fix_F s.

  Lemma PFix_eq : forall x:A, PFix x <-> F (fun (y:A) (p:R y x) => PFix y).

End Well_founded_FixPoint.

Unset Implicit Arguments.

Lemma eqlistA_eq_eq {A}:
  relation_equivalence (SetoidList.eqlistA (@eq A)) (eq).


Ltac induction_list_tac e I l H :=
  match type of e with
    list ?A =>
    let Eq := fresh in
    let Eql := H in
    remember e as l eqn:Eq;
      assert (exists l', e = l' ++ l) as Eql by (exists (@nil A); simpl; auto);
      clear Eq; move Eql at top; induction l as I;
      [clear Eql|
       match goal with
         IH: (exists l', e = l' ++ ?l'') -> ?P,
             EQ: (exists l', e = l' ++ ?x::?xs) |- _ =>
         let l' := fresh l in
         let E := fresh in
         destruct EQ as [l' Eql];
           rewrite <-app_last_app in Eql;
           assert (exists l', e = l' ++ xs) as E by (exists (l' ++ [x]); auto);
           specialize (IH E); clear E
       end]
  end.

Tactic Notation "induction_list" constr(E) "as" simple_intropattern(I) "with" ident(l) :=
  let H := fresh "H" l in
  induction_list_tac E I l H.
Tactic Notation "induction_list" constr(E) "as" simple_intropattern(I) :=
  let l := fresh "l" in
  induction_list E as I with l.
Tactic Notation "induction_list" constr(E) :=
  induction_list E as [|].
Tactic Notation "induction_list" constr(E) "with" ident(l) :=
  induction_list E as [|] with l.

Tactic Notation "induction_list" ident(E) "as" simple_intropattern(I) "with" ident(l) :=
  let H := fresh "H" l in
  induction_list_tac E I l H.

Section minmax.
  Fact min_fold_le : forall l x0,
    ((fold_right Pos.min x0 l) <= x0)%positive.

  Fact min_fold_in : forall x l x0,
      List.In x l ->
      ((fold_right Pos.min x0 l) <= x)%positive.

  Fact min_fold_eq : forall x1 x2 l,
      Pos.le x1 x2 ->
      Pos.le (fold_right Pos.min x1 l) (fold_right Pos.min x2 l).

  Fact max_fold_ge : forall l x0,
      (x0 <= (fold_left Pos.max l x0))%positive.

  Fact max_fold_in : forall x l x0,
      List.In x l ->
      (x <= (fold_left Pos.max l x0))%positive.
End minmax.

Ltac singleton_length :=
  simpl in *;
  let Hsingl := fresh "Hsingl" in
  match goal with
  | H : length ?x = 1 |- _ =>
    destruct x eqn:Hsingl; simpl in *; try congruence
  end;
  let Hsingl := fresh "Hsingl" in
  match goal with
  | H : S (length ?x) = 1 |- _ =>
    destruct x eqn:Hsingl; simpl in *; try congruence;
    clear H; repeat rewrite app_nil_r in *
  end;
  subst.

Lemma Forall_concat' {A} : forall P (l : (list (list A))),
    Forall (fun x => length x = 1) l ->
    Forall P (concat l) ->
    Forall (Forall P) l.

Lemma Forall2_eq_concat2 {A} : forall (l1 : (list A)) (l2 : (list (list A))),
    Forall (fun x => length x = 1) l2 ->
    Forall2 eq l1 (concat l2) ->
    Forall2 (fun x y => [x] = y) l1 l2.

Section map_filter.
  Context {A B : Type}.

  Variable (f : A -> option B).

  Fixpoint map_filter (ls : list A) : list B :=
    match ls with
    | [] => []
    | a::tl =>
      match f a with
      | Some b => b::(map_filter tl)
      | None => map_filter tl
      end
    end.

  Lemma map_filter_app : forall xs ys,
      map_filter (xs ++ ys) = map_filter xs ++ map_filter ys.

  Lemma map_filter_In : forall x y xs,
      In x xs ->
      f x = Some y ->
      In y (map_filter xs).

  Lemma map_filter_In' : forall y xs,
      In y (map_filter xs) ->
      exists x, In x xs /\ f x = Some y.
End map_filter.


Global Instance Permutation_map_filter_Proper {A B}:
  Proper ((@eq (A -> option B)) ==> Permutation (A:=A) ==> (Permutation (A:=B)))
         (@map_filter A B).

Section remove_member.
  Context {A B : Type}.
  Variable (eq_dec : forall x y : A, {x = y} + {x <> y}).

  Fixpoint remove_member (y : A) (xs : list (A * B)) : (list (A * B)) :=
    match xs with
    | [] => []
    | (x1, x2)::tl => if eq_dec y x1 then remove_member y tl
                    else (x1, x2)::remove_member y tl
    end.

  Lemma remove_member_incl : forall x xs,
      incl (remove_member x xs) xs.

  Lemma remove_member_nIn : forall x xs,
      ~InMembers x (remove_member x xs).

  Lemma remove_member_nIn_idem : forall x xs,
      ~InMembers x xs ->
      remove_member x xs = xs.

  Lemma remove_member_Perm : forall x y xs,
      NoDupMembers xs ->
      In (x, y) xs ->
      Permutation ((x, y)::(remove_member x xs)) xs.

  Lemma remove_member_NoDupMembers : forall x xs,
      NoDupMembers xs ->
      NoDupMembers (remove_member x xs).

  Lemma remove_member_neq_In : forall x xs x' y',
      x' <> x ->
      In (x', y') xs ->
      In (x', y') (remove_member x xs).

  Global Instance remove_member_Proper:
    Proper (@eq A ==> @Permutation (A * B) ==> @Permutation (A * B)) remove_member.

  Definition remove_members (ys : list A) (xs : list (A * B)) : (list (A * B)) :=
    fold_left (fun l x => remove_member x l) ys xs.

  Global Instance remove_members_Proper:
    Proper (@eq (list A) ==> @Permutation (A * B) ==> @Permutation (A * B)) remove_members.

  Lemma remove_members_Perm : forall (d : B) (xs : list A) (ys zs : list (A * B)),
      NoDupMembers zs ->
      Permutation (map (fun x => (x, d)) xs ++ ys) zs ->
      Permutation ys (remove_members xs zs).
End remove_member.

Section ForallTail.
  Context {A : Type}.

  Inductive ForallTail (P : A -> list A -> Prop) : list A -> Prop :=
  | FTnil : ForallTail P []
  | FTcons : forall x xs,
      P x xs ->
      ForallTail P xs ->
      ForallTail P (x::xs).
  Hint Constructors ForallTail.

  Lemma ForallTail_impl : forall (P Q : A -> list A -> Prop) (xs : list A),
      (forall x xs, P x xs -> Q x xs) ->
      ForallTail P xs ->
      ForallTail Q xs.

  Lemma ForallTail_impl_In : forall (P Q : A -> list A -> Prop) (xs : list A),
      (forall x xs', In x xs -> P x xs' -> Q x xs') ->
      ForallTail P xs ->
      ForallTail Q xs.

  Lemma ForallTail_ForallTail : forall (P Q : A -> list A -> Prop) (xs : list A),
      ForallTail P xs ->
      ForallTail Q xs ->
      ForallTail (fun x xs => P x xs /\ Q x xs) xs.

  Lemma ForallTail_insert : forall (P : A -> list A -> Prop) x xs1 xs2,
      ForallTail P (xs1 ++ xs2) ->
      P x xs2 ->
      Forall (fun x' => forall xs1, P x' (xs1 ++ xs2) -> P x' (xs1 ++ x :: xs2)) xs1 ->
      ForallTail P (xs1 ++ x :: xs2).

  Lemma ForallTail_middle : forall (P : A -> list A -> Prop) x xs1 xs2,
      ForallTail P (xs1 ++ x :: xs2) ->
      P x xs2.

End ForallTail.
Hint Constructors ForallTail.

Section Partition.
  Context {A : Type}.
  Variable P : A -> Prop.

  Inductive Partition : list A -> list A -> list A -> Prop :=
  | Partition_nil : Partition [] [] []
  | Partition_cons1 : forall x xs xs1 xs2,
      Partition xs xs1 xs2 ->
      P x ->
      Partition (x::xs) (x::xs1) xs2
  | Partition_cons2 : forall x xs xs1 xs2,
      Partition xs xs1 xs2 ->
      ~P x ->
      Partition (x::xs) xs1 (x::xs2).

  Lemma Partition_left_nil : forall xs xs2,
      Partition xs [] xs2 ->
      xs = xs2.

  Lemma Partition_Permutation : forall xs xs1 xs2,
      Partition xs xs1 xs2 ->
      Permutation xs (xs1++xs2).

  Lemma Partition_Forall1 : forall xs xs1 xs2,
      Partition xs xs1 xs2 ->
      Forall P xs1.

  Lemma dec_Partition : forall xs,
      (forall x, (P x) \/ (~ P x)) ->
      exists xs1 xs2, Partition xs xs1 xs2.
End Partition.
Hint Constructors Partition.

Lemma Partition_ext {A} : forall (P Q : A -> Prop) xs xs1 xs2,
    (forall x, P x <-> Q x) ->
    Partition P xs xs1 xs2 ->
    Partition Q xs xs1 xs2.

Lemma partition_Partition {A} : forall (f : A -> bool) xs xs1 xs2,
    partition f xs = (xs1, xs2) ->
    Partition (fun x => f x = true) xs xs1 xs2.

Section nth_error.
  Lemma nth_error_nth {A} : forall (l : list A) (n : nat) (x d : A),
      nth_error l n = Some x -> nth n l d = x.

  Lemma nth_error_nth' {A} : forall (l : list A) (n : nat) (d : A),
    n < length l -> nth_error l n = Some (nth n l d).

  Lemma nth_error_length_nth {A} : forall (l : list A) (n : nat) (x : A),
      nth_error l n = Some x <-> (forall d, n < Datatypes.length l /\ nth n l d = x).
End nth_error.