.. _sheet_1:

Tactics useful for M1F sheet 1 questions 1 to 4.
================================================

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

I will give examples of basic maths problems which are easy for humans, and show you how to solve them using Lean.

Numerical calculations with norm_num
------------------------------------

If your goal is a correct numerical equality or inequality between concrete integers, rational or real numbers, with no variables involved, then the ``norm_num`` tactic should solve it.

.. code-block:: lean

   import data.real.basic -- to get the rational and real numbers
   import tactic.norm_num -- the basic "number calculation" tactic.
		
   example : 2 + 2 = 4 :=
   begin
     norm_num
   end

   example : (2 : ℤ) + 2 = 4 :=
   begin
     norm_num
   end

   example : (2 : ℚ) + 2 = 4 :=
   begin
     norm_num
   end

   example : (2 : ℝ) + 2 = 4 :=
   begin
     norm_num
   end

This is a proof that ``2 + 2 = 4`` for the naturals, the integers, the rationals and the reals. Note : to get the nice symbols ``ℤ``, ``ℚ`` etc in VS Code you can write ``\Z``, ``\Q`` etc. If you import ``data.complex.basic`` you can even prove it for the complex numbers (although for some reason it's ``\Co`` for ``ℂ``). 

To a mathematician, all of these results are "the same theorem". But Lean is very particular about things, and if you just write ``2`` like in the first example Lean will assume you mean the natural number 2; to Lean, all these ``2`` s (the integer ``2``, the real number ``2`` etc) are different objects. In fact, although ``norm_num`` proves all of these goals, if you do a little experimentation you will find that there are other tactics which can prove some but not all of them.

``norm_num`` is a powerful tactic, and when working with reals it is essential. All of the below examples can be solved by ``norm_num``. Note also the trick of using ``by`` instead of ``begin .. end``, which works when your proof is just one tactic.

.. code-block:: lean
		
   import data.real.basic
   import tactic.norm_num

   example : (12345 : ℝ) * 54321 = 670592745 :=
   begin
     norm_num
   end

   example : (123/321 : ℚ) < 7 := by norm_num -- abbreviation for begin norm_num end

   example : (2 : ℝ) + 2 = 5 → false := by norm_num

   example : (2 : ℝ ) + 2 = 4 ∧ (3 : ℝ) ^ 3 = 27 ∧ (2 : ℚ) < 5 / 2 :=
   begin
     norm_num
   end

   example : (2 * 2 = 4 ∧ 4 + 1 = 7) → (3 + 2 < 5 ∨ 3 + 2 ≠ 6) := by norm_num

   example : ((false → false ∨ true) ∧ (¬false → true ∨ ¬false)
     ∧ (false ∧ true → ¬false) → false) → false := by norm_num
   -- should really be using `by cc` here
   
   example (H : 2 + 2 = 5) : 2 + 2 = 6 :=
   begin
     revert H,
     norm_num,
   end

That last example is a bit weird -- it might be worth checking that you understand the logic. We have a false hypothesis ``H : 2 + 2 = 5`` and we want to deduce a false conclusion ``2 + 2 = 6``. This should be possible, because false implies false. The problem is that that you can't use ``norm_num`` to prove false things. The trick is to use the ``revert`` tactic, which is the opposite of the ``intro`` tactic. After the application of ``revert`` the tactic state is this:

.. code-block:: python

   ⊢ 2 + 2 = 5 → 2 + 2 = 6

and ``norm_num`` can verify that each equality is false, reduce the goal to ``false → false``, and then solve it automatically.

To re-iterate then -- ``norm_num`` can check equalities and inequalities between concrete numbers, and also do a small amount of very basic logic (although if you _only_ have statements about ``true`` and ``false`` you should really use amore specialised tactic like ``cc``). But ``norm_num`` only works with numbers -- the tactic does not recognise variables. For example this fails:

.. code-block:: lean
		
   import data.real.basic
   import tactic.norm_num

   example (x : ℝ) : x = 2 → x + x = 4 :=
   begin
     norm_num -- fails
   end

My experience is that using Lean can be extremely frustrating if you do not have a *clear understanding* of what you can expect a given tactic to do and not to do, so I will say it again: ``norm_num`` will solve goals involving equalities or inequalities between any kinds of numbers -- *but they have to be explicit numbers*. ``norm_num`` does not deal with variables at all -- that is not its job. We need to learn more about the ``rewrite`` tactic to see how to prove ``x = 2 → x + x = 4``.

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

Before I start talking about the ``rewrite`` tactic let me briefly mention the sometimes useful and very easy ``refl`` tactic. The ``refl`` tactic closes all goals of the form ``X = X``. Here is an example:

.. code-block:: lean
		
   import data.real.basic

   example (x y z : ℝ) : (x + y) * z + x = (x + y) * z + x :=
   begin
     refl
   end
		
(or ``by refl``). But of course not all goals are quite this easy, and we need to learn how to do basic mathematical things such as expanding out brackets or subsituting. We have mentioned the rewrite tactic (``rw`` for short) before. This tactic is the way to do substitutions in Lean. Here are two simple examples of how it works.

.. code-block:: lean
		
   import data.real.basic
		
   example (x y : ℝ) (h1 : x = y)
     (h2 : y ^ 3 + 7 * y + 6 = 2) : x ^ 3 + 7 * x + 6 = 2 :=
   begin
     rw h1,
     exact h2
   end

Here ``x`` and ``y`` are numbers, ``h1`` is a proof that ``x = y``, and the line ``rw h1`` replaces all occurences of ``x`` in the goal with ``y``.

.. code-block:: lean

   example (P Q R : Prop) (h1 : P ↔ Q) (h2 : Q → (Q → R)) : P → (P → R) :=
   begin
     rw h1,
     exact h2
   end

Here ``P`` and ``Q`` are propositions, ``h1`` is a proof that ``P ↔ Q``, and the rewrite replaces all occurrences of ``P`` in the goal with ``Q``.

The ``rw`` tactic works in exactly these two situations -- if ``h`` is a proof of either an equality ``X = Y``, or an "if and only if" statement ``X ↔ Y`` , one can use ``rw h`` to replace all occurences of ``X`` in the goal with ``Y``.

There are a few variants. If ``h : X = Y`` but you want to replace all ``Y`` s in the goal with ``X`` s, then you can use ``rw ←h`` (type ``\l`` to get the left arrow). If you want to replace all ``X`` s with ``Y`` s in hypothesis ``h2`` then ``rw h at h2`` works. Finally, if after a rewrite the goal is of the form ``Z = Z`` then Lean proves it automatically, because for convenience Lean tries ``refl`` after every rewrite just to see if it gets lucky. Here are examples of these phenomena in action.

.. code-block:: lean

   import data.real.basic

   example (a b c d e : ℝ) (h1 : a = b ^ 2) (h2 : c + d = b)
     (h3 : e = a) : (c + d) ^ 2 = e :=
   begin
     rw ←h2 at h1, -- h1 now a = (c + d) ^ 2
     rw ←h1, -- goal now a = e
     rw h3 -- goal now a = a, which is automatically solved with ``refl``.
   end

One last trick is that whenever one is doing several rewrites on one object, one can do them all in one line as long as one puts the list of proofs in between square brackets. So for example this also works:

.. code-block:: lean

   import data.real.basic

   example (a b c d e : ℝ) (h1 : a = b ^ 2) (h2 : c + d = b)
     (h3 : e = a): (c + d) ^ 2 = e :=
   begin
     rw ←h2 at h1,
     rw [←h1,h3]
   end

   We can now see how to solve the problem we were stuck on before.

.. code-block:: lean

   import data.real.basic
   import tactic.norm_num

   example (x : ℝ) : x = 2 → x + x = 4 :=
   begin
     intro H, -- H : x = 2, goal x + x = 4
     rw H, -- goal now 2 + 2 = 4 
     norm_num -- now works
   end

Rewriting and ``norm_num`` put together will prove many simple results involving real numbers. Here is a convoluted example:

.. code-block:: lean

   import data.real.basic

   example (x y : ℝ) (h1 : x ^ 2 = 7) (h2 : y = 4) : x ^ 2 + 2 * y ≠ 16 :=
   begin
     rw h1,
     rw h2, -- goal now 7 + 2 * 4 ≠ 16 so we're ready for norm_num
     norm_num
   end   

These examples make rewriting look simple. In fact in practice it can and does fail, and when it does the error messages are not always helpful. Here is an example of it failing.

.. code-block:: lean
		
   example (x y z : ℕ) (h : y + z = 3) : x + y + z = x + 3 :=
   begin
     rw h, -- error!
     sorry
     end

Lean reports the following error:

.. code-block:: python

   rewrite tactic failed, did not find instance of the pattern in the target expression
     y + z
   state:
   x y z : ℕ,
   h : y + z = 3
   ⊢ x + y + z = x + 3

Lean is claiming that it cannot find ``y + z`` in the goal, even though the goal contains ``x + y + z``. What is going on? Well, Lean is suppressing brackets here, and ``x + y + z`` actually means ``(x + y) + z``, so indeed there is no direct occurrence of ``y + z`` in the goal.

How do we fix this? Well, we need to persuade Lean that ``(x + y) + z = x + (y + z)``, namely associativity of addition. Of course associativity of addition is known to Lean; indeed if you type ``#check add_assoc`` into Lean and then look at the output (click on ``#check`` in VS Code), you will see that ``add_assoc`` is a proof that for all ``x, y, z`` we have ``x + y + z = x + (y + z)`` (remember that addition in Lean is "left associative", meaning that ``x + y + z`` means by definition ``(x + y) + z``). How can we use this theorem from Lean's library? Well, it's an equality, so we can just ``rw`` it.

.. code-block:: lean
		
   example (x y z : ℕ) (h : y + z = 3) : x + y + z = x + 3 :=
   begin
     rw add_assoc,
     rw h, -- works!
   end

, or if we wanted to look clever we could write

.. code-block:: lean
		
   example (x y z : ℕ) (h : y + z = 3) : x + y + z = x + 3 :=
   by rw [add_assoc,h]		

Exercise (contrived `rw` and `norm_num`)
----------------------------------------

.. code-block:: lean

   example (a b c : ℝ) (Ha : a = 6) (Hb : b = 4) (Hc : c = 2) :
   a ^ 2 > b ∧ c ^ 2 = b ∧ b - a < 0 := sorry

``∀ x, ...`` is a function!
----------------------------

Here's a mathematical statement using the mathematical notation ``∀``, pronounced "for all".

:math:`\forall x \in \mathbb{R}, (x+1)^2 \le 2(x^2+1)`

This statement is true (can you prove it?), but that is not relevant; what I am interested in here is how to destruct it -- that is, how to use it. Let's call this statement ``P``. Now ``P`` says that for every real number ``x``, some inequality ``(x + 1) ^ 2 ≤ 2 * (x ^ 2 + 1)`` holds. So, because :math:`\frac{1}{2}` is a real number, we should be able to deduce from ``P`` that :math:`(\frac{1}{2}+1)^2\le 2(\left(\frac{1}{2}\right)^2+1)`. How do we do this?

In Lean, the way to do this is perhaps surprising. Lean regards ``P`` as a function, which takes as input a real number ``r`` and outputs a proof of the inequality ``(r + 1) ^ 2 ≤ 2 * (r ^ 2 + 1)``. So in fact ``P (1/2)`` is the proof we require.

Let's see an example of this in Lean.

.. code-block:: lean
		
   import data.real.basic
   
   example (f : ℝ → ℝ) (P : ∀ x : ℝ, f x < x) : f 3 < 3 :=
   begin
     exact P 3
   end

Note that Lean, breaking with standard maths convention, does not require the brackets around 3; mathematicians would usually write :math:`P(3)` if ``P`` were a function, but the context here makes it clear what is going on.   

Here's another application. It is not true that ``∀ x : ℝ, x ^ 2 ≤ 10 * x``, because a number like :math:`x=11` is a counterexample. Let's see how this works in Lean.

.. code-block:: lean
		
   import data.real.basic
   import tactic.norm_num

   example : ¬ (∀ x : ℝ, x ^ 2 ≤ 10 * x) :=
   begin
     intro H, -- what now??
     sorry
   end

We want to evaluate ``H`` at 11, giving us a false inequality between numbers, and then somehow use ``norm_num``, but this is difficult because ``norm_num`` only proves true goals, it doesn't know what to do with a false hypothesis. And how are we even going to make this hypothesis anyway?

To make the hypothesis we can use the ``have`` command.    
   
.. code-block::lean

   import data.real.basic
   import tactic.norm_num

   example : ¬ (∀ x : ℝ, x ^ 2 ≤ 10 * x) :=
   begin
     intro H,
     have H2 := H 11,
     sorry
   end

Before the ``have`` tactic is applied, the tactic state looks like this:

.. code-block:: python

   H : ∀ (x : ℝ), x ^ 2 ≤ 10 * x
   ⊢ false

After the ``have H2 := H 11,`` line, it looks like this:

.. code-block:: python

   H : ∀ (x : ℝ), x ^ 2 ≤ 10 * x,
   H2 : 11 ^ 2 ≤ 10 * 11
   ⊢ false

We have a new hypothesis ``H2`` which we built from the function ``H``. Now we use a technique we've seen before -- ``revert`` H2 into the goal and then use ``norm_num``.

Exercise (revert)
-----------------

Finish the proof.