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
Inductive Empty_set :
Set :=.
Register Empty_set as core.Empty_set.type.
unit is a singleton datatype with sole inhabitant tt
Inductive unit :
Set :=
tt :
unit.
Register unit as core.unit.type.
Register tt as core.unit.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.
Declare Scope bool_scope.
Delimit Scope bool_scope with bool.
Bind Scope bool_scope with bool.
Register bool as core.bool.type.
Register true as core.bool.true.
Register false as core.bool.false.
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.
Declare Scope hex_nat_scope.
Delimit Scope hex_nat_scope with xnat.
Declare Scope nat_scope.
Delimit Scope nat_scope with nat.
Bind Scope nat_scope with nat.
Arguments S _%
nat.
Register nat as num.nat.type.
Register O as num.nat.O.
Register S as num.nat.S.
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
#[
universes(
template)]
Inductive sum (
A B:
Type) :
Type :=
|
inl :
A -> sum A B
|
inr :
B -> sum A B.
Notation "x + y" := (
sum x y) :
type_scope.
Arguments inl {
A B}
_ , [
A]
B _.
Arguments inr {
A B}
_ ,
A [
B]
_.
Register sum as core.sum.type.
Register inl as core.sum.inl.
Register inr as core.sum.inr.
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.
Arguments pair {
A B}
_ _.
Register prod as core.prod.type.
Register pair as core.prod.intro.
Register prod_rect as core.prod.rect.
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.
Register fst as core.prod.proj1.
Register snd as core.prod.proj2.
End projections.
#[
global]
Hint Resolve pair inl inr:
core.
Lemma surjective_pairing (
A B:
Type) (
p:
A * B) :
p = (fst p, snd p).
Lemma injective_projections (
A B:
Type) (
p1 p2:
A * B) :
fst p1 = fst p2 -> snd p1 = snd p2 -> p1 = p2.
Lemma pair_equal_spec (
A B :
Type) (
a1 a2 :
A) (
b1 b2 :
B) :
(a1, b1) = (a2, b2) <-> a1 = a2 /\ b1 = b2.
Definition curry {
A B C:
Type} (
f:
A * B -> C)
(
x:
A) (
y:
B) :
C :=
f (x,y).
Definition uncurry {
A B C:
Type} (
f:
A -> B -> C)
(
p:
A * B) :
C :=
match p with (x, y) =>
f x y end.
#[
deprecated(
since = "8.13",
note = "Use curry instead.")]
Definition prod_uncurry (
A B C:
Type) :
(A * B -> C) -> A -> B -> C :=
curry.
#[
deprecated(
since = "8.13",
note = "Use uncurry instead.")]
Definition prod_curry (
A B C:
Type) :
(A -> B -> C) -> A * B -> C :=
uncurry.
Import EqNotations.
Lemma rew_pair 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.
Arguments nil {
A}.
Arguments cons {
A}
a l.
Declare Scope list_scope.
Delimit Scope list_scope with list.
Bind Scope list_scope with list.
Infix "::" :=
cons (
at level 60,
right associativity) :
list_scope.
Register list as core.list.type.
Register nil as core.list.nil.
Register cons as core.list.cons.
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.
Inductive identity (
A:
Type) (
a:
A) :
A -> Type :=
identity_refl :
identity a a.
#[
global]
Hint Resolve identity_refl:
core.
Arguments identity_ind [
A]
a P f y i.
Arguments identity_rec [
A]
a P f y i.
Arguments identity_rect [
A]
a P f y i.
Register identity as core.identity.type.
Register identity_refl as core.identity.refl.
Register identity_ind as core.identity.ind.
Identity type
Definition ID :=
forall A:
Type,
A -> A.
Definition id :
ID :=
fun A x =>
x.
Definition IDProp :=
forall A:
Prop,
A -> A.
Definition idProp :
IDProp :=
fun A x =>
x.
Register IDProp as core.IDProp.type.
Register idProp as core.IDProp.idProp.