.. _predicate_logic:

Predicate logic
=======================

Predicates, relations and quantifiers
--------------------------------------

Predicate logic extends propositional logic, we can use it to talk about objects and their properties. 
The objects are organized in *types*, such as ``ℕ : Type`` the type of natural
numbers  :math:`\{0,1,2,3,\dots\}`  or ``bool : Type`` the type of
booleans  :math:`\{\mathrm{tt} , \mathrm{ff}\}`, or lists over a
given ``A : Type``: ``list A : Type``,  which we will
introduce in more detail soon. To avoid talking about specific types 
we introduce some type variables:

.. code-block:: lean

  variables A B C : Type

We talk about types where you may be used to *sets*. While they are
subtle differences (types are static while we can reason about set
membership in set theory) for our purposes types are just a replacement of
sets. 

A predicate is just another word for a property, e.g. we may use ``Prime : ℕ →
Prop`` to express that a number is a prime number. We can form
propositions such as ``Prime 3`` and ``Prime 4``, the first one
should be provable while the negation of the second holds. Predicates
may have several inputs in which case we usually call them relations,
examples are ``≤ : ℕ → ℕ → Prop`` or ``inList : A → list A → Prop`` to
form propositions like ``2 ≤ 3`` and ``InList 1 [1,2,3]`` (both of
them should be provable).  

In the sequel we will use some generic predicates for examples, such
as

.. code-block:: lean

  variables P Q R : Prop
  variables A B C : Type
   
 -- BEGIN
  
  variables PP QQ : A → Prop
  -- END
  #check ∀ x : A, PP x ∧ Q
  #check (∀ x : A , PP x) ∧ Q 
  #check ∀ x:A , (∃ x : A , PP x) ∧ QQ x
  #check ∀ y:A , (∃ z : A , PP z) ∧ QQ y

The most important innovation of predicate logic are the quantifiers,
which we can use to form new propositions:

* universal quantification (``∀``), read ``∀ x : A , PP x`` as all
  ``x`` in ``A`` satisfy ``PP x``.
* existential quantification (``∃``), read ``∃ x : A, PP x`` as there
  is an ``x`` in ``A`` satsifying ``PP x``.

Both quantifiers bind weaker then any other propositional operator,
that is we read ``∀ x : A, PP x ∧ Q`` as ``∀ x : A , (PP x ∧ Q)``. We
need parenheses to limit the scope, e.g. ``(∀ x : A, PP x) ∧ Q`` which
has a different meanting to the proposition before.

It is important to understand bound variables, essentially they work
like scoped variables in programming. We can shadow variables as in
``∀ x:A , (∃ x : A , PP x) ∧ QQ x``, here the ``x`` in  ``PP x``
referes to ``∃ x : A`` while the ``x`` in ``QQ x`` refers to ``∀ x :
A``. Bound variables can be consistently renamed, hence the previous
proposition is the same as ``∀ y:A , (∃ z : A , PP z) ∧ QQ y``, which
is actually preferable since shadowing variables should be avoided
because it confuses the human reader.

Now we have introduced all these variables what can we do with
them. We have  new primitive proposition: 

* equality (``=``), given ``a b : A`` we write ``a = b`` which we read
  as ``a`` is equal to ``b``.

In the moment we only have variables as elements of types but this
will change soon when we introduce datatypes and functions.

The universal quantifier
------------------------

To prove that a proposition of the form ``∀ x : A , PP x`` holds we
assume that there is given an arbitrary element ``a`` in ``A`` and
prove it for this generic element, i.e. to prove ``PP a``, we use ``assumption a`` to do
this. If we have an assumption ``h : ∀ x : A , PP x`` and our current
goal is ``PP a`` for some ``a : A`` then we can use ``apply h`` to
prove our goal. Usuall we have some combination of implication and for
all like ``h : ∀ x : A, PP x → QQ x`` and now if our current goal is
``QQ a`` and we invoke ``apply h`` Lean will instantiate ``x`` with
``a`` and it remains to show ``QQ a``.

Best to do some examples. Let's say we want to prove

``(∀ x : A, PP x) → (∀ y : A, PP y → QQ y) → ∀ z : A , QQ z``

Here is a possible translation into english where we assume that ``A``
stands for the type of students in the class, ``PP x`` means ``x`` *is
clever* and ``QQ x`` means ``x`` *is funny* then we arrive at:

  *If all students are clever then if all clever students are funny
  then all students are funny.*

.. code-block:: lean

  variables P Q R : Prop
  variables A B C : Type
  variables PP QQ : A → Prop
  
 -- BEGIN
  example : (∀ x : A, PP x)
    → (∀ y : A, PP y → QQ y)
    → ∀ z : A , QQ z :=
  begin
    assume p pq a,
    apply pq,
    apply p,
  end
   -- END

Note that after ``assume`` the proof state is::

  p : ∀ (x : A), PP x,
  pq : ∀ (y : A), PP y → QQ y,
  a : A
  ⊢ QQ a

That is the ``x`` in ``QQ x`` has been replaced by ``a``. I could have
used ``x`` again but I though this may be misleading because you may
think that you have to use the same variable as in the quantifier.

Let's prove a logical equivalence imvolving ``∀`` and ``∧``, namely
that we can interchange them. That is we are going to prove

``(∀ x : A, PP x ∧ QQ x)  ↔ (∀ x : A , PP x) ∧ (∀ x : A, QQ x)``

To illustrate this: to say that *all students are clever and funny* is
the same as saying that *all students are clever and all students are
funny*.

Here is the Lean proof:

.. code-block:: lean

  variables P Q R : Prop
  variables A B C : Type
  variables PP QQ : A → Prop
  
  -- BEGIN
  example : (∀ x : A, PP x ∧ QQ x) 
    ↔ (∀ x : A , PP x) ∧ (∀ x : A, QQ x) :=
    begin
      constructor,
      assume h,
      constructor,
      assume a,
      have pq : PP a ∧ QQ a,
      apply h,
      cases pq with pa qa,
      exact pa,
      assume a,
      have pq : PP a ∧ QQ a,
      apply h,
      cases pq with pa qa,
      exact qa,
      assume h,
      cases h with hp hq,
      assume a,
      constructor,
      apply hp,
      apply hq,
    end
  -- END

I am using a new structural rule here. After ``assume a`` I am in the
following state (ignoring the parts not relevant now)::

  h : ∀ (x : A), PP x ∧ QQ x,
  a : A
  ⊢ PP a   

Now I cannot say ``apply h`` because ``PP a`` is not the conclusion of
the assumption. My idea is that I can prove ``PP a ∧ QQ a`` from ``h``
and from this I can prove ``PP a``. Hence I am using

``have pq : PP a ∧ QQ a,``

which creats a new goal::

  h : ∀ (x : A), PP x ∧ QQ x,
  a : A
  ⊢ PP a ∧ QQ a

  h : ∀ (x : A), PP x ∧ QQ x,
  a : A,
  pq : PP a ∧ QQ a
  ⊢ PP a

but also inserts an assumption ``pq`` in my original goal. Now I can
prove ``PP a ∧ QQ a`` using ``apply h`` and then I am left with:: 

  h : ∀ (x : A), PP x ∧ QQ x,
  a : A,
  pq : PP a ∧ QQ a
  ⊢ PP a

which I can prove using ``cases`` on ``pq``.

The existential quantifier
--------------------------

To prove a proposition of the form ``∃ x : A , PP x`` it is enough to
prove ``PP a`` for any ``a : A``. We use ``existsi a`` for
this and we are left having to prove ``PP a``. Note that ``a`` can be
any expression of type ``A`` not necessarily a variable. However so
far we haven't seen any way to construct elements, but this will
change soon.

On the other hand to use an assumption of the form
``h : ∃ x : A ,  P x`` we are using ``cases h with x px`` which
replaces ``h`` with two assumptions ``x : A`` and ``px : P x``.

Again it is best to look at an example. We are going to prove a
proposition very similar to the one for ``∀``:

``(∃ x : A, PP x) → (∀ y : A, PP y → QQ y) → ∃ z : A , QQ z``

Here is the english version using the same translation as before:

  *If there is a clever student and all clever students are funny then
  there is a funny student.*

Here is the Lean proof:

.. code-block:: lean

  variables P Q R : Prop
  variables A B C : Type
  variables PP QQ : A → Prop
  
  -- BEGIN
  example : (∃ x : A, PP x)
    → (∀ y : A, PP y → QQ y)
    → ∃ z : A , QQ z :=
  begin
    assume p pq,
    cases p with a pa,
    existsi a,
    apply pq,
    exact pa,
  end
  -- END

After the ``assume`` we are in the following state::

  p : ∃ (x : A), PP x,
  pq : ∀ (y : A), PP y → QQ y
  ⊢ ∃ (z : A), QQ z

We first take ``p`` apart using ``cases p with a pa``::

  pq : ∀ (y : A), PP y → QQ y,
  a : A,
  pa : PP a
  ⊢ ∃ (z : A), QQ z

and now we can use ``existsi a``::

  pq : ∀ (y : A), PP y → QQ y,
  a : A,
  pa : PP a
  ⊢ QQ a

which we now should know how to complete.

As ``∀`` can be exchanged with ``∧``, ``∃`` can be exchanged with
``∨``. That is we are going to prove the following equivalence:

``(∃ x : A, PP x ∨ QQ x) ↔ (∃ x : A , PP x) ∨ (∃ x : A, QQ x)``

Here is the english version

  *There is a student who is clever or funny is the same as saying
  there is a student who is funny or there is a student who is clever.*

Here is the complete lean proof (for you to step through online):
  
.. code-block:: lean

  variables P Q R : Prop
  variables A B C : Type
  variables PP QQ : A → Prop
  
  -- BEGIN
  example : (∃ x : A, PP x ∨ QQ x)
		↔ (∃ x : A , PP x) ∨ (∃ x : A, QQ x) :=
  begin
    constructor,
    assume h,
    cases h with a ha,
    cases ha with pa qa,
    left,
    existsi a,
    exact pa,
    right,
    existsi a,
    exact qa,
    assume h,
    cases h with hp hq,
    cases hp with a pa,
    existsi a,
    left,
    exact pa,
    cases hq with a qa,
    existsi a,
    right,
    exact qa,
  end
  -- END

Another Currying equivalence
----------------------------

You may have noticed that the way we prove propositions involving ``→``
and ``∀`` is very similar. In both cases wem use ``assume`` to prove
them by introducing an assumption in the first case a proposition and
in the secnde an element in a type and in both cases we use them using
``apply`` to prove the current goal. Similarily ``∧`` and ``∃`` behave
similar: in both cases we prove them using constructor where we have
to construct two components in the first case the two sides of the
conjunction and in the second the element and the proof that it
satisfies the property. And in both case we are using ``cases`` with
two components which basically replaces the assumption by its two
components. 

The similarity can be seen by establishing another currying-style
equivalence. While currying in propositional logic had the form

``P ∧ Q → R ↔ P → Q → R``

where we turn a conjunction into an implication, currying for
predicate logic has the form

``(∃ x : A, QQ x) → R  ↔ (∀ x : A , QQ x → R)``

ths time we turn an existential into a universal quantifier. For the
intuition, we use ``QQ x`` to mean ``x`` *is clever* and ``R`` means *the
professor is happy*.  Hence the equivalence is:

  *If there is a student who is clever then the professor is happy is
  equivalent to saying if any student is clever then the professor is happy.*

Here is the proof in Lean:
  
.. code-block:: lean

  variables P Q R : Prop
  variables A B C : Type
  variables PP QQ : A → Prop
  
  -- BEGIN
  theorem curry_pred : (∃ x : A, PP x) → R  ↔ (∀ x : A , PP x → R)  :=
  begin
    constructor,
    assume ppr a p,
    apply ppr,
    existsi a,
    exact p,
    assume ppr pp,
    cases pp with a p,
    apply ppr,
    exact p,
  end 
  -- END

Equality
----------------------------

There is a generic relation which can be applied to any type:
*equality*.  Given ``a b : A`` we can construct ``a = b : Prop``
expressing that ``a`` and ``b`` are equal. we can prove that
everything is equal to itself using the tactic ``reflexivity``.

.. code-block:: lean

  variables P Q R : Prop
  variables A B C : Type
  variables PP QQ : A → Prop
  
  -- BEGIN
  example : ∀ x : A, x=x :=
  begin
    assume a,
    reflexivity,
  end
  -- END

If we have assumed an equality ``h : a=b`` we can use it to *rewrite*
``a`` into ``b`` in the goal. That is if our goal is ``PP a`` we say
``rewrite h`` and this changes the goal into ``PP b``. Here is a
simple example (with a little twist):

.. code-block:: lean

  variables P Q R : Prop
  variables A B C : Type
  variables PP QQ : A → Prop
  
  -- BEGIN
  example:  ∀ x y : A, x=y → PP y → PP x :=
  begin
    assume x y eq p,
    rewrite eq,
    exact p,
  end
  -- END

Sometimes we want to use the equality in the other direction, that is
we want to replace ``b`` by ``a``. In this case we use ``rewrite←
h``. Here is another example which is actually what I wanted to do first:

.. code-block:: lean

  variables P Q R : Prop
  variables A B C : Type
  variables PP QQ : A → Prop
  
  -- BEGIN
  example:  ∀ x y : A, x=y → PP x → PP y :=
  begin
    assume x y eq p,
    rewrite← eq,
    exact p,
  end
  -- END

Equality is an *equivalence relation*, it mens that it is

- reflexive  (``∀ x : A, x=x``),
- symmetric (``∀ x y : A, x=y → y=x``)
- transitive (``∀ x y z : A, x=y → y=z → x=z``)

We have already shown reflexivity using the appropriately named
tactic. We can show symmetry and transitivity using ``rewrite``:

.. code-block:: lean

  variables P Q R : Prop
  variables A B C : Type
  variables PP QQ : A → Prop
  
  -- BEGIN
  theorem sym_eq : ∀ x y : A, x=y → y=x :=
  begin
    assume x y p,
    rewrite p,
  end
  -- END

After the assume the goal is::

  x y : A,
  p : x = y
  ⊢ y = x

Now I was expecting that after ``rewrite p`` the goal would be::

  x y : A,
  p : x = y
  ⊢ y = y

but actually ``rewrite`` automatically applies reflexivity if
possible, hence we are already done.

Moving on to transitivity:

.. code-block:: lean

  variables P Q R : Prop
  variables A B C : Type
  variables PP QQ : A → Prop
  
  -- BEGIN
  theorem trans_eq : ∀ x y z : A, x=y → y=z → x=z :=
  begin
    assume x y z xy yz,
    rewrite xy,
    exact yz,
  end
  -- END

Sometimes we want to use an equality not to rewrite the goal but to
reqrite another assumption. We can do this giving rise to another
proof of trans.

.. code-block:: lean

  variables P Q R : Prop
  variables A B C : Type
  variables PP QQ : A → Prop
  
  -- BEGIN
  theorem trans_eq : ∀ x y z : A, x=y → y=z → x=z :=
  begin
    assume x y z xy yz,
    rewrite<- xy at yz,
    exact yz,
  end
  -- END
  
That is by saying ``rewrite xy at yz`` we are using ``xy`` to rewrite
``yz``. The same works for ``rewrite←``.

Actually Lean already has built-in tactics to deal with symmetry and
transitivity which are often easier to use:

.. code-block:: lean

  variables P Q R : Prop
  variables A B C : Type
  variables PP QQ : A → Prop
  
  -- BEGIN
  example : ∀ x y : A, x=y → y=x :=
  begin
    assume x y p,
    symmetry,
    exact p
  end

  example : ∀ x y z : A, x=y → y=z → x=z :=
  begin
    assume x y z xy yz,
    transitivity,
    exact xy,
    exact yz,
  end
  -- END

After we say``transitivity`` the goals looks a bit strange::

  2 goals
  A : Type,
  x y z : A,
  xy : x = y,
  yz : y = z
  ⊢ x = ?m_1

  A : Type,
  x y z : A,
  xy : x = y,
  yz : y = z
  ⊢ ?m_1 = z

The ``?m_1`` is a placeholder since Lean cannot figure out at this
point what we are going to use as the intermidiate term. We can just
proceed, because as soon as we say ``exact xy``, Lean can figure out
that ``?m_1`` is ``y`` and we are left with::

  A : Type,
  x y z : A,
  xy : x = y,
  yz : y = z
  ⊢ y = z

which is the 2nd goal with ``?m_1`` instantiated. Actually we are not
going to use transitivity in equational proofs but we use a special
format for equational proofs indicated by ``calc``:

.. code-block:: lean

  variables P Q R : Prop
  variables A B C : Type
  variables PP QQ : A → Prop
  
  -- BEGIN
  example : ∀ x y z : A, x=y → y=z → x=z :=
  begin
    assume x y z xy yz,
    calc 
      x = y   : by exact xy
      ... = z : by exact yz,
  end
  -- END

After ``calc`` we prove a sequence of equalities where each step is
using ``by`` followed by some tactics. Any subsequent line starts with
``...`` which stends for the last expression of the previous line, in
this case ``y``.
  
There is one more property we expect from equality. Assume we have a
function ``f : A → B`` and we know that ``x = y`` for some ``x y : A``
then we want to be able to conclude that ``f x = f y``.  We say that
equality is a congruence. We can prove this easily using ``rewrite``:

.. code-block:: lean

  namespace eq		
  variables A B : Type
  
  -- BEGIN
  theorem congr_arg : ∀ f : A → B , ∀ x y : A, x = y → f x = f y :=
  begin
    assume f x y h,
    rewrite h,
  end
  -- END
  end eq
  
We will use ``congr_arg f :  ∀ x y : A, x = y → f x = f y`` when we
need that ``f`` preserves equality. 
  
There is a special proof style in Lean for equational proofs ``calc``
which enables to have more readable equational derivations, which we
will introduce later.

Classical Predicate Logic
----------------------------

We can use classical logic in predicate logic even though the
explanation using truth tables doesn't work anymore, or let's say we
have to be prepared to use infinite truth tables which need a lot of
paper to write out.

There are predicate logic counterparts of the de Morgan laws which now
say that you can move negation through a quantifier by negating the
component and switching the quantifier. And again one of them is
provable intuitionistically:

.. code-block:: lean

  variables P Q R : Prop
  variables A B C : Type
  variables PP QQ : A → Prop
  
  -- BEGIN
  theorem dm1_pred : ¬ (∃ x : A, PP x) ↔ ∀ x : A, ¬ PP x :=
  begin
    constructor,
    assume h x p,
    apply h,
    existsi x,
    exact p,
    assume h p,
    cases p with a pa,
    apply h,
    exact pa,
  end
  -- END

While the other direction again needs classical logic:

.. code-block:: lean

  variables P Q R : Prop
  variables A B C : Type
  variables PP QQ : A → Prop

  open classical

  theorem raa : ¬ ¬ P → P := 
  begin
    assume nnp,
    cases (em P) with p np,
    exact p,
    have f : false,
    apply nnp,
    exact np,
    cases f,
  end
  
  -- BEGIN
  theorem dm2_pred : ¬ (∀ x : A, PP x) ↔ ∃ x : A, ¬ PP x :=
  begin
    constructor,
    assume h,
    apply raa,
    assume ne,
    apply h,
    assume a,
    apply raa,
    assume np,
    apply ne,
    existsi a,
    exact np,
    assume h na,
    cases h with a np,
    apply np,
    apply na,
  end
  -- END

Actually I had to use indirect proof `raa` twice to derive the left to
right direction. Still our explanation we had given previously still
applies: the existential statement ``∃ x : A, ¬ PP x`` conatins
information but the negated universal one ``¬ (∀ x : A, PP x)``
deosn't. Intuitively: *knowing that not all students are stupid doesn't
give you a way to come up with a student who is not stupid*.   

Summary of tactics
---------------------

Here is the summary of basic tactics for predicate logic:

+-----------+-----------------+---------------------+
|           | How to prove ?  | How to use?         |
+===========+=================+=====================+
| ``∀``     | ``assume h``    | ``apply h``         |
+-----------+-----------------+---------------------+
| ``∃``     | ``existsi a``   | ``cases h with x p``|
+-----------+-----------------+---------------------+
| ``=``     | ``reflexivity`` | ``rewrite h``       |
|           |                 | ``rewrite← h``      |
+-----------+-----------------+---------------------+

Note that the ``a`` after ``exsistsi`` can be any expression of type
``A``, while ``h x p`` are variables.