Having to rearrange variables manually using commutativity and associativity is very tedious. We start by reminding you of this. add_left_comm is a key component in the first algorithm which we'll explain, but we need to prove it manually.

Remember that you can do precision commutativity rewriting with things like rw [add_comm b c]. And remember that a + b + c means (a + b) + c.

If a, b, c are numbers, then a+(b+c)=b+(a+c).

theorem add_left_comm (a b c : ℕ) : a + (b + c) = b + (a + c)

In some later worlds, we're going to see some much nastier levels, like (a + a + 1) + (b + b + 1) = (a + b + 1) + (a + b + 1). Brackets need to be moved around, and variables need to be swapped.

In this level, (a + b) + (c + d) = ((a + c) + d) + b, let's forget about the brackets and just think about the variable order. To turn a+b+c+d into a+c+d+b we need to swap b and c, and then swap b and d. But this is easier than you think with add_left_comm.

If a, b, c and d are numbers, we have (a + b) + (c + d) = ((a + c) + d) + b.

example (a b c d : ℕ) : a + b + (c + d) = a + c + d + b

Lean's simplifier, simp, is "rw on steroids". It will rewrite every lemma tagged with simp and every lemma fed to it by the user, as much as it can.

This level is not a level which you want to solve by hand. Get the simplifier to solve it for you.

If a, b,\ldots h are arbitrary natural numbers, we have (d + f) + (h + (a + c)) + (g + e + b) = a + b + c + d + e + f + g + h.

New: simp

Overview

Lean's simplifier, simp, will rewrite every lemma tagged with simp and every lemma fed to it by the user, as much as it can. Furthermore, it will attempt to order variables into an internal order if fed lemmas such as add_comm, so that it does not go into an infinite loop.

example (a b c d e f g h : ℕ) :
    (d + f) + (h + (a + c)) + (g + e + b) = a + b + c + d + e + f + g + h

You can make your own tactics in Lean. This code here

macro "simp_add" : tactic => `(tactic|(
  simp only [add_assoc, add_left_comm, add_comm]))

was used to create a new tactic simp_add, which runs simp only [add_assoc, add_left_comm, add_comm]. Try running simp_add to solve this level!

If a, b,\ldots h are arbitrary natural numbers, we have (d + f) + (h + (a + c)) + (g + e + b) = a + b + c + d + e + f + g + h.

New: simp_add

Overview

Our home-made tactic simp_add will solve arbitrary goals of the form a + (b + c) + (d + e) = e + (d + (c + b)) + a.

example (a b c d e f g h : ℕ) :
    (d + f) + (h + (a + c)) + (g + e + b) = a + b + c + d + e + f + g + h

We now start work on an algorithm to do addition more efficiently. Recall that we defined addition by recursion, saying what it did on 0 and successors. It is an axiom of Lean that recursion is a valid way to define functions from types such as the naturals.

Let's define a new function pred from the naturals to the naturals, which attempts to subtract 1 from the input. The definition is this:

pred 0 := 37
pred (succ n) := n

We cannot subtract one from 0, so we just return a junk value. As well as this definition, we also create a new lemma pred_succ, which says that pred (succ n) = n. Let's use this lemma to prove succ_inj, the theorem which Peano assumed as an axiom and which we have already used extensively without justification.

If \operatorname{succ}(a)=\operatorname{succ}(b) then a=b.

New: pred_succ

pred_succ n is a proof of pred (succ n) = n.

example (a b : ℕ) (h : succ a = succ b) : a = b

We define a function is_zero thus:

is_zero 0 := True
is_zero (succ n) := False

We also create two lemmas, is_zero_zero and is_zero_succ n, saying that is_zero 0 = True and is_zero (succ n) = False. Let's use these lemmas to prove succ_ne_zero, Peano's Last Axiom. Actually, we have been using zero_ne_succ before, but it's handy to have this opposite version too, which can be proved in the same way. Note: you can cheat here by using zero_ne_succ but the point of this world is to show you how to prove results like that.

If you can turn your goal into True, then the trivial tactic will solve it.

\operatorname{succ}(a) \neq 0.

New: trivial

Summary

trivial will solve the goal True.

New: is_zero_succ

is_zero_succ a is a proof of is_zero (succ a) = False.

New: is_zero_zero

is_zero_zero is a proof of is_zero 0 = True.

theorem succ_ne_zero (a : ℕ) : succ a ≠ 0

Here we begin to develop an algorithm which, given two naturals a and b, returns the answer to "does a = b?"

Here is the algorithm. First note that a and b are numbers, and hence are either 0 or successors.

*) If a and b are both 0, return "yes".

*) If one is 0 and the other is succ n, return "no".

*) If a = succ m and b = succ n, then return the answer to "does m = n?"

Our job now is to prove that this algorithm always gives the correct answer. The proof that 0 = 0 is rfl. The proof that 0 ≠ succ n is zero_ne_succ n, and the proof that succ m ≠ 0 is succ_ne_zero m. The proof that if h : m = n then succ m = succ n is rw [h] and then rfl. This level is a proof of the one remaining job we have to do: if a ≠ b then succ a ≠ succ b.

If a \neq b then \operatorname{succ}(a) \neq\operatorname{succ}(b).

New: contrapose

Summary

If you have a hypothesis

h : a ≠ b

and goal

c ≠ d

then contrapose! h replaces the set-up with its so-called "contrapositive": a hypothesis

h : c = d

and goal

a = b.

theorem succ_ne_succ (m n : ℕ) (h : m ≠ n) : succ m ≠ succ n

Implementing the algorithm for equality of naturals, and the proof that it is correct, looks like this:

instance instDecidableEq : DecidableEq ℕ
| 0, 0 => isTrue <| by
  show 0 = 0
  rfl
| succ m, 0 => isFalse <| by
  show succ m ≠ 0
  exact succ_ne_zero m
| 0, succ n => isFalse <| by
  show 0 ≠ succ n
  exact zero_ne_succ n
| succ m, succ n =>
  match instDecidableEq m n with
  | isTrue (h : m = n) => isTrue <| by
    show succ m = succ n
    rw [h]
    rfl
  | isFalse (h : m ≠ n) => isFalse <| by
    show succ m ≠ succ n
    exact succ_ne_succ m n h

This Lean code is a formally verified algorithm for deciding equality between two naturals. I've typed it in already, behind the scenes. Because the algorithm is formally verified to be correct, we can use it in Lean proofs. You can run the algorithm with the decide tactic.

20+20=40.

New: decide

Summary

decide will attempt to solve a goal if it can find an algorithm which it can run to solve it.

Example

A term of type DecidableEq ℕ is an algorithm to decide whether two naturals are equal or different. Hence, once this term is made and made into an instance, the decide tactic can use it to solve goals of the form a = b or a ≠ b.

example : (20 : ℕ) + 20 = 40

We gave a pretty unsatisfactory proof of 2 + 2 ≠ 5 earlier on; now give a nicer one.

2+2 \neq 5.

example : (2 : ℕ) + 2 ≠ 5