summaryrefslogtreecommitdiff
path: root/theories/Init
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-28 21:54:47 +0000
committerGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-28 21:54:47 +0000
commit6b649aba925b6f7462da07599fe67ebb12a3460e (patch)
tree43656bcaa51164548f3fa14e5b10de5ef1088574 /theories/Init
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'theories/Init')
-rwxr-xr-xtheories/Init/Datatypes.v121
-rwxr-xr-xtheories/Init/Logic.v279
-rwxr-xr-xtheories/Init/Logic_Type.v89
-rw-r--r--theories/Init/Notations.v78
-rwxr-xr-xtheories/Init/Peano.v210
-rwxr-xr-xtheories/Init/Prelude.v16
-rwxr-xr-xtheories/Init/Specif.v212
-rwxr-xr-xtheories/Init/Wf.v171
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.