diff options
Diffstat (limited to 'theories/Init/Datatypes.v')
| -rw-r--r--[-rwxr-xr-x] | theories/Init/Datatypes.v | 85 |
1 files changed, 56 insertions, 29 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 6aeabe13..56dc7e95 100755..100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -6,19 +6,19 @@ (* * 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*) +(*i $Id: Datatypes.v 9245 2006-10-17 12:53:34Z notin $ i*) + +Set Implicit Arguments. 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] *) +(** [bool] is the datatype of the boolean values [true] and [false] *) Inductive bool : Set := | true : bool @@ -27,7 +27,9 @@ Inductive bool : Set := 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 *) + note that the constructor name is the letter O. + Numbers in [nat] can be denoted using a decimal notation; + e.g. [3%nat] abbreviates [S (S (S O))] *) Inductive nat : Set := | O : nat @@ -45,25 +47,31 @@ Inductive Empty_set : Set :=. 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. +Inductive identity (A:Type) (a:A) : A -> Type := + 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 *) +(** [option A] is the extension of [A] with an extra element [None] *) -Inductive option (A:Set) : Set := +Inductive option (A:Type) : Type := | 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] *) +Definition option_map (A B:Type) (f:A->B) o := + match o with + | Some a => Some (f a) + | None => None + end. + +(** [sum A B], written [A + B], is the disjoint sum of [A] and [B] *) (* Syntax defined in Specif.v *) -Inductive sum (A B:Set) : Set := +Inductive sum (A B:Type) : Type := | inl : A -> sum A B | inr : B -> sum A B. @@ -72,39 +80,46 @@ 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. +Inductive prod (A B:Type) : Type := + 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. + Variables A B : Type. + 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). + forall (A B:Type) (p:A * B), p = pair (fst p) (snd p). Proof. -destruct p; reflexivity. + 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. + forall (A B:Type) (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. + destruct p1; destruct p2; simpl in |- *; intros Hfst Hsnd. + rewrite Hfst; rewrite Hsnd; reflexivity. Qed. +Definition prod_uncurry (A B C:Type) (f:prod A B -> C) + (x:A) (y:B) : C := f (pair x y). + +Definition prod_curry (A B C:Type) (f:A -> B -> C) + (p:prod A B) : C := match p with + | pair x y => f x y + end. (** Comparison *) @@ -115,7 +130,19 @@ Inductive comparison : Set := Definition CompOpp (r:comparison) := match r with - | Eq => Eq - | Lt => Gt - | Gt => Lt + | Eq => Eq + | Lt => Gt + | Gt => Lt end. + +(* Compatibility *) + +Notation prodT := prod (only parsing). +Notation pairT := pair (only parsing). +Notation prodT_rect := prod_rect (only parsing). +Notation prodT_rec := prod_rec (only parsing). +Notation prodT_ind := prod_ind (only parsing). +Notation fstT := fst (only parsing). +Notation sndT := snd (only parsing). +Notation prodT_uncurry := prod_uncurry (only parsing). +Notation prodT_curry := prod_curry (only parsing). |