Module LibLists

Require Export List.
Require Export Tactics.
Require Export Coqlib.
Require Import Wf_nat.
Require Import Recdef.

Load Param.

Hint Resolve in_eq in_cons.

Lemma list_inj : forall A (a : A) a' b b', a::b = a'::b' -> (a=a' /\ b=b').

Lemma list_cons_right_inj : forall (A : Type) l1 (a1: A) l2 a2, l1 ++ a1 :: nil = l2 ++ a2 :: nil -> l1 = l2 /\ a1 = a2.

Remark list_cons_inj : forall (T : Type) (a1 a2 : T) q1 q2,
  a1 :: q1 = a2 :: q2 ->
  a1 = a2 /\ q1 = q2.


Open Scope nat_scope.

Section List_addons.

Variable A : Type.

List membership.

Lemma member_nil : forall (x : A), In x nil -> False.

Hint Resolve member_nil.

Lemma member_step : forall (x : A) a, x <> a ->
forall l, In x (a::l) -> In x l.

Fixpoint find_in_list (l : list A) (n : nat) {struct n} : option A :=
  match l with
    | nil => None
    | a' :: l' =>
      match n with
        | O => Some a'
        | S n' => find_in_list l' n'
      end
  end.

Lemma find_in_list_member : forall n l a,
find_in_list l n = Some a -> In a l.

Lemma member_find_in_list : forall l a, In a l ->
  exists n, find_in_list l n = Some a.


Section Member_dec.
Hypothesis eq_A_dec : forall x y : A, {x = y} + {x <> y}.

Lemma member_dec :
forall (x : A) l, {In x l} + {In x l -> False}.

Lemma member_which_dec :
forall (a : A) l x, In x (a::l) -> {x = a} + {In x l}.

Definition member_rect : forall (e : A) (P : list A -> Type),
 (forall l : list A, P (e :: l)) ->
       (forall l : list A, In e l -> P l -> forall a : A, P (a :: l)) ->
       forall l : list A, In e l -> P l.

Definition find_in_list_constr : forall l e, In e l ->
{n | find_in_list l n = Some e}.

End Member_dec.

Universal property on all items of a list.

Section List_forall.

Variable P : A -> Prop.

Fixpoint list_forall (l : list A) {struct l} : Prop :=
  match l with
    | nil => True
    | a' :: l' => P a' /\ list_forall l'
  end.


Theorem list_forall_correct : forall l,
list_forall l -> forall x, In x l -> P x.

Theorem list_forall_complete : forall l,
(forall x, In x l -> P x) -> list_forall l.

End List_forall.

No duplicates A list not containing twice the same item.

End List_addons.

Ltac automem :=
match goal with
| [ H: In _ nil |- _ ] => apply False_rect ; inversion H
| _ => idtac
end.



Lemma member_map : forall (A : Type) l x, In x l -> forall (B : Type) (f : A -> B),
In (f x) (map f l).

Lemma map_intro : forall (A : Type) l x, In x l -> forall (B : Type) (f : A -> B) y,
  y = f x -> In y (map f l).

Lemma map_elim : forall (A : Type) (B : Type) (f : A -> B) l y, In y (map f l) ->
  exists x, In x l /\ f x = y.


Lemma map_length : forall (A B : Type) (f : A -> B) l, length l = length (map f l).

Remark map_some_inj : forall (T : Type) l1 l2,
  map (@Some T) l1 = map (@Some _) l2 ->
  l1 = l2.



Section App_facts.
Variable A : Type.

Require Import Arith.

Lemma app_fix_left : forall (l l0 : list A), l = l ++ l0 -> l0 = nil.

Lemma app_fix_right : forall (l l0 : list A), l = l0 ++ l -> l0 = nil.

Lemma app_reg_l : forall l l1 l2 : list A, l ++ l1 = l ++ l2 -> l1 = l2.

Lemma rev_inj : forall l1 l2 : list A, rev l1 = rev l2 -> l1 = l2.

Lemma app_reg_r : forall l l1 l2 : list A, l1 ++ l = l2 ++ l -> l1 = l2.

Lemma rev_app : forall l1 l2 : _ A, rev (l1 ++ l2) = rev l2 ++ rev l1.

Remark app_cons : forall (A : Type) (sf : A) l l1 l2,
  l = l1 ++ sf :: l2 ->
  forall a,
    a :: l = (a :: l1) ++ sf :: l2.

Remark app_ass2 : forall (A : Type) (sf1 sf2 : A) l1 l2,
l1 ++ sf1 :: sf2 :: l2 = (l1 ++ sf1 :: nil) ++ sf2 :: l2.

Lemma no_self_append_no_nil : forall (A : Type) (l : _ A),
  (exists l', l = l ++ l' /\ l' <> nil) -> False.




Lemma member_or : forall l1 l2 (b : A), In b (l1 ++ l2) -> In b l1 \/ In b l2.

Lemma member_app_left : forall l1 (b : A), In b l1 -> forall l2, In b (l1 ++ l2).

Lemma member_app_right : forall l1 l2 (b : A), In b l2 -> In b (l1 ++ l2).

Lemma no_duplicates_no_member_app : forall l1 l2, NoDup (l1 ++ l2) -> forall x : A, In x l1 -> In x l2 -> False.

Lemma member_extract : forall l (b : A), In b l -> exists l1, exists l2, l = l1 ++ (b :: l2).

Fixpoint flatten l :=
  match l with
    | nil => nil (A := A)
    | a::b => a ++ flatten b
  end.

Lemma member_flatten_elim : forall l a, In a (flatten l) ->
  exists l0, In l0 l /\ In a l0.

Lemma member_flatten_intro : forall l l0,
  In l0 l -> forall a, In a l0 -> In a (flatten l).

Hypothesis eq_A_dec : forall a b : A, {a = b} + {a <> b}.

Let md := member_rect eq_A_dec.

Lemma member_flatten_elim_type : forall l a, In a (flatten l) ->
  {l0 | In l0 l /\ In a l0}.

Lemma member_extract_dec :
forall l (b : A), In b l -> {l1 : _ & {l2 | l = l1 ++ (b :: l2)}}.

Lemma member_map_recip_type :
  forall (B : Type) (f : B -> A) l a,
    In a (map f l) ->
    {b | f b = a /\ In b l}.
   

End App_facts.

Section Sorted.
Variable A : Type.
Variable ord : A -> A -> Prop.

Inductive sorted : list A -> Prop :=
| sorted_O: sorted nil
| sorted_1: forall x, sorted (cons x nil)
| sorted_S: forall x y, ord x y -> forall l, sorted (cons y l) -> sorted (cons x (cons y l)).

Hint Constructors sorted.

Lemma sorted_tail : forall a l, sorted (a::l) -> sorted l.

Hypothesis eq_A_dec : forall a b : A, {a = b} + {a <> b}.

Fixpoint occur a l {struct l} := match l with
| nil => O
| cons b m => match eq_A_dec a b with
  | left _ => S (@occur a m)
  | right _ => @occur a m
  end
end.

Lemma occur_member : forall l a n, occur a l = S n -> In a l.

Lemma occur_not_member : forall l a, occur a l = O -> In a l -> False.

Definition sameocc l1 l2 := forall a, occur a l1 = occur a l2.

Lemma sameocc_member l1 l2 : sameocc l1 l2 -> forall c, In c l1 -> In c l2.

Hypothesis ord_dec : forall a b, {ord a b} + {ord a b -> False}.

Hypothesis ord_total : forall a b, ord a b \/ ord b a.

Hypothesis ord_trans : forall a b, ord a b -> forall c, ord b c -> ord a c.

Lemma head_minimal : forall l, sorted l -> forall c l', l = c::l' -> forall d, In d l' -> ord c d.


Fixpoint sorted2 (l : list A) : Prop :=
  match l with
    | nil => True
    | a' :: l' => (forall i, In i l' -> ord a' i) /\ sorted2 l'
  end.

Lemma sorted_sorted2 : forall l, sorted l -> sorted2 l.

Lemma sorted2_sorted : forall l, sorted2 l -> sorted l.

Lemma sorted_app : forall l1 l2, sorted (l1 ++ l2) -> forall a1, In a1 l1 ->
forall a2, In a2 l2 -> ord a1 a2.

Lemma sorted_app_left : forall l1 l2, sorted (l1 ++ l2) -> sorted l1.

Lemma sorted_app_right : forall l1 l2, sorted (l1 ++ l2) -> sorted l2.

Lemma sorted_app_intro : forall l1,
  sorted l1 ->
  forall l2,
    sorted l2 ->
    (forall i1, In i1 l1 -> forall i2, In i2 l2 -> ord i1 i2) ->
    sorted (l1 ++ l2)
.
 

Definition sort_insert l : sorted l -> forall b, {l' | sorted l' /\ sameocc l' (b::l)}.

Definition sort l : {l' | sorted l' /\ sameocc l' l}.

End Sorted.
Hint Constructors sorted.

Lemma imp_sorted_weak :
  forall (A : Type) (P Q : A -> A -> Prop) (l : list A),
    (forall a b, In a l -> In b l -> P a b -> Q a b) ->
    sorted P l -> sorted Q l.

Corollary imp_sorted :
  forall (A : Type) (P Q : A -> A -> Prop), (forall a b : A, P a b -> Q a b) ->
    forall l, sorted P l -> sorted Q l.

Fixpoint repeat (A : Type) (a : A) (n : nat) {struct n} : list A :=
  match n with
    | O => nil
    | S n' => a :: (repeat a n')
  end.


Section Minimum_partial_order.

Variable A : Type.

Variable le : A -> A -> Prop.

Hypothesis le_antisym : forall a b,
  le a b -> le b a -> a = b.

Hypothesis le_trans : forall a b,
le a b -> forall c, le b c -> le a c.

Hypothesis le_dec : forall a b,
{le a b} + {~ le a b}.


Theorem minimum_partial_order : forall l
(le_refl : forall a, In a l -> le a a ) ,
{a | In a l /\ forall b, In b l -> le a b} +
{forall a, In a l -> (forall b, In b l -> le a b) -> False}.

End Minimum_partial_order.

Section Minimals.

Variable A : Type.

Variable le : A -> A -> Prop.

Hypothesis le_antisym : forall a b,
  le a b -> le b a -> a = b.

Hypothesis le_trans : forall a b,
le a b -> forall c, le b c -> le a c.

Hypothesis le_dec : forall a b,
{le a b} + {~ le a b}.

Lemma is_minimal : forall i
  (le_refl_i : le i i)
  l
  (le_refl_l : forall j, In j l -> le j j) ,
  {j | In j l /\ le j i /\ j <> i} + {forall j, In j l -> le j i -> j = i}.

Lemma minimals_aux : forall l accu m
  (le_refl_accu_l : forall i, In i (accu ++ l) -> le i i)
  (le_refl_m : forall i, In i m -> le i i)
  (hyp : forall j, In j accu -> forall k, In k m -> le k j -> k = j),
  {n | forall j, In j n <-> (In j (accu ++ l) /\ forall k, In k m -> le k j -> k = j)}.

Theorem minimals : forall l
  (le_refl_l : forall j, In j l -> le j j) ,
  {n | forall j, In j n <-> (In j l /\ forall k, In k l -> le k j -> k = j)}.

End Minimals.



Section List_product.

  Variable A B : Type.

  Variable P : A -> B -> Prop.

  Hypothesis P_dec : forall a b, {P a b} + {~ P a b}.

  Lemma list_product : forall la lb,
    {lab | forall a b,
      In (a, b) lab <->
      (In a la /\ In b lb /\ P a b)}.

End List_product.

Section At_most_list.
  Variable A : Type.
  Hypothesis eq_dec : forall a b : A, {a = b} + {a <> b}.

  Lemma at_most_list : forall l,
    {i : A & {j | In i l /\ In j l /\ i <> j}} +
    {forall i, In i l -> forall j, In j l -> i = j}.
    
End At_most_list.

Section Assoc.

  Variable key : Type.
  Hypothesis key_eq_dec : forall a b : key, {a = b} + {a <> b}.
  Variable value : Type.

  Function assoc (to_find : key) (l : list (key * value)) {struct l} : option value :=
    match l with
      | nil => None
      | (k, v) :: q =>
        if key_eq_dec k to_find
          then Some v
          else assoc to_find q
    end.

  Lemma assoc_In : forall to_find l val,
    assoc to_find l = Some val ->
    In (to_find, val) l.

  Lemma assoc_not_In : forall to_find l,
    assoc to_find l = None ->
    forall val, ~ In (to_find, val) l.

  Lemma assoc_app_some : forall l1 to_find v,
    assoc to_find l1 = Some v ->
    forall l2,
    assoc to_find (l1 ++ l2) = Some v
    .

  Lemma assoc_app_none : forall l1 to_find,
    assoc to_find l1 = None ->
    forall l2,
    assoc to_find (l1 ++ l2) = assoc to_find l2.

End Assoc.

Section Assoc_map.

  Variable key : Type.
  Hypothesis key_eq_dec : forall a b : key, {a = b} + {a <> b}.
  Variables value1 value2 : Type.

Section Assoc_map_aux.

  Variable f : key -> value1 -> option value2.

  Function assoc_map_aux (accu : list (key * value2)) (l : list (key * value1)) {struct l} : list (key * value2) :=
    match l with
      | nil => accu
      | (a, va) :: l' =>
        match f a va with
          | None => assoc_map_aux accu l'
          | Some vb =>
            match assoc key_eq_dec a accu with
              | None => assoc_map_aux ((a, vb) :: accu) l'
              | _ => assoc_map_aux accu l'
            end
        end
    end.

  Lemma assoc_map_aux_cons_right : forall l accu a,
    assoc_map_aux accu (l ++ a :: nil) = assoc_map_aux (assoc_map_aux accu l) (a :: nil).

  Corollary assoc_map_aux_app : forall l accu l1,
    assoc_map_aux accu (l1 ++ l) = assoc_map_aux (assoc_map_aux accu l1) l.

    

End Assoc_map_aux.

Variable f : value1 -> value2.


  Function map_snd (xy : key * value1) : key * value2 :=
    let (x, y) := xy in (x, f y).

  Lemma assoc_map_none : forall l x,
    assoc key_eq_dec x l = None ->
    assoc key_eq_dec x (map map_snd l) = None.

  Lemma assoc_map_none_recip : forall l x,
    assoc key_eq_dec x (map map_snd l) = None ->
    assoc key_eq_dec x l = None.

  Lemma assoc_map_some : forall l x y,
    assoc key_eq_dec x l = Some y ->
    assoc key_eq_dec x (map map_snd l) = Some (f y).

  Lemma assoc_map_some_recip : forall l x y2,
    assoc key_eq_dec x (map map_snd l) = Some y2 ->
    exists y1, assoc key_eq_dec x l = Some y1 /\ f y1 = y2.

End Assoc_map.


Section Merge_sort.

Variable ident : Type.

Hypothesis peq : forall t1 t2 : ident, {t1 = t2} + {t1 <> t2}.

Variable Plt : ident -> ident -> Prop.

Hypothesis plt : forall t1 t2, {Plt t1 t2} + {~ Plt t1 t2}.

Function merge_aux
  (accu : list ident)
  (x : list ident * list ident)
  {measure
    (fun x0 : list ident * list ident => let (l1, l2) := x0 in length l1 + length l2)%nat
    x
  } : list ident :=
  let (l1, l2) := x in
    match l1 with
      | nil => rev' accu ++ l2
      | a1 :: q1 =>
        match l2 with
          | nil => rev' accu ++ l1
          | a2 :: q2 =>
            if peq a1 a2
              then merge_aux (a1 :: accu) (q1, q2)
              else if plt a1 a2
                then merge_aux (a1 :: accu) (q1, l2)
                else
                  merge_aux (a2 :: accu) (l1, q2)
        end
    end.

Lemma merge_aux_prop : forall accu x l1 l2,
  x = (l1, l2) ->
  forall i, In i (accu ++ l1 ++ l2) <-> In i (merge_aux accu x)
.
   
Definition merge l1 l2 := merge_aux nil (l1, l2).

Lemma merge_prop : forall l1 l2,
  forall i, In i (l1 ++ l2) <-> In i (merge l1 l2)
.

Lemma merge_intro : forall l1 l2,
  forall i, In i (l1 ++ l2) -> In i (merge l1 l2)
.

Lemma merge_elim : forall l1 l2,
  forall i, In i (merge l1 l2) -> In i (l1 ++ l2)
.

Function flatten_merge (l : list (list ident)) : list ident :=
  match l with
    | nil => nil
    | a::b => merge a (flatten_merge b)
  end.

Lemma flatten_merge_prop : forall l i,
  In i (flatten l) <-> In i (flatten_merge l)
.

Definition flatten_merge_intro l i :=
  let (h, _) := @flatten_merge_prop l i in h.


Definition flatten_merge_elim l i :=
  let (_, h) := @flatten_merge_prop l i in h.
 
Function split_aux (accu1 accu2 l : list ident) {struct l} : list ident * list ident :=
  match l with
    | nil => (accu1, accu2)
    | a :: nil => (a :: accu1, accu2)
    | a :: b :: q => split_aux (a :: accu1) (b :: accu2) q
  end.

Lemma split_aux_length_left : (forall l,
  length l >= 2 ->
  forall accu1 accu2 l1 l2,
    split_aux accu1 accu2 l = (l1, l2) ->
    length l1 < length l + length accu1)%nat.


Lemma split_aux_length_right : (forall l,
  length l >= 2 ->
  forall accu1 accu2 l1 l2,
    split_aux accu1 accu2 l = (l1, l2) ->
    length l2 < length l + length accu2)%nat.

Lemma split_aux_prop : forall l accu1 accu2 l1 l2,
  split_aux accu1 accu2 l = (l1, l2) ->
  forall i,
    In i (l1 ++ l2) <-> In i (accu1 ++ accu2 ++ l)
    .

Function merge_sort (l : list ident) {measure length l} : list ident :=
  match l with
    | nil => nil
    | a :: nil => a :: nil
    | a :: b :: q =>
      let (l1, l2) := split_aux nil nil l in
        merge (merge_sort l1) (merge_sort l2)
  end.

Lemma merge_sort_prop : forall l i,
  In i l <-> In i (merge_sort l)
.

Definition merge_sort_intro l i :=
  let (h, _) := merge_sort_prop l i in h.

Definition merge_sort_elim l i :=
  let (_, h) := merge_sort_prop l i in h.


Hypothesis Plt_strict : forall a, ~ Plt a a.

Implicit Arguments Plt_strict [].

Lemma sorted_decomp_unique : forall l,
  (forall l1 a l2 b l3, l = l1 ++ a :: l2 ++ b :: l3 -> Plt b a) ->
  forall l1 a l1',
    l = l1 ++ a :: l1' ->
    forall l2 l2',
      l = l2 ++ a :: l2' ->
      (l1, l1') = (l2, l2').

Lemma sorted_intro : forall l,
  (forall l1 a l2 b l3, l = l1 ++ a :: l2 ++ b :: l3 -> Plt b a) ->
  sorted (fun a b => Plt b a) l.

Hypothesis Plt_trans:
  forall (x y z: ident), Plt x y -> Plt y z -> Plt x z.

Implicit Arguments Plt_trans [].


Lemma sorted_elim : forall l,
  sorted (fun a b => Plt b a) l ->
  (forall l1 a l2 b l3, l = l1 ++ a :: l2 ++ b :: l3 -> Plt b a)
.

Lemma sorted_join_common : forall l1 a l2,
  sorted (fun a b => Plt b a) (l1 ++ a :: nil) ->
  sorted (fun a b => Plt b a) (a :: l2) ->
  sorted (fun a b => Plt b a) (l1 ++ a :: l2)
.

End Merge_sort.

Section Tag_list.

Variable A : Type.

Variable P : A -> Type.

Lemma tag_list : forall l, (forall a, In a l -> P a) -> {l' : list (sigT P) | forall a, In a l <-> exists p, In (existT _ a p) l'}.

End Tag_list.
  
Lemma In_dec_recip : forall (T : Type) (in_dec : forall (t : T) l, {In t l} + {~ In t l})
  (t1 t2 : T), {t1 = t2} + {t1 <> t2}.

Section NoDup.

Variable A : Type.

Lemma NoDup_elim :
  forall l : _ A, NoDup l -> forall l1 x l2 l3, l = l1 ++ x :: l2 ++ x :: l3 -> False.

Lemma NoDup_intro : forall l : _ A,
  (forall l1 x l2 l3, l = l1 ++ x :: l2 ++ x :: l3 -> False) ->
  NoDup l.

Lemma NoDup_app : forall l1 l2,
  NoDup (l1 ++ l2) ->
  forall x : A, In x l1 -> In x l2 -> False.

Lemma NoDup_app_recip : forall l,
  (forall l1 l2, l = l1 ++ l2 -> forall x : A, In x l1 -> In x l2 -> False) ->
  NoDup l.

Lemma NoDup_norepet : forall l : _ A, NoDup l -> list_norepet l.

Lemma norepet_NoDup : forall l : _ A, list_norepet l -> NoDup l.

  
End NoDup.

Section Discr.
Variable A : Type.
Variable P : A -> Type.

Lemma in_app_discr : forall l1,
  (forall x, In x l1 -> P x -> False) ->
  forall a,
  P a ->
  forall l1',
    (forall x, In x l1' -> P x -> False) ->
    forall a', P a' ->
      forall l2 l2',
    l1 ++ a :: l2 = l1' ++ a' :: l2' ->
    (l1, a, l2) = (l1', a', l2').

End Discr.

Section Left_include.

Variable A : Type.

Lemma left_include : forall l1' a' l2',
  (forall x : A, In x l1' -> x = a' -> False) ->
  forall l1, (In a' l1 -> False) ->
    forall l2,
      l1 ++ l2 = l1' ++ a' :: l2' ->
    exists l0, l1' = l1 ++ l0.

End Left_include.

Section List_ordering.
 Variable A : Type.

 Lemma NoDup_uniq : forall l1 (a : A) l2,
   NoDup (l1 ++ a :: l2) ->
   forall l3 l4,
     l1 ++ a :: l2 = l3 ++ a :: l4 ->
     (l1, l2) = (l3, l4).


Lemma nodup_right : forall l, NoDup l ->
  forall l1 (obj : A) l1', l = l1 ++ obj :: l1' ->
  forall l2 l2', l = l2 ++ obj :: l2' ->
    l1' = l2'.

 Lemma NoDup_uniq_recip : forall l,
   (forall (a : A) l1 l2, l = l1 ++ a :: l2 -> forall l3 l4, l = l3 ++ a :: l4 -> (l1, l2) = (l3, l4)) ->
   NoDup l.

 Lemma NoDup_filter : forall (f : A -> _) l a l', NoDup (l ++ a :: l') ->
   forall l2, filter f (l ++ a :: l') = a :: l2 ->
     forall x, In x l -> f x = false.

 Definition list_lt (l : list A) (a b : A) : Prop :=
   exists l1, exists l2, exists l3,
     l = l1 ++ a :: l2 ++ b :: l3.

 Lemma list_lt_trans : forall l, NoDup l -> forall a b,
   list_lt l a b -> forall c,
     list_lt l b c ->
     list_lt l a c.
   
 Lemma list_lt_irrefl : forall l, NoDup l -> forall a,
   list_lt l a a -> False.

 Lemma list_lt_In_left : forall l a b, list_lt l a b ->
   In a l.

 Lemma list_lt_In_right : forall l a b, list_lt l a b ->
   In b l.

 Lemma list_lt_app_reg_l : forall l a b,
   list_lt l a b -> forall l', list_lt (l' ++ l) a b.

   Lemma list_lt_app_reg_r : forall l a b,
   list_lt l a b -> forall l', list_lt (l ++ l') a b.
     
   Lemma list_lt_app : forall l a,
     In a l -> forall l' a', In a' l' -> list_lt (l ++ l') a a'.
       

 Hypothesis eq_dec : forall a b : A, {a = b} + {a <> b}.

 Lemma list_lt_total : forall l a, In a l -> forall b, In b l ->
   {list_lt l a b} + {list_lt l b a} + {a = b}.

End List_ordering.

Lemma NoDup_filter_compat : forall (A : Type) (l : _ A),
  NoDup l ->
  forall f, NoDup (filter f l).

Lemma NoDup_app_intro : forall (A : Type) (l1 : _ A),
  NoDup l1 ->
  forall l2, NoDup l2 ->
    (forall x, In x l1 -> In x l2 -> False) ->
    NoDup (l1 ++ l2).
   
Lemma NoDup_rev : forall (A : Type) (l : _ A),
  NoDup l ->
  NoDup (rev l).

Corollary rev_NoDup : forall (A : Type) (l : _ A),
 NoDup (rev l) ->
 NoDup l.

Definition in_rev_intro := (fun (A : Type) l x => let (h, _) := In_rev (A := A) l x in h).

Definition in_rev_elim := (fun (A : Type) l x => let (_, h) := In_rev (A := A) l x in h).

Lemma NoDup_app_left : forall (A : Type) (l1 l2 : _ A),
 NoDup (l1 ++ l2) ->
 NoDup l1
.

Lemma NoDup_app_right : forall (A : Type) (l1 l2 : _ A),
 NoDup (l1 ++ l2) ->
 NoDup l2
.


Lemma filter_app : forall (A : Type) (l1 l2 : _ A) f,
  filter f (l1 ++ l2) = filter f l1 ++ filter f l2.

Lemma filter_app_recip : forall (A : Type) l (f : A -> _) l'1 l'2,
  filter f l = l'1 ++ l'2 -> exists l1, exists l2, l = l1 ++ l2 /\ filter f l1 = l'1 /\ filter f l2 = l'2.

Lemma filter_commut : forall (A : Type) f1 f2 (l : _ A),
  filter f1 (filter f2 l) = filter f2 (filter f1 l).

Lemma filter_idem : forall (A : Type) f (l : _ A),
  filter f (filter f l) = filter f l.

Lemma list_lt_filter_recip : forall (A : Type) (f : A -> _) l a b, list_lt (filter f l) a b -> list_lt l a b.

Lemma list_lt_filter_aux : forall (A : Type) l a b, list_lt l a b -> forall (f : A -> _), f a = true -> f b = true -> list_lt (filter f l) a b.

Corollary list_lt_filter : forall (A : Type) l a b, list_lt l a b -> forall (f : A -> _), In a (filter f l) -> In b (filter f l) -> list_lt (filter f l) a b.



Section Last.

Variable A : Type.

Function last (l : list A) {struct l} : option A :=
  match l with
    | nil => None
    | a :: l' =>
      match l' with
        | nil => Some a
        | _ => last l'
      end
  end.

Lemma last_correct : forall l s, last l = Some s ->
  {l' | l = l' ++ s :: nil}.

Lemma last_complete : forall l a, last (l ++ a :: nil) = Some a.

Lemma last_app_left : forall l1, l1 <> nil -> forall l2,
  last (l2 ++ l1) = last l1.

Lemma last_nonempty : forall l, l <> nil -> last l <> None.


End Last.