summaryrefslogtreecommitdiff
path: root/theories/Init/Specif.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Init/Specif.v')
-rw-r--r--theories/Init/Specif.v123
1 files changed, 100 insertions, 23 deletions
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index cc5a1932..1384901b 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -45,11 +45,11 @@ Arguments sigT2 (A P Q)%type.
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)) :
+Notation "{ x : A | P }" := (sig (A:=A) (fun x => P)) : type_scope.
+Notation "{ x : A | P & Q }" := (sig2 (A:=A) (fun x => P) (fun x => Q)) :
type_scope.
-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)) :
+Notation "{ x : A & P }" := (sigT (A:=A) (fun x => P)) : type_scope.
+Notation "{ x : A & P & Q }" := (sigT2 (A:=A) (fun x => P) (fun x => Q)) :
type_scope.
Add Printing Let sig.
@@ -65,24 +65,57 @@ Add Printing Let sigT2.
[(proj1_sig y)] is the witness [a] and [(proj2_sig y)] is the
proof of [(P a)] *)
-
+(* Set Universe Polymorphism. *)
Section Subset_projections.
Variable A : Type.
Variable P : A -> Prop.
Definition proj1_sig (e:sig P) := match e with
- | exist a b => a
+ | exist _ a b => a
end.
Definition proj2_sig (e:sig P) :=
match e return P (proj1_sig e) with
- | exist a b => b
+ | exist _ a b => b
end.
End Subset_projections.
+(** [sig2] of a predicate can be projected to a [sig].
+
+ This allows [proj1_sig] and [proj2_sig] to be usable with [sig2].
+
+ The [let] statements occur in the body of the [exist] so that
+ [proj1_sig] of a coerced [X : sig2 P Q] will unify with [let (a,
+ _, _) := X in a] *)
+
+Definition sig_of_sig2 (A : Type) (P Q : A -> Prop) (X : sig2 P Q) : sig P
+ := exist P
+ (let (a, _, _) := X in a)
+ (let (x, p, _) as s return (P (let (a, _, _) := s in a)) := X in p).
+
+(** Projections of [sig2]
+
+ An element [y] of a subset [{x:A | (P x) & (Q x)}] is the triple
+ of an [a] of type [A], a of a proof [h] that [a] satisfies [P],
+ and a proof [h'] that [a] satisfies [Q]. Then
+ [(proj1_sig (sig_of_sig2 y))] is the witness [a],
+ [(proj2_sig (sig_of_sig2 y))] is the proof of [(P a)], and
+ [(proj3_sig y)] is the proof of [(Q a)]. *)
+
+Section Subset_projections2.
+
+ Variable A : Type.
+ Variables P Q : A -> Prop.
+
+ Definition proj3_sig (e : sig2 P Q) :=
+ let (a, b, c) return Q (proj1_sig (sig_of_sig2 e)) := e in c.
+
+End Subset_projections2.
+
+
(** Projections of [sigT]
An element [x] of a sigma-type [{y:A & P y}] is a dependent pair
@@ -90,31 +123,71 @@ End Subset_projections.
[(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 : Type.
Variable P : A -> Type.
Definition projT1 (x:sigT P) : A := match x with
- | existT a _ => a
+ | existT _ a _ => a
end.
+
Definition projT2 (x:sigT P) : P (projT1 x) :=
match x return P (projT1 x) with
- | existT _ h => h
+ | existT _ _ h => h
end.
End Projections.
+(** [sigT2] of a predicate can be projected to a [sigT].
+
+ This allows [projT1] and [projT2] to be usable with [sigT2].
+
+ The [let] statements occur in the body of the [existT] so that
+ [projT1] of a coerced [X : sigT2 P Q] will unify with [let (a,
+ _, _) := X in a] *)
+
+Definition sigT_of_sigT2 (A : Type) (P Q : A -> Type) (X : sigT2 P Q) : sigT P
+ := existT P
+ (let (a, _, _) := X in a)
+ (let (x, p, _) as s return (P (let (a, _, _) := s in a)) := X in p).
+
+(** Projections of [sigT2]
+
+ An element [x] of a sigma-type [{y:A & P y & Q y}] is a dependent
+ pair made of an [a] of type [A], an [h] of type [P a], and an [h']
+ of type [Q a]. Then, [(projT1 (sigT_of_sigT2 x))] is the first
+ projection, [(projT2 (sigT_of_sigT2 x))] is the second projection,
+ and [(projT3 x)] is the third projection, the types of which
+ depends on the [projT1]. *)
+
+Section Projections2.
+
+ Variable A : Type.
+ Variables P Q : A -> Type.
+
+ Definition projT3 (e : sigT2 P Q) :=
+ let (a, b, c) return Q (projT1 (sigT_of_sigT2 e)) := e in c.
+
+End Projections2.
+
(** [sigT] of a predicate is equivalent to [sig] *)
-Lemma sig_of_sigT : forall (A:Type) (P:A->Prop), sigT P -> sig P.
-Proof. destruct 1 as (x,H); exists x; trivial. Defined.
+Definition sig_of_sigT (A : Type) (P : A -> Prop) (X : sigT P) : sig P
+ := exist P (projT1 X) (projT2 X).
+
+Definition sigT_of_sig (A : Type) (P : A -> Prop) (X : sig P) : sigT P
+ := existT P (proj1_sig X) (proj2_sig X).
-Lemma sigT_of_sig : forall (A:Type) (P:A->Prop), sig P -> sigT P.
-Proof. destruct 1 as (x,H); exists x; trivial. Defined.
+(** [sigT2] of a predicate is equivalent to [sig2] *)
-Coercion sigT_of_sig : sig >-> sigT.
-Coercion sig_of_sigT : sigT >-> sig.
+Definition sig2_of_sigT2 (A : Type) (P Q : A -> Prop) (X : sigT2 P Q) : sig2 P Q
+ := exist2 P Q (projT1 (sigT_of_sigT2 X)) (projT2 (sigT_of_sigT2 X)) (projT3 X).
+
+Definition sigT2_of_sig2 (A : Type) (P Q : A -> Prop) (X : sig2 P Q) : sigT2 P Q
+ := existT2 P Q (proj1_sig (sig_of_sig2 X)) (proj2_sig (sig_of_sig2 X)) (proj3_sig X).
(** [sumbool] is a boolean type equipped with the justification of
their value *)
@@ -142,6 +215,8 @@ Add Printing If sumor.
Arguments inleft {A B} _ , [A] B _.
Arguments inright {A B} _ , A [B] _.
+(* Unset Universe Polymorphism. *)
+
(** Various forms of the axiom of choice for specifications *)
Section Choice_lemmas.
@@ -187,10 +262,10 @@ Section Dependent_choice_lemmas.
(forall x:X, {y | R x y}) ->
forall x0, {f : nat -> X | f O = x0 /\ forall n, R (f n) (f (S n))}.
Proof.
- intros H x0.
+ intros H x0.
set (f:=fix f n := match n with O => x0 | S n' => proj1_sig (H (f n')) end).
exists f.
- split. reflexivity.
+ split. reflexivity.
induction n; simpl; apply proj2_sig.
Defined.
@@ -203,12 +278,14 @@ End Dependent_choice_lemmas.
[Inductive Exc [A:Type] : Type := value : A->(Exc A) | error : (Exc A)].
It is implemented using the option type. *)
+Section Exc.
+ Variable A : Type.
-Definition Exc := option.
-Definition value := Some.
-Definition error := @None.
-
-Arguments error [A].
+ Definition Exc := option A.
+ Definition value := @Some A.
+ Definition error := @None A.
+End Exc.
+Arguments error {A}.
Definition except := False_rec. (* for compatibility with previous versions *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 01:43:03 +0000