Library Coq.Init.Datatypes
unit is a singleton datatype with sole inhabitant tt
bool is the datatype of the boolean values true and false
Inductive bool :
Set :=
|
true :
bool
|
false :
bool.
Add Printing If bool.
Delimit Scope bool_scope with bool.
Basic boolean operators
Interpretation of booleans as propositions
Additional rewriting lemmas about eq_true
nat is the datatype of natural numbers built from O and successor S;
note that the constructor name is the letter O.
Numbers in nat can be denoted using a decimal notation;
e.g. 3%nat abbreviates S (S (S O))
Inductive nat :
Set :=
|
O :
nat
|
S :
nat ->
nat.
Delimit Scope nat_scope with nat.
Empty_set has no inhabitant
identity A a is the family of datatypes on A whose sole non-empty
member is the singleton datatype identity A a a whose
sole inhabitant is denoted refl_identity A a
option A is the extension of A with an extra element None
sum A B, written A + B, is the disjoint sum of A and B
Inductive sum (
A B:Type) :
Type :=
|
inl :
A ->
sum A B
|
inr :
B ->
sum A B.
Notation "x + y" := (
sum x y) :
type_scope.
prod A B, written A * B, is the product of A and B;
the pair pair A B a b of a and b is abbreviated (a,b)
Inductive prod (
A B:Type) :
Type :=
pair :
A ->
B ->
prod A B.
Add Printing Let prod.
Notation "x * y" := (
prod x y) :
type_scope.
Notation "( x , y , .. , z )" := (
pair ..
Section projections.
Variables A B :
Type.
Definition fst (
p:A *
B) :=
match p with
| (
x,
y) =>
x
end.
Definition snd (
p:A *
B) :=
match p with
| (
x,
y) =>
y
end.
End projections.
Hint Resolve pair inl inr:
core.
Lemma surjective_pairing :
forall (
A B:Type) (
p:A *
B),
p =
pair (
fst p) (
snd p).
Lemma injective_projections :
forall (
A B:Type) (
p1 p2:A *
B),
fst p1 =
fst p2 ->
snd p1 =
snd p2 ->
p1 =
p2.
Definition prod_uncurry (
A B C:Type) (
f:prod
A B ->
C)
(
x:A) (
y:B) :
C :=
f (
pair x y).
Definition prod_curry (
A B C:Type) (
f:A ->
B ->
C)
(
p:prod
A B) :
C :=
match p with
|
pair x y =>
f x y
end.
Comparison
Identity
Definition ID :=
forall A:Type,
A ->
A.
Definition id :
ID :=
fun A x =>
x.