.. _the_booleans:

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:

.. code-block:: lean

  namespace bool

  -- BEGIN
  inductive bool : Type
  | ff : bool
  | tt : bool  
  -- END

  end 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.

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:

.. code-block:: lean

  namespace bool

  -- BEGIN
   def bnot : bool → bool 
  | tt := ff
  | ff := tt    
  -- END

  end bool

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:

.. code-block:: lean

  namespace bool

  -- BEGIN
  def band : bool → bool → bool 
  | tt b := b
  | ff b := ff
  -- END

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:

.. code-block:: lean

  namespace bool

  -- BEGIN
  def bor : bool → bool → bool 
  | tt b := tt
  | ff b := b
  -- END

  end bool
		
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``:

.. code-block:: lean

  namespace bool

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

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

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

  local notation x && y := band x y
  local notation x || y := bor x y

  -- BEGIN
  #reduce ff && (tt || ff)
  #reduce tt && (tt || ff)  
  -- END

  end bool
  
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:

.. code-block:: lean

  namespace bool

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

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

  end bool
		
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:

.. code-block:: lean

  namespace bool

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

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

  -- BEGIN
  variable x : bool

  #reduce band tt x
  #reduce band2 tt x
  #reduce band x tt
  #reduce band2 x tt  
  -- END
  end bool
  
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.

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``:

.. code-block:: lean

  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:

.. code-block:: lean

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

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

.. code-block:: lean

  def is_tt : bool → Prop 
  | ff := false
  | tt := true
		
  -- BEGIN
  theorem cons : tt ≠ ff :=
  begin
    assume h,
    change is_tt ff,
    rewrite ← h,
    trivial,
  end

  -- 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:

.. code-block:: lean

  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.
  

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:

.. code-block:: lean

  namespace bool

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

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

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

  -- BEGIN
  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
  -- END
  end bool
  
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:

.. code-block:: lean

  namespace bool

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

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

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

  -- BEGIN
  theorem distr_b : ∀ x y z : bool, 
    x && (y || z) = x && y || x && z :=
  begin
    assume x y z,
    cases x,
    refl,
    refl,
  end
  -- END
  end bool
  
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``?

.. code-block:: lean

  namespace bool

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

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

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

  -- BEGIN
  example : ∀ x y z : bool, 
    x && (y || z) = x && y || x && z :=
  begin
    assume x y z,
    cases z,
    sorry
  end
  -- END
  end bool
  
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:

.. code-block:: lean

  namespace bool

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

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

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

  -- BEGIN
  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 
  -- END
  end bool
  
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
``&&``:

.. code-block:: lean

  namespace bool

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

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

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

  local notation x && y := band x y
  local notation x || y := bor x y

  -- BEGIN
  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
  -- END
  end bool
  
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:

.. code-block:: lean

  namespace bool

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

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

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

  local notation x && y := band x y
  local notation x || y := bor x y

  -- BEGIN
  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
  -- END
  end bool
  
Another challenge is to define

``implb : bool → bool → bool``

and

``eqb : bool → bool → bool``

and show that they implement ``→`` and ``↔`` for ``bool``.