Require Import List Permutation Vbase Classical.
Set Implicit Arguments.

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

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

Definition appA := app_assoc_reverse.

Lemma In_eq : ∀ A (a:A) (l:list A), In a (a :: l).

Lemma In_cons : ∀ A (a b:A) (l:list A), In b l → In b (a :: l).

Lemma In_nil : ∀ A (a:A), ¬ In a nil.

Lemma In_split : ∀ A x (l:list A), In x l → ∃ l1 l2, l = l1++x::l2.

Lemma In_dec :
  ∀ A (D: ∀ x y:A, {x = y} + {x ≠ y}) (a: A) l, {In a l} + {¬ In a l}.

Lemma In_appI1 : ∀ A (x:A) l (IN: In x l) l', In x (l++l').

Lemma In_appI2 : ∀ A (x:A) l' (IN: In x l') l, In x (l++l').

Lemma In_appD : ∀ A (x:A) l l' (IN: In x (l++l')), In x l ∨ In x l'.

Lemma In_app : ∀ A (x:A) l l', In x (l++l') ↔ In x l ∨ In x l'.

Lemma In_rev : ∀ A (x: A) l, In x (rev l) ↔ In x l.

Lemma In_revI : ∀ A (x: A) l (IN: In x l), In x (rev l).

Lemma In_revD : ∀ A (x: A) l (IN: In x (rev l)), In x l.

Lemma In_mapI : ∀ A B (f: A → B) x l (IN: In x l), In (f x) (map f l).

Lemma In_mapD :
  ∀ A B (f: A→B) y l, In y (map f l) → ∃ x, f x = y ∧ In x l.

Lemma In_map :
  ∀ A B (f: A→B) y l, In y (map f l) ↔ ∃ x, f x = y ∧ In x l.

Lemma In_filter :
  ∀ A (x:A) f l, In x (filter f l) ↔ In x l ∧ f x.

Lemma In_filterI :
  ∀ A x l (IN: In x l) (f: A→bool) (F: f x), In x (filter f l).

Lemma In_filterD :
  ∀ A (x:A) f l (D: In x (filter f l)), In x l ∧ f x.

Lemma In_flatten A (x:A) l :
  In x (flatten l) ↔ ∃ y, In x y ∧ In y l.

Hint Resolve In_eq In_cons In_appI1 In_appI2 In_mapI In_revI In_filterI : vlib.

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 NoDup_eq_one A (x : A) l :
   NoDup l → In x l → (∀ y (IN: In y l), y = x) → l = x :: nil.

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

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

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