(* 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.