(**************************************************************)
(*   Copyright Dominique Larchey-Wendling *                 *)
(*                                                            *)
(*                             * Affiliation LORIA -- CNRS  *)
(**************************************************************)
(*      This file is distributed under the terms of the       *)
(*         CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT          *)
(**************************************************************)

Require Import List Arith Omega Permutation.

From Undecidability.Shared.Libs.DLW.Utils Require Import list_focus utils_tac.

Set Implicit Arguments.

Create HintDb length_db.

Tactic Notation "rew" "length" := autorewrite with length_db.
Tactic Notation "rew" "length" "in" hyp(H) := autorewrite with length_db in H.

Infix "~p" := (@Permutation _) (at level 70).

Section In_t.

  Variable (X : Type).

  Fixpoint In_t (x : X) l : Type :=
    match l with
      | nil False
      | y::l ((y = x) + In_t x l)%type
    end.

  Fact In_t_In x l : In_t x l In x l.
  Proof. induction l; simpl; tauto. Qed.

  Fact In_In_t x l (P : Prop) : (In_t x l P) In x l P.
  Proof.
    induction l as [ | y l IHl ].
    + intros _ [].
    + intros [ | ].
      * apply ; simpl; auto.
      * apply IHl; auto.
        intros; apply ; simpl; auto.
  Qed.


End In_t.

Section length.

  Variable X : Type.

  Implicit Type l : list X.

  Fact length_nil : length (@nil X) = 0.
  Proof. auto. Qed.

  Fact length_cons x l : length (x::l) = S (length l).
  Proof. auto. Qed.

End length.

Hint Rewrite length_nil length_cons app_length map_length rev_length : length_db.

Section list_an.

  Fixpoint list_an a n :=
    match n with
      | 0 nil
      | S n a::list_an (S a) n
    end.

  Fact list_an_S a n : list_an a (S n) = a::list_an (S a) n.
  Proof. auto. Qed.

  Fact list_an_plus a n m : list_an a (n+m) = list_an a n list_an (n+a) m.
  Proof.
    revert a; induction n; intros a; simpl; auto.
    rewrite IHn; do 3 f_equal; omega.
  Qed.


  Fact list_an_length a n : length (list_an a n) = n.
  Proof.
    revert a; induction n; intro; simpl; f_equal; auto.
  Qed.


  Fact list_an_spec a n m : In m (list_an a n) a m < a+n.
  Proof.
    revert a; induction n as [ | n IHn ]; simpl; intros a; [ | rewrite IHn ]; omega.
  Qed.


  Fact map_S_list_an a n : map S (list_an a n) = list_an (S a) n.
  Proof. revert a; induction n; simpl; intro; f_equal; auto. Qed.

  Fact list_an_app_inv a n l r : list_an a n = lr l = list_an a (length l) r = list_an (a+length l) (length r).
  Proof.
    revert a l r; induction n as [ | n IHn ]; intros a l r; simpl.
    + destruct l; destruct r; intros; auto; discriminate.
    + destruct l as [ | x l ]; simpl; intros .
      * split; auto.
        rewrite ; simpl; rewrite Nat.add_0_r, list_an_length; auto.
      * injection ; clear ; intros .
        apply IHn in ; destruct ; split; f_equal; auto.
        rewrite at 1; f_equal; omega.
  Qed.


  Fact list_an_duplicate_inv a n l x m y r :
        list_an a n = lx::my::r a x x < y < a+n.
  Proof.
    intros H.
    generalize H; intros .
    apply f_equal with (f := @length _) in .
    rewrite list_an_length in .
    apply list_an_app_inv in H; simpl in H.
    destruct H as ( & H); injection H; clear H; intros H .
    symmetry in H; apply list_an_app_inv in H; simpl in H.
    destruct H as ( & H); injection H; clear H; intros .
    do 2 (rewrite app_length in ; simpl in ).
    omega.
  Qed.


End list_an.

Hint Rewrite list_an_length : length_db.

Definition list_fun_inv X (l : list X) (x : X) : { f : X | l = map f (list_an 0 (length l)) }.
Proof.
  induction l as [ | y l IHl ].
  + exists ( _ x); auto.
  + destruct IHl as (f & Hf).
    exists ( i match i with 0 y | S i f i end); simpl.
    f_equal.
    rewrite Hf, map_S_list_an, map_length, list_an_length, map_map; auto.
Qed.


Fact list_upper_bound (l : list ) : { m | x, In x l x < m }.
Proof.
  induction l as [ | x l (m & Hm) ].
  + exists 0; simpl; tauto.
  + exists (1+x+m); intros y [ [] | H ]; simpl; try omega.
    generalize (Hm _ H); intros; omega.
Qed.


Section list_injective.

  Variable X : Type.

  Definition list_injective (ll : list X) := l a m b r, ll = l a :: m b :: r a b.

  Fact in_list_injective_0 : list_injective nil.
  Proof. intros [] ? ? ? ? ?; discriminate. Qed.

  Fact in_list_injective_1 x ll : In x ll list_injective ll list_injective (x::ll).
  Proof.
    intros l a m b r .
    destruct l as [ | u l ].
    inversion ; subst.
    destruct m as [ | v m ].
    contradict ; subst; simpl; auto.
    contradict ; subst; simpl; right; apply in_or_app; right; left; auto.
    inversion ; subst.
    apply ( l _ m _ r); auto.
  Qed.


  Fact list_injective_inv x ll : list_injective (x::ll) In x ll list_injective ll.
  Proof.
    split.
    intros ; apply in_split in ; destruct as (l & r & ?); subst.
    apply (H nil x l x r); auto.
    intros l a m b r ?; apply (H (x::l) a m b r); subst; solve list eq.
  Qed.


  Variable P : list X Type.

  Hypothesis ( : P nil).
  Hypothesis ( : x l, In x l P l P (x::l)).

  Theorem list_injective_rect l : list_injective l P l.
  Proof.
    induction l as [ [ | x l ] IHl ] using (measure_rect (@length _)).
    intro; apply .
    intros; apply .
    apply list_injective_inv, H.
    apply IHl; simpl; auto.
    apply list_injective_inv with (1 := H).
  Qed.


End list_injective.

Fact list_injective_map X Y (f : X Y) ll :
       ( x y, f x = f y x = y) list_injective ll list_injective (map f ll).
Proof.
  intros Hf.
  induction 1 as [ | x l Hl IHl ] using list_injective_rect.
  apply in_list_injective_0.
  simpl; apply in_list_injective_1; auto.
  contradict Hl.
  apply in_map_iff in Hl.
  destruct Hl as (y & Hl & ?).
  apply Hf in Hl; subst; auto.
Qed.


Fact list_app_head_not_nil X (u v : list X) : u nil v uv.
Proof.
  intros H; contradict H.
  destruct u as [ | a u ]; auto; exfalso.
  apply f_equal with (f := @length _) in H.
  revert H; simpl; rewrite app_length; intros; omega.
Qed.


Section iter.

  Variable (X : Type) (f : X X).

  Fixpoint iter x n :=
    match n with
      | 0 x
      | S n iter (f x) n
    end.

  Fact iter_plus x a b : iter x (a+b) = iter (iter x a) b.
  Proof. revert x; induction a; intros x; simpl; auto. Qed.

  Fact iter_swap x n : iter (f x) n = f (iter x n).
  Proof.
    change (iter (f x) n) with (iter x (1+n)).
    rewrite plus_comm, iter_plus; auto.
  Qed.


  Fact iter_S x n : iter x (S n) = f (iter x n).
  Proof. apply iter_swap. Qed.

End iter.

Fixpoint list_repeat X (x : X) n :=
  match n with
    | 0 nil
    | S n x::list_repeat x n
  end.

Fact list_repeat_plus X x a b : @list_repeat X x (a+b) = list_repeat x a list_repeat x b.
Proof. induction a; simpl; f_equal; auto. Qed.

Fact list_repeat_length X x n : length (@list_repeat X x n) = n.
Proof. induction n; simpl; f_equal; auto. Qed.

Fact In_list_repeat X (x y : X) n : In y (list_repeat x n) x = y 0 < n.
Proof.
  induction n; simpl; intros [].
  split; auto; omega.
  split; try omega; apply IHn; auto.
Qed.


Fact map_list_repeat X Y f x n : @map X Y f (list_repeat x n) = list_repeat (f x) n.
Proof. induction n; simpl; f_equal; auto. Qed.

Fact map_cst_repeat X Y (y : Y) ll : map ( _ : X y) ll = list_repeat y (length ll).
Proof. induction ll; simpl; f_equal; auto. Qed.

Fact map_cst_snoc X Y (y : Y) ll mm : y :: map ( _ : X y) llmm = map ( _ y) ll y::mm.
Proof. induction ll; simpl; f_equal; auto. Qed.

Fact map_cst_rev X Y (y : Y) ll : map ( _ : X y) (rev ll) = map ( _ y) ll.
Proof. do 2 rewrite map_cst_repeat; rewrite rev_length; auto. Qed.

Fact In_perm X (x : X) l : In x l m, x::m p l.
Proof.
  intros H; apply in_split in H.
  destruct H as (m & k & ?); subst.
  exists (mk).
  apply Permutation_cons_app; auto.
Qed.


Fact list_app_eq_inv X ( : list X) :
        = { m | m = = m }
                        + { m | m = = m }.
Proof.
  revert ; induction as [ | x IH ].
  intros; left; exists ; auto.
  intros [ | y ] ; simpl; intros H.
  right; exists (x::); auto.
  inversion H.
  destruct (IH ) as [ (m & Hm) | (m & Hm) ]; auto;
    [ left | right ]; exists m; split; f_equal; tauto.
Qed.


Fact list_app_cons_eq_inv X ( : list X) x :
        = x:: { m | m = = mx:: }
                           + { m | x::m = = m }.
Proof.
  intros H.
  apply list_app_eq_inv in H.
  destruct H as [ H | (m & & ) ]; auto.
  destruct m as [ | y m ].
  left; exists nil; simpl in *; split; auto.
  revert ; do 2 rewrite app_nil_end; auto.
  inversion ; subst.
  right; exists m; auto.
Qed.


Fact list_cons_app_cons_eq_inv X ( : list X) x y :
       x:: = y:: ( = nil x = y = )
                          + { m | = x::m = my:: }.
Proof.
  intros H.
  destruct as [ | z m ]; simpl in H.
  + left; inversion H; auto.
  + right; exists m; inversion H; auto.
Qed.


Fact list_app_inj X ( : list X) : length = length = = = .
Proof.
  revert ; induction as [ | x IH ]; intros [ | y ]; try discriminate.
  simpl; auto.
  intros ; inversion ; inversion .
  apply IH in ; auto.
  split; f_equal; tauto.
Qed.


Fact list_split_length X (ll : list X) k : k length ll { l : _ & { r | ll = lr length l = k } }.
Proof.
  revert k; induction ll as [ | x ll IHll ]; intros k.
  exists nil, nil; split; simpl in * |- *; auto; omega.
  destruct k as [ | k ]; intros Hk.
  exists nil, (x::ll); simpl; split; auto.
  destruct (IHll k) as (l & r & & ).
  simpl in Hk; omega.
  exists (x::l), r; split; simpl; auto; f_equal; auto.
Qed.


Fact list_pick X (ll : list X) k : k < length ll { x : _ & { l : _ & { r | ll = lx::r length l = k } } }.
Proof.
  revert k; induction ll as [ | x ll IHll ]; intros k.
  simpl; omega.
  destruct k as [ | k ]; intros H.
  exists x, nil, ll; simpl; auto.
  simpl in H.
  destruct IHll with (k := k) as (y & l & r & ? & ?); try omega.
  exists y, (x::l), r; subst; simpl; split; auto.
Qed.


Fact list_split_middle X ( : X) :
        In In :: = :: = = = .
Proof.
  intros H.
  apply list_app_eq_inv in H.
  destruct H as [ (m & & ) | (m & & ) ]; destruct m.
  inversion ; subst; rewrite app_nil_end; auto.
  inversion ; subst; destruct ; apply in_or_app; right; left; auto.
  inversion ; subst; rewrite app_nil_end; auto.
  inversion ; subst; destruct ; apply in_or_app; right; left; auto.
Qed.


Section flat_map.

  Variable (X Y : Type) (f : X list Y).

  Fact flat_map_app : flat_map f () = flat_map f flat_map f .
  Proof.
    induction ; simpl; auto; solve list eq; f_equal; auto.
  Qed.


  Fact flat_map_app_inv l y : flat_map f l = y:: x , l = x:: f x = y::
                                                                   = flat_map f = flat_map f .
  Proof.
    revert y .
    induction l as [ | x l IHl ]; intros y H.
    + destruct ; discriminate.
    + simpl in H.
      apply list_app_cons_eq_inv in H.
      destruct H as [ (m & & ) | (m & & ) ].
      - apply IHl in .
        destruct as ( & & x' & & & & & & ); subst.
        exists (x::), , x', , ; simpl; repeat (split; auto).
        rewrite app_ass; auto.
      - exists nil, , x, m, l; auto.
  Qed.


End flat_map.

Fact in_concat_iff X (ll : list (list X)) x : In x (concat ll) l, In x l In l ll.
Proof.
  rewrite (map_id ll) at 1.
  rewrite flat_map_concat_map, in_flat_map.
  firstorder.
Qed.


Fact flat_map_flat_map X Y Z (f : X list Y) (g : Y list Z) l :
       flat_map g (flat_map f l) = flat_map ( x flat_map g (f x)) l.
Proof.
  induction l; simpl; auto.
  rewrite flat_map_app; f_equal; auto.
Qed.


Fact flat_map_single X Y (f : X Y) l : flat_map ( x f x::nil) l = map f l.
Proof. induction l; simpl; f_equal; auto. Qed.

Section list_in_map.

  Variable (X Y : Type).

  Fixpoint list_in_map l : ( x, @In X x l Y) list Y.
  Proof.
    refine (match l with
      | nil _ nil
      | x::l f f x _ :: @list_in_map l _
    end).
    + left; auto.
    + intros y Hy; apply (f y); right; auto.
  Defined.


  Theorem In_list_in_map l f x (Hx : In x l) : In (f x Hx) (list_in_map l f).
  Proof.
    revert f x Hx.
    induction l as [ | x l IHl ]; intros f y Hy.
    + destruct Hy.
    + destruct Hy as [ | Hy ].
      * left; auto.
      * right.
        apply (IHl ( z Hz f z (or_intror Hz))).
  Qed.


  Theorem In_list_in_map_inv l f y : In y (list_in_map l f) x Hx, y = f x Hx.
  Proof.
    revert f y; induction l as [ | x l IHl ]; intros f y; simpl; try tauto.
    intros [ H | H ].
    + now exists x, (or_introl eq_refl).
    + destruct IHl with (1 := H) as (z & Hz & E).
      now exists z, (or_intror Hz).
  Qed.


End list_in_map.

Definition prefix X (l ll : list X) := r, ll = lr.

Infix "<p" := (@prefix _) (at level 70, no associativity).

Section prefix. (* as an inductive predicate *)

  Variable X : Type.

  Implicit Types (l ll : list X).

  Fact in_prefix_0 ll : nil <p ll.
  Proof.
    exists ll; auto.
  Qed.


  Fact in_prefix_1 x l ll : l <p ll x::l <p x::ll.
  Proof.
    intros (r & ?); subst; exists r; auto.
  Qed.


  Fact prefix_length l m : l <p m length l length m.
  Proof. intros (? & ?); subst; rew length; omega. Qed.

  Fact prefix_app_lft l : <p l <p l.
  Proof.
    intros (a & ?); subst.
    exists a; rewrite app_ass; auto.
  Qed.


  Fact prefix_inv x y l ll : x::l <p y::ll x = y l <p ll.
  Proof.
    intros (r & Hr).
    inversion Hr; split; auto.
    exists r; auto.
  Qed.


  Fact prefix_list_inv l r rr : lr <p lrr r <p rr.
  Proof.
    induction l as [ | x l IHl ]; simpl; auto.
    intros H; apply prefix_inv, proj2, IHl in H; auto.
  Qed.


  Fact prefix_refl l : l <p l.
  Proof. exists nil; rewrite app_nil_end; auto. Qed.

  Fact prefix_trans : <p <p <p .
  Proof. intros ( & ) ( & ); subst; exists (); solve list eq. Qed.

  Section prefix_rect.

    Variables (P : list X list X Type)
              ( : ll, P nil ll)
              ( : x l ll, l <p ll P l ll P (x::l) (x::ll)).

    Definition prefix_rect l ll : prefix l ll P l ll.
    Proof.
      revert l; induction ll as [ | x ll IHll ]; intros l H.

      replace l with (nil : list X).
      apply .
      destruct H as (r & Hr).
      destruct l; auto; discriminate.

      destruct l as [ | y l ].
      apply .
      apply prefix_inv in H.
      destruct H as (? & E); subst y.
      apply ; [ | apply IHll ]; trivial.
    Qed.


  End prefix_rect.

  Fact prefix_app_inv : <p { <p } + { <p }.
  Proof.
    revert ; induction as [ | x IH ].
    left; apply in_prefix_0.
    intros [ | y ] .
    right; apply in_prefix_0.
    simpl; intros H; apply prefix_inv in H.
    destruct H as (E & H); subst y.
    destruct IH with (1 := H); [ left | right ];
      apply in_prefix_1; auto.
  Qed.


End prefix.

Definition prefix_spec X (l ll : list X) : l <p ll { r | ll = l r }.
Proof.
  induction 1 as [ ll | x l ll _ (r & Hr) ] using prefix_rect.
  exists ll; trivial.
  exists r; simpl; f_equal; auto.
Qed.


Fact prefix_app_lft_inv X ( m : list X) : <p m { | m = <p }.
Proof.
  intros H.
  apply prefix_spec in H.
  destruct H as (r & H).
  exists (r); simpl.
  solve list eq in H; split; auto.
  exists r; auto.
Qed.


Section list_assoc.

  Variables (X Y : Type) (eq_X_dec : eqdec X).

  Fixpoint list_assoc x l : option Y :=
    match l with
      | nil None
      | (y,a)::l if eq_X_dec x y then Some a else list_assoc x l
    end.

  Fact list_assoc_eq x y l x' : x = x' list_assoc x' ((x,y)::l) = Some y.
  Proof.
    intros []; simpl.
    destruct (eq_X_dec x x) as [ | [] ]; auto.
  Qed.


  Fact list_assoc_neq x y l x' : x x' list_assoc x' ((x,y)::l) = list_assoc x' l.
  Proof.
    intros H; simpl.
    destruct (eq_X_dec x' x) as [ | ]; auto.
    destruct H; auto.
  Qed.


  Fact list_assoc_In x l :
    match list_assoc x l with
      | None In x (map fst l)
      | Some y In (x,y) l
    end.
  Proof.
    induction l as [ | (x',y) l IHl ]; simpl; auto.
    destruct (eq_X_dec x x'); subst; auto.
    destruct (list_assoc x l); auto.
    intros [ ? | ]; subst; tauto.
  Qed.


  Fact In_list_assoc x l : In x (map fst l) { y | list_assoc x l = Some y In (x,y) l }.
  Proof.
    intros H.
    generalize (list_assoc_In x l).
    destruct (list_assoc x l) as [ y | ].
    exists y; auto.
    tauto.
  Qed.


  Fact not_In_list_assoc x l : In x (map fst l) list_assoc x l = None.
  Proof.
    intros H.
    generalize (list_assoc_In x l).
    destruct (list_assoc x l) as [ y | ]; auto.
    intros ; contradict H.
    apply in_map_iff.
    exists (x,y); simpl; auto.
  Qed.


  Fact list_assoc_app x ll mm : list_assoc x (llmm)
                              = match list_assoc x ll with
                                  | None list_assoc x mm
                                  | Some y Some y
                                end.
  Proof.
    induction ll as [ | (x',?) ]; simpl; auto.
    destruct (eq_X_dec x x'); auto.
  Qed.


End list_assoc.

Section list_first_dec.

  Variable (X : Type) (P : X Prop) (Pdec : x, { P x } + { P x }).

  Theorem list_choose_dec ll : { l : _ & { x : _ & { r | ll = lx::r P x y, In y l P y } } }
                             + { x, In x ll P x }.
  Proof.
    induction ll as [ | a ll IH ];
      [ | destruct (Pdec a) as [ Ha | Ha ]; [ | destruct IH as [ (l & x & r & & & ) | H ]] ].
    * right; intros _ [].
    * left; exists nil, a, ll; repeat split; auto.
    * left; exists (a::l), x, r; repeat split; subst; auto.
      intros ? [ | ]; subst; auto.
    * right; intros ? [ | ]; subst; auto.
  Qed.


  Theorem list_first_dec a ll : P a In a ll { l : _ & { x : _ & { r | ll = lx::r P x y, In y l P y } } }.
  Proof.
    intros .
    destruct (list_choose_dec ll) as [ H | H ]; trivial.
    destruct (H _ ).
  Qed.


End list_first_dec.

Section list_dec.

  Variable (X : Type) (P Q : X Prop) (H : x, { P x } + { Q x }).

  Theorem list_dec l : { x | In x l P x } + { x, In x l Q x }.
  Proof.
    induction l as [ | x l IHl ].
    + right; intros _ [].
    + destruct (H x) as [ Hx | Hx ].
      1: { left; exists x; simpl; auto. }
      destruct IHl as [ (y & & ) | ].
      * left; exists y; split; auto; right; auto.
      * right; intros ? [ | ? ]; auto.
  Qed.


End list_dec.

Section map.

  Variable (X Y : Type) (f : X Y).

  Fact map_cons_inv ll y m : map f ll = y::m { x : _ & { l | ll = x::l f x = y map f l = m } }.
  Proof.
    destruct ll as [ | x l ]; try discriminate; simpl.
    intros H; inversion H; subst; exists x, l; auto.
  Qed.


  Fact map_app_inv ll m n : map f ll = mn { l : _ & { r | ll = lr m = map f l n = map f r } }.
  Proof.
    revert m n; induction ll as [ | x ll IH ]; intros m n H.
    * destruct m; destruct n; try discriminate; exists nil, nil; auto.
    * destruct m as [ | y m ]; simpl in H.
      + exists nil, (x::ll); auto.
      + inversion H; subst y.
        destruct IH with (1 := ) as (l & r & & & ); subst.
        exists (x::l), r; auto.
  Qed.


  Fact map_middle_inv ll m y n : map f ll = my::n { l : _ & { x : _ & { r | ll = lx::r map f l = m f x = y map f r = n } } }.
  Proof.
    intros H.
    destruct map_app_inv with (1 := H) as (l & r & & & ).
    symmetry in .
    destruct map_cons_inv with (1 := ) as (x & r' & & & ); subst.
    exists l, x, r'; auto.
  Qed.


  Fact map_duplicate_inv ll l' m' r' :
            map f ll = l'::m'::r'
        { l : _ &
          { : _ &
          { m : _ &
          { : _ &
          { r | l' = map f l = f
              m' = map f m = f
              r' = map f r ll = l::m::r } } } } }.
  Proof.
    intros .
    apply map_middle_inv in .
    destruct as (l & & k & & & & ).
    apply map_middle_inv in .
    destruct as (m & & r & & & & ).
    now exists l, , m, , r.
  Qed.


End map.

Fact Forall2_mono X Y (R S : X Y Prop) :
         ( x y, R x y S x y) l m, R l m S l m.
Proof.
  induction 2; constructor; auto.
Qed.


Fact Forall2_nil_inv_l X Y R m : @ X Y R nil m m = nil.
Proof.
  inversion_clear 1; reflexivity.
Qed.


Fact Forall2_nil_inv_r X Y R m : @ X Y R m nil m = nil.
Proof.
  inversion_clear 1; reflexivity.
Qed.


Fact Forall2_cons_inv X Y R x l y m : @ X Y R (x::l) (y::m) R x y R l m.
Proof.
  split.
  inversion_clear 1; auto.
  intros []; constructor; auto.
Qed.


Fact Forall2_app_inv_l X Y R m :
    @ X Y R () m { : _ & { | R R m = } }.
Proof.
  revert m;
  induction as [ | x IH ]; simpl; intros m H.
  exists nil, m; repeat split; auto.
  destruct m as [ | y m ].
  apply Forall2_nil_inv_r in H; discriminate H.
  apply Forall2_cons_inv in H; destruct H as [ ].
  apply IH in .
  destruct as ( & & & & ); subst m.
  exists (y::), ; repeat split; auto.
Qed.


Fact Forall2_app_inv_r X Y R l :
    @ X Y R l () { : _ & { | R R l = } }.
Proof.
  revert l;
  induction as [ | y IH ]; simpl; intros l H.
  exists nil, l; repeat split; auto.
  destruct l as [ | x l ].
  apply Forall2_nil_inv_l in H; discriminate H.
  apply Forall2_cons_inv in H; destruct H as [ ].
  apply IH in .
  destruct as ( & & & & ); subst l.
  exists (x::), ; repeat split; auto.
Qed.


Fact Forall2_cons_inv_l X Y R a ll mm :
      @ X Y R (a::ll) mm
    { b : _ & { mm' | R a b mm = b::mm' R ll mm' } }.
Proof.
  intros H.
  apply Forall2_app_inv_l with ( := a::nil) ( := ll) in H.
  destruct H as (l & mm' & & & ).
  destruct l as [ | y l ].
  exfalso; inversion .
  apply Forall2_cons_inv in .
  destruct as [ ].
  apply Forall2_nil_inv_l in ; subst l.
  exists y, mm'; auto.
Qed.


Fact Forall2_cons_inv_r X Y R b ll mm :
      @ X Y R ll (b::mm)
    { a : _ & { ll' | R a b ll = a::ll' R ll' mm } }.
Proof.
  intros H.
  apply Forall2_app_inv_r with ( := b::nil) ( := mm) in H.
  destruct H as (l & ll' & & & ).
  destruct l as [ | x l ].
  exfalso; inversion .
  apply Forall2_cons_inv in .
  destruct as [ ].
  apply Forall2_nil_inv_r in ; subst l.
  exists x, ll'; auto.
Qed.


Fact Forall2_map_left X Y Z (R : Y X Prop) (f : Z Y) ll mm : R (map f ll) mm ( x y R (f x) y) ll mm.
Proof.
  split.
  revert mm.
  induction ll; intros [ | y mm ] H; simpl in H; auto; try (inversion H; fail).
  apply Forall2_cons_inv in H; constructor.
  tauto.
  apply IHll; tauto.
  induction 1; constructor; auto.
Qed.


Fact Forall2_map_right X Y Z (R : Y X Prop) (f : Z X) mm ll : R mm (map f ll) ( y x R y (f x)) mm ll.
Proof.
  split.
  revert mm.
  induction ll; intros [ | y mm ] H; simpl in H; auto; try (inversion H; fail).
  apply Forall2_cons_inv in H; constructor.
  tauto.
  apply IHll; tauto.
  induction 1; constructor; auto.
Qed.


Fact Forall2_map_both X Y X' Y' (R : X Y Prop) (f : X' X) (g : Y' Y) ll mm : R (map f ll) (map g mm) ( x y R (f x) (g y)) ll mm.
Proof.
  rewrite Forall2_map_left, Forall2_map_right; split; auto.
Qed.


Fact Forall2_Forall X (R : X X Prop) ll : R ll ll Forall ( x R x x) ll.
Proof.
  split.
  induction ll as [ | x ll ]; inversion_clear 1; auto.
  induction 1; auto.
Qed.


Fact Forall_app X (P : X Prop) ll mm : Forall P (llmm) Forall P ll Forall P mm.
Proof.
  repeat rewrite Forall_forall.
  split.
  firstorder.
  intros ( & ) x Hx.
  apply in_app_or in Hx; firstorder.
Qed.


Fact Forall_cons_inv X (P : X Prop) x ll : Forall P (x::ll) P x Forall P ll.
Proof.
  split.
  + inversion 1; auto.
  + constructor; tauto.
Qed.


Fact Forall_rev X (P : X Prop) ll : Forall P ll Forall P (rev ll).
Proof.
  induction 1 as [ | x ll Hll IH ].
  constructor.
  simpl.
  apply Forall_app; split; auto.
Qed.


Fact Forall_map X Y (f : X Y) (P : Y Prop) ll : Forall P (map f ll) Forall ( x P (f x)) ll.
Proof.
  split.
  + induction ll; simpl; try rewrite Forall_cons_inv; constructor; tauto.
  + induction 1; simpl; constructor; auto.
Qed.


Fact Forall_forall_map X (f : X) n l (P : X Prop) :
           l = map f (list_an 0 n) ( i, i < n P (f i)) Forall P l.
Proof.
  intros Hl; rewrite Forall_forall.
  split.
  + intros H x; rewrite Hl, in_map_iff.
    intros (y & ? & ).
    apply list_an_spec in ; subst; apply H; omega.
  + intros H x Hx; apply H; rewrite Hl, in_map_iff.
    exists x; split; auto; apply list_an_spec; omega.
Qed.


Fact Forall_impl X (P Q : X Prop) ll : ( x, In x ll P x Q x) Forall P ll Forall Q ll.
Proof.
  intros H; induction 1 as [ | x ll Hx Hll IH ]; constructor.
  + apply H; simpl; auto.
  + apply IH; intros ? ?; apply H; simpl; auto.
Qed.


Fact Forall_filter X (P : X Prop) (f : X bool) ll : Forall P ll Forall P (filter f ll).
Proof. induction 1; simpl; auto; destruct (f x); auto. Qed.

Section list_discrim.

  Variable (X : Type) (P Q : X Prop) (PQdec : x, { P x } + { Q x}).

  Definition list_discrim l : { lP : _ & { lQ | l p lPlQ Forall P lP Forall Q lQ } }.
  Proof.
    induction l as [ | x l (lP & lQ & & & ) ].
    + exists nil, nil; simpl; auto.
    + destruct (PQdec x) as [ H | H ].
      * exists (x::lP), lQ; repeat split; auto; constructor; auto.
      * exists lP, (x::lQ); repeat split; auto.
        apply Permutation_cons_app; auto.
  Qed.


End list_discrim.