Library Bool
Section Bool.
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 (...):
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
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.
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, ....
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:
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.
reflexivity.
b = false
right.
reflexivity.
Qed.
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:
~ (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.
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:
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.