Require Import List Vbase Varith Vlistbase Vlist.
Require Import Classical ClassicalDescription.
Require Import Permutation Relations.
Require Import Omega.
Require Import Wf Wf_nat.

Set Implicit Arguments.

Notation sval := (@proj1_sig _ _).
Notation "@ 'sval'" := (@proj1_sig) (at level 10, format "@ 'sval'").

Definition mydec (P: Prop) :=
  if (excluded_middle_informative P) then true else false.

Lemma forall_and_dist T (P Q: T → Prop):
  (∀ x, P x ∧ Q x) ↔ (∀ x, P x) ∧ (∀ x, Q x).
Proof.
  repeat split; ins; try specialize (H x); desf.
Qed.

Lemma list_destruct_end: ∀ A (l: list A), l = nil ∨ ∃ l' a, l = l' ++ a :: nil.
  induction l; desf; eauto.
  by right; eexists nil, _; rewrite app_nil_l.
  eby right; eexists _, _; rewrite app_comm_cons.
Qed.

Ltac des_list_tail l l' a :=
  let F := fresh in destruct (list_destruct_end l) as [ | [l' F]]; [ | destruct F as [a]]; subst l.

Ltac find_in_list := (by repeat progress (rewrite ?In_app; ins); eauto 10).

Lemma map_is_nil: ∀ T1 T2 (f: T1 → T2) l, map f l = nil → l = nil.
Proof.
  by destruct l.
Qed.

Lemma not_or_and_iff : ∀ P Q, ¬ (P ∨ Q) ↔ ¬ P ∧ ¬ Q.
Proof.
  split; ins.
    by apply not_or_and.
  intro; desf.
Qed.

Lemma true_imp_b: ∀ (b : bool), (true → b) ↔ b = true.
Proof.
   by split; ins; rewrite H.
Qed.

Definition disjoint A (l1 l2 : list A) :=
  ∀ a (IN1: In a l1) (IN2: In a l2), False.

Lemma nodup_one A (x: A) : NoDup (x :: nil).
Proof. vauto. Qed.
Hint Resolve NoDup_nil nodup_one.

Lemma nodup_map:
  ∀ (A B: Type) (f: A → B) (l: list A),
  NoDup l →
  (∀ x y, In x l → In y l → x ≠ y → f x ≠ f y) →
  NoDup (map f l).
Proof.
  induction 1; ins; vauto.
  constructor; eauto.
  intro; rewrite In_map in *; desf.
  edestruct H1; try eapply H2; eauto.
  intro; desf.
Qed.

Lemma nodup_append_commut:
  ∀ (A: Type) (a b: list A),
  NoDup (a ++ b) → NoDup (b ++ a).
Proof.
  intro A.
  assert (∀ (x: A) (b: list A) (a: list A),
           NoDup (a ++ b) → ~(In x a) → ~(In x b) →
           NoDup (a ++ x :: b)).
    induction a; simpl; intros.
    constructor; auto.
    inversion H. constructor. red; intro.
    elim (in_app_or _ _ _ H6); intro.
    elim H4. apply in_or_app. tauto.
    elim H7; intro. subst a. elim H0. left. auto.
    elim H4. apply in_or_app. tauto.
    auto.
  induction a; simpl; intros.
  rewrite <- app_nil_end. auto.
  inversion H0. apply H. auto.
  red; intro; elim H3. apply in_or_app. tauto.
  red; intro; elim H3. apply in_or_app. tauto.
Qed.

Lemma nodup_cons A (x: A) l:
  NoDup (x :: l) ↔ ¬ In x l ∧ NoDup l.
Proof. split; inversion 1; vauto. Qed.

Lemma NoDup_two A: ∀ (x y: A), NoDup (x :: y :: nil) ↔ x ≠ y.
Proof.
  ins; rewrite nodup_cons; firstorder.
Qed.

Lemma nodup_app:
  ∀ (A: Type) (l1 l2: list A),
  NoDup (l1 ++ l2) ↔
  NoDup l1 ∧ NoDup l2 ∧ disjoint l1 l2.
Proof.
  induction l1; ins.
    by split; ins; desf; vauto.
  rewrite !nodup_cons, IHl1, In_app; unfold disjoint.
  ins; intuition (subst; eauto).
Qed.

Lemma nodup_append:
  ∀ (A: Type) (l1 l2: list A),
  NoDup l1 → NoDup l2 → disjoint l1 l2 →
  NoDup (l1 ++ l2).
Proof.
  generalize nodup_app; firstorder.
Qed.

Lemma nodup_append_right:
  ∀ (A: Type) (l1 l2: list A),
  NoDup (l1 ++ l2) → NoDup l2.
Proof.
  generalize nodup_app; firstorder.
Qed.

Lemma nodup_append_left:
  ∀ (A: Type) (l1 l2: list A),
  NoDup (l1 ++ l2) → NoDup l1.
Proof.
  generalize nodup_app; firstorder.
Qed.

Lemma not_NoDup_split T:
  ∀ (l: list T) (D: ¬ NoDup l),
  ∃ a l1 l2 l3, l = l1 ++ a :: l2 ++ a :: l3.
Proof.
  induction l; ins.
  destruct (classic (NoDup l)).
  × assert (IN: In a l) by (apply NNPP; intro; destruct D; vauto).
    apply In_split in IN; desf.
    by ∃ a, nil, l1, l2.
  × exploit IHl; ins; desf.
    by ∃ a0, (a :: l1), l2, l3.
Qed.

Lemma too_long_implies_not_NoDup T:
  ∀ (l U: list T) (SUBSET: ∀ x (IN: In x l), In x U) (LEN: length l > length U), ¬ NoDup l.
Proof.
  induction l; ins.
  intro ND.
  assert (NIN := NoDup_remove_2 nil _ _ ND); ins.
  apply (NoDup_remove_1 nil) in ND; ins.
  exploit (SUBSET a); eauto.
  intro IN; apply In_split in IN; desf.
  rewrite length_app in LEN; ins.
  rewrite <- plus_n_Sm, ltSS, <- length_app in LEN.
  eapply IHl; try eassumption; ins.
  exploit (SUBSET x); eauto.
  rewrite !In_app; intro I; ins; desf; eauto.
Qed.


Definition mupd (A: eqType) B (h : A → B) y z :=
  fun x ⇒ if x == y then z else h x.
Arguments mupd [A B] h y z x.

Lemma mupds (A: eqType) B (f: A → B) x y : mupd f x y x = y.
Proof. by unfold mupd; desf; desf. Qed.

Lemma mupdo (A: eqType) B (f: A → B) x y z : x ≠ z → mupd f x y z = f z.
Proof. by unfold mupd; desf; desf. Qed.


Lemma In_perm A l l' (P: perm_eq (T:=A) l l') x : In x l ↔ In x l'.
Proof.
  by split; ins; apply/inP; instantiate;
     [rewrite <- (perm_eq_mem P)|rewrite (perm_eq_mem P)]; apply/inP.
Qed.

Lemma In_implies_perm A (x : A) l (IN: In x l) :
  ∃ l', Permutation l (x :: l').
Proof.
  induction l; ins; desf; eauto.
  destruct IHl; eauto using Permutation.
Qed.

Lemma nodup_perm A l l' (P: perm_eq (T:=A) l l') : NoDup l ↔ NoDup l'.
Proof.
  by split; ins; apply/uniqP; instantiate;
     [rewrite <- (perm_eq_uniq P)|rewrite (perm_eq_uniq P)]; apply/uniqP.
Qed.

Lemma Permutation_filter_split T:
  ∀ (l: list T) (f: T → bool), Permutation l ((filter f l) ++ (filter (fun x ⇒ negb (f x)) l)).
Proof.
  ins; induction l; ins; desf; try done; ins.
  by apply perm_skip.
  by apply Permutation_cons_app.
Qed.

Lemma In_mem_eq (A: eqType) (l l': list A) (P: l =i l') x : In x l ↔ In x l'.
Proof.
  by split; ins; apply/inP; instantiate; [rewrite <- P | rewrite P]; apply/inP.
Qed.

Lemma NoDup_filter A (l: list A) (ND: NoDup l) f : NoDup (filter f l).
Proof.
  induction l; ins; inv ND; desf; eauto using NoDup.
  econstructor; eauto; rewrite In_filter; tauto.
Qed.

Hint Resolve NoDup_filter.

Lemma NoDup_eq_one A (x : A) l :
   NoDup l → In x l → (∀ y (IN: In y l), y = x) → l = x :: nil.
Proof.
  destruct l; ins; f_equal; eauto.
  inv H; desf; clear H H5; induction l; ins; desf; case H4; eauto using eq_sym.
  rewrite IHl in H0; ins; desf; eauto.
Qed.

Lemma map_perm :
  ∀ A B (f: A → B) l l', Permutation l l' → Permutation (map f l) (map f l').
Proof.
  induction 1; eauto using Permutation.
Qed.

Lemma perm_from_subset :
  ∀ A (l : list A) l',
    NoDup l' →
    (∀ x, In x l' → In x l) →
    ∃ l'', Permutation l (l' ++ l'').
Proof.
  induction l; ins; vauto.
    by destruct l'; ins; vauto; exfalso; eauto.
  destruct (classic (In a l')).

    eapply In_split in H1; desf; rewrite ?nodup_app, ?nodup_cons in *; desf.
    destruct (IHl (l1 ++ l2)); ins.
      by rewrite ?nodup_app, ?nodup_cons in *; desf; repeat split; ins; red; eauto using In_cons.
      by specialize (H0 x); rewrite In_app in *; ins; desf;
         destruct (classic (a = x)); subst; try tauto; exfalso; eauto using In_eq.
    eexists; rewrite appA in *; ins.
    by eapply Permutation_trans, Permutation_middle; eauto.

  destruct (IHl l'); eauto; ins.
    by destruct (H0 x); auto; ins; subst.
  by eexists (a :: _); eapply Permutation_trans, Permutation_middle; eauto.
Qed.

Lemma Permutation_NoDup A ( l l' : list A) :
  Permutation l l' → NoDup l → NoDup l'.
Proof.
  induction 1; eauto; rewrite !nodup_cons in *; ins; desf; intuition.
  eby symmetry in H; eapply H0; eapply Permutation_in.
Qed.

Lemma NoDup_mapD A B (f : A→ B) l :
  NoDup (map f l) → NoDup l.
Proof.
  induction l; ins; rewrite !nodup_cons, In_map in *; desf; eauto 8.
Qed.

Lemma NoDup_neq: ∀ {A} a b (l: list A), NoDup (a :: b :: l) → a ≠ b.
Proof.
  ins; intro; subst.
  rewrite <- app_nil_l in H; apply NoDup_remove_2 in H.
  by destruct H; rewrite app_nil_l; left.
Qed.

Lemma olast_inv A l x :
  olast (T:=A) l = Some x → ∃ prefix, l = prefix ++ x :: nil.
Proof.
  destruct l; ins; desf; induction[a] l; ins; [by ∃ nil|].
  by specialize (IHl a); desf; ∃ (a0 :: prefix); ins; f_equal.
Qed.

Lemma In_flatten A (x:A) l :
  In x (flatten l) ↔ ∃ y, In x y ∧ In y l.
Proof.
  induction l; ins. by split; ins; desf.
  rewrite flatten_cons, In_app, IHl; clear; split; ins; desf; eauto.
Qed.

Lemma list_not_nil: ∀ {A} (l: list A), l ≠ nil ↔ ∃ a, In a l.
Proof.
  split.
  by induction l as [ | head l']; ins; eexists; eauto.
  by ins; intro; desf.
Qed.

Lemma list_zero_one: ∀ {A} a (l: list A) (ND: NoDup l),
                     (∀ x (IN: In x l), x = a) ↔ l = nil ∨ l = a :: nil.
Proof.
  split; ins.
  × destruct l as [ | a' l']; [by left | right].
    f_equal.
    by apply H.
    destruct l' as [ | b l'']; [done | exfalso].
    exploit (H a'); exploit (H b); ins; try tauto.
    apply NoDup_neq in ND; congruence.
  × by desf; red in IN; desf.
Qed.

Lemma neq_contra: ∀ (x: nat), ¬ (x != x).
Proof.
  ins; intro.
  rewrite eqnn in H.
  unfold is_true in H.
  rewrite Bool.negb_true_iff in H.
  congruence.
Qed.

Lemma subset_perm: ∀ {A} (X Y: list A) (NDX: NoDup X) (NDY: NoDup Y)
                          (SUBSET: ∀ a, In a Y → In a X),
                   ∃ Y', Permutation X (Y ++ Y').
Proof.
  induction X as [ | x X'].
  × ins; ∃ nil.
    assert (YN: Y = nil).
    {
      apply NNPP; intro CONTRA.
      apply list_not_nil in CONTRA; desf.
      eby eapply SUBSET.
    }
    by subst; simpl; apply perm_nil.
  × ins.
    destruct (classic (In x Y)) as [IN | NotIN].
    + apply In_implies_perm in IN as [Y' PERM]; desf.
      assert (SUBSET': ∀ a, In a Y' → In a X').
      {
        ins.
        destruct (SUBSET a); try done.
        + symmetry in PERM; eapply Permutation_in; eauto.
          by right.
        + subst; exfalso.
          apply (Permutation_NoDup PERM ) in NDY.
          by rewrite nodup_cons in NDY; desf.
      }
      rewrite nodup_cons in NDX; desf.
      apply (Permutation_NoDup PERM ) in NDY.
      rewrite nodup_cons in NDY; desf.
      specialize (IHX' _ NDX0 NDY0 SUBSET'); desf.
      ∃ Y'0.
      eapply (Permutation_cons eq_refl) in IHX'.
      assert (P := Permutation_app PERM (Permutation_refl Y'0)); simpls.
      by symmetry in P; eapply Permutation_trans; eauto.
    + assert (SUBSET': ∀ a : A, In a Y → In a X') by (ins; specialize (SUBSET a H); desf).
      rewrite nodup_cons in NDX; desf.
      specialize (IHX' _ NDX0 NDY SUBSET'); desf.
      apply Permutation_cons_app with (a := x) in IHX'.
      by eexists; eauto.
Qed.

Lemma first_exists:
  ∀ A (l: list A) phi (EX: ∃ a, In a l ∧ phi a),
  ∃ a' l1 l2, l = l1 ++ a' :: l2 ∧ phi a' ∧ ∀ b (IN: In b l1), ¬ phi b.
Proof.
  intro.
  induction l using (well_founded_induction (well_founded_ltof _ (@length A))).
  ins; desf.
  apply In_split in EX; desf.
  destruct (classic (∃ a1, In a1 l1 ∧ phi a1)).
  × desf.
    exploit (H l1); eauto.
      by red; rewrite length_app; ins; omega.
    ins; desf.
    ∃ a', l0, (l3 ++ a :: l2); split; eauto.
    by rewrite <- app_assoc, app_comm_cons.
  × eexists _, _, _; repeat split; eauto.
Qed.

Lemma last_exists:
  ∀ A (l: list A) phi (EX: ∃ a, In a l ∧ phi a),
  ∃ a' l1 l2, l = l1 ++ a' :: l2 ∧ phi a' ∧ ∀ b (IN: In b l2), ¬ phi b.
Proof.
  intro.
  induction l using (well_founded_induction (well_founded_ltof _ (@length A))).
  ins; desf.
  apply In_split in EX; desf.
  destruct (classic (∃ a2, In a2 l2 ∧ phi a2)).
  × desf.
    exploit (H l2); eauto.
      by red; rewrite length_app; ins; omega.
    ins; desf.
    ∃ a', (l1 ++ a :: l0), l3; split; eauto.
    by rewrite <- app_assoc, app_comm_cons.
  × eexists _, _, _; repeat split; eauto.
Qed.

Lemma map_eq A B:
  ∀ (f g: A → B) (l: list A) (fEQ: ∀ x (IN: In x l), f x = g x), map f l = map g l.
Proof.
  induction l; ins.
  f_equal.
    by apply fEQ; eauto.
  apply IHl; ins.
  by apply fEQ; eauto.
Qed.

Lemma map_eq_cons T1 T2 (l : list T1) (l' : list T2) x f :
  map f l = x :: l' → ∃ a l'', l = a :: l'' ∧ f a = x ∧ map f l'' = l'.
Proof.
  destruct l; ins.
  injection H; ins; desf; repeat eexists.
Qed.

Lemma map_eq_app T1 T2 (l : list T1) (l1 l2 : list T2) f :
  map f l = l1 ++ l2 → ∃ l' l'', l = l' ++ l'' ∧ map f l' = l1 ∧ map f l'' = l2.
Proof.
  revert l l2; induction l1; ins.
    by ∃ nil; repeat eexists.
  apply map_eq_cons in H; desf.
  exploit IHl1; try eassumption; ins; desf.
  eexists _, _; repeat split.
    by rewrite app_comm_cons.
  done.
Qed.

Lemma clos_rt_inclusion A R Q:
  inclusion A R Q → inclusion A (clos_refl_trans A R) (clos_refl_trans A Q).
Proof.
  unfold inclusion; ins.
  induction H0; vauto.
  apply rt_step; eauto.
Qed.

Lemma clos_t_inclusion A R Q:
  inclusion A R Q → inclusion A (clos_trans A R) (clos_trans A Q).
Proof.
  unfold inclusion; ins.
  induction H0; vauto.
  apply t_step; eauto.
Qed.

Fixpoint index_of A (a : A) (l: list A) :=
  match l with
    | nil ⇒ 0
    | x :: l' ⇒ if excluded_middle_informative (x = a) then 0 else 1 + index_of a l'
  end.

Lemma equal_index_of A (a b: A) (l : list A) (Ina: In a l) (INb: In b l):
  index_of a l = index_of b l → a = b.
Proof.
  induction l; ins; desf.
  by apply IHl.
Qed.