(* Copyright (c) 2011, Thorsten Altenkirch *)
(** %\chapter{%##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] }.
*)
(*
In Coq we write:
[
Inductive bool : Set :=
| true : bool
| false: bool.
]
*)
(** 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.
*)
(** * Reasoning about Bool *)
(** 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:A,forall 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.