5. The Booleans

The logic we have introduced so far was very generic. We fix this in this chapter by looking at a very simple type, the booleans bool which has just two elements tt (for true) and ff (for false) and functions on this type. Then we are going to use predicate logic to prove some simple theorems about booleans.

In the lean prelude bool is defined as an inductive type:

try it!

inductive bool : Type
| ff : bool
| tt : bool

This declaration means:

• There is a new type bool : Type,
• There are two elements tt ff : bool,
• These are the only elements of bool,
• tt and ff are different elements of bool.

Inductive is quite versatile we can use it to define other finite types, infinite types like ℕ and type constructors like maybe or list. It is similar to the data type constructor in Haskell but not exactly since there are data definitions in Haskell which are not permitted in Lean.

5.1. Functions on bool

Let’s define negation on booleans this is a function bnot : bool → bool. By a function here we mean something which we can feed an element of the input type (here bool) and it will return an element of the output type (here bool again. We can do this by matching all possible inputs:

try it!

 def bnot : bool → bool
| tt := ff
| ff := tt

To define a function with two inputs, like and for booleans band we use currying, that is band applied to a boolean returns a function which applied to the 2nd boolean returns a boolean, hence band : bool → bool → bool. As we have already seen → is right associative hence putting the extra brackets in the type is band :bool → (bool → bool).

We could list all the four cases, reproducing the truth table, but we get away with just two matching only on the first argument:

try it!

def band : bool → bool → bool
| tt b := b
| ff b := ff

If the first argument is tt, that is we look at band tt : bool → bool then this is just the identity on the snd argument, because band tt tt = tt and band tt ff = ff. If the first argument is ff then the outcome wil be ff whatever the 2nd argument its. With other words band ff : bool → bool is the constant function which will always return ff.

Symmetrically we can define bor : bool → bool → bool with just two cases:

try it!

def bor : bool → bool → bool
| tt b := tt
| ff b := b

In this case if the first argument is tt, bor tt : bool → bool is always tt while if the first argument is ff, bor ff : bool → bool is just the identity.

The lean prelude also introduces the standard infix notation for operations on bool:

x && y := band x y

and

x || y := bor x y.

We can evaluate boolean expressions using #reduce:

try it!

#reduce ff && (tt || ff)
#reduce tt && (tt || ff)

When I defined the binary boolean functions my choice to match on the first argument was quite arbitrary, I could have used the 2nd argument just as well:

try it!

def band2 : bool → bool → bool
| b tt := b
| b ff := ff

def bor2 : bool → bool → bool
| b tt := tt
| b ff := b

These functions produce the same truth table as the ones we have defined before but their computational behaviour is different which is important when we prove something about them. This can be seen by applying them to a variable:

try it!

variable x : bool

#reduce band tt x
#reduce band2 tt x
#reduce band x tt
#reduce band2 x tt

We see that band tt x reduces to x because it matches on the first argument, while band2 x tt is stuck, it needs to see what x turns out to be. If we fix the 2nd argument it is just the other way around, this time band2 is better behaved.

When we are doing proofs it is important to remember how the function is defined because when we are doing case analysis we should instantiate the arguments which allow us to reduce the function, if possible.

5.2. Proving some basic properties

To reason about bool we can use cases x to analyze a variable x : bool which means that there are two possibilities tt and ff. For example we can state and prove in predicate logic that every element of bool is either tt or ff:

try it!

example : ∀ x : bool, x=tt ∨ x=ff :=
begin
  assume x,
  cases x,
  right,
  refl,
  left,
  refl,
end

After assume x we are in the following state:

x : bool
⊢ x = tt ∨ x = ff

And after cases x we get two subgoals:

2 goals
case bool.ff
⊢ ff = tt ∨ ff = ff

case bool.tt
⊢ tt = tt ∨ tt = ff

Both of them are straightforward to prove. Now lets prove that both are different. The idea is to define a predicate is_tt : bool → Prop by case analysis:

try it!

def is_tt : bool → Prop
| ff := false
| tt := true

Now we can use is_tt to show that tt and ff cannot be equal:

try it!

theorem cons : tt ≠ ff :=
begin
  assume h,
  change is_tt ff,
  rewrite ← h,
  trivial,
end

Here I am using tt ≠ ff which just a shorthand for ¬ (tt = ff) (and which again is just short for tt = ff → false).

I am also using a new tactic change which replaces the current goal with another one that is definitionally the same. In our case we have::

h : tt = ff
⊢ false

and we know that is_tt ff = false hance we can say change  is_tt ff to replace the goal:

h : tt = ff ⊢ is_tt ff

But now we can use rewrite ← h to change the goal to is_tt tt which is equal to true and hence provable by trivial.

However, since this is a common situation Lean provides the tactic contradiction which we can use to prove goals like this:

try it!

example :   tt ≠ ff  :=
begin
  assume h,
  contradiction,
end

contradiction will solve the current goal if there is an inconsistent assumption like assuming that two different constructors of an inductive type are equal.

5.3. Proving equations about bool

Ok next let’s prove some interesting equalities. We are going to revisit our old friend, distributivity but this time for booleans:

try it!

theorem distr_b : ∀ x y z : bool,
  x && (y || z) = x && y || x && z :=
begin
  assume x y z,
  cases x,
  dsimp [band],
  dsimp [bor],
  refl,
  dsimp [band],
  refl,
end

After assume x y z, we are in the following state:

x y z : bool
⊢ x && (y || z) = x && y || x && z

We do case analysis on x which can be either tt or ff. Hence after cases x we are left with two subgoals:

2 goals
case bool.ff
y z : bool
⊢ ff && (y || z) = ff && y || ff && z

case bool.tt
y z : bool
⊢ tt && (y || z) = tt && y || tt && z

Let’s just discuss the first one. We can instruct Lean to use the definition of && (i.e. band) by saying dsimp [band], we are left with

y z : bool
⊢ ff = ff || ff

Now we just need to apply the definition of || (i..e bor) using dsimp [bor]:

y z : bool
⊢ ff = ff

and now we only need to use refl to dispose of this goal.

Can you see why in the 2nd case it is enough to use dsimp [band].

We can apply several definitions in one tactic, i.e. in the first case dsimp [band,bor] would have done the same. But actually in this proof there is no need for dsimp at all because refl will automatically reduce its arguments, hence we could have just written:

try it!

theorem distr_b : ∀ x y z : bool,
  x && (y || z) = x && y || x && z :=
begin
  assume x y z,
  cases x,
  refl,
  refl,
end

However, when doing proofs interactively it may be helpful to see the reductions. Also, later we will encounter cases where using dsimp is actually necessary.

Could we have used another variable than x. Let’s see what about z?

try it!

example : ∀ x y z : bool,
  x && (y || z) = x && y || x && z :=
begin
  assume x y z,
  cases z,
  sorry
end

After cases zz we are in stuck in the following state:

x y : bool
⊢ x && (y || ff) = x && y || x && ff

No reduction is possible because we have defined the functions matching on the first argument. Using cases y would have done a bit reduction but not enough. cases x was the right choice.

Now have a go at the de Morgan laws for bool yourselves, both are provable just using case analysis:

try it!

theorem dm1_b : ∀ x y : bool, bnot (x || y) = bnot x && bnot y :=
begin
  sorry,
end

theorem dm2_b : ∀ x y : bool, bnot (x && y) = bnot x || bnot y :=
begin
  sorry,
end

5.4. Relating bool and Prop

I am sure it has not escaped you that we seem to define logical operations twice: once for Prop and once for bool. How are the two related? Indeed we can use is_tt for example to relate ∧ and &&:

try it!

theorem and_thm : ∀ x y : bool, is_tt x ∧ is_tt y ↔ is_tt (x && y) :=
begin
  assume x y,
  constructor,
  assume h,
  cases h with xtt ytt,
  cases x,
  cases xtt,
  cases y,
  cases ytt,
  constructor,
  assume h,
  cases x,
  cases h,
  cases y,
  cases h,
  constructor,
  constructor,
  constructor,
end

I recommend to step through the proof, we are only using tactics I have already explained. Note that cases x is used for two things: for doing case analysis on booleans and to eliminate inconsistent assumptions.

I leave it is an exercise to prove the corresponding facts about negation and disjunction:

try it!

theorem not_thm : ∀ x : bool, ¬ (is_tt x) ↔ is_tt (bnot x) :=
begin
  sorry,
end

theorem or_thm : ∀ x y : bool, is_tt x ∨ is_tt y ↔ is_tt (x || y) :=
begin
  sorry,
end

Another challenge is to define

implb : bool → bool → bool

and

eqb : bool → bool → bool

and show that they implement → and ↔ for bool.