summaryrefslogtreecommitdiff
path: root/theories/Init
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Init')
-rw-r--r--theories/Init/Datatypes.v49
-rw-r--r--theories/Init/Logic.v33
-rw-r--r--theories/Init/Logic_Type.v28
-rw-r--r--theories/Init/Notations.v5
-rw-r--r--theories/Init/Specif.v113
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).
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-29 09:25:38 +0000