Library Coq.Init.Specif
Basic specifications : sets that may contain logical information
Subsets and Sigma-types
(sig A P), or more suggestively {x:A | P x}, denotes the subset
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 type A which satisfy both P and Q.
Inductive sig (
A:Type) (
P:A ->
Prop) :
Type :=
exist :
forall x:A,
P x ->
sig P.
Inductive sig2 (
A:Type) (
P Q:A ->
Prop) :
Type :=
exist2 :
forall x:A,
P x ->
Q x ->
sig2 P Q.
(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 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.
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 }" := (
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 sigT.
Add Printing Let sigT2.
Projections of sig
An element y of a subset {x:A & (P x)} is the pair of an a
of type A and of a proof h that a satisfies P. Then
(proj1_sig y) is the witness a and (proj2_sig y) is the
proof of (P a)
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,
(projT1 x) is the first projection and (projT2 x) is the
second projection, the type of which depends on the projT1.
sigT of a predicate is equivalent to sig
sumbool is a boolean type equipped with the justification of
their value
Inductive sumbool (
A B:Prop) :
Set :=
|
left :
A -> {
A} + {
B}
|
right :
B -> {
A} + {
B}
where "{ A } + { B }" := (
sumbool A B) :
type_scope.
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:Type) (
B:Prop) :
Type :=
|
inleft :
A ->
A + {
B}
|
inright :
B ->
A + {
B}
where "A + { B }" := (
sumor A B) :
type_scope.
Add Printing If sumor.
Various forms of the axiom of choice for specifications
Section Choice_lemmas.
Variables S S' :
Set.
Variable R :
S ->
S' ->
Prop.
Variable R' :
S ->
S' ->
Set.
Variables R1 R2 :
S ->
Prop.
Lemma Choice :
(
forall x:S,
sig (
fun y:S' =>
R x y)) ->
sig (
fun f:S ->
S' =>
forall z:S,
R z (
f z)).
Lemma Choice2 :
(
forall x:S,
sigT (
fun y:S' =>
R' x y)) ->
sigT (
fun f:S ->
S' =>
forall z:S,
R' z (
f z)).
Lemma bool_choice :
(
forall x:S, {
R1 x} + {
R2 x}) ->
sig
(
fun f:S ->
bool =>
forall x:S,
f x =
true /\
R1 x \/
f x =
false /\
R2 x).
End Choice_lemmas.
A result of type (Exc A) is either a normal value of type A or
an error :
Inductive Exc [A:Type] : Type := value : A->(Exc A) | error : (Exc A).
It is implemented using the option type.