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

Definition disjoint A (l1 l2 : list A) :=
  forall 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:
  forall (A B: Type) (f: A -> B) (l: list A),
  NoDup l ->
  (forall x y, In x l -> In y l -> x <> y -> f x <> f y) ->
  NoDup (map f l).

Lemma nodup_append_commut:
  forall (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:
  forall (A: Type) (l1 l2: list A),
  NoDup (l1 ++ l2) <->
  NoDup l1 /\ NoDup l2 /\ disjoint l1 l2.

Lemma nodup_append:
  forall (A: Type) (l1 l2: list A),
  NoDup l1 -> NoDup l2 -> disjoint l1 l2 ->
  NoDup (l1 ++ l2).

Lemma nodup_append_right:
  forall (A: Type) (l1 l2: list A),
  NoDup (l1 ++ l2) -> NoDup l2.

Lemma nodup_append_left:
  forall (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 nodup_perm A l l' (P: perm_eq (T:=A) l l') : NoDup l <-> NoDup 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 -> (forall y (IN: In y l), y = x) -> l = x :: nil.


Lemma map_perm :
  forall A B (f: A -> B) l l', Permutation l l' -> Permutation (map f l) (map f l').

Lemma perm_from_subset :
  forall A (l : list A) l',
    NoDup l' ->
    (forall x, In x l' -> In x l) ->
    exists 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 olast_inv A l x :
  olast (T:=A) l = Some x -> exists prefix, l = prefix ++ x :: nil.

Lemma In_flatten A (x:A) l :
  In x (flatten l) <-> exists y, In x y /\ In y l.