Imported Upstream version 8.0pl1upstream/8.0pl1

6 files changed, 1926 insertions, 0 deletions

diff --git a/theories/Lists/List.v b/theories/Lists/List.v
new file mode 100755
index 00000000..c3f65d67
--- /dev/null
+++ b/theories/Lists/List.v
@@ -0,0 +1,655 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: List.v,v 1.9.2.1 2004/07/16 19:31:05 herbelin Exp $ i*)
+
+Require Import Le.
+
+
+Section Lists.
+
+Variable A : Set.
+
+Set Implicit Arguments.
+
+Inductive list : Set :=
+  | nil : list
+  | cons : A -> list -> list.
+
+Infix "::" := cons (at level 60, right associativity) : list_scope.
+
+Open Scope list_scope.
+
+(*************************)
+(** Discrimination       *)
+(*************************)
+
+Lemma nil_cons : forall (a:A) (m:list), nil <> a :: m.
+Proof. 
+  intros; discriminate.
+Qed.
+
+(*************************)
+(** Concatenation        *)
+(*************************)
+
+Fixpoint app (l m:list) {struct l} : list :=
+  match l with
+  | nil => m
+  | a :: l1 => a :: app l1 m
+  end.
+
+Infix "++" := app (right associativity, at level 60) : list_scope.
+
+Lemma app_nil_end : forall l:list, l = l ++ nil.
+Proof. 
+	induction l; simpl in |- *; auto.
+        rewrite <- IHl; auto.
+Qed.
+Hint Resolve app_nil_end.
+
+Ltac now_show c := change c in |- *.
+
+Lemma app_ass : forall l m n:list, (l ++ m) ++ n = l ++ m ++ n.
+Proof. 
+	intros. induction l; simpl in |- *; auto.
+        now_show (a :: (l ++ m) ++ n = a :: l ++ m ++ n).
+	rewrite <- IHl; auto.
+Qed.
+Hint Resolve app_ass.
+
+Lemma ass_app : forall l m n:list, l ++ m ++ n = (l ++ m) ++ n.
+Proof. 
+	auto.
+Qed.
+Hint Resolve ass_app.
+
+Lemma app_comm_cons : forall (x y:list) (a:A), a :: x ++ y = (a :: x) ++ y.
+Proof.
+ auto.
+Qed.
+
+Lemma app_eq_nil : forall x y:list, x ++ y = nil -> x = nil /\ y = nil.
+Proof.
+  destruct x as [| a l]; [ destruct y as [| a l] | destruct y as [| a0 l0] ];
+   simpl in |- *; auto.
+  intros H; discriminate H.
+  intros; discriminate H.
+Qed.
+
+Lemma app_cons_not_nil : forall (x y:list) (a:A), nil <> x ++ a :: y.
+Proof.
+unfold not in |- *.
+  destruct x as [| a l]; simpl in |- *; intros.
+  discriminate H.
+  discriminate H.
+Qed.
+
+Lemma app_eq_unit :
+ forall (x y:list) (a:A),
+   x ++ y = a :: nil -> x = nil /\ y = a :: nil \/ x = a :: nil /\ y = nil.
+
+Proof.
+  destruct x as [| a l]; [ destruct y as [| a l] | destruct y as [| a0 l0] ];
+   simpl in |- *.
+  intros a H; discriminate H.
+  left; split; auto.
+  right; split; auto.
+  generalize H.
+  generalize (app_nil_end l); intros E.
+  rewrite <- E; auto.
+  intros.
+  injection H.
+  intro.
+  cut (nil = l ++ a0 :: l0); auto.
+  intro.
+  generalize (app_cons_not_nil _ _ _ H1); intro.
+  elim H2.
+Qed.
+
+Lemma app_inj_tail :
+ forall (x y:list) (a b:A), x ++ a :: nil = y ++ b :: nil -> x = y /\ a = b.
+Proof.
+  induction x as [| x l IHl];
+   [ destruct y as [| a l] | destruct y as [| a l0] ]; 
+   simpl in |- *; auto.
+  intros a b H.
+  injection H.
+  auto.
+  intros a0 b H.
+  injection H; intros.
+  generalize (app_cons_not_nil _ _ _ H0); destruct 1.
+  intros a b H.
+  injection H; intros.
+  cut (nil = l ++ a :: nil); auto.
+  intro.
+  generalize (app_cons_not_nil _ _ _ H2); destruct 1.
+  intros a0 b H.
+  injection H; intros.
+  destruct (IHl l0 a0 b H0). 
+  split; auto.
+  rewrite <- H1; rewrite <- H2; reflexivity.
+Qed.
+
+(*************************)
+(** Head and tail        *)
+(*************************)
+
+Definition head (l:list) :=
+  match l with
+  | nil => error
+  | x :: _ => value x
+  end.
+
+Definition tail (l:list) : list :=
+  match l with
+  | nil => nil
+  | a :: m => m
+  end.
+
+(****************************************)
+(** Length of lists                     *)
+(****************************************)
+
+Fixpoint length (l:list) : nat :=
+  match l with
+  | nil => 0
+  | _ :: m => S (length m)
+  end.
+
+(******************************)
+(** Length order of lists     *)
+(******************************)
+
+Section length_order.
+Definition lel (l m:list) := length l <= length m.
+
+Variables a b : A.
+Variables l m n : list.
+
+Lemma lel_refl : lel l l.
+Proof. 
+	unfold lel in |- *; auto with arith.
+Qed.
+
+Lemma lel_trans : lel l m -> lel m n -> lel l n.
+Proof. 
+	unfold lel in |- *; intros.
+        now_show (length l <= length n).
+        apply le_trans with (length m); auto with arith.
+Qed.
+
+Lemma lel_cons_cons : lel l m -> lel (a :: l) (b :: m).
+Proof. 
+	unfold lel in |- *; simpl in |- *; auto with arith.
+Qed.
+
+Lemma lel_cons : lel l m -> lel l (b :: m).
+Proof. 
+	unfold lel in |- *; simpl in |- *; auto with arith.
+Qed.
+
+Lemma lel_tail : lel (a :: l) (b :: m) -> lel l m.
+Proof. 
+	unfold lel in |- *; simpl in |- *; auto with arith.
+Qed.
+
+Lemma lel_nil : forall l':list, lel l' nil -> nil = l'.
+Proof. 
+	intro l'; elim l'; auto with arith.
+	intros a' y H H0.
+        now_show (nil = a' :: y).
+	absurd (S (length y) <= 0); auto with arith.
+Qed.
+End length_order.
+
+Hint Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons.
+
+(*********************************)
+(** The [In] predicate           *)
+(*********************************)
+
+Fixpoint In (a:A) (l:list) {struct l} : Prop :=
+  match l with
+  | nil => False
+  | b :: m => b = a \/ In a m
+  end.
+
+Lemma in_eq : forall (a:A) (l:list), In a (a :: l).
+Proof. 
+	simpl in |- *; auto.
+Qed.
+Hint Resolve in_eq.
+
+Lemma in_cons : forall (a b:A) (l:list), In b l -> In b (a :: l).
+Proof. 
+	simpl in |- *; auto.
+Qed.
+Hint Resolve in_cons.
+
+Lemma in_nil : forall a:A, ~ In a nil.
+Proof.
+  unfold not in |- *; intros a H; inversion_clear H.
+Qed.
+
+
+Lemma in_inv : forall (a b:A) (l:list), In b (a :: l) -> a = b \/ In b l.
+Proof.
+ intros a b l H; inversion_clear H; auto.
+Qed.
+
+Lemma In_dec :
+ (forall x y:A, {x = y} + {x <> y}) ->
+ forall (a:A) (l:list), {In a l} + {~ In a l}.
+
+Proof.
+  induction l as [| a0 l IHl].
+  right; apply in_nil.
+  destruct (H a0 a); simpl in |- *; auto.
+  destruct IHl; simpl in |- *; auto. 
+  right; unfold not in |- *; intros [Hc1| Hc2]; auto.
+Qed.
+
+Lemma in_app_or : forall (l m:list) (a:A), In a (l ++ m) -> In a l \/ In a m.
+Proof. 
+	intros l m a.
+	elim l; simpl in |- *; auto.
+	intros a0 y H H0.
+	now_show ((a0 = a \/ In a y) \/ In a m).
+	elim H0; auto.
+	intro H1.
+        now_show ((a0 = a \/ In a y) \/ In a m).
+	elim (H H1); auto.
+Qed.
+Hint Immediate in_app_or.
+
+Lemma in_or_app : forall (l m:list) (a:A), In a l \/ In a m -> In a (l ++ m).
+Proof. 
+	intros l m a.
+	elim l; simpl in |- *; intro H.
+        now_show (In a m).
+	elim H; auto; intro H0.
+	now_show (In a m).
+	elim H0. (* subProof completed *)
+	intros y H0 H1.
+	now_show (H = a \/ In a (y ++ m)).
+	elim H1; auto 4.
+	intro H2.
+	now_show (H = a \/ In a (y ++ m)).
+	elim H2; auto.
+Qed.
+Hint Resolve in_or_app.
+
+(***************************)
+(** Set inclusion on list  *)
+(***************************)
+
+Definition incl (l m:list) := forall a:A, In a l -> In a m.
+Hint Unfold incl.
+
+Lemma incl_refl : forall l:list, incl l l.
+Proof. 
+	auto.
+Qed.
+Hint Resolve incl_refl.
+
+Lemma incl_tl : forall (a:A) (l m:list), incl l m -> incl l (a :: m).
+Proof. 
+	auto.
+Qed.
+Hint Immediate incl_tl.
+
+Lemma incl_tran : forall l m n:list, incl l m -> incl m n -> incl l n.
+Proof. 
+	auto.
+Qed.
+
+Lemma incl_appl : forall l m n:list, incl l n -> incl l (n ++ m).
+Proof. 
+	auto.
+Qed.
+Hint Immediate incl_appl.
+
+Lemma incl_appr : forall l m n:list, incl l n -> incl l (m ++ n).
+Proof. 
+	auto.
+Qed.
+Hint Immediate incl_appr.
+
+Lemma incl_cons :
+ forall (a:A) (l m:list), In a m -> incl l m -> incl (a :: l) m.
+Proof. 
+	unfold incl in |- *; simpl in |- *; intros a l m H H0 a0 H1.
+        now_show (In a0 m).
+	elim H1.
+	now_show (a = a0 -> In a0 m).
+	elim H1; auto; intro H2.
+	now_show (a = a0 -> In a0 m).
+	elim H2; auto. (* solves subgoal *)
+	now_show (In a0 l -> In a0 m).
+	auto.
+Qed.
+Hint Resolve incl_cons.
+
+Lemma incl_app : forall l m n:list, incl l n -> incl m n -> incl (l ++ m) n.
+Proof. 
+	unfold incl in |- *; simpl in |- *; intros l m n H H0 a H1.
+        now_show (In a n).
+	elim (in_app_or _ _ _ H1); auto.
+Qed.
+Hint Resolve incl_app.
+
+(**************************)
+(** Nth element of a list *)
+(**************************)
+
+Fixpoint nth (n:nat) (l:list) (default:A) {struct l} : A :=
+  match n, l with
+  | O, x :: l' => x
+  | O, other => default
+  | S m, nil => default
+  | S m, x :: t => nth m t default
+  end.
+
+Fixpoint nth_ok (n:nat) (l:list) (default:A) {struct l} : bool :=
+  match n, l with
+  | O, x :: l' => true
+  | O, other => false
+  | S m, nil => false
+  | S m, x :: t => nth_ok m t default
+  end.
+
+Lemma nth_in_or_default :
+ forall (n:nat) (l:list) (d:A), {In (nth n l d) l} + {nth n l d = d}.
+(* Realizer nth_ok. Program_all. *)
+Proof. 
+  intros n l d; generalize n; induction l; intro n0.
+  right; case n0; trivial.
+  case n0; simpl in |- *.
+  auto.
+  intro n1; elim (IHl n1); auto.     
+Qed.
+
+Lemma nth_S_cons :
+ forall (n:nat) (l:list) (d a:A),
+   In (nth n l d) l -> In (nth (S n) (a :: l) d) (a :: l).
+Proof. 
+  simpl in |- *; auto.
+Qed.
+
+Fixpoint nth_error (l:list) (n:nat) {struct n} : Exc A :=
+  match n, l with
+  | O, x :: _ => value x
+  | S n, _ :: l => nth_error l n
+  | _, _ => error
+  end.
+
+Definition nth_default (default:A) (l:list) (n:nat) : A :=
+  match nth_error l n with
+  | Some x => x
+  | None => default
+  end.
+
+Lemma nth_In :
+ forall (n:nat) (l:list) (d:A), n < length l -> In (nth n l d) l.
+
+Proof.
+unfold lt in |- *; induction n as [| n hn]; simpl in |- *.
+destruct l; simpl in |- *; [ inversion 2 | auto ].
+destruct l as [| a l hl]; simpl in |- *.
+inversion 2.
+intros d ie; right; apply hn; auto with arith.
+Qed.
+
+(********************************)
+(** Decidable equality on lists *)
+(********************************)
+
+
+Lemma list_eq_dec :
+ (forall x y:A, {x = y} + {x <> y}) -> forall x y:list, {x = y} + {x <> y}.
+Proof.
+  induction x as [| a l IHl]; destruct y as [| a0 l0]; auto.
+  destruct (H a a0) as [e| e].
+  destruct (IHl l0) as [e'| e'].
+  left; rewrite e; rewrite e'; trivial.
+  right; red in |- *; intro.
+  apply e'; injection H0; trivial.
+  right; red in |- *; intro.
+  apply e; injection H0; trivial.
+Qed.
+
+(*************************)
+(**  Reverse             *)
+(*************************)
+
+Fixpoint rev (l:list) : list :=
+  match l with
+  | nil => nil
+  | x :: l' => rev l' ++ x :: nil
+  end.
+
+Lemma distr_rev : forall x y:list, rev (x ++ y) = rev y ++ rev x.
+Proof.
+ induction x as [| a l IHl].
+ destruct y as [| a l].
+ simpl in |- *.
+ auto.
+
+ simpl in |- *.
+ apply app_nil_end; auto.
+
+ intro y.
+ simpl in |- *.
+ rewrite (IHl y).
+ apply (app_ass (rev y) (rev l) (a :: nil)).
+Qed.
+
+Remark rev_unit : forall (l:list) (a:A), rev (l ++ a :: nil) = a :: rev l.
+Proof.
+ intros.
+ apply (distr_rev l (a :: nil)); simpl in |- *; auto.
+Qed.
+
+Lemma rev_involutive : forall l:list, rev (rev l) = l.
+Proof.
+ induction l as [| a l IHl].
+ simpl in |- *; auto.
+
+ simpl in |- *.
+ rewrite (rev_unit (rev l) a).
+ rewrite IHl; auto.
+Qed.
+
+(*********************************************)
+(**  Reverse Induction Principle on Lists    *)
+(*********************************************)
+
+Section Reverse_Induction.
+
+Unset Implicit Arguments.
+
+Remark rev_list_ind :
+ forall P:list -> Prop,
+   P nil ->
+   (forall (a:A) (l:list), P (rev l) -> P (rev (a :: l))) ->
+   forall l:list, P (rev l).
+Proof.
+ induction l; auto.
+Qed.
+Set Implicit Arguments.
+
+Lemma rev_ind :
+ forall P:list -> Prop,
+   P nil ->
+   (forall (x:A) (l:list), P l -> P (l ++ x :: nil)) -> forall l:list, P l.
+Proof.
+ intros.
+ generalize (rev_involutive l).
+ intros E; rewrite <- E.
+ apply (rev_list_ind P).
+ auto.
+
+ simpl in |- *.
+ intros.
+ apply (H0 a (rev l0)).
+ auto.
+Qed.
+
+End Reverse_Induction.
+
+End Lists.
+
+Implicit Arguments nil [A].
+
+Hint Resolve nil_cons app_nil_end ass_app app_ass: datatypes v62.
+Hint Resolve app_comm_cons app_cons_not_nil: datatypes v62.
+Hint Immediate app_eq_nil: datatypes v62.
+Hint Resolve app_eq_unit app_inj_tail: datatypes v62. 
+Hint Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons:
+  datatypes v62.
+Hint Resolve in_eq in_cons in_inv in_nil in_app_or in_or_app: datatypes v62.
+Hint Resolve incl_refl incl_tl incl_tran incl_appl incl_appr incl_cons
+  incl_app: datatypes v62.
+
+Section Functions_on_lists.
+
+(****************************************************************)
+(** Some generic functions on lists and basic functions of them *)
+(****************************************************************)
+
+Section Map.
+Variables A B : Set.
+Variable f : A -> B.
+Fixpoint map (l:list A) : list B :=
+  match l with
+  | nil => nil
+  | cons a t => cons (f a) (map t)
+  end.
+End Map.
+
+Lemma in_map :
+ forall (A B:Set) (f:A -> B) (l:list A) (x:A), In x l -> In (f x) (map f l).
+Proof. 
+  induction l as [| a l IHl]; simpl in |- *;
+   [ auto
+   | destruct 1; [ left; apply f_equal with (f := f); assumption | auto ] ].
+Qed.
+
+Fixpoint flat_map (A B:Set) (f:A -> list B) (l:list A) {struct l} : 
+ list B :=
+  match l with
+  | nil => nil
+  | cons x t => app (f x) (flat_map f t)
+  end.
+
+Fixpoint list_prod (A B:Set) (l:list A) (l':list B) {struct l} :
+ list (A * B) :=
+  match l with
+  | nil => nil
+  | cons x t => app (map (fun y:B => (x, y)) l') (list_prod t l')
+  end.
+
+Lemma in_prod_aux :
+ forall (A B:Set) (x:A) (y:B) (l:list B),
+   In y l -> In (x, y) (map (fun y0:B => (x, y0)) l).
+Proof. 
+  induction l;
+   [ simpl in |- *; auto
+   | simpl in |- *; destruct 1 as [H1| ];
+      [ left; rewrite H1; trivial | right; auto ] ].
+Qed.
+
+Lemma in_prod :
+ forall (A B:Set) (l:list A) (l':list B) (x:A) (y:B),
+   In x l -> In y l' -> In (x, y) (list_prod l l').
+Proof. 
+  induction l;
+   [ simpl in |- *; tauto
+   | simpl in |- *; intros; apply in_or_app; destruct H;
+      [ left; rewrite H; apply in_prod_aux; assumption | right; auto ] ].
+Qed.
+
+(** [(list_power x y)] is [y^x], or the set of sequences of elts of [y]
+    indexed by elts of [x], sorted in lexicographic order. *)
+
+Fixpoint list_power (A B:Set) (l:list A) (l':list B) {struct l} :
+ list (list (A * B)) :=
+  match l with
+  | nil => cons nil nil
+  | cons x t =>
+      flat_map (fun f:list (A * B) => map (fun y:B => cons (x, y) f) l')
+        (list_power t l')
+  end.
+
+(************************************)
+(** Left-to-right iterator on lists *)
+(************************************)
+
+Section Fold_Left_Recursor.
+Variables A B : Set.
+Variable f : A -> B -> A.
+Fixpoint fold_left (l:list B) (a0:A) {struct l} : A :=
+  match l with
+  | nil => a0
+  | cons b t => fold_left t (f a0 b)
+  end.
+End Fold_Left_Recursor.
+
+(************************************)
+(** Right-to-left iterator on lists *)
+(************************************)
+
+Section Fold_Right_Recursor.
+Variables A B : Set.
+Variable f : B -> A -> A.
+Variable a0 : A.
+Fixpoint fold_right (l:list B) : A :=
+  match l with
+  | nil => a0
+  | cons b t => f b (fold_right t)
+  end.
+End Fold_Right_Recursor.
+
+Theorem fold_symmetric :
+ forall (A:Set) (f:A -> A -> A),
+   (forall x y z:A, f x (f y z) = f (f x y) z) ->
+   (forall x y:A, f x y = f y x) ->
+   forall (a0:A) (l:list A), fold_left f l a0 = fold_right f a0 l.
+Proof.
+destruct l as [| a l].
+reflexivity.
+simpl in |- *.
+rewrite <- H0.
+generalize a0 a.
+induction l as [| a3 l IHl]; simpl in |- *.
+trivial.
+intros.
+rewrite H.
+rewrite (H0 a2).
+rewrite <- (H a1).
+rewrite (H0 a1).
+rewrite IHl.
+reflexivity.
+Qed.
+
+End Functions_on_lists.
+
+
+(** Exporting list notations *)
+
+Infix "::" := cons (at level 60, right associativity) : list_scope.
+
+Infix "++" := app (right associativity, at level 60) : list_scope.
+
+Open Scope list_scope.
+
+(** Declare Scope list_scope with key list *)
+Delimit Scope list_scope with list.
+
+Bind Scope list_scope with list.
diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v
new file mode 100644
index 00000000..d5ecad9c
--- /dev/null
+++ b/theories/Lists/ListSet.v
@@ -0,0 +1,398 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: ListSet.v,v 1.13.2.1 2004/07/16 19:31:05 herbelin Exp $ i*)
+
+(** A Library for finite sets, implemented as lists 
+    A Library with similar interface will soon be available under
+    the name TreeSet in the theories/Trees directory *)
+
+(** PolyList is loaded, but not exported.
+    This allow to "hide" the definitions, functions and theorems of PolyList
+    and to see only the ones of ListSet *)
+
+Require Import List.
+
+Set Implicit Arguments.
+
+Section first_definitions.
+
+  Variable A : Set.
+  Hypothesis Aeq_dec : forall x y:A, {x = y} + {x <> y}.
+
+  Definition set := list A.
+
+  Definition empty_set : set := nil.
+
+  Fixpoint set_add (a:A) (x:set) {struct x} : set :=
+    match x with
+    | nil => a :: nil
+    | a1 :: x1 =>
+        match Aeq_dec a a1 with
+        | left _ => a1 :: x1
+        | right _ => a1 :: set_add a x1
+        end
+    end.
+
+
+  Fixpoint set_mem (a:A) (x:set) {struct x} : bool :=
+    match x with
+    | nil => false
+    | a1 :: x1 =>
+        match Aeq_dec a a1 with
+        | left _ => true
+        | right _ => set_mem a x1
+        end
+    end.
+ 
+  (** If [a] belongs to [x], removes [a] from [x]. If not, does nothing *)
+  Fixpoint set_remove (a:A) (x:set) {struct x} : set :=
+    match x with
+    | nil => empty_set
+    | a1 :: x1 =>
+        match Aeq_dec a a1 with
+        | left _ => x1
+        | right _ => a1 :: set_remove a x1
+        end
+    end.
+
+  Fixpoint set_inter (x:set) : set -> set :=
+    match x with
+    | nil => fun y => nil
+    | a1 :: x1 =>
+        fun y =>
+          if set_mem a1 y then a1 :: set_inter x1 y else set_inter x1 y
+    end.
+
+  Fixpoint set_union (x y:set) {struct y} : set :=
+    match y with
+    | nil => x
+    | a1 :: y1 => set_add a1 (set_union x y1)
+    end.
+        
+  (** returns the set of all els of [x] that does not belong to [y] *)
+  Fixpoint set_diff (x y:set) {struct x} : set :=
+    match x with
+    | nil => nil
+    | a1 :: x1 =>
+        if set_mem a1 y then set_diff x1 y else set_add a1 (set_diff x1 y)
+    end.
+   
+
+  Definition set_In : A -> set -> Prop := In (A:=A).
+
+  Lemma set_In_dec : forall (a:A) (x:set), {set_In a x} + {~ set_In a x}.
+
+  Proof.
+    unfold set_In in |- *.
+    (*** Realizer set_mem. Program_all. ***)
+    simple induction x.
+    auto.
+    intros a0 x0 Ha0. case (Aeq_dec a a0); intro eq.
+    rewrite eq; simpl in |- *; auto with datatypes.
+    elim Ha0.
+    auto with datatypes.
+    right; simpl in |- *; unfold not in |- *; intros [Hc1| Hc2];
+     auto with datatypes.
+  Qed.
+
+  Lemma set_mem_ind :
+   forall (B:Set) (P:B -> Prop) (y z:B) (a:A) (x:set),
+     (set_In a x -> P y) -> P z -> P (if set_mem a x then y else z).
+
+  Proof.
+    simple induction x; simpl in |- *; intros.
+    assumption.
+    elim (Aeq_dec a a0); auto with datatypes.
+  Qed.
+
+  Lemma set_mem_ind2 :
+   forall (B:Set) (P:B -> Prop) (y z:B) (a:A) (x:set),
+     (set_In a x -> P y) ->
+     (~ set_In a x -> P z) -> P (if set_mem a x then y else z).
+
+  Proof.
+    simple induction x; simpl in |- *; intros.
+    apply H0; red in |- *; trivial.
+    case (Aeq_dec a a0); auto with datatypes.
+    intro; apply H; intros; auto.
+    apply H1; red in |- *; intro.
+    case H3; auto.
+  Qed.
+
+ 
+  Lemma set_mem_correct1 :
+   forall (a:A) (x:set), set_mem a x = true -> set_In a x.
+  Proof.
+    simple induction x; simpl in |- *.
+    discriminate.
+    intros a0 l; elim (Aeq_dec a a0); auto with datatypes.
+  Qed.
+
+  Lemma set_mem_correct2 :
+   forall (a:A) (x:set), set_In a x -> set_mem a x = true.
+  Proof.
+    simple induction x; simpl in |- *.
+    intro Ha; elim Ha.
+    intros a0 l; elim (Aeq_dec a a0); auto with datatypes.
+    intros H1 H2 [H3| H4].
+    absurd (a0 = a); auto with datatypes.
+    auto with datatypes.
+  Qed.
+
+  Lemma set_mem_complete1 :
+   forall (a:A) (x:set), set_mem a x = false -> ~ set_In a x.
+  Proof.
+    simple induction x; simpl in |- *.
+    tauto.
+    intros a0 l; elim (Aeq_dec a a0).
+    intros; discriminate H0.
+    unfold not in |- *; intros; elim H1; auto with datatypes.
+  Qed.
+
+  Lemma set_mem_complete2 :
+   forall (a:A) (x:set), ~ set_In a x -> set_mem a x = false.
+  Proof.
+    simple induction x; simpl in |- *.
+    tauto.
+    intros a0 l; elim (Aeq_dec a a0).
+    intros; elim H0; auto with datatypes.
+    tauto.
+  Qed.
+
+  Lemma set_add_intro1 :
+   forall (a b:A) (x:set), set_In a x -> set_In a (set_add b x).
+
+  Proof.
+    unfold set_In in |- *; simple induction x; simpl in |- *.
+    auto with datatypes.
+    intros a0 l H [Ha0a| Hal].
+    elim (Aeq_dec b a0); left; assumption.
+    elim (Aeq_dec b a0); right; [ assumption | auto with datatypes ].
+  Qed.
+
+  Lemma set_add_intro2 :
+   forall (a b:A) (x:set), a = b -> set_In a (set_add b x).
+
+  Proof.
+    unfold set_In in |- *; simple induction x; simpl in |- *.
+    auto with datatypes.
+    intros a0 l H Hab.
+    elim (Aeq_dec b a0);
+     [ rewrite Hab; intro Hba0; rewrite Hba0; simpl in |- *;
+        auto with datatypes
+     | auto with datatypes ].
+  Qed.
+
+  Hint Resolve set_add_intro1 set_add_intro2.
+
+  Lemma set_add_intro :
+   forall (a b:A) (x:set), a = b \/ set_In a x -> set_In a (set_add b x).
+  
+  Proof.
+    intros a b x [H1| H2]; auto with datatypes.
+  Qed.
+ 
+  Lemma set_add_elim :
+   forall (a b:A) (x:set), set_In a (set_add b x) -> a = b \/ set_In a x.
+
+  Proof.
+    unfold set_In in |- *.
+    simple induction x.
+    simpl in |- *; intros [H1| H2]; auto with datatypes.
+    simpl in |- *; do 3 intro.
+    elim (Aeq_dec b a0).
+    simpl in |- *; tauto.
+    simpl in |- *; intros; elim H0.
+    trivial with datatypes.
+    tauto.
+    tauto.
+  Qed.
+
+  Lemma set_add_elim2 :
+   forall (a b:A) (x:set), set_In a (set_add b x) -> a <> b -> set_In a x.
+   intros a b x H; case (set_add_elim _ _ _ H); intros; trivial.
+   case H1; trivial.
+   Qed.
+
+  Hint Resolve set_add_intro set_add_elim set_add_elim2.
+
+  Lemma set_add_not_empty : forall (a:A) (x:set), set_add a x <> empty_set.
+  Proof.
+    simple induction x; simpl in |- *.
+    discriminate.
+    intros; elim (Aeq_dec a a0); intros; discriminate.
+  Qed.   
+
+
+  Lemma set_union_intro1 :
+   forall (a:A) (x y:set), set_In a x -> set_In a (set_union x y).
+  Proof.
+    simple induction y; simpl in |- *; auto with datatypes.
+  Qed.
+
+  Lemma set_union_intro2 :
+   forall (a:A) (x y:set), set_In a y -> set_In a (set_union x y).
+  Proof.
+    simple induction y; simpl in |- *.
+    tauto.
+    intros; elim H0; auto with datatypes.
+  Qed.
+
+  Hint Resolve set_union_intro2 set_union_intro1.
+
+  Lemma set_union_intro :
+   forall (a:A) (x y:set),
+     set_In a x \/ set_In a y -> set_In a (set_union x y).
+  Proof.
+    intros; elim H; auto with datatypes.
+  Qed.
+
+  Lemma set_union_elim :
+   forall (a:A) (x y:set),
+     set_In a (set_union x y) -> set_In a x \/ set_In a y.
+  Proof.
+    simple induction y; simpl in |- *.
+    auto with datatypes.
+    intros.
+    generalize (set_add_elim _ _ _ H0).
+    intros [H1| H1].
+    auto with datatypes.
+    tauto.
+  Qed.
+
+  Lemma set_union_emptyL :
+   forall (a:A) (x:set), set_In a (set_union empty_set x) -> set_In a x.
+    intros a x H; case (set_union_elim _ _ _ H); auto || contradiction.
+  Qed.
+
+
+  Lemma set_union_emptyR :
+   forall (a:A) (x:set), set_In a (set_union x empty_set) -> set_In a x.
+    intros a x H; case (set_union_elim _ _ _ H); auto || contradiction.
+  Qed.
+
+
+  Lemma set_inter_intro :
+   forall (a:A) (x y:set),
+     set_In a x -> set_In a y -> set_In a (set_inter x y).
+  Proof.
+    simple induction x.
+    auto with datatypes.
+    simpl in |- *; intros a0 l Hrec y [Ha0a| Hal] Hy.
+    simpl in |- *; rewrite Ha0a.
+    generalize (set_mem_correct1 a y).
+    generalize (set_mem_complete1 a y).
+    elim (set_mem a y); simpl in |- *; intros.
+    auto with datatypes.
+    absurd (set_In a y); auto with datatypes.
+    elim (set_mem a0 y); [ right; auto with datatypes | auto with datatypes ].     
+  Qed.
+
+  Lemma set_inter_elim1 :
+   forall (a:A) (x y:set), set_In a (set_inter x y) -> set_In a x.
+  Proof.
+    simple induction x.
+    auto with datatypes.
+    simpl in |- *; intros a0 l Hrec y.
+    generalize (set_mem_correct1 a0 y).
+    elim (set_mem a0 y); simpl in |- *; intros.
+    elim H0; eauto with datatypes.
+    eauto with datatypes.
+  Qed.
+
+  Lemma set_inter_elim2 :
+   forall (a:A) (x y:set), set_In a (set_inter x y) -> set_In a y.
+  Proof.
+    simple induction x.
+    simpl in |- *; tauto.
+    simpl in |- *; intros a0 l Hrec y.
+    generalize (set_mem_correct1 a0 y).
+    elim (set_mem a0 y); simpl in |- *; intros.
+    elim H0;
+     [ intro Hr; rewrite <- Hr; eauto with datatypes | eauto with datatypes ].
+    eauto with datatypes.
+  Qed.
+
+  Hint Resolve set_inter_elim1 set_inter_elim2.
+
+  Lemma set_inter_elim :
+   forall (a:A) (x y:set),
+     set_In a (set_inter x y) -> set_In a x /\ set_In a y.
+  Proof.
+    eauto with datatypes.
+  Qed. 
+
+  Lemma set_diff_intro :
+   forall (a:A) (x y:set),
+     set_In a x -> ~ set_In a y -> set_In a (set_diff x y).
+  Proof.
+    simple induction x.
+    simpl in |- *; tauto.
+    simpl in |- *; intros a0 l Hrec y [Ha0a| Hal] Hay.
+    rewrite Ha0a; generalize (set_mem_complete2 _ _ Hay).
+    elim (set_mem a y);
+     [ intro Habs; discriminate Habs | auto with datatypes ].
+    elim (set_mem a0 y); auto with datatypes.
+  Qed.
+
+  Lemma set_diff_elim1 :
+   forall (a:A) (x y:set), set_In a (set_diff x y) -> set_In a x.
+  Proof.
+    simple induction x.
+    simpl in |- *; tauto.
+    simpl in |- *; intros a0 l Hrec y; elim (set_mem a0 y).
+    eauto with datatypes.
+    intro; generalize (set_add_elim _ _ _ H).
+    intros [H1| H2]; eauto with datatypes.
+  Qed.
+
+  Lemma set_diff_elim2 :
+   forall (a:A) (x y:set), set_In a (set_diff x y) -> ~ set_In a y.
+  intros a x y; elim x; simpl in |- *.
+  intros; contradiction.
+  intros a0 l Hrec. 
+  apply set_mem_ind2; auto.
+  intros H1 H2; case (set_add_elim _ _ _ H2); intros; auto.
+  rewrite H; trivial.
+  Qed.
+
+  Lemma set_diff_trivial : forall (a:A) (x:set), ~ set_In a (set_diff x x).
+  red in |- *; intros a x H.
+  apply (set_diff_elim2 _ _ _ H).
+  apply (set_diff_elim1 _ _ _ H).
+  Qed.
+
+Hint Resolve set_diff_intro set_diff_trivial.
+
+
+End first_definitions.
+
+Section other_definitions.
+
+  Variables A B : Set.
+
+  Definition set_prod : set A -> set B -> set (A * B) :=
+    list_prod (A:=A) (B:=B).
+
+  (** [B^A], set of applications from [A] to [B] *)
+  Definition set_power : set A -> set B -> set (set (A * B)) :=
+    list_power (A:=A) (B:=B).
+
+  Definition set_map : (A -> B) -> set A -> set B := map (A:=A) (B:=B).
+
+  Definition set_fold_left : (B -> A -> B) -> set A -> B -> B :=
+    fold_left (A:=B) (B:=A).
+
+  Definition set_fold_right (f:A -> B -> B) (x:set A) 
+    (b:B) : B := fold_right f b x.
+
+ 
+End other_definitions.
+
+Unset Implicit Arguments.
\ No newline at end of file
diff --git a/theories/Lists/MonoList.v b/theories/Lists/MonoList.v
new file mode 100755
index 00000000..d639a39d
--- /dev/null
+++ b/theories/Lists/MonoList.v
@@ -0,0 +1,269 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: MonoList.v,v 1.2.2.1 2004/07/16 19:31:05 herbelin Exp $ i*)
+
+(** THIS IS A OLD CONTRIB. IT IS NO LONGER MAINTAINED ***)
+
+Require Import Le.
+
+Parameter List_Dom : Set.
+Definition A := List_Dom.
+
+Inductive list : Set :=
+  | nil : list
+  | cons : A -> list -> list.
+
+Fixpoint app (l m:list) {struct l} : list :=
+  match l return list with
+  | nil => m
+  | cons a l1 => cons a (app l1 m)
+  end.
+
+
+Lemma app_nil_end : forall l:list, l = app l nil.
+Proof. 
+	intro l; elim l; simpl in |- *; auto.
+        simple induction 1; auto.
+Qed.
+Hint Resolve app_nil_end: list v62.
+
+Lemma app_ass : forall l m n:list, app (app l m) n = app l (app m n).
+Proof. 
+	intros l m n; elim l; simpl in |- *; auto with list.
+	simple induction 1; auto with list.
+Qed.
+Hint Resolve app_ass: list v62.
+
+Lemma ass_app : forall l m n:list, app l (app m n) = app (app l m) n.
+Proof. 
+	auto with list.
+Qed.
+Hint Resolve ass_app: list v62.
+
+Definition tail (l:list) : list :=
+  match l return list with
+  | cons _ m => m
+  | _ => nil
+  end.
+                   
+
+Lemma nil_cons : forall (a:A) (m:list), nil <> cons a m.
+  intros; discriminate.
+Qed.
+
+(****************************************)
+(* Length of lists                      *)
+(****************************************)
+
+Fixpoint length (l:list) : nat :=
+  match l return nat with
+  | cons _ m => S (length m)
+  | _ => 0
+  end.
+
+(******************************)
+(* Length order of lists      *)
+(******************************)
+
+Section length_order.
+Definition lel (l m:list) := length l <= length m.
+
+Hint Unfold lel: list.
+
+Variables a b : A.
+Variables l m n : list.
+
+Lemma lel_refl : lel l l.
+Proof. 
+	unfold lel in |- *; auto with list.
+Qed.
+
+Lemma lel_trans : lel l m -> lel m n -> lel l n.
+Proof. 
+	unfold lel in |- *; intros.
+        apply le_trans with (length m); auto with list.
+Qed.
+
+Lemma lel_cons_cons : lel l m -> lel (cons a l) (cons b m).
+Proof. 
+	unfold lel in |- *; simpl in |- *; auto with list arith.
+Qed.
+
+Lemma lel_cons : lel l m -> lel l (cons b m).
+Proof. 
+	unfold lel in |- *; simpl in |- *; auto with list arith.
+Qed.
+
+Lemma lel_tail : lel (cons a l) (cons b m) -> lel l m.
+Proof. 
+	unfold lel in |- *; simpl in |- *; auto with list arith.
+Qed.
+
+Lemma lel_nil : forall l':list, lel l' nil -> nil = l'.
+Proof. 
+	intro l'; elim l'; auto with list arith.
+	intros a' y H H0.
+	(*  <list>nil=(cons a' y)
+	    ============================
+	      H0 : (lel (cons a' y) nil)
+	      H : (lel y nil)->(<list>nil=y)
+	      y : list
+	      a' : A
+	      l' : list *)
+	absurd (S (length y) <= 0); auto with list arith.
+Qed.
+End length_order.
+
+Hint Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons: list
+  v62.
+
+Fixpoint In (a:A) (l:list) {struct l} : Prop :=
+  match l with
+  | nil => False
+  | cons b m => b = a \/ In a m
+  end.
+
+Lemma in_eq : forall (a:A) (l:list), In a (cons a l).
+Proof. 
+	simpl in |- *; auto with list.
+Qed.
+Hint Resolve in_eq: list v62.
+
+Lemma in_cons : forall (a b:A) (l:list), In b l -> In b (cons a l).
+Proof. 
+	simpl in |- *; auto with list.
+Qed.
+Hint Resolve in_cons: list v62.
+
+Lemma in_app_or : forall (l m:list) (a:A), In a (app l m) -> In a l \/ In a m.
+Proof. 
+	intros l m a.
+	elim l; simpl in |- *; auto with list.
+	intros a0 y H H0.
+	(*  ((<A>a0=a)\/(In a y))\/(In a m)
+	    ============================
+	      H0 : (<A>a0=a)\/(In a (app y m))
+	      H : (In a (app y m))->((In a y)\/(In a m))
+	      y : list
+	      a0 : A
+	      a : A
+	      m : list
+	      l : list *)
+	elim H0; auto with list.
+	intro H1.
+	(*  ((<A>a0=a)\/(In a y))\/(In a m)
+	    ============================
+	      H1 : (In a (app y m)) *)
+	elim (H H1); auto with list.
+Qed.
+Hint Immediate in_app_or: list v62.
+
+Lemma in_or_app : forall (l m:list) (a:A), In a l \/ In a m -> In a (app l m).
+Proof. 
+	intros l m a.
+	elim l; simpl in |- *; intro H.
+	(* 1 (In a m)
+	    ============================
+	      H : False\/(In a m)
+	      a : A
+	      m : list
+	      l : list *)
+	elim H; auto with list; intro H0.
+	(*  (In a m)
+	    ============================
+	      H0 : False *)
+	elim H0. (* subProof completed *)
+	intros y H0 H1.
+	(*  2 (<A>H=a)\/(In a (app y m))
+	    ============================
+	      H1 : ((<A>H=a)\/(In a y))\/(In a m)
+	      H0 : ((In a y)\/(In a m))->(In a (app y m))
+	      y : list *)
+	elim H1; auto 4 with list.
+	intro H2.
+	(*  (<A>H=a)\/(In a (app y m))
+	    ============================
+	      H2 : (<A>H=a)\/(In a y) *)
+	elim H2; auto with list.
+Qed.
+Hint Resolve in_or_app: list v62.
+
+Definition incl (l m:list) := forall a:A, In a l -> In a m.
+
+Hint Unfold incl: list v62.
+
+Lemma incl_refl : forall l:list, incl l l.
+Proof. 
+	auto with list.
+Qed.
+Hint Resolve incl_refl: list v62.
+
+Lemma incl_tl : forall (a:A) (l m:list), incl l m -> incl l (cons a m).
+Proof. 
+	auto with list.
+Qed.
+Hint Immediate incl_tl: list v62.
+
+Lemma incl_tran : forall l m n:list, incl l m -> incl m n -> incl l n.
+Proof. 
+	auto with list.
+Qed.
+
+Lemma incl_appl : forall l m n:list, incl l n -> incl l (app n m).
+Proof. 
+	auto with list.
+Qed.
+Hint Immediate incl_appl: list v62.
+
+Lemma incl_appr : forall l m n:list, incl l n -> incl l (app m n).
+Proof. 
+	auto with list.
+Qed.
+Hint Immediate incl_appr: list v62.
+
+Lemma incl_cons :
+ forall (a:A) (l m:list), In a m -> incl l m -> incl (cons a l) m.
+Proof. 
+	unfold incl in |- *; simpl in |- *; intros a l m H H0 a0 H1.
+	(*  (In a0 m)
+	    ============================
+	      H1 : (<A>a=a0)\/(In a0 l)
+	      a0 : A
+	      H0 : (a:A)(In a l)->(In a m)
+	      H : (In a m)
+	      m : list
+	      l : list
+	      a : A *)
+	elim H1.
+	(*  1 (<A>a=a0)->(In a0 m) *)
+	elim H1; auto with list; intro H2.
+	(*  (<A>a=a0)->(In a0 m)
+	    ============================
+	      H2 : <A>a=a0 *)
+	elim H2; auto with list. (* solves subgoal *)
+	(*  2 (In a0 l)->(In a0 m) *)
+	auto with list.
+Qed.
+Hint Resolve incl_cons: list v62.
+
+Lemma incl_app : forall l m n:list, incl l n -> incl m n -> incl (app l m) n.
+Proof. 
+	unfold incl in |- *; simpl in |- *; intros l m n H H0 a H1.
+	(*  (In a n)
+	    ============================
+	      H1 : (In a (app l m))
+	      a : A
+	      H0 : (a:A)(In a m)->(In a n)
+	      H : (a:A)(In a l)->(In a n)
+	      n : list
+	      m : list
+	      l : list *)
+	elim (in_app_or l m a); auto with list.
+Qed.
+Hint Resolve incl_app: list v62.
\ No newline at end of file
diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v
new file mode 100755
index 00000000..3c433ba2
--- /dev/null
+++ b/theories/Lists/Streams.v
@@ -0,0 +1,177 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: Streams.v,v 1.15.2.1 2004/07/16 19:31:05 herbelin Exp $ i*)
+
+Set Implicit Arguments.
+
+(** Streams *)
+
+Section Streams.
+
+Variable A : Set.
+
+CoInductive Stream : Set :=
+    Cons : A -> Stream -> Stream.
+
+
+Definition hd (x:Stream) := match x with
+                            | Cons a _ => a
+                            end.
+
+Definition tl (x:Stream) := match x with
+                            | Cons _ s => s
+                            end.
+
+
+Fixpoint Str_nth_tl (n:nat) (s:Stream) {struct n} : Stream :=
+  match n with
+  | O => s
+  | S m => Str_nth_tl m (tl s)
+  end.
+
+Definition Str_nth (n:nat) (s:Stream) : A := hd (Str_nth_tl n s).
+
+
+Lemma unfold_Stream :
+ forall x:Stream, x = match x with
+                      | Cons a s => Cons a s
+                      end. 
+Proof.
+  intro x.
+  case x.
+  trivial.
+Qed.
+
+Lemma tl_nth_tl :
+ forall (n:nat) (s:Stream), tl (Str_nth_tl n s) = Str_nth_tl n (tl s).
+Proof.
+  simple induction n; simpl in |- *; auto.
+Qed.
+Hint Resolve tl_nth_tl: datatypes v62.
+
+Lemma Str_nth_tl_plus :
+ forall (n m:nat) (s:Stream),
+   Str_nth_tl n (Str_nth_tl m s) = Str_nth_tl (n + m) s.
+simple induction n; simpl in |- *; intros; auto with datatypes.
+rewrite <- H.
+rewrite tl_nth_tl; trivial with datatypes.
+Qed.
+
+Lemma Str_nth_plus :
+ forall (n m:nat) (s:Stream), Str_nth n (Str_nth_tl m s) = Str_nth (n + m) s.
+intros; unfold Str_nth in |- *; rewrite Str_nth_tl_plus;
+ trivial with datatypes.
+Qed.
+
+(** Extensional Equality between two streams  *)
+
+CoInductive EqSt : Stream -> Stream -> Prop :=
+    eqst :
+      forall s1 s2:Stream,
+        hd s1 = hd s2 -> EqSt (tl s1) (tl s2) -> EqSt s1 s2.
+
+(** A coinduction principle *)
+
+Ltac coinduction proof :=
+  cofix proof; intros; constructor;
+   [ clear proof | try (apply proof; clear proof) ].
+
+
+(** Extensional equality is an equivalence relation *)
+
+Theorem EqSt_reflex : forall s:Stream, EqSt s s.
+coinduction EqSt_reflex.
+reflexivity.
+Qed.
+
+Theorem sym_EqSt : forall s1 s2:Stream, EqSt s1 s2 -> EqSt s2 s1.
+coinduction Eq_sym.
+case H; intros; symmetry  in |- *; assumption.
+case H; intros; assumption.
+Qed.
+
+
+Theorem trans_EqSt :
+ forall s1 s2 s3:Stream, EqSt s1 s2 -> EqSt s2 s3 -> EqSt s1 s3.
+coinduction Eq_trans.
+transitivity (hd s2).
+case H; intros; assumption.
+case H0; intros; assumption.
+apply (Eq_trans (tl s1) (tl s2) (tl s3)).
+case H; trivial with datatypes.
+case H0; trivial with datatypes.
+Qed.
+
+(** The definition given is equivalent to require the elements at each
+    position to be equal *)
+
+Theorem eqst_ntheq :
+ forall (n:nat) (s1 s2:Stream), EqSt s1 s2 -> Str_nth n s1 = Str_nth n s2.
+unfold Str_nth in |- *; simple induction n.
+intros s1 s2 H; case H; trivial with datatypes.
+intros m hypind.
+simpl in |- *.
+intros s1 s2 H.
+apply hypind.
+case H; trivial with datatypes.
+Qed.
+
+Theorem ntheq_eqst :
+ forall s1 s2:Stream,
+   (forall n:nat, Str_nth n s1 = Str_nth n s2) -> EqSt s1 s2.
+coinduction Equiv2.
+apply (H 0).
+intros n; apply (H (S n)).
+Qed.
+
+Section Stream_Properties.
+
+Variable P : Stream -> Prop.
+
+(*i
+Inductive Exists : Stream -> Prop :=
+  | Here    : forall x:Stream, P x -> Exists x
+  | Further : forall x:Stream, ~ P x -> Exists (tl x) -> Exists x.
+i*)
+
+Inductive Exists : Stream -> Prop :=
+  | Here : forall x:Stream, P x -> Exists x
+  | Further : forall x:Stream, Exists (tl x) -> Exists x.
+
+CoInductive ForAll : Stream -> Prop :=
+    HereAndFurther : forall x:Stream, P x -> ForAll (tl x) -> ForAll x.
+
+
+Section Co_Induction_ForAll.
+Variable Inv : Stream -> Prop.
+Hypothesis InvThenP : forall x:Stream, Inv x -> P x.
+Hypothesis InvIsStable : forall x:Stream, Inv x -> Inv (tl x).
+
+Theorem ForAll_coind : forall x:Stream, Inv x -> ForAll x.
+coinduction ForAll_coind; auto.
+Qed.
+End Co_Induction_ForAll.
+
+End Stream_Properties.
+
+End Streams.
+
+Section Map.
+Variables A B : Set.
+Variable f : A -> B.
+CoFixpoint map (s:Stream A) : Stream B := Cons (f (hd s)) (map (tl s)).
+End Map.
+
+Section Constant_Stream.
+Variable A : Set.
+Variable a : A.
+CoFixpoint const  : Stream A := Cons a const.
+End Constant_Stream.
+
+Unset Implicit Arguments.
\ No newline at end of file
diff --git a/theories/Lists/TheoryList.v b/theories/Lists/TheoryList.v
new file mode 100755
index 00000000..fbeb97ce
--- /dev/null
+++ b/theories/Lists/TheoryList.v
@@ -0,0 +1,403 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: TheoryList.v,v 1.15.2.1 2004/07/16 19:31:06 herbelin Exp $ i*)
+
+(** Some programs and results about lists following CAML Manual *)
+
+Require Export List.
+Set Implicit Arguments.
+Section Lists.
+
+Variable A : Set.
+
+(**********************)
+(** The null function *)
+(**********************)
+
+Definition Isnil (l:list A) : Prop := nil = l.
+
+Lemma Isnil_nil : Isnil nil.
+red in |- *; auto.
+Qed.
+Hint Resolve Isnil_nil.
+
+Lemma not_Isnil_cons : forall (a:A) (l:list A), ~ Isnil (a :: l).
+unfold Isnil in |- *.
+intros; discriminate.
+Qed.
+
+Hint Resolve Isnil_nil not_Isnil_cons.
+
+Lemma Isnil_dec : forall l:list A, {Isnil l} + {~ Isnil l}.
+intro l; case l; auto.
+(*
+Realizer (fun l => match l with
+  | nil => true
+  | _ => false
+  end).
+*)
+Qed.
+
+(************************)
+(** The Uncons function *)
+(************************)
+
+Lemma Uncons :
+ forall l:list A, {a : A &  {m : list A | a :: m = l}} + {Isnil l}.
+intro l; case l.
+auto.
+intros a m; intros; left; exists a; exists m; reflexivity.
+(*
+Realizer (fun l => match l with
+  | nil => error
+  | (cons a m) => value (a,m)
+  end).
+*)
+Qed.
+
+(********************************)
+(** The head function           *)
+(********************************)
+
+Lemma Hd :
+ forall l:list A, {a : A |  exists m : list A, a :: m = l} + {Isnil l}.
+intro l; case l.
+auto.
+intros a m; intros; left; exists a; exists m; reflexivity.
+(*
+Realizer (fun l => match l with
+  | nil => error
+  | (cons a m) => value a
+  end).
+*)
+Qed.
+
+Lemma Tl :
+ forall l:list A,
+   {m : list A | (exists a : A, a :: m = l) \/ Isnil l /\ Isnil m}.
+intro l; case l.
+exists (nil (A:=A)); auto.
+intros a m; intros; exists m; left; exists a; reflexivity.
+(*
+Realizer (fun l => match l with
+  | nil => nil
+  | (cons a m) => m
+  end).
+*)
+Qed.
+
+(****************************************)
+(** Length of lists                     *)
+(****************************************)
+
+(* length is defined in List *)
+Fixpoint Length_l (l:list A) (n:nat) {struct l} : nat :=
+  match l with
+  | nil => n
+  | _ :: m => Length_l m (S n)
+  end.
+
+(* A tail recursive version *)
+Lemma Length_l_pf : forall (l:list A) (n:nat), {m : nat | n + length l = m}.
+induction l as [| a m lrec].
+intro n; exists n; simpl in |- *; auto.
+intro n; elim (lrec (S n)); simpl in |- *; intros.
+exists x; transitivity (S (n + length m)); auto.
+(*
+Realizer Length_l.
+*)
+Qed.
+
+Lemma Length : forall l:list A, {m : nat | length l = m}.
+intro l. apply (Length_l_pf l 0).
+(*
+Realizer (fun l -> Length_l_pf l O).
+*)
+Qed.
+
+(*******************************)
+(** Members of lists           *)
+(*******************************)
+Inductive In_spec (a:A) : list A -> Prop :=
+  | in_hd : forall l:list A, In_spec a (a :: l)
+  | in_tl : forall (l:list A) (b:A), In a l -> In_spec a (b :: l).
+Hint Resolve in_hd in_tl.
+Hint Unfold In.
+Hint Resolve in_cons.
+
+Theorem In_In_spec : forall (a:A) (l:list A), In a l <-> In_spec a l.
+split.
+elim l;
+ [ intros; contradiction
+ | intros; elim H0; [ intros; rewrite H1; auto | auto ] ].
+intros; elim H; auto.
+Qed.
+
+Inductive AllS (P:A -> Prop) : list A -> Prop :=
+  | allS_nil : AllS P nil
+  | allS_cons : forall (a:A) (l:list A), P a -> AllS P l -> AllS P (a :: l).
+Hint Resolve allS_nil allS_cons.
+
+Hypothesis eqA_dec : forall a b:A, {a = b} + {a <> b}.
+
+Fixpoint mem (a:A) (l:list A) {struct l} : bool :=
+  match l with
+  | nil => false
+  | b :: m => if eqA_dec a b then true else mem a m
+  end.
+
+Hint Unfold In.
+Lemma Mem : forall (a:A) (l:list A), {In a l} + {AllS (fun b:A => b <> a) l}.
+intros a l.
+induction l.
+auto.
+elim (eqA_dec a a0).
+auto.
+simpl in |- *. elim IHl; auto.
+(*
+Realizer mem.
+*)
+Qed.
+
+(*********************************)
+(** Index of elements            *)
+(*********************************)
+
+Require Import Le.
+Require Import Lt.
+
+Inductive nth_spec : list A -> nat -> A -> Prop :=
+  | nth_spec_O : forall (a:A) (l:list A), nth_spec (a :: l) 1 a
+  | nth_spec_S :
+      forall (n:nat) (a b:A) (l:list A),
+        nth_spec l n a -> nth_spec (b :: l) (S n) a.
+Hint Resolve nth_spec_O nth_spec_S.
+
+Inductive fst_nth_spec : list A -> nat -> A -> Prop :=
+  | fst_nth_O : forall (a:A) (l:list A), fst_nth_spec (a :: l) 1 a
+  | fst_nth_S :
+      forall (n:nat) (a b:A) (l:list A),
+        a <> b -> fst_nth_spec l n a -> fst_nth_spec (b :: l) (S n) a.
+Hint Resolve fst_nth_O fst_nth_S.
+
+Lemma fst_nth_nth :
+ forall (l:list A) (n:nat) (a:A), fst_nth_spec l n a -> nth_spec l n a.
+induction 1; auto.
+Qed.
+Hint Immediate fst_nth_nth.
+
+Lemma nth_lt_O : forall (l:list A) (n:nat) (a:A), nth_spec l n a -> 0 < n.
+induction 1; auto.
+Qed.
+
+Lemma nth_le_length :
+ forall (l:list A) (n:nat) (a:A), nth_spec l n a -> n <= length l.
+induction 1; simpl in |- *; auto with arith.
+Qed.
+
+Fixpoint Nth_func (l:list A) (n:nat) {struct l} : Exc A :=
+  match l, n with
+  | a :: _, S O => value a
+  | _ :: l', S (S p) => Nth_func l' (S p)
+  | _, _ => error
+  end.
+
+Lemma Nth :
+ forall (l:list A) (n:nat),
+   {a : A | nth_spec l n a} + {n = 0 \/ length l < n}.
+induction l as [| a l IHl].
+intro n; case n; simpl in |- *; auto with arith.
+intro n; destruct n as [| [| n1]]; simpl in |- *; auto.
+left; exists a; auto.
+destruct (IHl (S n1)) as [[b]| o].
+left; exists b; auto.
+right; destruct o.
+absurd (S n1 = 0); auto.
+auto with arith.
+(*
+Realizer Nth_func.
+*)
+Qed.
+
+Lemma Item :
+ forall (l:list A) (n:nat), {a : A | nth_spec l (S n) a} + {length l <= n}.
+intros l n; case (Nth l (S n)); intro.
+case s; intro a; left; exists a; auto.
+right; case o; intro.
+absurd (S n = 0); auto.
+auto with arith.
+Qed.
+
+Require Import Minus.
+Require Import DecBool.
+
+Fixpoint index_p (a:A) (l:list A) {struct l} : nat -> Exc nat :=
+  match l with
+  | nil => fun p => error
+  | b :: m => fun p => ifdec (eqA_dec a b) (value p) (index_p a m (S p))
+  end.
+
+Lemma Index_p :
+ forall (a:A) (l:list A) (p:nat),
+   {n : nat | fst_nth_spec l (S n - p) a} + {AllS (fun b:A => a <> b) l}.
+induction l as [| b m irec].
+auto.
+intro p.
+destruct (eqA_dec a b) as [e| e].
+left; exists p.
+destruct e; elim minus_Sn_m; trivial; elim minus_n_n; auto with arith.
+destruct (irec (S p)) as [[n H]| ].
+left; exists n; auto with arith.
+elim minus_Sn_m; auto with arith.
+apply lt_le_weak; apply lt_O_minus_lt; apply nth_lt_O with m a;
+ auto with arith.
+auto.
+Qed.
+
+Lemma Index :
+ forall (a:A) (l:list A),
+   {n : nat | fst_nth_spec l n a} + {AllS (fun b:A => a <> b) l}.
+
+intros a l; case (Index_p a l 1); auto.
+intros [n P]; left; exists n; auto.
+rewrite (minus_n_O n); trivial.
+(*
+Realizer (fun a l -> Index_p a l (S O)).
+*)
+Qed.
+
+Section Find_sec.
+Variables R P : A -> Prop.
+
+Inductive InR : list A -> Prop :=
+  | inR_hd : forall (a:A) (l:list A), R a -> InR (a :: l)
+  | inR_tl : forall (a:A) (l:list A), InR l -> InR (a :: l).
+Hint Resolve inR_hd inR_tl.
+
+Definition InR_inv (l:list A) :=
+  match l with
+  | nil => False
+  | b :: m => R b \/ InR m
+  end.
+
+Lemma InR_INV : forall l:list A, InR l -> InR_inv l.
+induction 1; simpl in |- *; auto.
+Qed.
+
+Lemma InR_cons_inv : forall (a:A) (l:list A), InR (a :: l) -> R a \/ InR l.
+intros a l H; exact (InR_INV H).
+Qed.
+
+Lemma InR_or_app : forall l m:list A, InR l \/ InR m -> InR (l ++ m).
+intros l m [| ].
+induction 1; simpl in |- *; auto.
+intro. induction l; simpl in |- *; auto.
+Qed.
+
+Lemma InR_app_or : forall l m:list A, InR (l ++ m) -> InR l \/ InR m.
+intros l m; elim l; simpl in |- *; auto.
+intros b l' Hrec IAc; elim (InR_cons_inv IAc); auto.
+intros; elim Hrec; auto.
+Qed.
+
+Hypothesis RS_dec : forall a:A, {R a} + {P a}.
+
+Fixpoint find (l:list A) : Exc A :=
+  match l with
+  | nil => error
+  | a :: m => ifdec (RS_dec a) (value a) (find m)
+  end.
+
+Lemma Find : forall l:list A, {a : A | In a l &  R a} + {AllS P l}.
+induction l as [| a m [[b H1 H2]| H]]; auto.
+left; exists b; auto.
+destruct (RS_dec a).
+left; exists a; auto.
+auto.
+(*
+Realizer find.
+*)
+Qed.
+
+Variable B : Set.
+Variable T : A -> B -> Prop.
+
+Variable TS_dec : forall a:A, {c : B | T a c} + {P a}.
+
+Fixpoint try_find (l:list A) : Exc B :=
+  match l with
+  | nil => error
+  | a :: l1 =>
+      match TS_dec a with
+      | inleft (exist c _) => value c
+      | inright _ => try_find l1
+      end
+  end.
+
+Lemma Try_find :
+ forall l:list A, {c : B |  exists2 a : A, In a l & T a c} + {AllS P l}.
+induction l as [| a m [[b H1]| H]].
+auto.
+left; exists b; destruct H1 as [a' H2 H3]; exists a'; auto.
+destruct (TS_dec a) as [[c H1]| ].
+left; exists c.
+exists a; auto.
+auto.
+(* 
+Realizer try_find.
+*)
+Qed.
+
+End Find_sec.
+
+Section Assoc_sec.
+
+Variable B : Set.
+Fixpoint assoc (a:A) (l:list (A * B)) {struct l} : 
+ Exc B :=
+  match l with
+  | nil => error
+  | (a', b) :: m => ifdec (eqA_dec a a') (value b) (assoc a m)
+  end.
+
+Inductive AllS_assoc (P:A -> Prop) : list (A * B) -> Prop :=
+  | allS_assoc_nil : AllS_assoc P nil
+  | allS_assoc_cons :
+      forall (a:A) (b:B) (l:list (A * B)),
+        P a -> AllS_assoc P l -> AllS_assoc P ((a, b) :: l).
+
+Hint Resolve allS_assoc_nil allS_assoc_cons.
+
+(* The specification seems too weak: it is enough to return b if the
+   list has at least an element (a,b); probably the intention is to have
+   the specification
+
+   (a:A)(l:(list A*B)){b:B|(In_spec (a,b) l)}+{(AllS_assoc [a':A]~(a=a') l)}.
+*)
+
+Lemma Assoc :
+ forall (a:A) (l:list (A * B)), B + {AllS_assoc (fun a':A => a <> a') l}.
+induction l as [| [a' b] m assrec]. auto.
+destruct (eqA_dec a a').
+left; exact b.
+destruct assrec as [b'| ].
+left; exact b'.
+right; auto.
+(*
+Realizer assoc.
+*)
+Qed.
+
+End Assoc_sec.
+
+End Lists.
+
+Hint Resolve Isnil_nil not_Isnil_cons in_hd in_tl in_cons allS_nil allS_cons:
+  datatypes.
+Hint Immediate fst_nth_nth: datatypes.
diff --git a/theories/Lists/intro.tex b/theories/Lists/intro.tex
new file mode 100755
index 00000000..344bba59
--- /dev/null
+++ b/theories/Lists/intro.tex
@@ -0,0 +1,24 @@
+\section{Lists}\label{Lists}
+
+This library includes the following files:
+
+\begin{itemize}
+
+\item {\tt List.v} THIS OLD LIBRARY IS HERE ONLY FOR COMPATIBILITY
+  WITH OLDER VERSIONS OF COQS. THE USER SHOULD USE POLYLIST INSTEAD.
+
+\item {\tt PolyList.v} contains definitions of (polymorphic) lists, 
+  functions on lists such as head, tail, map, append and prove some
+  properties of these functions. Implicit arguments are used in this
+  library, so you should read the Referance Manual about implicit
+  arguments before using it.
+
+\item {\tt TheoryList.v} contains complementary results on lists. Here
+  a more theoric point of view is assumed : one extracts functions
+  from propositions, rather than defining functions and then prove them.
+
+\item {\tt Streams.v} defines the type of infinite lists (streams). It is a
+  coinductive type. Basic facts are stated and proved. The streams are
+  also polymorphic.
+
+\end{itemize}