# Library Coq.Init.Datatypes

Require Import Notations.
Require Import Logic.

unit is a singleton datatype with sole inhabitant tt

Inductive unit : Set :=
tt : unit.

bool is the datatype of the boolean values true and false

Inductive bool : Set :=
| true : bool
| false : 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.

# 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

Inductive eq_true : bool -> Prop := is_eq_true : eq_true 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.

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

Inductive Empty_set : Set :=.

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

Inductive identity (A:Type) (a:A) : A -> Type :=
refl_identity : identity (A:=A) a a.
Hint Resolve refl_identity: core.

Implicit Arguments identity_ind [A].
Implicit Arguments identity_rec [A].
Implicit Arguments identity_rect [A].

option A is the extension of A with an extra element None

Inductive option (A:Type) : Type :=
| Some : A -> option A
| None : option A.

Implicit Arguments None [A].

Definition option_map (A B:Type) (f:A->B) o :=
match o with
| Some a => Some (f a)
| None => None
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.

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

Inductive comparison : Set :=
| Eq : comparison
| Lt : comparison
| Gt : comparison.

Definition CompOpp (r:comparison) :=
match r with
| Eq => Eq
| Lt => Gt
| Gt => Lt
end.

Identity

Definition ID := forall A:Type, A -> A.
Definition id : ID := fun A x => x.