1 files changed, 121 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.