Require Import Omega.
Require Import Vbase Relations List Permutation Sorting MMergesort.
Require Import ClassicalDescription.

Set Implicit Arguments.

Definition appA := app_ass.

Lemma in_cons_iff A (a b : A) l : In b (a :: l) ↔ a = b ∨ In b l.

Lemma In_split2 :
  ∀ A (x: A) l (IN: In x l),
  ∃ l1 l2, l = l1 ++ x :: l2 ∧ ¬ In x l1.

Lemma map_eq_app_inv A B (f : A → B) l l1 l2 :
  map f l = l1 ++ l2 →
  ∃ l1' l2', l = l1' ++ l2' ∧ map f l1' = l1 ∧ map f l2' = l2.

Lemma in_filter_iff A l f (x : A) : In x (filter f l) ↔ In x l ∧ f x.

Lemma filter_app A f (l l' : list A) :
  filter f (l ++ l') = filter f l ++ filter f l'.

Fixpoint flatten A (l: list (list A)) :=
  match l with
    | nil ⇒ nil
    | x :: l' ⇒ x ++ flatten l'
  end.

Lemma in_flatten_iff A (x: A) ll :
  In x (flatten ll) ↔ ∃ l, In l ll ∧ In x l.

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

Fixpoint undup A (l: list A) :=
  match l with nil ⇒ nil
    | x :: l ⇒
      if excluded_middle_informative (In x l) then undup l else x :: undup l
  end.

Lemma nodup_one A (x: A) : NoDup (x :: nil).

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

Lemma nodup_append_commut:
  ∀ (A: Type) (a b: list A),
  NoDup (a ++ b) → NoDup (b ++ a).

Lemma nodup_cons A (x: A) l:
  NoDup (x :: l) ↔ ¬ In x l ∧ NoDup l.

Lemma nodup_app:
  ∀ (A: Type) (l1 l2: list A),
  NoDup (l1 ++ l2) ↔
  NoDup l1 ∧ NoDup l2 ∧ disjoint l1 l2.

Lemma nodup_append:
  ∀ (A: Type) (l1 l2: list A),
  NoDup l1 → NoDup l2 → disjoint l1 l2 →
  NoDup (l1 ++ l2).

Lemma nodup_append_right:
  ∀ (A: Type) (l1 l2: list A),
  NoDup (l1 ++ l2) → NoDup l2.

Lemma nodup_append_left:
  ∀ (A: Type) (l1 l2: list A),
  NoDup (l1 ++ l2) → NoDup l1.

Lemma nodup_filter A (l: list A) (ND: NoDup l) f : NoDup (filter f l).

Hint Resolve nodup_filter.

Lemma Permutation_nodup A ( l l' : list A) :
  Permutation l l' → NoDup l → NoDup l'.

Lemma nodup_eq_one A (x : A) l :
   NoDup l → In x l → (∀ y (IN: In y l), y = x) → l = x :: nil.

Lemma nodup_consD A (x : A) l : NoDup (x :: l) → NoDup l.

Lemma nodup_mapD A B (f : A→ B) l : NoDup (map f l) → NoDup l.

Lemma In_NoDup_Permutation A (a : A) l (IN: In a l) (ND : NoDup l) :
  ∃ l', Permutation l (a :: l') ∧ ¬ In a l'.

Lemma in_undup_iff A (x : A) (l : list A) : In x (undup l) ↔ In x l.

Lemma nodup_undup A (l : list A) : NoDup (undup l).

Hint Resolve nodup_undup.

Lemma undup_nodup A (l : list A) : NoDup l → undup l = l.

Lemma Sorted_undup A p (l : list A) :
  StronglySorted p l → StronglySorted p (undup l).

Lemma undup_nonnil A (l : list A) : l ≠ nil → undup l ≠ nil.

Lemma Permutation_undup A (l l' : list A) :
  Permutation l l' → Permutation (undup l) (undup l').

Definition upd A B (f : A → B) a b x :=
  if excluded_middle_informative (x = a) then b else f x.

Lemma upds A B (f: A → B) a b : upd f a b a = b.

Lemma updo A B (f: A → B) a b c (NEQ: c ≠ a) : upd f a b c = f c.

Ltac rupd := repeat first [rewrite upds | rewrite updo ; try done].

Lemma updss A B (f : A → B) l x y : upd (upd f l x) l y = upd f l y.

Lemma updC A l l' (NEQ: l ≠ l') B (f : A → B) x y :
  upd (upd f l x) l' y = upd (upd f l' y) l x.

Lemma updI A B (f : A → B) a : upd f a (f a) = f.

Lemma map_upd_irr A (a: A) l (NIN: ¬ In a l) B f (b : B) :
  map (upd f a b) l = map f l.

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

Lemma mupds (A: eqType) B (f: A → B) x y : mupd f x y x = y.

Lemma mupdo (A: eqType) B (f: A → B) x y z : x ≠ z → mupd f x y z = f z.

Lemma sorted_perm_eq : ∀ A (cmp: A → A → Prop)
  (TRANS: transitive _ cmp)
  (ANTIS: antisymmetric _ cmp)
  l l' (P: Permutation l l')
  (S : StronglySorted cmp l) (S' : StronglySorted cmp l'), l = l'.

Lemma perm_sort_eq A (l l': list A) (P: Permutation l l') cmp
    (TOTAL: ∀ x y, In x l → In y l → cmp x y = true ∨ cmp y x = true)
    (TRANS: transitive _ cmp)
    (ANTIS: antisymmetric _ cmp) :
  sort cmp l = sort cmp l'.

Lemma In_sort A (x: A) cmp l : In x (sort cmp l) ↔ In x l.

Lemma NoDup_sort A cmp (l : list A) : NoDup (sort cmp l) ↔ NoDup l.

Lemma NoDup_sort1 A cmp (l : list A) : NoDup l → NoDup (sort cmp l).

Hint Resolve NoDup_sort1.

Lemma Sorted_total :
  ∀ A cmp (R: reflexive _ cmp) (l: list A), StronglySorted cmp l →
    ∀ x y, In x l → In y l →
      cmp x y ∨ cmp y x.

Lemma Sorted_app_end_inv A (cmp : A → A → Prop) l x :
  StronglySorted cmp (l ++ x :: nil) →
  ∀ y, In y l → cmp y x.

Fixpoint dprod A B al (f : A → list B) :=
  match al with
    | nil ⇒ nil
    | a :: al ⇒ map (fun b ⇒ (a, b)) (f a) ++ dprod al f
  end.

Lemma in_dprod_iff A B x al (f : A → list B) :
  In x (dprod al f) ↔ In (fst x) al ∧ In (snd x) (f (fst x)).

Lemma perm_from_subset :
  ∀ A (l : list A) l',
    NoDup l' →
    (∀ x, In x l' → In x l) →
    ∃ l'', Permutation l (l' ++ l'').

Lemma seq_split_gen :
  ∀ l n a,
  n ≤ a < n + l →
  seq n l = seq n (a - n) ++ a :: seq (S a) (l + n - a - 1).

Lemma seq_split0 :
  ∀ l a,
  a < l →
  seq 0 l = seq 0 a ++ a :: seq (S a) (l - a - 1).

Lemma list_prod_app A (l l' : list A) B (m : list B) :
  list_prod (l ++ l') m = list_prod l m ++ list_prod l' m.

Lemma list_prod_nil_r A (l : list A) B :
  list_prod l (@nil B) = nil.

Lemma list_prod_cons_r A (l : list A) B a (m : list B) :
  Permutation (list_prod l (a :: m)) (map (fun x ⇒ (x,a)) l ++ list_prod l m).

Lemma list_prod_app_r A (l : list A) B (m m' : list B) :
  Permutation (list_prod l (m ++ m')) (list_prod l m ++ list_prod l m').

Lemma in_seq_iff a n l : In a (seq n l) ↔ n ≤ a < n + l.

Lemma in_seq0_iff x a : In x (seq 0 a) ↔ x < a.

Lemma nodup_seq n l : NoDup (seq n l).

Lemma seq_split :
  ∀ l a,
  a < l →
  ∃ l', Permutation (seq 0 l) (a :: l') ∧ ¬ In a l'.

Lemma Permutation_listprod_r A (l : list A) B (m m' : list B) :
  Permutation m m' →
  Permutation (list_prod l m) (list_prod l m').

Ltac in_simp :=
  try match goal with |- ¬ _ ⇒ intro end;
  repeat first [
    rewrite in_flatten_iff in *; desc; clarify |
    rewrite in_map_iff in *; desc; clarify |
    rewrite in_seq0_iff in *; desc; clarify ].

Global Opaque seq.