Require Import List Vbase Varith Vlistbase Vlist.
Require Import Permutation Classical.
Set Implicit Arguments.

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


Lemma forall_and_dist T (P Q: T → Prop):
  (∀ x, P x ∧ Q x) ↔ (∀ x, P x) ∧ (∀ x, Q x).

Lemma list_destruct_end: ∀ A (l: list A), l = nil ∨ ∃ l´ a, l = l´ ++ a :: nil.

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

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

Lemma not_or_and_iff : ∀ P Q, ¬ (P ∨ Q) ↔ ¬ P ∧ ¬ Q.

Lemma true_imp_b: ∀ (b : bool), (true → b) ↔ b = true.

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).
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_two A: ∀ (x y: A), NoDup (x :: y :: nil) ↔ x ≠ y.

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.



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 In_perm A l l´ (P: perm_eq (T:=A) l l´) x : In x l ↔ In x l´.

Lemma In_implies_perm A (x : A) l (IN: In x l) :
  ∃ l´, Permutation l (x :: l´).

Lemma nodup_perm A l l´ (P: perm_eq (T:=A) l l´) : NoDup l ↔ NoDup l´.

Lemma Permutation_filter_split T:
  ∀ (l: list T) (f: T → bool), Permutation l ((filter f l) ++ (filter (fun x ⇒ negb (f x)) l)).

Lemma In_mem_eq (A: eqType) (l l´: list A) (P: l =i l´) x : In x l ↔ In x l´.

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 map_perm :
  ∀ A B (f: A → B) l l´, Permutation l l´ → Permutation (map f l) (map f l´).

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

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 NoDup_neq: ∀ {A} a b (l: list A), NoDup (a :: b :: l) → a ≠ b.

Lemma olast_inv A l x :
  olast (T:=A) l = Some x → ∃ prefix, l = prefix ++ x :: nil.

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

Lemma list_not_nil: ∀ {A} (l: list A), l ≠ nil ↔ ∃ a, In a l.

Lemma list_zero_one: ∀ {A} a (l: list A) (ND: NoDup l),
                     (∀ x (IN: In x l), x = a) ↔ l = nil ∨ l = a :: nil.

Lemma neq_contra: ∀ (x: nat), ¬ (x != x).

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

Require Import Wf Wf_nat.

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.

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.

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.