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
Another way of interpreting booleans as propositions
is_true can be activated as a coercion by
(Local) Coercion is_true : bool >-> Prop.
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)
Comparison
The CompSpec inductive will be used to relate a compare function
(returning a comparison answer) and some equality and order predicates.
Interest: CompSpec behave nicely with case and destruct.
For having clean interfaces after extraction, CompSpec is declared
in Prop. For some situations, it is nonetheless useful to have a
version in Type. Interestingly, these two versions are equivalent.
Identity
Definition ID :=
forall A:
Type,
A ->
A.
Definition id :
ID :=
fun A x =>
x.
Polymorphic lists and some operations
Inductive list (
A :
Type) :
Type :=
|
nil :
list A
|
cons :
A ->
list A ->
list A.
Implicit Arguments nil [
A].
Infix "::" :=
cons (
at level 60,
right associativity) :
list_scope.
Delimit Scope list_scope with list.
Local Open Scope list_scope.
Definition length (
A :
Type) :
list A ->
nat :=
fix length l :=
match l with
|
nil =>
O
|
_ :: l' =>
S (
length l')
end.
Concatenation of two lists
Definition app (
A :
Type) :
list A ->
list A ->
list A :=
fix app l m :=
match l with
|
nil =>
m
|
a :: l1 =>
a :: app l1 m
end.
Infix "++" :=
app (
right associativity,
at level 60) :
list_scope.