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.
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.
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:
⊢ 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:
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:
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.
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.
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.
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:
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.
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:
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.
example (x y z : ℕ) (h : y + z = 3) : x + y + z = x + 3 :=
begin
rw h, -- error!
sorry
end
Lean reports the following error:
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.
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
example (x y z : ℕ) (h : y + z = 3) : x + y + z = x + 3 :=
by rw [add_assoc,h]
Exercise (contrived rw and norm_num)¶
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”.
\(\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 \(\frac{1}{2}\) is a real number, we should be able to deduce from P that \((\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.
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 \(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 \(x=11\) is a counterexample. Let’s see how this works in 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.
Before the have tactic is applied, the tactic state looks like this:
H : ∀ (x : ℝ), x ^ 2 ≤ 10 * x
⊢ false
After the have H2 := H 11, line, it looks like this:
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.