Library Coq.Init.Datatypes
Set Implicit Arguments.
Require Import Notations.
Require Import Ltac.
Require Import Logic.
Datatypes with zero and one element
Empty_set is a datatype with no inhabitant
unit is a singleton datatype with sole inhabitant tt
The boolean datatype
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
Basic properties of andb
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 >-> Sortclass.
Additional rewriting lemmas about
eq_true
The BoolSpec inductive will be used to relate a boolean value
and two propositions corresponding respectively to the true
case and the false case.
Interest: BoolSpec behave nicely with case and destruct.
See also Bool.reflect when Q = ~P.
Peano natural numbers
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 hex_nat_scope with xnat.
Delimit Scope nat_scope with nat.
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
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)
#[
universes(
template)]
Inductive prod (
A B:
Type) :
Type :=
pair :
A -> B -> A * B
where "x * y" := (
prod x y) :
type_scope.
Add Printing Let prod.
Notation "( x , y , .. , z )" := (
pair .. (
pair x y) ..
z) :
core_scope.
Section projections.
Context {
A :
Type} {
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 = (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.
Lemma pair_equal_spec :
forall (
A B :
Type) (
a1 a2 :
A) (
b1 b2 :
B),
(a1, b1) = (a2, b2) <-> a1 = a2 /\ b1 = b2.
Definition prod_uncurry (
A B C:
Type) (
f:
A * B -> C)
(
x:
A) (
y:
B) :
C :=
f (x,y).
Definition prod_curry (
A B C:
Type) (
f:
A -> B -> C)
(
p:
A * B) :
C :=
match p with (x, y) =>
f x y end.
Import EqNotations.
Lemma rew_pair :
forall A (
P Q :
A->Type)
x1 x2 (
y1:
P x1) (
y2:
Q x1) (
H:
x1=x2),
(rew H in y1, rew H in y2) = rew [fun x => (
P x * Q x)%
type] H in (y1,y2).
Polymorphic lists and some operations
#[
universes(
template)]
Inductive list (
A :
Type) :
Type :=
|
nil :
list A
|
cons :
A -> list A -> list A.
Delimit Scope list_scope with list.
Infix "::" :=
cons (
at level 60,
right associativity) :
list_scope.
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
The CompareSpec inductive relates a comparison value with three
propositions, one for each possible case. Typically, it can be used to
specify a comparison function via some equality and order predicates.
Interest: CompareSpec behave nicely with case and destruct.
For having clean interfaces after extraction, CompareSpec is declared
in Prop. For some situations, it is nonetheless useful to have a
version in Type. Interestingly, these two versions are equivalent.
As an alternate formulation, one may also directly refer to predicates
eq and lt for specifying a comparison, rather that fully-applied
propositions. This CompSpec is now a particular case of CompareSpec.
Misc Other Datatypes
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
identity_refl A a Beware: this inductive actually falls into
Prop, as the sole
constructor has no arguments and
-indices-matter is not
activated in the standard library.
Identity type