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

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

End list_an.

Hint Rewrite list_an_length : length_db.

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.

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.

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 flat_map_app X Y (f : X -> list Y) 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 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_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.

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

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