(**************************************************************)
(*   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 H1 [ -> | H2 ].
      * apply H1; simpl; auto.
      * apply IHl; auto.
        intros; apply H1; 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 = l++r -> 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 H1.
      * split; auto.
        rewrite <- H1; simpl; rewrite Nat.add_0_r, list_an_length; auto.
      * injection H1; clear H1; intros H1 H0.
        apply IHn in H1; destruct H1; split; f_equal; auto.
        rewrite H1 at 1; f_equal; omega.
  Qed.

  Fact list_an_duplicate_inv a n l x m y r :
        list_an a n = l++x::m++y::r -> a <= x /\ x < y < a+n.
  Proof.
    intros H.
    generalize H; intros H1.
    apply f_equal with (f := @length _) in H1.
    rewrite list_an_length in H1.
    apply list_an_app_inv in H; simpl in H.
    destruct H as (E1 & H); injection H; clear H; intros H E2.
    symmetry in H; apply list_an_app_inv in H; simpl in H.
    destruct H as (E3 & H); injection H; clear H; intros E4 E5.
    do 2 (rewrite app_length in H1; simpl in H1).
    omega.
  Qed.

End list_an.

Hint Rewrite list_an_length : length_db.

Definition list_fun_inv X (l : list X) (x : X) : { f : nat -> X | l = map f (list_an 0 (length l)) }.
Proof.
  induction l as [ | y l IHl ].
  + exists (fun _ => x); auto.
  + destruct IHl as (f & Hf).
    exists (fun 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 nat) : { m | forall 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) := forall 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 H1 H2 l a m b r H3.
    destruct l as [ | u l ].
    inversion H3; subst.
    destruct m as [ | v m ].
    contradict H1; subst; simpl; auto.
    contradict H1; subst; simpl; right; apply in_or_app; right; left; auto.
    inversion H3; subst.
    apply (H2 l _ m _ r); auto.
  Qed.

  Fact list_injective_inv x ll : list_injective (x::ll) -> ~ In x ll /\ list_injective ll.
  Proof.
    split.
    intros H1; apply in_split in H1; destruct H1 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 (HP0 : P nil).
  Hypothesis (HP1 : forall 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 HP0.
    intros; apply HP1.
    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 :
       (forall 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 <> u++v.
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 (fun _ : 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 (fun _ : X => y) ll++mm = map (fun _ => y) ll ++ y::mm.
Proof. induction ll; simpl; f_equal; auto. Qed.

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

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

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

Fact list_app_cons_eq_inv X (l1 l2 r1 r2 : list X) x :
       l1++r1 = l2++x::r2 -> { m | l1++m = l2 /\ r1 = m++x::r2 }
                           + { m | l2++x::m = l1 /\ r2 = m++r1 }.
Proof.
  intros H.
  apply list_app_eq_inv in H.
  destruct H as [ H | (m & H1 & H2) ]; auto.
  destruct m as [ | y m ].
  left; exists nil; simpl in *; split; auto.
  revert H1; do 2 rewrite <- app_nil_end; auto.
  inversion H2; subst.
  right; exists m; auto.
Qed.

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

Fact list_app_inj X (l1 l2 r1 r2 : list X) : length l1 = length l2 -> l1++r1 = l2++r2 -> l1 = l2 /\ r1 = r2.
Proof.
  revert l2; induction l1 as [ | x l1 IH ]; intros [ | y l2 ]; try discriminate.
  simpl; auto.
  intros H1 H2; inversion H1; inversion H2.
  apply IH in H4; auto.
  split; f_equal; tauto.
Qed.

Fact list_split_length X (ll : list X) k : k <= length ll -> { l : _ & { r | ll = l++r /\ 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 & H1 & H2).
  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 = l++x::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 l1 (x1 : X) r1 l2 x2 r2 :
       ~ In x1 l2 -> ~ In x2 l1 -> l1++x1::r1 = l2++x2::r2 -> l1 = l2 /\ x1 = x2 /\ r1 = r2.
Proof.
  intros H1 H2 H.
  apply list_app_eq_inv in H.
  destruct H as [ (m & H3 & H4) | (m & H3 & H4) ]; destruct m.
  inversion H4; subst; rewrite <- app_nil_end; auto.
  inversion H4; subst; destruct H1; apply in_or_app; right; left; auto.
  inversion H4; subst; rewrite <- app_nil_end; auto.
  inversion H4; subst; destruct H2; apply in_or_app; right; left; auto.
Qed.

Section flat_map.

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

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

  Fact flat_map_app_inv l r1 y r2 : flat_map f l = r1++y::r2 -> exists l1 m1 x m2 l2, l = l1++x::l2 /\ f x = m1++y::m2
                                                                  /\ r1 = flat_map f l1++m1 /\ r2 = m2++flat_map f l2.
  Proof.
    revert r1 y r2.
    induction l as [ | x l IHl ]; intros r1 y r2 H.
    + destruct r1; discriminate.
    + simpl in H.
      apply list_app_cons_eq_inv in H.
      destruct H as [ (m & Hm1 & Hm2) | (m & Hm1 & Hm2) ].
      - apply IHl in Hm2.
        destruct Hm2 as (l1 & m1 & x' & m2 & l2 & G1 & G2 & G3 & G4); subst.
        exists (x::l1), m1, x', m2, l2; simpl; repeat (split; auto).
        rewrite app_ass; auto.
      - exists nil, r1, x, m, l; auto.
  Qed.

End flat_map.

Fact in_concat_iff X (ll : list (list X)) x : In x (concat ll) <-> exists 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 (fun 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 (fun 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 : (forall x, @In X x l -> Y) -> list Y.
  Proof.
    refine (match l with
      | nil => fun _ => nil
      | x::l => fun 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 (fun z Hz => f z (or_intror Hz))).
  Qed.

  Theorem In_list_in_map_inv l f y : In y (list_in_map l f) -> exists 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) := exists r, ll = l++r.

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 r1 r2 : r1 <p r2 -> l++r1 <p l++r2.
  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 : l++r <p l++rr -> 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 l1 l2 l3 : l1 <p l2 -> l2 <p l3 -> l1 <p l3.
  Proof. intros (m1 & H1) (m2 & H2); subst; exists (m1++m2); solve list eq. Qed.

  Section prefix_rect.

    Variables (P : list X -> list X -> Type)
              (HP0 : forall ll, P nil ll)
              (HP1 : forall 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 HP0.
      destruct H as (r & Hr).
      destruct l; auto; discriminate.

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

  End prefix_rect.

  Fact prefix_app_inv l1 l2 r1 r2 : l1++l2 <p r1++r2 -> { l1 <p r1 } + { r1 <p l1 }.
  Proof.
    revert l2 r1 r2; induction l1 as [ | x l1 IH ].
    left; apply in_prefix_0.
    intros l2 [ | y r1 ] r2.
    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 (l1 l2 m : list X) : l1++l2 <p m -> { m2 | m = l1++m2 /\ l2 <p m2 }.
Proof.
  intros H.
  apply prefix_spec in H.
  destruct H as (r & H).
  exists (l2++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 H1; contradict H.
    apply in_map_iff.
    exists (x,y); simpl; auto.
  Qed.

  Fact list_assoc_app x ll mm : list_assoc x (ll++mm)
                              = 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 : forall x, { P x } + { ~ P x }).

  Theorem list_choose_dec ll : { l : _ & { x : _ & { r | ll = l++x::r /\ P x /\ forall y, In y l -> ~ P y } } }
                             + { forall 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 & H1 & H2 & H3) | 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 = l++x::r /\ P x /\ forall y, In y l -> ~ P y } } }.
  Proof.
    intros H1 H2.
    destruct (list_choose_dec ll) as [ H | H ]; trivial.
    destruct (H _ H2 H1).
  Qed.

End list_first_dec.

Section list_dec.

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

  Theorem list_dec l : { x | In x l /\ P x } + { forall 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 & H1 & H2) | H1 ].
      * 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 = m++n -> { l : _ & { r | ll = l++r /\ 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 := H2) as (l & r & H3 & H4 & H5); subst.
        exists (x::l), r; auto.
  Qed.

  Fact map_middle_inv ll m y n : map f ll = m++y::n -> { l : _ & { x : _ & { r | ll = l++x::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 & H1 & H2 & H3).
    symmetry in H3.
    destruct map_cons_inv with (1 := H3) as (x & r' & H4 & H5 & H6); subst.
    exists l, x, r'; auto.
  Qed.

  Fact map_duplicate_inv ll l' y1 m' y2 r' :
            map f ll = l'++y1::m'++y2::r'
       -> { l : _ &
          { x1 : _ &
          { m : _ &
          { x2 : _ &
          { r | l' = map f l /\ y1 = f x1
             /\ m' = map f m /\ y2 = f x2
             /\ r' = map f r /\ ll = l++x1::m++x2::r } } } } }.
  Proof.
    intros H1.
    apply map_middle_inv in H1.
    destruct H1 as (l & x1 & k & H1 & H3 & H4 & H5).
    apply map_middle_inv in H5.
    destruct H5 as (m & x2 & r & -> & H6 & H7 & H8).
    now exists l, x1, m, x2, r.
  Qed.

End map.

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

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

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

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

Fact Forall2_app_inv_l X Y R l1 l2 m :
    @Forall2 X Y R (l1++l2) m -> { m1 : _ & { m2 | Forall2 R l1 m1 /\ Forall2 R l2 m2 /\ m = m1++m2 } }.
Proof.
  revert l2 m;
  induction l1 as [ | x l1 IH ]; simpl; intros l2 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 [ H1 H2 ].
  apply IH in H2.
  destruct H2 as (m1 & m2 & H2 & H3 & H4); subst m.
  exists (y::m1), m2; repeat split; auto.
Qed.

Fact Forall2_app_inv_r X Y R l m1 m2 :
    @Forall2 X Y R l (m1++m2) -> { l1 : _ & { l2 | Forall2 R l1 m1 /\ Forall2 R l2 m2 /\ l = l1++l2 } }.
Proof.
  revert m2 l;
  induction m1 as [ | y m1 IH ]; simpl; intros m2 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 [ H1 H2 ].
  apply IH in H2.
  destruct H2 as (l1 & l2 & H2 & H3 & H4); subst l.
  exists (x::l1), l2; repeat split; auto.
Qed.

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

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

Fact Forall2_map_left X Y Z (R : Y -> X -> Prop) (f : Z -> Y) ll mm : Forall2 R (map f ll) mm <-> Forall2 (fun 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 : Forall2 R mm (map f ll) <-> Forall2 (fun 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 : Forall2 R (map f ll) (map g mm) <-> Forall2 (fun 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 : Forall2 R ll ll <-> Forall (fun 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 (ll++mm) <-> Forall P ll /\ Forall P mm.
Proof.
  repeat rewrite Forall_forall.
  split.
  firstorder.
  intros (H1 & H2) 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 (fun 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 : nat -> X) n l (P : X -> Prop) :
           l = map f (list_an 0 n) -> (forall 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 & ? & H1).
    apply list_an_spec in H1; 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 : (forall 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 : forall x, { P x } + { Q x}).

  Definition list_discrim l : { lP : _ & { lQ | l ~p lP++lQ /\ Forall P lP /\ Forall Q lQ } }.
  Proof.
    induction l as [ | x l (lP & lQ & H1 & H2 & H3) ].
    + 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.