Computing on booleans

Define the functions associated with the following boolean connectives : Notice that these functions are already defined in the standard library under the names negb, orb, andb , xorb and Bool.eqb.

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_or_and_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.

Pierre Castéran