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)}.
#[
universes(
template)]
Inductive sigT (
A:
Type) (
P:
A -> Type) :
Type :=
existT :
forall x:
A,
P x -> sigT P.
#[
universes(
template)]
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 & P }" := (
sigT (
fun x =>
P)) :
type_scope.
Notation "{ x & P & Q }" := (
sigT2 (
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.
Notation "{ ' pat | P }" := (
sig (
fun pat =>
P)) :
type_scope.
Notation "{ ' pat | P & Q }" := (
sig2 (
fun pat =>
P) (
fun pat =>
Q)) :
type_scope.
Notation "{ ' pat : A | P }" := (
sig (
A:=
A) (
fun pat =>
P)) :
type_scope.
Notation "{ ' pat : A | P & Q }" := (
sig2 (
A:=
A) (
fun pat =>
P) (
fun pat =>
Q)) :
type_scope.
Notation "{ ' pat & P }" := (
sigT (
fun pat =>
P)) :
type_scope.
Notation "{ ' pat & P & Q }" := (
sigT2 (
fun pat =>
P) (
fun pat =>
Q)) :
type_scope.
Notation "{ ' pat : A & P }" := (
sigT (
A:=
A) (
fun pat =>
P)) :
type_scope.
Notation "{ ' pat : A & P & Q }" := (
sigT2 (
A:=
A) (
fun pat =>
P) (
fun pat =>
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
η Principles
exists x : A, B is equivalent to inhabited {x : A | B}
Equality of sigma types
Import EqNotations.
Equality for sigT
Section sigT.
Local Unset Implicit Arguments.
Projecting an equality of a pair to equality of the first components
Projecting an equality of a pair to equality of the second components
Equality of sigT is itself a sigT (forwards-reasoning version)
Equality of sigT is itself a sigT (backwards-reasoning version)
Curried version of proving equality of sigma types
Equality of sigT when the property is an hProp
Equivalence of equality of sigT with a sigT of equality We could actually prove an isomorphism here, and not just <->,
but for simplicity, we don't.
Induction principle for @eq (sigT _)
Equivalence of equality of sigT involving hProps with equality of the first components
Non-dependent classification of equality of sigT
Classification of transporting across an equality of sigTs
Equality for sig
Section sig.
Local Unset Implicit Arguments.
Projecting an equality of a pair to equality of the first components
Projecting an equality of a pair to equality of the second components
Equality of sig is itself a sig (forwards-reasoning version)
Equality of sig is itself a sig (backwards-reasoning version)
Curried version of proving equality of sigma types
Induction principle for @eq (sig _)
Equality of sig when the property is an hProp
Equivalence of equality of sig with a sig of equality We could actually prove an isomorphism here, and not just <->,
but for simplicity, we don't.
Equivalence of equality of sig involving hProps with equality of the first components
Equality for sigT
Section sigT2.
Local Unset Implicit Arguments.
Projecting an equality of a pair to equality of the first components
Projecting an equality of a pair to equality of the second components
Projecting an equality of a pair to equality of the third components
Equality of sigT2 is itself a sigT2 (forwards-reasoning version)
Equality of sigT2 is itself a sigT2 (backwards-reasoning version)
Curried version of proving equality of sigma types
Equality of sigT2 when the second property is an hProp
Equivalence of equality of sigT2 with a sigT2 of equality We could actually prove an isomorphism here, and not just <->,
but for simplicity, we don't.
Induction principle for @eq (sigT2 _ _)
Equivalence of equality of sigT2 involving hProps with equality of the first components
Non-dependent classification of equality of sigT
Classification of transporting across an equality of sigT2s
Equality for sig2
Section sig2.
Local Unset Implicit Arguments.
Projecting an equality of a pair to equality of the first components
Projecting an equality of a pair to equality of the second components
Projecting an equality of a pair to equality of the third components
Equality of sig2 is itself a sig2 (fowards-reasoning version)
Equality of sig2 is itself a sig2 (backwards-reasoning version)
Curried version of proving equality of sigma types
Equality of sig2 when the second property is an hProp
Equivalence of equality of sig2 with a sig2 of equality We could actually prove an isomorphism here, and not just <->,
but for simplicity, we don't.
Induction principle for @eq (sig2 _ _)
Equivalence of equality of sig2 involving hProps with equality of the first components
Non-dependent classification of equality of sig
Classification of transporting across an equality of sig2s
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.