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.
(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 (
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 (
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.
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)
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
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).
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.
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
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.
sigT of a predicate is equivalent to sig
sigT2 of a predicate is equivalent to sig2
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
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 [A:Type] : Type := value : A->(Exc A) | error : (Exc A).
It is implemented using the option type.