Require Import List Permutation Vbase Classical.
Set Implicit Arguments.

Fixpoint flatten A (l: list (list A)) :=
  match l with
    | nilnil
    | 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.

Properties of In

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 lIn 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: AB) x l (IN: In x l), In (f x) (map f l).

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

Lemma In_map :
   A B (f: AB) 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: Abool) (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: AB) (l: list A),
  NoDup l
  ( x y, In x lIn y lx yf 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 l1NoDup l2disjoint 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 lIn x l → ( y (IN: In y l), y = x) → l = x :: nil.

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

Lemma NoDup_mapD A B (f : AB) 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'').


This page has been generated by coqdoc