# Computing on booleans

Define the functions associated with the following boolean connectives :
bool_not : bool -> bool
bool_or : bool->bool->bool
bool-and : bool->bool->bool
bool_xor : bool->bool->bool
bool_eq : bool->bool->bool

Prove the following theorems :
Theorem bool_xor_not_eq :
(b1,b2:bool)(bool_xor b1 b2)=(bool_not (bool_eq b1 b2)).
Theorem bool_not_and :
(b1,b2:bool)(bool_not (bool_and b1 b2))=
(bool_or (bool_not b1) (bool_not b2)).
Theorem bool_not_not : (b:bool)(bool_not (bool_not b))=b.
Theorem bool_tex : (b:bool)(bool_or b (bool_not b))=true.
Theorem bool_eq_reflect : (b1,b2:bool)(bool_eq b1 b2)=true -> b1=b2.
Theorem bool_eq_reflect2 : (b1,b2:bool)b1=b2 ->(bool_eq b1 b2)=true.
Theorem bool_not_or : (b1,b2:bool)(bool_not (bool_or b1 b2))=
(bool_and (bool_not b1) (bool_not b2)).
Theorem bool_distr: (b1,b2,b3:bool)
(bool_or (bool_and b1 b3) (bool_and b2 b3))=
(bool_and (bool_or b1 b2) b3).

## Solution

exobool.v
### Note

Please notice the difference between the data type ` bool : Set `,
which has only two inhabitants, and the type ` Prop : Type `
of all propositions, which has an infinite number of inhabitants.

Since `Prop` and `bool` are very different types,
the reader must not be puzzled by the boolean versions of double negation
(`bool_not_not`) and excluded middle (`bool_tex`).
Let us recall that the following propositions *do not hold*
in *Coq*!
(P:Prop)~~P <->P
(P:Prop) P \/~P

Notice also that the theorems `bool_eq_reflect` and
`bool_eq_reflect2` establish a bridge between the boolean
function `bool_eq` and the Leibniz equality `eq`.

Going home

Pierre Castéran