diff options
Diffstat (limited to 'theories7/Init/Datatypes.v')
-rwxr-xr-x | theories7/Init/Datatypes.v | 125 |
1 files changed, 125 insertions, 0 deletions
diff --git a/theories7/Init/Datatypes.v b/theories7/Init/Datatypes.v new file mode 100755 index 00000000..006ec08e --- /dev/null +++ b/theories7/Init/Datatypes.v @@ -0,0 +1,125 @@ +(************************************************************************) +(* 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.3.2.1 2004/07/16 19:31:26 herbelin Exp $ i*) + +Require Notations. +Require Logic. + +Set Implicit Arguments. +V7only [Unset 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. + +Delimits 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). +Hints Resolve refl_identity : core v62. + +Implicits identity_ind [1]. +Implicits identity_rec [1]. +Implicits identity_rect [1]. +V7only [ +Implicits identity_ind []. +Implicits identity_rec []. +Implicits identity_rect []. +]. + +(** [option A] is the extension of A with a dummy element None *) + +Inductive option [A:Set] : Set := Some : A -> (option A) | None : (option A). + +Implicits None [1]. +V7only [Implicits None [].]. + +(** [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. +V7only [Notation "( x , y )" := (pair ? ? x y) : core_scope.]. +V8Notation "( x , y , .. , z )" := (pair ? ? .. (pair ? ? x y) .. z) : core_scope. + +Section projections. + Variables A,B:Set. + Definition fst := [p:(prod A B)]Cases p of (pair x y) => x end. + Definition snd := [p:(prod A B)]Cases p of (pair x y) => y end. +End projections. + +V7only [ +Notation Fst := (fst ? ?). +Notation Snd := (snd ? ?). +]. +Hints Resolve pair inl inr : core v62. + +Lemma surjective_pairing : (A,B:Set;p:A*B)p=(pair A B (Fst p) (Snd p)). +Proof. +NewDestruct p; Reflexivity. +Qed. + +Lemma injective_projections : + (A,B:Set;p1,p2:A*B)(Fst p1)=(Fst p2)->(Snd p1)=(Snd p2)->p1=p2. +Proof. +NewDestruct p1; NewDestruct p2; Simpl; Intros Hfst Hsnd. +Rewrite Hfst; Rewrite Hsnd; Reflexivity. +Qed. + +V7only[ +(** Parsing only of things in [Datatypes.v] *) +Notation "< A , B > ( x , y )" := (pair A B x y) (at level 1, only parsing, A annot). +Notation "< A , B > 'Fst' ( p )" := (fst A B p) (at level 1, only parsing, A annot). +Notation "< A , B > 'Snd' ( p )" := (snd A B p) (at level 1, only parsing, A annot). +]. + +(** Comparison *) + +Inductive relation : Set := + EGAL :relation | INFERIEUR : relation | SUPERIEUR : relation. + +Definition Op := [r:relation] + Cases r of + EGAL => EGAL + | INFERIEUR => SUPERIEUR + | SUPERIEUR => INFERIEUR + end. |