Bool

Section Bool.

# Defining bool and operations

We define bool : Set as a finite set with two elements: true : bool and false : bool. In set theoretic notation we would write bool = { true , false }.

The function negb : bool -> bool (boolean negation) can be defined by pattern matching using the match construct.

Definition negb (b:bool) : bool :=
match b with
| true => false
| false => true
end.

This should be familiar from g51fun - in Haskell match is called case. Indeed Haskell offers a more convenient syntax for top-level pattern.

We can evaluate the function using the slightly lengthy phrase Eval compute in (...):

Eval compute in (negb true).

The evaluator replaces

negb true

with

match true with | true => false | false => true end.

which in turn evaluates to

false

Eval compute in negb (negb true).

We know already that negb true evaluates to false hence negb (negb true) evaluates to negb false which in turn evaluates to true.

Other boolean functions can be defined just as easily:

Definition andb(b c:bool) : bool :=
if b then c else false.

Definition orb (b c : bool) : bool :=
if b then true else c.

The Coq prelude also defines the infix operators && and || for andb and orb respectively, with && having higher precedence than ||. Note however, that you cannot use ! (for negb) since this is used for other purposes in Coq.

We can now use predicate logic to show properties of boolean functions. As a first example we show that the function negb is idempotent, that is

forall b :bool, negb (negb b) = b

To prove this, the only additional thing we have to know is that we can analyze a boolean variable b : bool using destruct b which creates a case for b = true and one for b = false.

Lemma negb_idem : forall b :bool, negb (negb b) = b.
intro b.
destruct b.

Case for b = true
Our goal is negb (negb true) = true. As we have already seen negb (negb true) evaluates to true. Hence this goal can be proven using reflexivity. Indeed, we can make this visible by using simpl.

simpl.
reflexivity.

Case for b = false
This case is exactly the same as before.

simpl.
reflexivity.
Qed.

There is a shorter way to write this proof by using ; instead of , after destruct. We can also omit the simpl which we only use for cosmetic reasons.

Lemma negb_idem' : forall b :bool, negb (negb b) = b.
intro b.
destruct b;
reflexivity.
Qed.

Indeed, proving equalities of boolean functions is very straightforward. All we need is to analyze all cases and then use refl. For example to prove that andb is commutative, i.e.

forall x y : bool, andb x y = andb y x

(we use the abbrevation: forall x y : A,... is the same as forall x:Aforall, y:A, ....

Lemma andb_comm : forall x y : bool, andb x y = andb y x.
intros x y.
destruct x;
(destruct y;
reflexivity).
Qed.

We can also prove other properties of bool not directly related to the functions, for example, we know that every boolean is either true or false. That is

forall b : bool, b = true \/ b = false

This is easy to prove:

Lemma true_or_false : forall b : bool,
b = true \/ b = false.
intro b.
destruct b.
b = true
left.
reflexivity.
b = false
right.
reflexivity.
Qed.

Next we want to prove something which doesn't involve any quantifiers, namely

~ (true = false)

This is not so easy, we need a little trick. We need to embed bool into Prop, mapping true to True and false to False. This is achieved via the function Istrue:

Definition Istrue (b : bool) : Prop :=
match b with
| true => True
| false => False
end.

Lemma diff_true_false :
~ (true = false).
intro h.

We now need to use a new tactic to replace False by IsTrue False. This is possible because IsTrue False evaluates to false. We are using fold which is the inverse to unfold which we have seen earlier.

fold (Istrue false).

Now we can simply apply the equation h backwards.

rewrite<- h.

Now by unfolding we can replace Istrue true by True

unfold Istrue.

Which is easy to prove.

split.
Qed.

Actually there is a tactic discriminate which implements this proof and which allows us to prove directly that any two different constructors (like true and false) are different. We shall use discriminate in future.

# Reflection

We notice that there is a logical operator /\ which acts on Prop and a boolean operator andb (or &&) which acts on bool. How are the two related?

We can use /\ to specify andb, namely we say that andb x y = true is equivalent to x = true and y = true. That is we prove:

Lemma and_ok : forall x y : bool,
andb x y = true <-> x = true /\ y = true.
intros x y.
split.

->

destruct x.

x=true

intro h.
split.
reflexivity.
simpl in h.
exact h.

Why did the last step work?

x = false

intro h.
simpl in h.
discriminate h.

<-

intro h.
destruct h as [hx hy].
rewrite hx.
exact hy.

Qed.

End Bool.