Imported Upstream version 8.0pl1upstream/8.0pl1

8 files changed, 1176 insertions, 0 deletions

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
new file mode 100755
index 00000000..6aeabe13
--- /dev/null
+++ b/theories/Init/Datatypes.v
@@ -0,0 +1,121 @@
+(************************************************************************)
+(*  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: Datatypes.v,v 1.26.2.1 2004/07/16 19:31:03 herbelin Exp $ i*)
+
+Require Import Notations.
+Require Import Logic.
+
+Set Implicit Arguments.
+
+(** [unit] is a singleton datatype with sole inhabitant [tt] *)
+
+Inductive unit : Set :=
+    tt : unit.
+
+(** [bool] is the datatype of the booleans values [true] and [false] *)
+
+Inductive bool : Set :=
+  | true : bool
+  | false : bool.
+
+Add Printing If bool.
+
+(** [nat] is the datatype of natural numbers built from [O] and successor [S];
+    note that zero is the letter O, not the numeral 0 *)
+
+Inductive nat : Set :=
+  | O : nat
+  | S : nat -> nat.
+
+Delimit Scope nat_scope with nat.
+Bind Scope nat_scope with nat.
+Arguments Scope S [nat_scope].
+
+(** [Empty_set] has no inhabitant *)
+
+Inductive Empty_set : Set :=.
+
+(** [identity A a] is the family of datatypes on [A] whose sole non-empty
+    member is the singleton datatype [identity A a a] whose
+    sole inhabitant is denoted [refl_identity A a] *)
+
+Inductive identity (A:Type) (a:A) : A -> Set :=
+    refl_identity : identity (A:=A) a a.
+Hint Resolve refl_identity: core v62.
+
+Implicit Arguments identity_ind [A].
+Implicit Arguments identity_rec [A].
+Implicit Arguments identity_rect [A].
+
+(** [option A] is the extension of A with a dummy element None *)
+
+Inductive option (A:Set) : Set :=
+  | Some : A -> option A
+  | None : option A.
+
+Implicit Arguments None [A].
+
+(** [sum A B], equivalently [A + B], is the disjoint sum of [A] and [B] *)
+(* Syntax defined in Specif.v *)
+Inductive sum (A B:Set) : Set :=
+  | inl : A -> sum A B
+  | inr : B -> sum A B.
+
+Notation "x + y" := (sum x y) : type_scope.
+
+(** [prod A B], written [A * B], is the product of [A] and [B];
+    the pair [pair A B a b] of [a] and [b] is abbreviated [(a,b)] *)
+
+Inductive prod (A B:Set) : Set :=
+    pair : A -> B -> prod A B.
+Add Printing Let prod.
+
+Notation "x * y" := (prod x y) : type_scope.
+Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
+
+Section projections.
+   Variables A B : Set.
+   Definition fst (p:A * B) := match p with
+                               | (x, y) => x
+                               end.
+   Definition snd (p:A * B) := match p with
+                               | (x, y) => y
+                               end.
+End projections. 
+
+Hint Resolve pair inl inr: core v62.
+
+Lemma surjective_pairing :
+ forall (A B:Set) (p:A * B), p = pair (fst p) (snd p).
+Proof.
+destruct p; reflexivity.
+Qed.
+
+Lemma injective_projections :
+ forall (A B:Set) (p1 p2:A * B),
+   fst p1 = fst p2 -> snd p1 = snd p2 -> p1 = p2.
+Proof.
+destruct p1; destruct p2; simpl in |- *; intros Hfst Hsnd.
+rewrite Hfst; rewrite Hsnd; reflexivity. 
+Qed.
+
+
+(** Comparison *)
+
+Inductive comparison : Set :=
+  | Eq : comparison
+  | Lt : comparison
+  | Gt : comparison.
+
+Definition CompOpp (r:comparison) :=
+  match r with
+  | Eq => Eq
+  | Lt => Gt
+  | Gt => Lt
+  end.
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
new file mode 100755
index 00000000..bae8d4a1
--- /dev/null
+++ b/theories/Init/Logic.v
@@ -0,0 +1,279 @@
+(************************************************************************)
+(*  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: Logic.v,v 1.29.2.1 2004/07/16 19:31:03 herbelin Exp $ i*)
+
+Set Implicit Arguments.
+
+Require Import Notations.
+
+(** * Propositional connectives *)
+
+(** [True] is the always true proposition *)
+Inductive True : Prop :=
+    I : True. 
+
+(** [False] is the always false proposition *)
+Inductive False : Prop :=. 
+
+(** [not A], written [~A], is the negation of [A] *)
+Definition not (A:Prop) := A -> False.
+
+Notation "~ x" := (not x) : type_scope.
+
+Hint Unfold not: core.
+
+Inductive and (A B:Prop) : Prop :=
+    conj : A -> B -> A /\ B 
+ where "A /\ B" := (and A B) : type_scope.
+
+
+Section Conjunction.
+
+  (** [and A B], written [A /\ B], is the conjunction of [A] and [B]
+
+      [conj p q] is a proof of [A /\ B] as soon as 
+      [p] is a proof of [A] and [q] a proof of [B]
+
+      [proj1] and [proj2] are first and second projections of a conjunction *)
+
+  Variables A B : Prop.
+
+  Theorem proj1 : A /\ B -> A.
+  Proof.
+  destruct 1; trivial.
+  Qed.
+
+  Theorem proj2 : A /\ B -> B.
+  Proof.
+  destruct 1; trivial.
+  Qed.
+
+End Conjunction.
+
+(** [or A B], written [A \/ B], is the disjunction of [A] and [B] *)
+
+Inductive or (A B:Prop) : Prop :=
+  | or_introl : A -> A \/ B
+  | or_intror : B -> A \/ B 
+ where "A \/ B" := (or A B) : type_scope.
+
+(** [iff A B], written [A <-> B], expresses the equivalence of [A] and [B] *)
+
+Definition iff (A B:Prop) := (A -> B) /\ (B -> A).
+
+Notation "A <-> B" := (iff A B) : type_scope.
+
+Section Equivalence.
+
+Theorem iff_refl : forall A:Prop, A <-> A.
+  Proof.
+    split; auto.
+  Qed.
+
+Theorem iff_trans : forall A B C:Prop, (A <-> B) -> (B <-> C) -> (A <-> C).
+  Proof.
+    intros A B C [H1 H2] [H3 H4]; split; auto.
+  Qed.
+
+Theorem iff_sym : forall A B:Prop, (A <-> B) -> (B <-> A).
+  Proof.
+    intros A B [H1 H2]; split; auto.
+  Qed.
+
+End Equivalence.
+
+(** [(IF_then_else P Q R)], written [IF P then Q else R] denotes
+    either [P] and [Q], or [~P] and [Q] *)
+
+Definition IF_then_else (P Q R:Prop) := P /\ Q \/ ~ P /\ R.
+
+Notation "'IF' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3)
+  (at level 200) : type_scope.
+
+(** * First-order quantifiers
+  - [ex A P], or simply [exists x, P x], expresses the existence of an 
+      [x] of type [A] which satisfies the predicate [P] ([A] is of type 
+      [Set]). This is existential quantification.
+  - [ex2 A P Q], or simply [exists2 x, P x & Q x], expresses the
+      existence of an [x] of type [A] which satisfies both the predicates
+      [P] and [Q].
+  - Universal quantification (especially first-order one) is normally 
+    written [forall x:A, P x]. For duality with existential quantification, 
+    the construction [all P] is provided too.
+*)
+
+Inductive ex (A:Type) (P:A -> Prop) : Prop :=
+    ex_intro : forall x:A, P x -> ex (A:=A) P.
+
+Inductive ex2 (A:Type) (P Q:A -> Prop) : Prop :=
+    ex_intro2 : forall x:A, P x -> Q x -> ex2 (A:=A) P Q.
+
+Definition all (A:Type) (P:A -> Prop) := forall x:A, P x. 
+
+(* Rule order is important to give printing priority to fully typed exists *)
+
+Notation "'exists' x , p" := (ex (fun x => p))
+  (at level 200, x ident) : type_scope.
+Notation "'exists' x : t , p" := (ex (fun x:t => p))
+  (at level 200, x ident, format "'exists'  '/  ' x  :  t ,  '/  ' p")
+  : type_scope.
+
+Notation "'exists2' x , p & q" := (ex2 (fun x => p) (fun x => q))
+  (at level 200, x ident, p at level 200) : type_scope.
+Notation "'exists2' x : t , p & q" := (ex2 (fun x:t => p) (fun x:t => q))
+  (at level 200, x ident, t at level 200, p at level 200,
+   format "'exists2'  '/  ' x  :  t ,  '/  ' '[' p  &  '/' q ']'")
+  : type_scope.
+
+
+(** Derived rules for universal quantification *)
+
+Section universal_quantification.
+
+  Variable A : Type.
+  Variable P : A -> Prop.
+
+  Theorem inst : forall x:A, all (fun x => P x) -> P x.
+  Proof.
+  unfold all in |- *; auto.
+  Qed.
+
+  Theorem gen : forall (B:Prop) (f:forall y:A, B -> P y), B -> all P.
+  Proof.
+  red in |- *; auto.
+  Qed.
+
+End universal_quantification.
+
+(** * Equality *)
+
+(** [eq x y], or simply [x=y], expresses the (Leibniz') equality
+    of [x] and [y]. Both [x] and [y] must belong to the same type [A].
+    The definition is inductive and states the reflexivity of the equality.
+    The others properties (symmetry, transitivity, replacement of 
+    equals) are proved below. The type of [x] and [y] can be made explicit
+    using the notation [x = y :> A] *)
+
+Inductive eq (A:Type) (x:A) : A -> Prop :=
+    refl_equal : x = x :>A 
+ where "x = y :> A" := (@eq A x y) : type_scope.
+
+Notation "x = y" := (x = y :>_) : type_scope.
+Notation "x <> y  :> T" := (~ x = y :>T) : type_scope.
+Notation "x <> y" := (x <> y :>_) : type_scope.
+
+Implicit Arguments eq_ind [A].
+Implicit Arguments eq_rec [A].
+Implicit Arguments eq_rect [A].
+
+Hint Resolve I conj or_introl or_intror refl_equal: core v62.
+Hint Resolve ex_intro ex_intro2: core v62.
+
+Section Logic_lemmas.
+
+  Theorem absurd : forall A C:Prop, A -> ~ A -> C.
+  Proof.
+    unfold not in |- *; intros A C h1 h2.
+    destruct (h2 h1).
+  Qed.
+
+  Section equality.
+    Variables A B : Type.
+    Variable f : A -> B.
+    Variables x y z : A.
+
+    Theorem sym_eq : x = y -> y = x.
+    Proof.
+     destruct 1; trivial.
+    Defined.
+    Opaque sym_eq.
+
+    Theorem trans_eq : x = y -> y = z -> x = z.
+    Proof.
+     destruct 2; trivial.
+    Defined.
+    Opaque trans_eq.
+
+    Theorem f_equal : x = y -> f x = f y.
+    Proof.
+     destruct 1; trivial.
+    Defined.
+    Opaque f_equal.
+
+    Theorem sym_not_eq : x <> y -> y <> x.
+    Proof.
+     red in |- *; intros h1 h2; apply h1; destruct h2; trivial.
+    Qed.
+
+    Definition sym_equal := sym_eq.
+    Definition sym_not_equal := sym_not_eq.
+    Definition trans_equal := trans_eq.
+
+  End equality.
+
+(* Is now a primitive principle 
+  Theorem eq_rect: (A:Type)(x:A)(P:A->Type)(P x)->(y:A)(eq ? x y)->(P y).
+  Proof.
+   Intros.
+   Cut (identity A x y).
+   NewDestruct 1; Auto.
+   NewDestruct H; Auto.
+  Qed.
+*)
+
+  Definition eq_ind_r :
+    forall (A:Type) (x:A) (P:A -> Prop), P x -> forall y:A, y = x -> P y.
+   intros A x P H y H0; elim sym_eq with (1 := H0); assumption.
+  Defined.
+
+  Definition eq_rec_r :
+    forall (A:Type) (x:A) (P:A -> Set), P x -> forall y:A, y = x -> P y.
+    intros A x P H y H0; elim sym_eq with (1 := H0); assumption.
+  Defined.
+
+  Definition eq_rect_r :
+    forall (A:Type) (x:A) (P:A -> Type), P x -> forall y:A, y = x -> P y.
+    intros A x P H y H0; elim sym_eq with (1 := H0); assumption.
+  Defined.
+End Logic_lemmas.
+
+Theorem f_equal2 :
+ forall (A1 A2 B:Type) (f:A1 -> A2 -> B) (x1 y1:A1) 
+   (x2 y2:A2), x1 = y1 -> x2 = y2 -> f x1 x2 = f y1 y2.
+Proof.
+  destruct 1; destruct 1; reflexivity.
+Qed.
+
+Theorem f_equal3 :
+ forall (A1 A2 A3 B:Type) (f:A1 -> A2 -> A3 -> B) (x1 y1:A1) 
+   (x2 y2:A2) (x3 y3:A3),
+   x1 = y1 -> x2 = y2 -> x3 = y3 -> f x1 x2 x3 = f y1 y2 y3.
+Proof.
+  destruct 1; destruct 1; destruct 1; reflexivity.
+Qed.
+
+Theorem f_equal4 :
+ forall (A1 A2 A3 A4 B:Type) (f:A1 -> A2 -> A3 -> A4 -> B) 
+   (x1 y1:A1) (x2 y2:A2) (x3 y3:A3) (x4 y4:A4),
+   x1 = y1 -> x2 = y2 -> x3 = y3 -> x4 = y4 -> f x1 x2 x3 x4 = f y1 y2 y3 y4.
+Proof.
+  destruct 1; destruct 1; destruct 1; destruct 1; reflexivity.
+Qed.
+
+Theorem f_equal5 :
+ forall (A1 A2 A3 A4 A5 B:Type) (f:A1 -> A2 -> A3 -> A4 -> A5 -> B)
+   (x1 y1:A1) (x2 y2:A2) (x3 y3:A3) (x4 y4:A4) (x5 y5:A5),
+   x1 = y1 ->
+   x2 = y2 ->
+   x3 = y3 -> x4 = y4 -> x5 = y5 -> f x1 x2 x3 x4 x5 = f y1 y2 y3 y4 y5.
+Proof.
+  destruct 1; destruct 1; destruct 1; destruct 1; destruct 1; reflexivity.
+Qed.
+
+Hint Immediate sym_eq sym_not_eq: core v62.
diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v
new file mode 100755
index 00000000..0e62e842
--- /dev/null
+++ b/theories/Init/Logic_Type.v
@@ -0,0 +1,89 @@
+(************************************************************************)
+(*  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: Logic_Type.v,v 1.19.2.1 2004/07/16 19:31:03 herbelin Exp $ i*)
+
+Set Implicit Arguments.
+
+(** This module defines quantification on the world [Type]
+    ([Logic.v] was defining it on the world [Set]) *)
+
+Require Import Datatypes.
+Require Export Logic.
+
+Definition notT (A:Type) := A -> False.
+
+Section identity_is_a_congruence.
+
+ Variables A B : Type.
+ Variable f : A -> B.
+
+ Variables x y z : A.
+ 
+ Lemma sym_id : identity x y -> identity y x.
+ Proof.
+  destruct 1; trivial.
+ Qed.
+
+ Lemma trans_id : identity x y -> identity y z -> identity x z.
+ Proof.
+  destruct 2; trivial.
+ Qed.
+
+ Lemma congr_id : identity x y -> identity (f x) (f y).
+ Proof.
+  destruct 1; trivial.
+ Qed.
+
+ Lemma sym_not_id : notT (identity x y) -> notT (identity y x).
+ Proof.
+  red in |- *; intros H H'; apply H; destruct H'; trivial.
+ Qed.
+
+End identity_is_a_congruence.
+
+Definition identity_ind_r :
+  forall (A:Type) (a:A) (P:A -> Prop), P a -> forall y:A, identity y a -> P y.
+ intros A x P H y H0; case sym_id with (1 := H0); trivial.
+Defined.
+
+Definition identity_rec_r :
+  forall (A:Type) (a:A) (P:A -> Set), P a -> forall y:A, identity y a -> P y.
+ intros A x P H y H0; case sym_id with (1 := H0); trivial.
+Defined.
+
+Definition identity_rect_r :
+  forall (A:Type) (a:A) (P:A -> Type), P a -> forall y:A, identity y a -> P y.
+ intros A x P H y H0; case sym_id with (1 := H0); trivial.
+Defined.
+
+Inductive prodT (A B:Type) : Type :=
+    pairT : A -> B -> prodT A B.
+
+Section prodT_proj.
+
+  Variables A B : Type.
+
+  Definition fstT (H:prodT A B) := match H with
+                                   | pairT x _ => x
+                                   end.
+  Definition sndT (H:prodT A B) := match H with
+                                   | pairT _ y => y
+                                   end.
+
+End prodT_proj.
+
+Definition prodT_uncurry (A B C:Type) (f:prodT A B -> C) 
+  (x:A) (y:B) : C := f (pairT x y).
+
+Definition prodT_curry (A B C:Type) (f:A -> B -> C) 
+  (p:prodT A B) : C := match p with
+                       | pairT x y => f x y
+                       end.
+
+Hint Immediate sym_id sym_not_id: core v62.
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
new file mode 100644
index 00000000..2e7cb1fc
--- /dev/null
+++ b/theories/Init/Notations.v
@@ -0,0 +1,78 @@
+(************************************************************************)
+(*  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: Notations.v,v 1.24.2.1 2004/07/16 19:31:03 herbelin Exp $ i*)
+
+(** These are the notations whose level and associativity is imposed by Coq *)
+
+(** Notations for logical connectives *)
+
+Reserved Notation "x <-> y" (at level 95, no associativity).
+Reserved Notation "x /\ y" (at level 80, right associativity).
+Reserved Notation "x \/ y" (at level 85, right associativity).
+Reserved Notation "~ x" (at level 75, right associativity).
+
+(** Notations for equality and inequalities *)
+
+Reserved Notation "x = y  :> T"
+(at level 70, y at next level, no associativity).
+Reserved Notation "x = y" (at level 70, no associativity).
+Reserved Notation "x = y = z"
+(at level 70, no associativity, y at next level).
+
+Reserved Notation "x <> y  :> T"
+(at level 70, y at next level, no associativity).
+Reserved Notation "x <> y" (at level 70, no associativity).
+
+Reserved Notation "x <= y" (at level 70, no associativity).
+Reserved Notation "x < y" (at level 70, no associativity).
+Reserved Notation "x >= y" (at level 70, no associativity).
+Reserved Notation "x > y" (at level 70, no associativity).
+
+Reserved Notation "x <= y <= z" (at level 70, y at next level).
+Reserved Notation "x <= y < z" (at level 70, y at next level).
+Reserved Notation "x < y < z" (at level 70, y at next level).
+Reserved Notation "x < y <= z" (at level 70, y at next level).
+
+(** Arithmetical notations (also used for type constructors) *)
+
+Reserved Notation "x + y" (at level 50, left associativity).
+Reserved Notation "x - y" (at level 50, left associativity).
+Reserved Notation "x * y" (at level 40, left associativity).
+Reserved Notation "x / y" (at level 40, left associativity).
+Reserved Notation "- x" (at level 35, right associativity).
+Reserved Notation "/ x" (at level 35, right associativity).
+Reserved Notation "x ^ y" (at level 30, right associativity).
+
+(** Notations for pairs *)
+
+Reserved Notation "( x , y , .. , z )" (at level 0).
+
+(** Notation "{ x }" is reserved and has a special status as component
+    of other notations; it is at level 0 to factor with {x:A|P} etc *)
+
+Reserved Notation "{ x }" (at level 0, x at level 99).
+
+(** Notations for sum-types *)
+
+Reserved Notation "{ A } + { B }" (at level 50, left associativity).
+Reserved Notation "A + { B }" (at level 50, left associativity).
+
+(** Notations for sigma-types or subsets *)
+
+Reserved Notation "{ x : A  |  P }" (at level 0, x at level 99).
+Reserved Notation "{ x : A  |  P  &  Q }" (at level 0, x at level 99).
+
+Reserved Notation "{ x : A  &  P }" (at level 0, x at level 99).
+Reserved Notation "{ x : A  &  P  &  Q }" (at level 0, x at level 99).
+
+Delimit Scope type_scope with type.
+Delimit Scope core_scope with core.
+
+Open Scope core_scope.
+Open Scope type_scope.
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
new file mode 100755
index 00000000..789a020f
--- /dev/null
+++ b/theories/Init/Peano.v
@@ -0,0 +1,210 @@
+(************************************************************************)
+(*  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: Peano.v,v 1.23.2.1 2004/07/16 19:31:03 herbelin Exp $ i*)
+
+(** Natural numbers [nat] built from [O] and [S] are defined in Datatypes.v *)
+
+(** This module defines the following operations on natural numbers :
+    - predecessor [pred]
+    - addition [plus]
+    - multiplication [mult]
+    - less or equal order [le]
+    - less [lt]
+    - greater or equal [ge]
+    - greater [gt]
+
+   This module states various lemmas and theorems about natural numbers,
+   including Peano's axioms of arithmetic (in Coq, these are in fact provable)
+   Case analysis on [nat] and induction on [nat * nat] are provided too *)
+
+Require Import Notations.
+Require Import Datatypes.
+Require Import Logic.
+
+Open Scope nat_scope.
+
+Definition eq_S := f_equal S.
+
+Hint Resolve (f_equal S): v62.
+Hint Resolve (f_equal (A:=nat)): core.
+
+(** The predecessor function *)
+
+Definition pred (n:nat) : nat := match n with
+                                 | O => 0
+                                 | S u => u
+                                 end.
+Hint Resolve (f_equal pred): v62.
+
+Theorem pred_Sn : forall n:nat, n = pred (S n).
+Proof.
+  auto.
+Qed.
+
+Theorem eq_add_S : forall n m:nat, S n = S m -> n = m.
+Proof.
+  intros n m H; change (pred (S n) = pred (S m)) in |- *; auto.
+Qed.
+
+Hint Immediate eq_add_S: core v62.
+
+(** A consequence of the previous axioms *)
+
+Theorem not_eq_S : forall n m:nat, n <> m -> S n <> S m.
+Proof.
+  red in |- *; auto.
+Qed.
+Hint Resolve not_eq_S: core v62.
+
+Definition IsSucc (n:nat) : Prop :=
+  match n with
+  | O => False
+  | S p => True
+  end.
+
+
+Theorem O_S : forall n:nat, 0 <> S n.
+Proof.
+  red in |- *; intros n H.
+  change (IsSucc 0) in |- *.
+  rewrite <- (sym_eq (x:=0) (y:=(S n))); [ exact I | assumption ].
+Qed.
+Hint Resolve O_S: core v62.
+
+Theorem n_Sn : forall n:nat, n <> S n.
+Proof.
+  induction n; auto.
+Qed.
+Hint Resolve n_Sn: core v62.
+
+(** Addition *)
+
+Fixpoint plus (n m:nat) {struct n} : nat :=
+  match n with
+  | O => m
+  | S p => S (plus p m)
+  end.
+Hint Resolve (f_equal2 plus): v62.
+Hint Resolve (f_equal2 (A1:=nat) (A2:=nat)): core.
+
+Infix "+" := plus : nat_scope.
+
+Lemma plus_n_O : forall n:nat, n = n + 0.
+Proof.
+  induction n; simpl in |- *; auto.
+Qed.
+Hint Resolve plus_n_O: core v62.
+
+Lemma plus_O_n : forall n:nat, 0 + n = n.
+Proof.
+  auto.
+Qed.
+
+Lemma plus_n_Sm : forall n m:nat, S (n + m) = n + S m.
+Proof.
+  intros n m; induction n; simpl in |- *; auto.
+Qed.
+Hint Resolve plus_n_Sm: core v62.
+
+Lemma plus_Sn_m : forall n m:nat, S n + m = S (n + m).
+Proof.
+  auto.
+Qed.
+
+(** Multiplication *)
+
+Fixpoint mult (n m:nat) {struct n} : nat :=
+  match n with
+  | O => 0
+  | S p => m + mult p m
+  end.
+Hint Resolve (f_equal2 mult): core v62.
+
+Infix "*" := mult : nat_scope.
+
+Lemma mult_n_O : forall n:nat, 0 = n * 0.
+Proof.
+  induction n; simpl in |- *; auto.
+Qed.
+Hint Resolve mult_n_O: core v62.
+
+Lemma mult_n_Sm : forall n m:nat, n * m + n = n * S m.
+Proof.
+  intros; induction n as [| p H]; simpl in |- *; auto.
+  destruct H; rewrite <- plus_n_Sm; apply (f_equal S).
+  pattern m at 1 3 in |- *; elim m; simpl in |- *; auto.
+Qed.
+Hint Resolve mult_n_Sm: core v62.
+
+(** Definition of subtraction on [nat] : [m-n] is [0] if [n>=m] *)
+
+Fixpoint minus (n m:nat) {struct n} : nat :=
+  match n, m with
+  | O, _ => 0
+  | S k, O => S k
+  | S k, S l => minus k l
+  end. 
+
+Infix "-" := minus : nat_scope.
+
+(** Definition of the usual orders, the basic properties of [le] and [lt] 
+    can be found in files Le and Lt *)
+
+(** An inductive definition to define the order *)
+
+Inductive le (n:nat) : nat -> Prop :=
+  | le_n : le n n
+  | le_S : forall m:nat, le n m -> le n (S m).
+
+Infix "<=" := le : nat_scope.
+
+Hint Constructors le: core v62.
+(*i equivalent to : "Hints Resolve le_n le_S : core v62." i*)
+
+Definition lt (n m:nat) := S n <= m.
+Hint Unfold lt: core v62.
+
+Infix "<" := lt : nat_scope.
+
+Definition ge (n m:nat) := m <= n.
+Hint Unfold ge: core v62.
+
+Infix ">=" := ge : nat_scope.
+
+Definition gt (n m:nat) := m < n.
+Hint Unfold gt: core v62.
+
+Infix ">" := gt : nat_scope.
+
+Notation "x <= y <= z" := (x <= y /\ y <= z) : nat_scope.
+Notation "x <= y < z" := (x <= y /\ y < z) : nat_scope.
+Notation "x < y < z" := (x < y /\ y < z) : nat_scope.
+Notation "x < y <= z" := (x < y /\ y <= z) : nat_scope.
+
+(** Pattern-Matching on natural numbers *)
+
+Theorem nat_case :
+ forall (n:nat) (P:nat -> Prop), P 0 -> (forall m:nat, P (S m)) -> P n.
+Proof.
+  induction n; auto.
+Qed.
+
+(** Principle of double induction *)
+
+Theorem nat_double_ind :
+ forall R:nat -> nat -> Prop,
+   (forall n:nat, R 0 n) ->
+   (forall n:nat, R (S n) 0) ->
+   (forall n m:nat, R n m -> R (S n) (S m)) -> forall n m:nat, R n m.
+Proof.
+  induction n; auto.
+  destruct m as [| n0]; auto.
+Qed.
+
+(** Notations *)
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
new file mode 100755
index 00000000..2fe520c4
--- /dev/null
+++ b/theories/Init/Prelude.v
@@ -0,0 +1,16 @@
+(************************************************************************)
+(*  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: Prelude.v,v 1.11.2.1 2004/07/16 19:31:03 herbelin Exp $ i*)
+
+Require Export Notations.
+Require Export Logic.
+Require Export Datatypes.
+Require Export Specif.
+Require Export Peano.
+Require Export Wf.
\ No newline at end of file
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
new file mode 100755
index 00000000..6855e689
--- /dev/null
+++ b/theories/Init/Specif.v
@@ -0,0 +1,212 @@
+(************************************************************************)
+(*  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: Specif.v,v 1.25.2.1 2004/07/16 19:31:04 herbelin Exp $ i*)
+
+Set Implicit Arguments.
+
+(** Basic specifications : Sets containing logical information *)
+
+Require Import Notations.
+Require Import Datatypes.
+Require Import Logic.
+
+(** Subsets *)
+
+(** [(sig A P)], or more suggestively [{x:A | (P x)}], denotes the subset 
+    of elements of the Set [A] which satisfy the predicate [P].
+    Similarly [(sig2 A P Q)], or [{x:A | (P x) & (Q x)}], denotes the subset 
+    of elements of the Set [A] which satisfy both [P] and [Q]. *)
+
+Inductive sig (A:Set) (P:A -> Prop) : Set :=
+    exist : forall x:A, P x -> sig (A:=A) P.
+
+Inductive sig2 (A:Set) (P Q:A -> Prop) : Set :=
+    exist2 : forall x:A, P x -> Q x -> sig2 (A:=A) P Q.
+
+(** [(sigS A P)], or more suggestively [{x:A & (P x)}], is a subtle variant
+    of subset where [P] is now of type [Set].
+    Similarly for [(sigS2 A P Q)], also written [{x:A & (P x) & (Q x)}]. *)
+     
+Inductive sigS (A:Set) (P:A -> Set) : Set :=
+    existS : forall x:A, P x -> sigS (A:=A) P.
+
+Inductive sigS2 (A:Set) (P Q:A -> Set) : Set :=
+    existS2 : forall x:A, P x -> Q x -> sigS2 (A:=A) P Q.
+
+Arguments Scope sig [type_scope type_scope].
+Arguments Scope sig2 [type_scope type_scope type_scope].
+Arguments Scope sigS [type_scope type_scope].
+Arguments Scope sigS2 [type_scope type_scope type_scope].
+
+Notation "{ x : A  |  P }" := (sig (fun x:A => P)) : type_scope.
+Notation "{ x : A  |  P  &  Q }" := (sig2 (fun x:A => P) (fun x:A => Q)) :
+  type_scope.
+Notation "{ x : A  &  P }" := (sigS (fun x:A => P)) : type_scope.
+Notation "{ x : A  &  P  &  Q }" := (sigS2 (fun x:A => P) (fun x:A => Q)) :
+  type_scope.
+
+Add Printing Let sig.
+Add Printing Let sig2.
+Add Printing Let sigS.
+Add Printing Let sigS2.
+
+
+(** Projections of sig *)
+
+Section Subset_projections.
+
+  Variable A : Set.
+  Variable P : A -> Prop.
+
+  Definition proj1_sig (e:sig P) := match e with
+                                    | exist a b => a
+                                    end.
+
+  Definition proj2_sig (e:sig P) :=
+    match e return P (proj1_sig e) with
+    | exist a b => b
+    end.
+
+End Subset_projections.
+
+
+(** Projections of sigS *)
+
+Section Projections.
+
+  Variable A : Set.
+  Variable P : A -> Set.
+
+ (** An element [y] of a subset [{x:A & (P x)}] is the pair of an [a] of 
+     type [A] and of a proof [h] that [a] satisfies [P].
+     Then [(projS1 y)] is the witness [a]
+     and [(projS2 y)] is the proof of [(P a)] *)
+
+  Definition projS1 (x:sigS P) : A := match x with
+                                      | existS a _ => a
+                                      end.
+  Definition projS2 (x:sigS P) : P (projS1 x) :=
+    match x return P (projS1 x) with
+    | existS _ h => h
+    end.
+
+End Projections.
+
+
+(** Extended_booleans *)
+
+Inductive sumbool (A B:Prop) : Set :=
+  | left : A -> {A} + {B}
+  | right : B -> {A} + {B} 
+ where "{ A } + { B }" := (sumbool A B) : type_scope.
+
+Add Printing If sumbool.
+
+Inductive sumor (A:Set) (B:Prop) : Set :=
+  | inleft : A -> A + {B}
+  | inright : B -> A + {B} 
+ where "A + { B }" := (sumor A B) : type_scope.
+
+Add Printing If sumor.
+
+(** Choice *)
+
+Section Choice_lemmas.
+
+  (** The following lemmas state various forms of the axiom of choice *)
+
+  Variables S S' : Set.
+  Variable R : S -> S' -> Prop.
+  Variable R' : S -> S' -> Set.
+  Variables R1 R2 : S -> Prop.
+
+  Lemma Choice :
+   (forall x:S, sig (fun y:S' => R x y)) ->
+   sig (fun f:S -> S' => forall z:S, R z (f z)).
+  Proof.
+   intro H.
+   exists (fun z:S => match H z with
+                      | exist y _ => y
+                      end).
+   intro z; destruct (H z); trivial.
+  Qed.
+
+  Lemma Choice2 :
+   (forall x:S, sigS (fun y:S' => R' x y)) ->
+   sigS (fun f:S -> S' => forall z:S, R' z (f z)).
+  Proof.
+    intro H.
+    exists (fun z:S => match H z with
+                       | existS y _ => y
+                       end).
+    intro z; destruct (H z); trivial.
+  Qed.
+
+  Lemma bool_choice :
+   (forall x:S, {R1 x} + {R2 x}) ->
+   sig
+     (fun f:S -> bool =>
+        forall x:S, f x = true /\ R1 x \/ f x = false /\ R2 x).
+  Proof.
+    intro H.
+    exists
+     (fun z:S => match H z with
+                 | left _ => true
+                 | right _ => false
+                 end).
+    intro z; destruct (H z); auto.
+  Qed.
+
+End Choice_lemmas.
+
+ (** A result of type [(Exc A)] is either a normal value of type [A] or 
+     an [error] :
+     [Inductive Exc [A:Set] : Set := value : A->(Exc A) | error : (Exc A)]
+     it is implemented using the option type. *) 
+
+Definition Exc := option.
+Definition value := Some.
+Definition error := @None.
+
+Implicit Arguments error [A].
+
+Definition except := False_rec. (* for compatibility with previous versions *)
+
+Implicit Arguments except [P].
+
+Theorem absurd_set : forall (A:Prop) (C:Set), A -> ~ A -> C.
+Proof.
+  intros A C h1 h2.
+  apply False_rec.
+  apply (h2 h1).
+Qed.
+
+Hint Resolve left right inleft inright: core v62.
+
+(** Sigma Type at Type level [sigT] *)
+
+Inductive sigT (A:Type) (P:A -> Type) : Type :=
+    existT : forall x:A, P x -> sigT (A:=A) P.
+
+Section projections_sigT.
+
+  Variable A : Type.
+  Variable P : A -> Type.
+
+  Definition projT1 (H:sigT P) : A := match H with
+                                      | existT x _ => x
+                                      end.
+   
+  Definition projT2 : forall x:sigT P, P (projT1 x) :=
+    fun H:sigT P => match H return P (projT1 H) with
+                    | existT x h => h
+                    end.
+
+End projections_sigT.
+
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
new file mode 100755
index 00000000..7ab3723d
--- /dev/null
+++ b/theories/Init/Wf.v
@@ -0,0 +1,171 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+Set Implicit Arguments.
+
+(*i $Id: Wf.v,v 1.17.2.1 2004/07/16 19:31:04 herbelin Exp $ i*)
+
+(** This module proves the validity of
+    - well-founded recursion (also called course of values)
+    - well-founded induction
+
+   from a well-founded ordering on a given set *)
+
+Require Import Notations.
+Require Import Logic.
+Require Import Datatypes.
+
+(** Well-founded induction principle on Prop *)
+
+Section Well_founded.
+
+ Variable A : Set.
+ Variable R : A -> A -> Prop.
+
+ (** The accessibility predicate is defined to be non-informative *)
+
+ Inductive Acc : A -> Prop :=
+     Acc_intro : forall x:A, (forall y:A, R y x -> Acc y) -> Acc x.
+
+ Lemma Acc_inv : forall x:A, Acc x -> forall y:A, R y x -> Acc y.
+  destruct 1; trivial.
+ Defined.
+
+  (** the informative elimination :
+     [let Acc_rec F = let rec wf x = F x wf in wf] *)
+
+ Section AccRecType.
+  Variable P : A -> Type.
+  Variable
+    F :
+      forall x:A,
+        (forall y:A, R y x -> Acc y) -> (forall y:A, R y x -> P y) -> P x.
+
+  Fixpoint Acc_rect (x:A) (a:Acc x) {struct a} : P x :=
+    F (Acc_inv a) (fun (y:A) (h:R y x) => Acc_rect (x:=y) (Acc_inv a h)).
+
+ End AccRecType.
+
+ Definition Acc_rec (P:A -> Set) := Acc_rect P.
+
+ (** A simplified version of Acc_rec(t) *)
+
+ Section AccIter.
+  Variable P : A -> Type. 
+  Variable F : forall x:A, (forall y:A, R y x -> P y) -> P x.
+
+  Fixpoint Acc_iter (x:A) (a:Acc x) {struct a} : P x :=
+    F (fun (y:A) (h:R y x) => Acc_iter (x:=y) (Acc_inv a h)).
+
+ End AccIter.
+
+ (** A relation is well-founded if every element is accessible *)
+
+ Definition well_founded := forall a:A, Acc a.
+
+ (** well-founded induction on Set and Prop *)
+
+ Hypothesis Rwf : well_founded.
+
+ Theorem well_founded_induction_type :
+  forall P:A -> Type,
+    (forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a.
+ Proof.
+  intros; apply (Acc_iter P); auto.
+ Defined.
+
+ Theorem well_founded_induction :
+  forall P:A -> Set,
+    (forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a.
+ Proof.
+  exact (fun P:A -> Set => well_founded_induction_type P).
+ Defined.
+
+ Theorem well_founded_ind :
+  forall P:A -> Prop,
+    (forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a.
+ Proof.
+  exact (fun P:A -> Prop => well_founded_induction_type P).
+ Defined.
+
+(** Building fixpoints  *) 
+
+Section FixPoint.
+
+Variable P : A -> Set.
+Variable F : forall x:A, (forall y:A, R y x -> P y) -> P x.
+
+Fixpoint Fix_F (x:A) (r:Acc x) {struct r} : P x :=
+  F (fun (y:A) (p:R y x) => Fix_F (x:=y) (Acc_inv r p)).
+
+Definition Fix (x:A) := Fix_F (Rwf x).
+
+(** Proof that [well_founded_induction] satisfies the fixpoint equation. 
+    It requires an extra property of the functional *)
+
+Hypothesis
+  F_ext :
+    forall (x:A) (f g:forall y:A, R y x -> P y),
+      (forall (y:A) (p:R y x), f y p = g y p) -> F f = F g.
+
+Scheme Acc_inv_dep := Induction for Acc Sort Prop.
+
+Lemma Fix_F_eq :
+ forall (x:A) (r:Acc x),
+   F (fun (y:A) (p:R y x) => Fix_F (Acc_inv r p)) = Fix_F r.
+destruct r using Acc_inv_dep; auto.
+Qed.
+
+Lemma Fix_F_inv : forall (x:A) (r s:Acc x), Fix_F r = Fix_F s.
+intro x; induction (Rwf x); intros.
+rewrite <- (Fix_F_eq r); rewrite <- (Fix_F_eq s); intros.
+apply F_ext; auto.
+Qed.
+
+
+Lemma Fix_eq : forall x:A, Fix x = F (fun (y:A) (p:R y x) => Fix y).
+intro x; unfold Fix in |- *.
+rewrite <- (Fix_F_eq (x:=x)).
+apply F_ext; intros.
+apply Fix_F_inv.
+Qed.
+
+End FixPoint.
+
+End Well_founded. 
+
+(** A recursor over pairs *)
+
+Section Well_founded_2.
+
+  Variables A B : Set.
+  Variable R : A * B -> A * B -> Prop.
+
+  Variable P : A -> B -> Type. 
+  Variable
+    F :
+      forall (x:A) (x':B),
+        (forall (y:A) (y':B), R (y, y') (x, x') -> P y y') -> P x x'.
+
+  Fixpoint Acc_iter_2 (x:A) (x':B) (a:Acc R (x, x')) {struct a} : 
+   P x x' :=
+    F
+      (fun (y:A) (y':B) (h:R (y, y') (x, x')) =>
+         Acc_iter_2 (x:=y) (x':=y') (Acc_inv a (y, y') h)).
+
+  Hypothesis Rwf : well_founded R.
+
+  Theorem well_founded_induction_type_2 :
+   (forall (x:A) (x':B),
+      (forall (y:A) (y':B), R (y, y') (x, x') -> P y y') -> P x x') ->
+   forall (a:A) (b:B), P a b.
+  Proof.
+   intros; apply Acc_iter_2; auto.
+  Defined.
+
+End Well_founded_2.