diff options
Diffstat (limited to 'theories/Init')
| -rw-r--r-- | theories/Init/Datatypes.v | 49 | ||||
| -rw-r--r-- | theories/Init/Logic.v | 33 | ||||
| -rw-r--r-- | theories/Init/Logic_Type.v | 28 | ||||
| -rw-r--r-- | theories/Init/Notations.v | 5 | ||||
| -rw-r--r-- | theories/Init/Specif.v | 113 |
5 files changed, 122 insertions, 106 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index f71f58c6..fdd7ba35 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Datatypes.v 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id: Datatypes.v 8872 2006-05-29 07:36:28Z herbelin $ i*) Set Implicit Arguments. @@ -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,15 @@ Definition CompOpp (r:comparison) := | 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). diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index cbf8d7a7..71583718 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Logic.v 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id: Logic.v 8936 2006-06-09 15:43:33Z herbelin $ i*) Set Implicit Arguments. @@ -280,13 +280,36 @@ Qed. Hint Immediate sym_eq sym_not_eq: core v62. -(** Other notations *) +(** Basic definitions about relations and properties *) -Notation "'exists' ! x , P" := - (exists x', (fun x => P) x' /\ forall x'', (fun x => P) x'' -> x' = x'') +Definition subrelation (A B : Type) (R R' : A->B->Prop) := + forall x y, R x y -> R' x y. + +Definition unique (A : Type) (P : A->Prop) (x:A) := + P x /\ forall (x':A), P x' -> x=x'. + +Definition uniqueness (A:Type) (P:A->Prop) := forall x y, P x -> P y -> x = y. + +(** Unique existence *) + +Notation "'exists' ! x , P" := (ex (unique (fun x => P))) (at level 200, x ident, right associativity, format "'[' 'exists' ! '/ ' x , '/ ' P ']'") : type_scope. Notation "'exists' ! x : A , P" := - (exists x' : A, (fun x => P) x' /\ forall x'':A, (fun x => P) x'' -> x' = x'') + (ex (unique (fun x:A => P))) (at level 200, x ident, right associativity, format "'[' 'exists' ! '/ ' x : A , '/ ' P ']'") : type_scope. + +Lemma unique_existence : forall (A:Type) (P:A->Prop), + ((exists x, P x) /\ uniqueness P) <-> (exists! x, P x). +Proof. +intros A P; split. + intros ((x,Hx),Huni); exists x; red; auto. + intros (x,(Hx,Huni)); split. + exists x; assumption. + intros x' x'' Hx' Hx''; transitivity x. + symmetry; auto. + auto. +Qed. + + diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v index 857ffe94..dbe944b0 100644 --- a/theories/Init/Logic_Type.v +++ b/theories/Init/Logic_Type.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Logic_Type.v 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id: Logic_Type.v 8866 2006-05-28 16:21:04Z herbelin $ i*) (** This module defines type constructors for types in [Type] ([Datatypes.v] and [Logic.v] defined them for types in [Set]) *) @@ -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 3ca93067..416647b4 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Notations.v 6410 2004-12-06 11:34:35Z herbelin $ i*) +(*i $Id: Notations.v 8866 2006-05-28 16:21:04Z herbelin $ i*) (** These are the notations whose level and associativity are imposed by Coq *) @@ -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 e7fc1ac4..dd2f7697 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Specif.v 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id: Specif.v 8866 2006-05-28 16:21:04Z herbelin $ i*) (** Basic specifications : sets that may contain logical information *) @@ -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). |