.. _chapter_1:

Propositions
============

What we will learn here.
------------------------

Brief summary: A *proposition* is a true/false statement. Here we will learn how to prove basic abstract propositions in Lean. We will learn notation: if ``P`` and ``Q`` are propositions, then ``P → Q`` means "``P`` implies ``Q``", ``P ∧ Q`` means "``P`` and ``Q``", ``P ∨ Q`` means "``P`` or ``Q``", and ``¬ P`` means "not ``P``". For each of these concepts we will learn how to *construct* them and how to *eliminate* them in Lean. For example, given proofs of ``P`` and ``Q`` we will learn how to construct a proof of ``P ∧ Q``, and conversely given a proof of ``P ∧ Q`` we will learn how to eliminate it by turning it into a proof of ``P`` and a proof of ``Q``. We will learn the use of the following basic tactics: ``exact``, ``assumption``, ``intro``, ``left``, ``right``, ``cases`` and ``split``. 

Introduction
------------

A *proposition* is a true/false statement, like :math:`2+2=4` or :math:`2+2=5`. Rather than working with specific propositions here, we will just work with variables called things like ``P`` or ``Q`` or ``R``. So ``P`` could represent the statement :math:`2+2=1000` and ``Q`` could represent the statement of Fermat's Last Theorem.

Here's an example of a situation you might run into in Lean:

.. code-block:: python

   P Q R : Prop,
   HP : P,
   HQ : Q,
   ⊢ P

See the "turnstile" symbol `` ⊢``? The stuff before that is our assumptions. The stuff after it is what we have to prove. In the situation above, ``P Q R : Prop`` means that we're assuming that we have three propositions ``P``, ``Q`` and ``R``. We also are assuming ``HP : P`` and ``HQ : Q``, which means that we are also assuming that we have two *proofs*: ``HP`` is a proof of ``P`` and ``HQ`` is a proof of ``Q``. Our *goal*, the thing we want to prove, is ``P``. Well this is pretty easy to do, because one of the things we already have is ``HP``, a proof of ``P``. So we can prove ``P`` by writing ``exact HP``, or ``assumption`` (both work).

Try it for yourself (assuming you have an internet connection). Here is the code which puts Lean into the situation above, and instead of the proof I have written ``sorry``. Click "try it!" below and a new window will open running a live Lean session. You might want to rig it so that you can see both this window and the Lean window at the same time.

.. code-block:: lean

    example (P Q R : Prop) (HP : P) (HQ : Q) : P :=
    begin
      sorry,
    end

Wait for the Lean window to stop saying "(running)" at the top. You should see a complaint on the right that we used ``sorry``, and you might spot that ``example`` is underlined in green. This means that Lean is unhappy -- you have not proved the theorem yet. Now change the ``sorry,`` on the left to ``exact HP,`` and check that Lean is happy that you've proved the theorem (i.e. solved the goal). Lean is happy when there is nothing underlined in red or green on the left. If you move your cursor to after the word ``end`` you will see no output at all on the right -- this is another indication that Lean is happy. ``exact`` is an example of a *tactic*, and between the ``begin`` and ``end`` of a proof Lean expects tactics, separated by commas.

Change your proof to ``exact HQ,`` and see that Lean becomes unhappy again: ``HQ`` is not a proof of ``P``. Change it to ``assumption,`` and it's happy once more. Change it to ``exact P,`` and it doesn't work -- ``P`` is the statement, not the proof. Lean wants the proof of ``P``, which is ``HP``. Don't confuse a statement and its proof. You can see the difference between a proposition and its proof; ``P : Prop`` means "the type of ``P`` is ``Prop``", which is a fancy way of saying that ``P`` is a proposition (a true/false statement)

Change your proof back to a correct proof, e.g. ``exact HP,``, and then click around a bit. See that sometimes there is no output on the right, and sometimes Lean prints something? If you are in the middle of the proof (e.g. if your cursor is just after the word ``begin``) then Lean prints the goal, which has not been proved yet: the proof happens one line later. Move your cursor up and down the arrow keys and see how the output on the right changes.

Implications ``P → Q`` (`intro`, `apply`)
-----------------------------------------

If ``P`` and ``Q`` are propositions, then so is ``P → Q``, pronounced "``P`` implies ``Q``". Here is the truth table for ``P → Q``:

= = ======
P Q P → Q
= = ======
T T      T
T F      F
F T      T
F F      T
= = ======

We're ready to see how to work with ``P → Q`` in Lean. The high-powered summary: to construct it, we use ``intro``, and to eliminate it we use ``apply``. Let me explain much more about what I mean.

First, let's assume we have a proof of ``P → Q``. Let's see how to deduce a proof of ``Q`` from a proof of ``P``.

.. code-block:: lean

   theorem easy (P Q : Prop) (HP : P) (HPQ : P → Q) : Q :=
   begin
     sorry,
   end
   
Click "try it!" to try solving this goal. Delete ``sorry,`` and see Lean complaining that there are unsolved goals. Lean's state looks like this:	

.. code-block:: python

   P Q : Prop,
   HP : P,
   HPQ : P → Q
   ⊢ Q

Our assumptions are that we have two propositions ``P`` and ``Q``, and a proof (called ``HP``) of ``P``, and a proof (called ``HPQ``) that ``P`` implies ``Q``. You can get that implication arrow by writing ``\r`` (r for right) by the way. We want a proof of ``Q``.

There are several ways to prove this theorem. The big question of course is how to use ``HPQ``. You can use it by ``apply`` ing it:

.. code-block:: lean
		
   theorem easy (P Q : Prop) (HP : P) (HPQ : P → Q) : Q :=
   begin
     apply HPQ,
     sorry,
   end
   
Applying ``HPQ``, the proof of ``P → Q``, turns the goal of proving ``Q`` to the new goal of proving ``P``. ``apply`` is of course a tactic. You should be able to finish the job now, so replace the sorry and finish the proof. Then put your cursor at the beginning of a line and move up and down through the proof script -- you will see the goal change as you move around.

An alternative approach is to regard ``HPQ`` as a function which sends proofs of ``P`` to proofs of ``Q``. This is quite a weird way of thinking about what ``P → Q`` means at first, but Lean is happy to think about ``HPQ`` as a function this way. This means that ``HPQ(HP)`` is a proof of ``Q``, so another way of proving the theorem is

.. code-block:: lean
		
   theorem easy (P Q : Prop) (HP : P) (HPQ : P → Q) : Q :=
   begin
     exact HPQ(HP),
   end

We could even say that because ``HPQ`` is a function expecting a proof of ``P`` as input, we don't even need the brackets, and can even write ``HPQ HP``:

.. code-block:: lean
		
   theorem easy (P Q : Prop) (HP : P) (HPQ : P → Q) : Q :=
   begin
     exact HPQ HP,
   end
   
Using ``apply``, or evaluating a proof of ``P → Q`` at a proof of ``P``, are two ways to *eliminate* (i.e. use) a proof of ``P → Q``. What about the other way? What if our goal is to *prove* ``P → Q``?

.. code-block:: lean

   theorem prove_P_implies_Q (P Q : Prop) (HQ : Q) : P → Q :=
   begin
     sorry,
   end

To prove ``P → Q`` the idea is that we should assume we have a proof of ``P``, and then simply try to prove ``Q``. The way to do this in Lean is the ``intro`` tactic (by the way, lines which begin ``--`` are just comments):

.. code-block:: lean

   theorem prove_P_implies_Q (P Q : Prop) (HQ : Q) : P → Q :=
   begin
     intro HP,
     -- we now have a proof HP of P in our assumptions
     -- and our goal is now to prove Q
     exact HQ,
   end

The ``intro`` tactic is a *constructor* for ``P → Q`` -- if our goal is ``P → Q`` then we can type ``intro HP`` and Lean then proves our goal, modulo some other simpler things (namely a proof of ``Q``) which we can work on later. 

Exercise (``P → P``)
---------------------

Try proving this:

.. code-block:: lean

   theorem P_implies_P (P : Prop) : P → P :=
   begin
     sorry,
   end
		
Exercise (intros)
-----------------

Now see if you can prove this:

.. code-block:: lean

   theorem needs_intros (P Q R : Prop) (HR : R) : P → (Q → R) :=
   begin
     sorry,
   end

A related question: what do you think ``P → Q → R`` means in Lean? It will surely either mean ``(P → Q) → R`` or ``P → (Q → R)`` (a fancy equivalent way of saying this is that ``→`` is either left associative or right associative): try replacing ``P → (Q → R)`` above with ``P → Q → R`` and see if the proof still works.
  
true, false, and ``¬``
----------------------

Some propositions, like the Riemann Hypothesis and other hard maths questions, are currently open questions -- we don't know whether they're true or false. At the other extreme, there is a proposition called ``true`` which is true by definition, and whose proof is called ``trivial``:

.. code-block:: lean

   theorem very_easy : true :=
   begin
     exact trivial,
   end

We could say that ``trivial`` is a constructor for ``true``. At the other extreme, there is also a proposition called ``false``, which is false, and if you can prove this without any hypotheses at all then you've either found a contradiction in mathematics, which would surprise many experts, or a serious bug in Lean, which I guess could be possible, but again is unlikely. Note that ``false`` has no constructors at all!

.. code-block:: lean

   theorem very_hard : false :=
   begin
     sorry,
   end

On the other hand, given some hypotheses which don't add up, we can indeed sometimes prove ``false`` using them. For example, ``false → false`` is true, indeed it's a special case of ``P → P``, so we should be able to prove it no problem:

.. code-block:: lean

   theorem false_implies_false : false → false :=
   begin
     intro Hfalse,
     exact Hfalse,
   end

After the `intro Hfalse` line, our state looks like this:

.. code-block:: python

   Hfalse : false
   ⊢ false
		
The moral is: you sometimes *can* prove ``false``, but only if your assumptions don't add up. In fact this is exactly what people do in the middle of a proof by contradiction.
   
But what is the point of having a proposition which is false? Well, I've already mentioned proofs by contradiction and we'll come back to these in a minute. But also it comes up in Lean's definition of "not" -- if ``P`` is a proposition, then ``not P``, written ``¬ P`` in Lean (use ``\not`` to get the not symbol), is *defined* to mean ``P → false``. Thinking about this, it makes sense: if ``P`` is true, then ``P → false`` is ``true → false``, which is false, and on the other hand if ``P`` is false, then ``P → false`` means ``false → false``, which is true.

Of course ``¬ (¬ P)`` will have the same truth value as ``P``. Let's see if we can get Lean to prove that ``P`` implies ``¬ (¬ P)``.

.. code-block:: lean

   theorem not_not (P : Prop) : P → ¬ (¬ P) :=
   begin
     sorry,
   end

Our goal is an implication, so we can start with ``intro HP,`` and we will end up with the following state:
   
.. code-block:: python
 
   P : Prop,
   HP : P
   ⊢ ¬¬P

Now our goal is ``¬¬P`` and this is by definition ``¬(¬P)`` which is by definition ``(¬P) → false``. This is another implication, so we can eliminate it with the ``intro`` tactic again:

.. code-block:: lean

   theorem not_not (P : Prop) : P → ¬ (¬ P) :=
   begin
     intro HP,
     intro HnP,
     sorry,
   end

Things are perhaps not looking good now, or at least they're looking a bit weird. Lean's state is this:

.. code-block:: python

   P : Prop,
   HP : P,
   HnP : ¬P
   ⊢ false

so our goal is something which can't be proved. Actually that's not quite true -- our goal is something which can't be proved given no hypotheses at all. But here we are still OK -- our hypotheses are contradictory; we have a proof that ``P`` is true and also a proof that it's not true, so we should be able to deduce a contradiction, which is the same thing as a proof of ``false``. You might want to think about how to do this, before we move on.

The trick is that ``HnP`` is a proof of ``¬P``, or in other words a proof of ``P → false``. Our goal is ``false``, so we can ``apply HnP`` to reduce our goal from ``false`` to ``P``. If this seems a bit weird, just imagine that ``Q`` was a random proposition, and our goal was ``Q``. If we had a proof of ``P → Q`` we could apply this proof and reduce our goal to proving ``P``. This is exactly what we're doing here, in the special case that ``Q`` turns out to be false.

.. code-block:: lean

   theorem not_not (P : Prop) : P → ¬ (¬ P) :=
   begin
     intro HP,
     intro HnP,
     apply HnP,
     exact HP,
   end

Remember -- ``¬ P`` is just another way of saying ``P → false``.

Exercise (contrapositive)
-------------------------

The *contrapositive* of the proposition ``P → Q`` is the proposition ``¬ Q → ¬ P``. The contrapositive of an implication is equivalent to the implication itself. See if you can deduce the contrapositive of ``P → Q`` given a proof of ``P → Q``.

.. code-block:: lean

   theorem contrapositive
     (P Q : Prop) (HPQ : P → Q) : ¬ Q → ¬ P :=
   begin
     sorry,
   end

For a bonus point, can you come up with a three-line proof of this theorem which uses the ``intro`` tactic twice and then the ``exact`` tactic once?

Working with "or": ``P ∨ Q``
-----------------------------

``P ∨ Q`` is true if either ``P`` is true, or ``Q`` is true (or both). Here's a truth table:

= = =====
P Q P ∨ Q
= = =====
T T T
T F T
F T T
F F F
= = =====

How do we construct a proof of ``P ∨ Q``? Well, there are two ways. We could either deduce it from a proof that ``P`` is true, or from a proof that ``Q`` is true. So there should be two constructors, that is, two ways of making progress if our goal is ``P ∨ Q``. The corresponding two tactics are called ``left`` and ``right``.

.. code-block:: lean

   theorem P_implies_P_or_Q (P Q : Prop) (HP : P) : P ∨ Q :=
   begin
     left,
     exact HP,
   end

Exercise (right)
----------------

Try the other one for yourself:

.. code-block:: lean

   theorem Q_implies_P_or_Q (P Q : Prop) (HQ : Q) : P ∨ Q :=
   begin
     sorry,
   end

Of course, deciding which constructor to use depends on the situation you are in. Choosing the wrong one can leave you in an impossible situation.

.. code-block:: lean

   theorem dont_get_lost (P Q :Prop) (HQ : Q) : P ∨ Q :=
   begin
     left,
     -- the goal is no longer provable!
     sorry
   end

If you take a wrong turn, you might be in trouble. Go back and try something else.

We've seen the two constructors for "or", but what about the eliminator? In other words, how can we use a hypothesis of the form ``P ∨ Q``? Let's try and prove that ``P ∨ Q`` implies ``Q ∨ P``.

.. code-block:: lean

   theorem or_symmetry (P Q : Prop) : P ∨ Q → Q ∨ P :=
   begin
     sorry,
   end
   
Fire up a Lean session with the above code. Our first move is obvious -- ``intro HPQ``. But now we can't use ``left`` or ``right`` next, because we don't know which one we are supposed to be proving. We need to eliminate (i.e., use) ``HPQ`` first. We can do this with the ``cases`` tactic.

.. code-block:: lean

   theorem or_symmetry (P Q : Prop) : P ∨ Q → Q ∨ P :=
   begin
     intro HPQ,
     cases HPQ with HP HQ,
     sorry,
   end

Try that. Wooah! Something weird happened!
   
.. code-block:: python

   2 goals
   case or.inl
   P Q : Prop,
   HP : P
   ⊢ Q ∨ P

   case or.inr
   P Q : Prop,
   HQ : Q
   ⊢ Q ∨ P
   
Instead of one goal, we now have two! In the first goal, we have a proof ``HP`` of ``P``, and in the second we have a proof of ``Q``. So now we want to go right in the first goal, and left in the second. What happens if we just type another tactic? Turns out it just gets applied to the goal at the top. So we could now finish the proof like this:

.. code-block:: lean

   theorem or_symmetry (P Q : Prop) : P ∨ Q → Q ∨ P :=
   begin
     intro HPQ,
     cases HPQ with HP HQ,
     right,
     exact HP,
     left,
     exact HQ,
   end

But this is generally regarded as bad style. There are two approved ways to do this; the first is to indent two more spaces whenever a new goal appears, and then unindent when one disappears, like this:

.. code-block:: lean
		
   theorem or_symmetry (P Q : Prop) : P ∨ Q → Q ∨ P :=
   begin
     intro HPQ,
     cases HPQ with HP HQ,
       right,
       exact HP,
     left,
     exact HQ,
   end
   
The second is to use squiggly brackets and deal with each goal individually:

.. code-block:: lean
		
   theorem or_symmetry (P Q : Prop) : P ∨ Q → Q ∨ P :=
   begin
     intro HPQ,
     cases HPQ with HP HQ,
     { right,
       exact HP,
     },
     { left,
       exact HQ,
     },
   end

Try running the above code in the Lean Web Editor, and move your cursor around to see what these squiggly brackets do. It can get confusing if there is more than one goal, and this technique ensures that only one goal can be seen at a time.
   
What do you think ``cases`` does on a goal of the form ``P ∨ Q ∨ R``? Try it and find out.

.. code-block:: lean

   theorem or_experiment (P Q R : Prop) (HPQR : P ∨ Q ∨ R) : true :=
   begin
     cases HPQR with H1 H2,
     sorry,
   end

Operators like ``∨`` have an "associativity" in Lean, and ``∨`` is *right-associative*, which means that ``P ∨ Q ∨ R`` is parsed by Lean as ``P ∨ (Q ∨ R)``.
   
Exercise (or_associativity)
---------------------------

Try proving this:

.. code-block:: lean

   theorem or_associative (P Q R : Prop) :
   P ∨ (Q ∨ R) → (P ∨ Q) ∨ R :=
   begin
     sorry,
   end

Working with And (``P ∧ Q``)
-----------------------------

If ``P`` and ``Q`` are propositions, then ``P ∧ Q`` is the proposition which is true exactly when both ``P`` and ``Q`` are true. Here is the truth table for and:

= = =
P Q P ∧ Q
= = =
T T T
T F F
F T F
F F F
= = =

If our goal is of the form ``P ∧ Q``, then the tactic we use to construct a proof of it is ``split``. Before you run the following code, think a little about what should happen after the ``split`` statement:

.. code-block:: lean

   theorem and_definition (P Q : Prop) (HP : P) (HQ : Q) : P ∧ Q :=
   begin
     split,
     -- what will the state be now?
     sorry,sorry,
   end

The ``split`` tactic turns our one goal of proving ``P ∧ Q`` into two goals, namely ``P`` and ``Q``.
   
Exercise (and_definition)
-------------------------

Finish the above proof.

So ``split`` can be thought of as a constructor. What about the eliminator? It's just ``cases`` again. In contrast to the ``and`` example, ``cases`` doesn't create two goals from one -- it just creates two hypotheses from one. Here is a proof of symmetry of ``and``:

.. code-block:: lean

   theorem and_symmetric (P Q : Prop) : P ∧ Q → Q ∧ P :=
   begin
     intro HPQ,
     cases HPQ with HP HQ,
     split,
     { exact HQ,},
     { exact HP,},
   end

Exercise (transitivity of and)

Try this one.

.. code-block:: lean

   theorem and_transitive (P Q R : Prop) :
   (P ∧ Q) ∧ (Q ∧ R) → (P ∧ R) :=
   begin
     sorry,
   end

Dealing with iff (↔)
---------------------

From the point of view of general abstract behaviour, iff (you can get the symbol with ``\iff`` in the Lean Web Editor) is rather like "and". To prove ``P ∧ Q`` you need to supply two things -- a proof of ``P`` and a proof of ``Q``. Similarly, to prove ``P ↔ Q`` you have to supply both a proof of ``P → Q`` and of ``Q → P``. So, just as with ``and``, if your goal is ``P ↔ Q`` you can make progress using ``split``, and if you have a hypothesis ``H : P ↔ Q`` you can use the tactic ``cases H with HPQ HQP``, which will leave you with two new hypotheses ``HPQ : P → Q`` and ``HQP : Q → P``. Try these.

Exercise (symmetry of iff)
--------------------------

.. code-block:: lean

   theorem iff_symmetric (P Q : Prop) : (P ↔ Q) ↔ (Q ↔ P) :=
   begin
     sorry
   end
		
Exercise (transitivity of iff)
------------------------------

.. code-block:: lean

   theorem iff_transitive (P Q R : Prop) :
   (P ↔ Q) ∧ (Q ↔ R) → (P ↔ R) :=
   begin
     sorry
   end

The rewrite tactic
------------------

If you did the above exercise you might have found it a bit tedious. But in fact
there are loads of tricks which you can use to make proofs shorter. To give
you an example, here is an extremely short proof of ``iff_transitive`` :

.. code-block:: lean

   theorem iff_transitive (P Q R : Prop) :
   (P ↔ Q) ∧ (Q ↔ R) → (P ↔ R) :=
   λ ⟨H1,H2⟩,by rwa H1

As you can see, Lean has lots of secrets, many of which have not yet been divulged.
But here is one -- the ``rewrite`` tactic, commonly abbreviated to ``rw``.

.. code-block:: lean

   theorem iff_transitive (P Q R : Prop) :
   (P ↔ Q) ∧ (Q ↔ R) → (P ↔ R) :=
   begin
     intro H,
     cases H with HPQ HQR,
     rw HPQ,
     exact HQR
   end

What's happening here is that because ``HPQ`` is a proof of ``(P ↔ Q)``, and hence a proof that ``P`` and ``Q`` are logically equivalent, you can use the ``rw`` tactic to replace any ``P`` in the goal with a ``Q``. Before the rewrite, the goal was ``P ↔ R``, and afterwards it is ``Q ↔ R``, which is precisely ``HQR``. Rewriting can be done with any ``iff`` statement and also any equality, and is a powerful and useful part of Lean's armoury.

		
If all else fails
-----------------

Mathematicians think of propositions as statements which can either be true or false. But surprisingly, we never used this assumption in the above arguments, we could always argue directly rather than proving things by checking that the truth tables worked out in every case. Assuming that a general proposition is either true or false actually has a name - it's called the "law of the excluded middle", and it is called ``classical.em`` (``em`` for "excluded middle") in Lean. Here's an example which we cannot prove given the tools introduced above:

.. code-block:: lean

   theorem not_not (P : Prop) :
   ¬ (¬ P) → P :=
   begin
     sorry
   end

This is hopeless to do with the tools we have, because ``¬ (¬ P)`` is barely usable as a hypothesis, and we really have to approach this one on a case by case basis. The trick is to break into the two cases ``P`` true and ``P`` false. We can do this because ``classical.em P`` is exactly the statement ``P ∨ ¬ P``, and we can just do ``cases`` on this.

.. code-block:: lean
		   
   theorem not_not (P : Prop) : ¬ (¬ P) → P :=
   begin
     cases (classical.em P) with HP HnP,
     { intro HnnP,
       exact HP,
     },
     { intro HnnP,
       exfalso,
       apply HnnP,
       exact HnP
     }
   end

Note ``exfalso``, which changes an arbitrary goal into the goal ``false`` by applying ``false → Q``, a statement which is true for any goal ``Q``.
   
Exercise (contrapositive)
-------------------------

We proved earlier that ``P → Q`` implied its contrapositive, ``¬ Q → ¬ P``. Now show that ``¬ Q → ¬ P`` implies ``P → Q``!

.. code-block:: lean

   theorem contra (P Q : Prop) : (¬ Q → ¬ P) → (P → Q) :=
   begin
     sorry
   end