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
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
A result of type (Exc A) is either a normal value of type A or
an error :
Inductive Exc [AType:] : Type := value : A->(Exc A) | error : (Exc A).
It is implemented using the option type.