Library Coq.Init.Datatypes
unit is a singleton datatype with sole inhabitant tt
Inductive bool : Set :=
| true : bool
| false : bool.
Add Printing If bool.
Delimit Scope bool_scope with bool.
Basic boolean operators
Definition andb (b1 b2:bool) : bool := if b1 then b2 else false.
Definition orb (b1 b2:bool) : bool := if b1 then true else b2.
Definition implb (b1 b2:bool) : bool := if b1 then b2 else true.
Definition xorb (b1 b2:bool) : bool :=
match b1, b2 with
| true, true => false
| true, false => true
| false, true => true
| false, false => false
end.
Definition negb (b:bool) := if b then false else true.
Infix "||" := orb : bool_scope.
Infix "&&" := andb : bool_scope.
Basic properties of andb
Lemma andb_prop : forall a b:bool, andb a b = true -> a = true /\ b = true.
Hint Resolve andb_prop: bool.
Lemma andb_true_intro :
forall b1 b2:bool, b1 = true /\ b2 = true -> andb b1 b2 = true.
Hint Resolve andb_true_intro: bool.
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
Lemma eq_true_ind_r :
forall (P : bool -> Prop) (b : bool), P b -> eq_true b -> P true.
Lemma eq_true_rec_r :
forall (P : bool -> Set) (b : bool), P b -> eq_true b -> P true.
Lemma eq_true_rect_r :
forall (P : bool -> Type) (b : bool), P b -> eq_true b -> P 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.
Inductive BoolSpec (P Q : Prop) : bool -> Prop :=
| BoolSpecT : P -> BoolSpec P Q true
| BoolSpecF : Q -> BoolSpec P Q false.
Hint Constructors BoolSpec.
Peano natural numbers
option A is the extension of A with an extra element None
Inductive option (A:Type) : Type :=
| Some : A -> option A
| None : option A.
Definition option_map (A B:Type) (f:A->B) (o : option A) : option B :=
match o with
| Some a => @Some B (f a)
| None => @None B
end.
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 .. (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 = 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.
Polymorphic lists and some operations
Inductive list (A : Type) : Type :=
| nil : list A
| cons : A -> list A -> list 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.
Inductive comparison : Set :=
| Eq : comparison
| Lt : comparison
| Gt : comparison.
Lemma comparison_eq_stable : forall c c' : comparison, ~~ c = c' -> c = c'.
Definition CompOpp (r:comparison) :=
match r with
| Eq => Eq
| Lt => Gt
| Gt => Lt
end.
Lemma CompOpp_involutive : forall c, CompOpp (CompOpp c) = c.
Lemma CompOpp_inj : forall c c', CompOpp c = CompOpp c' -> c = c'.
Lemma CompOpp_iff : forall c c', CompOpp c = c' <-> c = CompOpp c'.
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.
Inductive CompareSpec (Peq Plt Pgt : Prop) : comparison -> Prop :=
| CompEq : Peq -> CompareSpec Peq Plt Pgt Eq
| CompLt : Plt -> CompareSpec Peq Plt Pgt Lt
| CompGt : Pgt -> CompareSpec Peq Plt Pgt Gt.
Hint Constructors CompareSpec.
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.
Inductive CompareSpecT (Peq Plt Pgt : Prop) : comparison -> Type :=
| CompEqT : Peq -> CompareSpecT Peq Plt Pgt Eq
| CompLtT : Plt -> CompareSpecT Peq Plt Pgt Lt
| CompGtT : Pgt -> CompareSpecT Peq Plt Pgt Gt.
Hint Constructors CompareSpecT.
Lemma CompareSpec2Type : forall Peq Plt Pgt c,
CompareSpec Peq Plt Pgt c -> CompareSpecT Peq Plt Pgt c.
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.
Definition CompSpec {A} (eq lt : A->A->Prop)(x y:A) : comparison -> Prop :=
CompareSpec (eq x y) (lt x y) (lt y x).
Definition CompSpecT {A} (eq lt : A->A->Prop)(x y:A) : comparison -> Type :=
CompareSpecT (eq x y) (lt x y) (lt y x).
Hint Unfold CompSpec CompSpecT.
Lemma CompSpec2Type : forall A (eq lt:A->A->Prop) x y c,
CompSpec eq lt x y c -> CompSpecT eq lt x y c.
Misc Other Datatypes
Inductive identity (A:Type) (a:A) : A -> Type :=
identity_refl : identity a a.
Hint Resolve identity_refl: core.
Identity type