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 PeanoNat.
From Coq Require Import BinPos.
From Coq Require Import Lia.
From Coq Require Import Sorting.

From Velus Require Import CommonTactics.

Import List.ListNotations.
Open Scope list_scope.

Global Hint Resolve nth_In : datatypes.

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

  Fixpoint map2 (l: list A) (l': list B) : list C :=
    match l, l' with
    | [], []
    | [], _
    | _, [] => []
    | a :: l, b :: l' =>
      f a b :: map2 l l'
    end.

  Lemma map2_combine:
    forall l l',
      map2 l l' = map (fun '(a, b) => f a b) (combine l l').

  Lemma map2_nil_r:
    forall l,
      map2 l [] = [].

End map2.

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

  Fixpoint fold_left2 (l: list B) (l': list C) (acc: A) : A :=
    match l, l' with
    | [], []
    | [], _
    | _, [] => acc
    | b :: l, c :: l' =>
      fold_left2 l l' (f acc b c)
    end.

  Lemma fold_left2_combine:
    forall l l' acc,
      fold_left2 l l' acc = fold_left (fun a '(b, c) => f a b c) (combine l l') acc.

End fold_left2.

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

  Fixpoint fold_right2 (acc: A) (l: list B) (l': list C) : A :=
    match l, l' with
    | [], []
    | [], _
    | _, [] => acc
    | b :: l, c :: l' =>
      f b c (fold_right2 acc l l')
    end.

  Lemma fold_right2_combine:
    forall l l' acc,
      fold_right2 acc l l' = fold_right (fun '(b, c) => f b c) acc (combine l l').

End fold_right2.

Section Forall'.

  Context {A: Type}.

  Inductive Forall' (P: list A -> A -> Prop) : list A -> Prop :=
  | Forall'_nil:
      Forall' P []
  | Forall'_cons: forall x l,
      P l x ->
      Forall' P l ->
      Forall' P (x :: l).

  Lemma Forall'_app_r:
    forall P l l',
      Forall' P (l ++ l') -> Forall' P l'.

  Lemma Forall'_app_cons:
    forall P l1 x l2,
      Forall' P (l1 ++ x :: l2) ->
      P l2 x.

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

  Lemma Forall'_In:
    forall P l x,
      Forall' P l ->
      In x l ->
      exists l1 l2,
        l = l1 ++ x :: l2
        /\ P l2 x.

End Forall'.

Global Hint Constructors Forall' : datatypes.
Global Hint Constructors NoDup : datatypes.
Global Hint Constructors Permutation : datatypes.
Global Hint Resolve -> Exists_exists : datatypes.

Section Extra.

  Context {A: Type}.

  Lemma nth_error_last:
    forall (l: list A) x n d,
      n = length l ->
      nth_error (x :: l) n = Some (last (x :: l) d).

  Lemma map_last:
    forall {B} (l: list A) (f: A -> B) d,
      last (map f l) (f d) = f (last l d).

  Lemma map_removelast:
    forall {B} (l: list A) (f: A -> B),
      removelast (map f l) = map f (removelast l).

  Lemma last_In_cons:
    forall (l: list A) x d,
      In (last (x :: l) d) (x :: l).

  Lemma nth_error_app3:
    forall (l l': list A) x n,
      n = length l ->
      nth_error (l ++ x :: l') n = Some x.

  Lemma length_removelast_cons:
    forall (l: list A) x,
      length (removelast (x :: l)) = length l.

  Lemma nth_error_removelast:
    forall (l: list A) n,
      (n < length l - 1)%nat ->
      nth_error (removelast l) n = nth_error l n.

  Lemma map_nth_error_inv:
    forall {B} (f: A -> B) l y n,
      nth_error (map f l) n = Some y ->
      exists x,
        nth_error l n = Some x
        /\ y = f x.

  Lemma map_nth_error':
    forall {B} (f : A -> B) l n,
      nth_error (map f l) n = option_map f (nth_error l n).

  Lemma nth_error_nil:
    forall n,
      @nth_error A [] n = None.

  Lemma nth_error_length:
    forall {B} n (l: list A) (l': list B) x,
      nth_error l n = Some x ->
      length l' = length l ->
      exists x', nth_error l' n = Some x'.

  Lemma nth_error_Forall2:
    forall {A B} n (P: A -> B -> Prop) l l' x ,
      nth_error l n = Some x ->
      Forall2 P l l' ->
      exists x', nth_error l' n = Some x'
            /\ P x x'.

  Lemma app_inv:
    forall (l l' l1 l1': list A),
      l ++ l' = l1 ++ l1' ->
      length l = length l1 ->
      l = l1 /\ l' = l1'.

  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.

  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.

  Lemma fold_right_rev_left:
    forall {B} (f : B -> A -> B) (l : list A) (i : B),
      fold_left f (rev l) i = fold_right (fun x y => f y x) i l.
 
  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).

  Lemma filter_ext:
    forall (p1 p2:A -> bool) xs,
      (forall x, p1 x = p2 x) ->
      filter p1 xs = filter p2 xs.

  Lemma filter_filter: forall (p1 p2:A -> bool) xs,
      filter p2 (filter p1 xs) = filter (fun x => andb (p1 x) (p2 x)) xs.

  Corollary filter_filter':
    forall (p1 p2:A -> bool) xs,
      (forall x, p1 x = false -> p2 x = false) ->
      filter p2 (filter p1 xs) = filter p2 xs.

  Lemma Forall_filter:
    forall P p (l: list A),
      Forall P (filter p l) <-> Forall (fun x => p x = true -> P x) l.

  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 filter_nil : forall p (xs : list A),
      Forall (fun x => p x = false) xs ->
      filter p xs = [].

  Lemma filter_idem : forall p (xs : list A),
      Forall (fun x => p x = true) xs ->
      filter p xs = xs.

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

  Global Add Parametric Morphism : (@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.

  Lemma Forall2_map_eq {B} : forall (f : A -> B) l1 l2,
      Forall2 (fun x y => f x = f y) l1 l2 ->
      map f l1 = map f l2.

  Lemma Permutation_concat : forall (l1 l2 : list (list A)),
      Forall2 (fun x y => Permutation x y) l1 l2 ->
      Permutation (concat l1) (concat l2).

  Lemma incl_concat' : forall (l1 l2 : list (list A)),
      Forall2 (fun x y => incl x y) l1 l2 ->
      incl (concat l1) (concat l2).

End Extra.

Section is_nil.
  Context {A : Type}.

  Definition is_nil (l : list A) :=
    match l with
    | [] => true
    | _ => false
    end.

  Lemma is_nil_spec : forall l,
      is_nil l = true <-> l = [].

End is_nil.

Section RevTR.

  Context {A: Type}.


  Fixpoint rev_append (l1 l2: list A) : list A :=
    match l1 with
    | [] => l2
    | a :: l => rev_append l (a :: l2)
    end.

  Definition rev_tr (l: list A) := rev_append l [].

  Lemma rev_tr_spec:
    forall l,
      rev_tr l = rev l.

End RevTR.

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 : forall (x : list A) xs,
      In x xs ->
      incl x (concat xs).

  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).

  Lemma incl_filter':
    forall (l l': list A) p,
      incl l l' ->
      incl (filter p l) l'.

  Lemma incl_app':
    forall (l l' l'': list A),
      incl (l ++ l') l'' ->
      incl l l'' /\ incl l' l''.

  Lemma incl_in_app:
    forall (l l': list A) x,
      incl l l' ->
      (In x l' <-> In x (l ++ l')).
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'.

  Lemma NoDup_snd_det {B} : forall (x : A) (t t' : B) (xs : list (B * A)),
      NoDup (map snd xs) ->
      In (t, x) xs ->
      In (t', x) xs ->
      t = t'.

  Lemma NoDup_concat : forall (xss : list (list A)) xs,
      In xs xss ->
      NoDup (concat xss) ->
      NoDup xs.
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_cons2:
    forall (P : A -> Prop) x l,
      Forall P (x :: l) <-> P x /\ Forall P l.

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

  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 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 {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}.

  Fact Forall_eq {B} : forall (l1 : list A) (b : B) (l2 : list B),
      Forall (eq b) l2 ->
      length l1 = length l2 ->
      l2 = map (fun _ => b) l1.

  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_rev:
    forall (l: list A),
      Forall P l <-> Forall P (rev l).

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

  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_impl_In:
    forall (Q : A -> Prop) xs,
    (forall x, In x xs -> P x -> Q x) ->
    Exists P xs -> Exists Q xs.

  Lemma Exists_Exists_iff :
    forall (Q : A -> Prop) xs,
      (forall x, In x xs -> 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 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_3:
    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.

  Lemma skipn_all2 : forall n (xs: list A),
      length xs <= n ->
      skipn n xs = [].

End SkipnDropn.

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.

Definition reduce_with {A B} (f: A -> B -> A) (l: list B) (first: A) (g: B -> A) : A :=
  match l with
  | [] => first
  | b :: l => fold_left f l (g b)
  end.

Definition reduce {A} (f: A -> A -> A) (l: list A) (first: A) : A :=
  match l with
  | [] => first
  | b :: l => fold_left f l b
  end.

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 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.

  Lemma Forall2_rev:
    forall (l: list A) (l': list B) P,
      Forall2 P l l' <-> Forall2 P (rev l) (rev l').

End Forall2.

Global Hint Resolve -> Forall2_eq : core.
Global Hint Resolve <- Forall2_eq : core.

Lemma length_in_left_combine:
  forall {A B} (l: list A) (l': list B) x,
    length l = length l' ->
    In x l ->
    exists y, In (x, y) (combine l l').

Lemma length_in_right_combine:
  forall {A B} (l': list A) (l: list B) x,
    length l = length l' ->
    In x l' ->
    exists y, In (y, x) (combine l l').

Lemma combine_nth_error:
  forall {A B} (l: list A) (l': list B) x y n,
    nth_error (combine l l') n = Some (x, y) <-> nth_error l n = Some x /\ nth_error l' n = Some y.

Corollary In_combine_nth_error:
  forall {A B} (l: list A) (l': list B) x y,
    In (x, y) (combine l l') <-> exists n, nth_error l n = Some x /\ nth_error l' n = Some y.

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, In y ys /\ In z zs /\ R x y z) xs.

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

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

  Lemma Forall3_ignore1:
    forall xs ys zs,
      Forall3 xs ys zs ->
      Forall2 (fun y z => exists x, In x xs /\ R x y z) ys 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.

  Lemma Forall3_app_inv_1:
    forall xs1 xs2 ys zs,
      Forall3 (xs1++xs2) ys zs ->
      exists ys1 ys2 zs1 zs2,
        ys = ys1 ++ ys2 /\ zs = zs1 ++ zs2 /\
        Forall3 xs1 ys1 zs1 /\
        Forall3 xs2 ys2 zs2.
End Forall3.

Section Forall3_map.
  Context {A B C D : Type}.

  Lemma Forall3_map_1:
    forall (P : D -> B -> C -> Prop) (f: A -> D) xs ys zs,
      Forall3 P (map f xs) ys zs <-> Forall3 (fun x y z => P (f x) y z) xs ys zs.

  Lemma Forall3_map_2:
    forall (P : A -> D -> C -> Prop) (f: B -> D) xs ys zs,
      Forall3 P xs (map f ys) zs <-> Forall3 (fun x y z => P x (f y) z) xs ys zs.

  Lemma Forall3_map_3:
    forall (P : A -> B -> D -> Prop) (f: C -> D) xs ys zs,
      Forall3 P xs ys (map f zs) <-> Forall3 (fun x y z => P x y (f z)) xs ys zs.

End Forall3_map.

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_combine2 {A B C} : forall (P : A -> B -> C -> Prop) ys xs zs,
    length ys = length zs ->
    Forall2 (fun x '(y, z) => P x y z) xs (combine ys zs) ->
    Forall3 P 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_combine'2 {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 xs (combine 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_inv:
    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.

  Lemma filter_InMembers:
    forall p x (l: list (A * B)),
      InMembers x (filter p l) <-> exists b, In (x, b) l /\ p (x, b) = true.

  Corollary filter_InMembers':
    forall p x (l: list (A * B)),
      InMembers x (filter p l) -> InMembers x l.

  Fact InMembers_flat_map {C} : forall (f : C -> list (A * B)) (l : list C) (y : A),
      InMembers y (flat_map f l) <-> Exists (fun x => InMembers y (f x)) l.

  Fact NoDupMembers_flat_map {C} : forall (f : C -> list (A * B)) (l : list C),
      NoDupMembers (flat_map f l) ->
      Forall (fun x => NoDupMembers (f x)) l.

End InMembers.
Global Hint Constructors NoDupMembers : datatypes.
Global Hint Rewrite -> @fst_InMembers : list.

Lemma NoDupMembers_filter {A B} :
  forall f (l: list (A * B)),
    NoDupMembers l -> NoDupMembers (filter f l).

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}.

  Definition 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 SameElements.
  Import SetoidList.

  Context {A : Type}.
  Variable (eqA : A -> A -> Prop).

  Inductive SameElements : list A -> list A -> Prop :=
  | SE_nil : SameElements [] []
  | SE_skip : forall x x' l l',
      SameElements l l' ->
      eqA x x' ->
      SameElements (x::l) (x'::l')
  | SE_dup1 : forall x l,
      InA eqA x l ->
      SameElements (x::l) l
  | SE_dup2 : forall x l,
      InA eqA x l ->
      SameElements l (x::l)
  | SE_perm : forall l l',
      Permutation l l' ->
      SameElements l l'
  | SE_trans : forall l l' l'',
      SameElements l l' ->
      SameElements l' l'' ->
      SameElements l l''.
End SameElements.
Global Hint Constructors SameElements : datatypes.

Global Instance SameElements_sym' {A} {eqA : A -> A -> Prop}
  (Hsym : Symmetric eqA): Symmetric (SameElements eqA).

Global Instance SameElements_sym {A} : Symmetric (SameElements (@eq A)).

Section Forall2_SameElements_1.
  Import SetoidList.

  Context {A B : Type}.
  Context {eqA : A -> A -> Prop}.
  Context {eqB : B -> B -> Prop}.

  Hypothesis EqA_refl : Reflexive eqA.
  Hypothesis EqA_sym : Symmetric eqA.
  Hypothesis EqB_refl : Reflexive eqB.

  Variable (P : A -> B -> Prop).

  Hypothesis P_proper : forall x x' y y',
      eqA x x' ->
      eqB y y' ->
      P x y ->
      P x' y'.

  Hypothesis P_det : forall x y y',
      P x y ->
      P x y' ->
      eqB y y'.

  Lemma Forall2_inA_left : forall x l1 l2,
      Forall2 P l1 l2 ->
      InA eqA x l1 ->
      exists y, InA eqB y l2 /\ P x y.

  Lemma Forall2_SameElements_1 : forall l1 l1' l2,
      SameElements eqA l1 l1' ->
      Forall2 P l1 l2 ->
      exists l2' , SameElements eqB l2 l2' /\ Forall2 P l1' l2'.
End Forall2_SameElements_1.

Add Parametric Morphism {A} {eqA : A -> A -> Prop} (P: A -> Prop)
  (P_compat : Proper (eqA ==> Basics.impl) P): (Exists P)
    with signature SameElements eqA ==> Basics.impl
      as Exists_SameElements_morph.

Add Parametric Morphism {A} {eqA : A -> A -> Prop} (p: A -> bool)
  (P_compat : Proper (eqA ==> eq) p): (existsb p)
    with signature SameElements eqA ==> eq
      as existsb_SameElements_morph.


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_cons:
    forall l a,
      ltsuffix l (a :: l).

  Lemma ltsuffix_wf:
    well_founded ltsuffix.

  Lemma list_ind_ltsuffix:
    forall (P: list A -> Prop),
      (forall l, (forall l', ltsuffix l' l -> P l') -> P l) ->
    forall l, P l.

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.

Lemma Sorted_impl {A} : forall (R1 R2 : A -> A -> Prop) xs,
    (forall x y, R1 x y -> R2 x y) ->
    Sorted R1 xs ->
    Sorted R2 xs.

Lemma Sorted_map {A B} : forall (f : A -> B) (R : B -> B -> Prop) xs,
    Sorted R (map f xs) <->
    Sorted (fun x y => R (f x) (f y)) xs.

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 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.

  Lemma incl_map_filter : forall xs ys,
      incl xs ys ->
      incl (map_filter xs) (map_filter ys).

  Lemma map_filter_nil : forall xs,
      Forall (fun x => f x = None) xs ->
      map_filter xs = [].
End map_filter.

Lemma map_filter_ext {A B} : forall (f g : A -> option B) xs,
    (forall x, f x = g x) ->
    map_filter f xs = map_filter g xs.

Lemma map_map_filter {A B C} : forall (f : A -> option B) (g : B -> C) xs,
    map g (map_filter f xs) = map_filter (fun a => option_map g (f a)) xs.

Lemma map_filter_map {A B C} : forall (f : B -> option C) (g : A -> B) xs,
    (map_filter f (map g xs)) = map_filter (fun a => f (g a)) xs.

Lemma InMembers_map {A B C} :
  forall (f : _ -> (A * C)) x (l: list (A * B)),
    (forall a b, fst (f (a, b)) = a) ->
    InMembers x l ->
    InMembers x (map f l).

Lemma NoDupMembers_map {A B C} :
  forall (f : _ -> (A * C)) (l: list (A * B)),
    (forall a b, fst (f (a, b)) = a) ->
    NoDupMembers l ->
    NoDupMembers (map f l).

Lemma NoDupMembers_map_filter {A B C} :
  forall (f : _ -> option (A * C)) (l: list (A * B)),
    (forall a b, LiftO True (fun '(a', _) => a' = a) (f (a, b))) ->
    NoDupMembers l ->
    NoDupMembers (map_filter f l).

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 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 Partition_Forall2 : forall xs xs1 xs2,
      Partition xs xs1 xs2 ->
      Forall (fun x => ~P x) xs2.

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

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.

Corollary In_combine_seq {A} : forall (xs : list A) k x,
    In (k, x) (combine (seq 0 (length xs)) xs) <->
    nth_error xs k = Some x.

Fact in_app_map_flat_map {A B C} : forall (f : C -> B) (g : A -> list C) x xs y ys,
    In y ys ->
    In x (xs ++ map f (g y)) ->
    In x (xs ++ map f (flat_map g ys)).


Fact nodup_map_flat_map {A B C} : forall (f : C -> B) (g : A -> list C) x xs,
    In x xs ->
    NoDup (map f (flat_map g xs)) ->
    NoDup (map f (g x)).

Fact nodup_map_filter_flat_map {A B C D} : forall (f : C -> option B) (g : A -> list C) (h : B -> D) x xs,
    In x xs ->
    NoDup (map h (map_filter f (flat_map g xs))) ->
    NoDup (map h (map_filter f (g x))).

Fact nodup_app_map_flat_map {A B C} : forall (f : C -> B) (g : A -> list C) xs y ys,
    In y ys ->
    NoDup (xs ++ map f (flat_map g ys)) ->
    NoDup (xs ++ map f (g y)).

Fact NoDupMembers_app_map_flat_map {A B C D} : forall (f : B -> (C * D)) (g : A -> list B) xs y ys,
    In y ys ->
    NoDupMembers (xs ++ map f (flat_map g ys)) ->
    NoDupMembers (xs ++ map f (g y)).


Local Ltac simpl_map_In H :=
  let Hin := fresh "Hin" in
  let Heq := fresh "Heq" in
  apply in_map_iff in H as (?&Heq&Hin); destruct_conjs; inv Heq; subst.

Ltac simpl_In :=
  repeat autorewrite with list in *;
  repeat
    (match goal with
     | H: In _ (map ?f _) |- _ => simpl_map_In H
     | |- In _ (map ?f _) => rewrite in_map_iff
     | H: In _ (flat_map ?f _) |- _ =>
         let Hin1 := fresh "Hin" in
         let Hin2 := fresh "Hinf" in
         apply in_flat_map in H as (?&Hin1&Hin2)
     | H: In _ (filter _ _) |- _ =>
         let Hin := fresh "Hin" in
         let Hf := fresh "Hf" in
         apply filter_In in H as (Hin&Hf)
     | H:In _ (map_filter _ _) |- _ =>
         let Hin1 := fresh "Hin" in
         let Hin2 := fresh "Hf" in
         apply map_filter_In' in H as (?&Hin1&Hin2)
     | H:In _ (?f _) |- _ => autounfold with list in H; simpl_map_In H
     | |- In _ (?f _) => progress (autounfold with list); simpl_In
     end; simpl; inv_equalities).

Ltac solve_In :=
  repeat
    (simpl_In;
     match goal with
     | |- In _ (map_filter _ _) => eapply map_filter_In
     | |- In _ (filter _ _) => apply filter_In; split
     | |- exists _, _ /\ In _ _ => do 2 esplit; eauto; try solve_In; auto; simpl
     | |- In _ (flat_map _ _) => apply in_flat_map; do 2 esplit
     | H: In _ (combine _ _) |- In _ _ =>
         (eapply in_combine_l in H; now solve_In)||(eapply in_combine_r in H; now solve_In)
     end;
     eauto).

Ltac simpl_Forall :=
  repeat
    (match goal with
     | H: Forall _ [] |- _ => inv H
     | H: Forall _ [_] |- _ => inv H
     | H: Forall _ (_ :: _) |- _ => inv H
     | |- Forall _ [] => constructor
     | |- Forall _ [_] => constructor; auto

     | H: Forall _ ?xs, Hin: In _ ?xs |- _ =>
         eapply Forall_forall in H; [|eapply Hin]; simpl in *
     | H: Forall _ (map _ _) |- _ => rewrite Forall_map in H
     | |- Forall _ (map _ _) => rewrite Forall_map
     | |- Forall _ _ => apply Forall_forall; intros


     | H: Forall2 _ [_] _ |- _ => inv H
     | H: Forall2 _ [] _ |- _ => inv H
     | H: Forall2 _ _ [_] |- _ => inv H
     | H: Forall2 _ _ [] |- _ => inv H
     | |- Forall2 _ [] [] => constructor
     | |- Forall2 _ [_] [_] => constructor; auto

     | H: Forall2 _ (map _ _) _ |- _ => rewrite Forall2_map_1 in H
     | H: Forall2 _ _ (map _ _) |- _ => rewrite Forall2_map_2 in H
     | |- Forall2 _ (map _ _) _ => rewrite Forall2_map_1
     | |- Forall2 _ _ (map _ _) => rewrite Forall2_map_2
     | H: Forall2 _ ?xs ?xs |- _ => rewrite <-Forall2_same in H
     | |- Forall2 _ ?xs ?xs => rewrite <-Forall2_same

     | H1: Forall2 _ ?xs ?ys, H2: Forall2 _ ?xs ?ys |- _ =>
         eapply Forall2_Forall2 in H2; [|eapply H1]; clear H1

     | H: Forall2 _ ?xs ?ys |- Forall2 _ ?xs ?ys =>
         eapply Forall2_impl_In; [|eapply H]; intros
     end; destruct_conjs).

Ltac rewrite_Forall_forall :=
  repeat
    match goal with
    | H : Forall _ _ |- _ =>
        rewrite Forall_forall in H
    | H : Forall2 _ _ _ |- _ =>
        rewrite Forall2_forall2 in H; destruct H
    | H : Forall3 _ _ _ _ |- _ =>
        rewrite Forall3_forall3 in H; destruct H as [? [? ?]]
    | |- Forall _ _ =>
        rewrite Forall_forall; intros; subst
    | |- Forall2 _ _ _ =>
        rewrite Forall2_forall2; repeat split; auto; intros; subst
    | |- Forall3 _ _ _ _ =>
        rewrite Forall3_forall3; repeat split; auto; intros; subst
    end.

Ltac simpl_Exists :=
  repeat
    match goal with
    | H: Exists _ (map _ _) |- _ => rewrite Exists_map in H
    | |- Exists _ (map _ _) => rewrite Exists_map
    | H: Exists _ _ |- _ =>
        let Hin := fresh "Hin" in
        apply Exists_exists in H as (?&Hin&H)
    end; destruct_conjs.

Ltac solve_Exists :=
  simpl_Exists;
  repeat
    match goal with
    | |- Exists _ _ => apply Exists_exists; do 2 esplit; [eauto|]
    end; simpl; eauto.


Create HintDb list.

Ltac simpl_app :=
  autounfold with list in *;
  repeat (simpl in *; (rewrite map_app in * || rewrite map_filter_app in * || rewrite <-app_assoc in * )).

Ltac solve_incl_app :=
  simpl_app; eauto using incl_nil, incl_refl;
  match goal with
  | |- incl [] _ => now apply incl_nil
  | |- incl ?xs ?xs => now apply incl_refl
  | |- incl ?xs (?xs ++ _) => now apply incl_appl, incl_refl
  | |- incl (?xs ++ _) (?xs ++ _) =>
    apply incl_appr'; solve_incl_app
  | |- incl _ (?xs2 ++ _) =>
    apply incl_appr; solve_incl_app
  | _ => idtac
  end.

Lemma NoDup_incl_app1 {A : Type} : forall (xs ys zs : list A),
    incl zs ys ->
    (NoDup ys -> NoDup zs) ->
    NoDup (xs ++ ys) ->
    NoDup (xs ++ zs).

Lemma NoDup_incl_app2 {A : Type} : forall (xs ys zs : list A),
    incl zs xs ->
    (NoDup xs -> NoDup zs) ->
    NoDup (xs ++ ys) ->
    NoDup (zs ++ ys).

Ltac solve_NoDup_app :=
  simpl_app;
  match goal with
  | |- NoDup [] => now constructor
  | Hnd:NoDup ?xs |- NoDup ?xs => assumption
  | Hnd:NoDup (?xs1++?ys1) |- NoDup ?xs1 =>
    now eapply NoDup_app_l, Hnd
  | Hnd:NoDup (?xs1++?ys1) |- NoDup (?xs1++_) =>
    eapply NoDup_incl_app1 with (ys:=ys1);
    [| |eauto]; [now solve_incl_app|clear Hnd; intros; solve_NoDup_app]
  | Hnd:NoDup (_++_) |- NoDup _ =>
    eapply NoDup_app_r in Hnd; solve_NoDup_app
  end.

Lemma NoDupMembers_incl_app (A B : Type) : forall (xs ys zs : list (A * B)),
    incl zs ys ->
    (NoDupMembers ys -> NoDupMembers zs) ->
    NoDupMembers (xs ++ ys) ->
    NoDupMembers (xs ++ zs).

Ltac solve_NoDupMembers_app :=
  simpl_app;
  match goal with
  | |- NoDupMembers [] => now constructor
  | Hnd:NoDupMembers ?xs |- NoDupMembers ?xs => assumption
  | Hnd:NoDupMembers (?xs1++?ys1) |- NoDupMembers ?xs1 =>
    now eapply NoDupMembers_app_l, Hnd
  | Hnd:NoDupMembers (?xs1++?ys1) |- NoDupMembers (?xs1++_) =>
    eapply NoDupMembers_incl_app with (ys:=ys1);
    [| |eauto]; [now solve_incl_app|clear Hnd; intros; solve_NoDupMembers_app]
  | Hnd:NoDupMembers (_++_) |- NoDupMembers _ =>
    eapply NoDupMembers_app_r in Hnd; solve_NoDupMembers_app
  end.

Ltac solve_Permutation_app :=
  simpl_app;
  match goal with
  | |- Permutation _ _ => apply Permutation_refl
  | |- Permutation (_ ++ _) (_ ++ _) => apply Permutation_app_head; solve_Permutation_app
  | |- Permutation (?xs ++ ?ys) _ => rewrite (Permutation_app_comm xs ys); solve_Permutation_app
  end.

Example solve_Perm_app {A} : forall (l1 l2 l3 l4 l5 l6 l7 : list A),
    Permutation (l1 ++ l2 ++ l3 ++ l4 ++ l5 ++ l6 ++ l7) (l2 ++ (l3 ++ l5) ++ l4 ++ l1 ++ (l7 ++ l6)).