From 10fa54f60acdfc8de6b59659f9fa8bc1ed3c18e6 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 28 May 2006 16:21:04 +0000 Subject: - Déplacement des types paramétriques prod, sum, option, identity, sig, sig2, sumor, list et vector dans Type - Branchement de prodT/listT vers les nouveaux prod/list - Abandon sigS/sigS2 au profit de sigT et du nouveau sigT2 - Changements en conséquence dans les théories (notamment Field_Tactic), ainsi que dans les modules ML Coqlib/Equality/Hipattern/Field git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8866 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Init/Datatypes.v | 44 ++++++++++++------ theories/Init/Logic_Type.v | 26 ----------- theories/Init/Notations.v | 3 ++ theories/Init/Specif.v | 111 ++++++++++++++++++++++----------------------- 4 files changed, 87 insertions(+), 97 deletions(-) (limited to 'theories/Init') diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 369fd2cbd7..6ec1943252 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -47,7 +47,7 @@ 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 := +Inductive identity (A:Type) (a:A) : A -> Type := refl_identity : identity (A:=A) a a. Hint Resolve refl_identity: core v62. @@ -57,13 +57,13 @@ Implicit Arguments identity_rect [A]. (** [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]. -Definition option_map (A B:Set) (f:A->B) o := +Definition option_map (A B:Type) (f:A->B) o := match o with | Some a => Some (f a) | None => None @@ -71,7 +71,7 @@ Definition option_map (A B:Set) (f:A->B) o := (** [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. @@ -80,7 +80,7 @@ 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 := +Inductive prod (A B:Type) : Type := pair : A -> B -> prod A B. Add Printing Let prod. @@ -88,31 +88,38 @@ 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. Qed. Lemma injective_projections : - forall (A B:Set) (p1 p2:A * B), + 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. 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 *) @@ -127,3 +134,12 @@ Definition CompOpp (r:comparison) := | Lt => Gt | Gt => Lt end. + +(* Compatibility *) + +Notation prodT := prod (only parsing). +Notation pairT := pair (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). diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v index 464c8071df..faeecdf9d9 100644 --- a/theories/Init/Logic_Type.v +++ b/theories/Init/Logic_Type.v @@ -20,32 +20,6 @@ Require Export Logic. Definition notT (A:Type) := A -> False. -(** Conjunction of types in [Type] *) - -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. - (** Properties of [identity] *) Section identity_is_a_congruence. diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index fe24706e41..ffbf83d808 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -62,6 +62,9 @@ Reserved Notation "{ x }" (at level 0, x at level 99). (** Notations for sigma-types or subsets *) +Reserved Notation "{ x | P }" (at level 0, x at level 99). +Reserved Notation "{ x | 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). diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index f427492939..5bf9621b14 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -19,42 +19,45 @@ Require Import Logic. (** Subsets and Sigma-types *) (** [(sig A P)], or more suggestively [{x:A | P x}], denotes the subset - of elements of the Set [A] which satisfy the predicate [P]. + of elements of the type [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]. *) + of elements of the type [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 sig (A:Type) (P:A -> Prop) : Type := + exist : forall x:A, P x -> sig P. -Inductive sig2 (A:Set) (P Q:A -> Prop) : Set := - exist2 : forall x:A, P x -> Q x -> sig2 (A:=A) P Q. +Inductive sig2 (A:Type) (P Q:A -> Prop) : Type := + exist2 : forall x:A, P x -> Q x -> sig2 P Q. -(** [(sigS A P)], or more suggestively [{x:A & (P x)}] is a Sigma-type. - It is a 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. +(** [(sigT A P)], or more suggestively [{x:A & (P x)}] is a Sigma-type. + Similarly for [(sigT2 A P Q)], also written [{x:A & (P x) & (Q x)}]. *) -Inductive sigS2 (A:Set) (P Q:A -> Set) : Set := - existS2 : forall x:A, P x -> Q x -> sigS2 (A:=A) P Q. +Inductive sigT (A:Type) (P:A -> Type) : Type := + existT : forall x:A, P x -> sigT P. + +Inductive sigT2 (A:Type) (P Q:A -> Type) : Type := + existT2 : forall x:A, P x -> Q x -> sigT2 P Q. + +(* Notations *) 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]. +Arguments Scope sigT [type_scope type_scope]. +Arguments Scope sigT2 [type_scope type_scope type_scope]. +Notation "{ x | P }" := (sig (fun x => P)) : type_scope. +Notation "{ x | P & Q }" := (sig2 (fun x => P) (fun x => Q)) : 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)) : +Notation "{ x : A & P }" := (sigT (fun x:A => P)) : type_scope. +Notation "{ x : A & P & Q }" := (sigT2 (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. +Add Printing Let sigT. +Add Printing Let sigT2. (** Projections of [sig] @@ -67,7 +70,7 @@ Add Printing Let sigS2. Section Subset_projections. - Variable A : Set. + Variable A : Type. Variable P : A -> Prop. Definition proj1_sig (e:sig P) := match e with @@ -82,24 +85,24 @@ Section Subset_projections. End Subset_projections. -(** Projections of [sigS] +(** Projections of [sigT] An element [x] of a sigma-type [{y:A & P y}] is a dependent pair made of an [a] of type [A] and an [h] of type [P a]. Then, - [(projS1 x)] is the first projection and [(projS2 x)] is the - second projection, the type of which depends on the [projS1]. *) + [(projT1 x)] is the first projection and [(projT2 x)] is the + second projection, the type of which depends on the [projT1]. *) Section Projections. - Variable A : Set. - Variable P : A -> Set. + Variable A : Type. + Variable P : A -> Type. - Definition projS1 (x:sigS P) : A := match x with - | existS a _ => a + Definition projT1 (x:sigT P) : A := match x with + | existT a _ => a end. - Definition projS2 (x:sigS P) : P (projS1 x) := - match x return P (projS1 x) with - | existS _ h => h + Definition projT2 (x:sigT P) : P (projT1 x) := + match x return P (projT1 x) with + | existT _ h => h end. End Projections. @@ -118,7 +121,7 @@ Add Printing If sumbool. (** [sumor] is an option type equipped with the justification of why it may not be a regular value *) -Inductive sumor (A:Set) (B:Prop) : Set := +Inductive sumor (A:Type) (B:Prop) : Type := | inleft : A -> A + {B} | inright : B -> A + {B} where "A + { B }" := (sumor A B) : type_scope. @@ -146,12 +149,12 @@ Section Choice_lemmas. 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)). + (forall x:S, sigT (fun y:S' => R' x y)) -> + sigT (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 + | existT y _ => y end). intro z; destruct (H z); trivial. Qed. @@ -176,7 +179,7 @@ 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)]. + [Inductive Exc [A:Type] : Type := value : A->(Exc A) | error : (Exc A)]. It is implemented using the option type. *) @@ -199,24 +202,18 @@ Qed. Hint Resolve left right inleft inright: core v62. -(** Sigma-type for types in [Type] *) - -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. - +(* Compatibility *) + +Notation sigS := sigT (only parsing). +Notation existS := existT (only parsing). +Notation sigS_rect := sigT_rect (only parsing). +Notation sigS_rec := sigT_rec (only parsing). +Notation sigS_ind := sigT_ind (only parsing). +Notation projS1 := projT1 (only parsing). +Notation projS2 := projT2 (only parsing). + +Notation sigS2 := sigT2 (only parsing). +Notation existS2 := existT2 (only parsing). +Notation sigS2_rect := sigT2_rect (only parsing). +Notation sigS2_rec := sigT2_rec (only parsing). +Notation sigS2_ind := sigT2_ind (only parsing). -- cgit v1.2.3