In this level we're going to prove that 0+n=n, where n is a secret natural number.

Wait, don't we already know that? No! We know that n+0=n, but that's add_zero. This is zero_add, which is different.

The difficulty with proving 0 + n = n is that we do not have a formula for 0 + n in general, we can only use add_zero and add_succ once we know whether n is 0 or a successor. The induction tactic splits into these two cases.

The base case will require us to prove 0 + 0 = 0, and the inductive step will ask us to show that if 0 + d = d then 0 + succ d = succ d. Because 0 and successor are the only way to make numbers, this will cover all the cases.

See if you can do your first induction proof in Lean.

(By the way, if you are still in the "Editor mode" from the last world, you can swap back to "Typewriter mode" by clicking the >_ button in the top right.)

For all natural numbers n, we have 0 + n = n.

0 + n = n

theorem zero_add (n : ℕ) : 0 + n = n

Oh no! On the way to add_comm, a wild succ_add appears. succ_add a b is the proof that (succ a) + b = succ (a + b) for a and b numbers. This result is what's standing in the way of x + y = y + x. Again we have the problem that we are adding b to things, so we need to use induction to split into the cases where b = 0 and b is a successor.

For all natural numbers a, b, we have \operatorname{succ}(a) + b = \operatorname{succ}(a + b).

theorem succ_add (a b : ℕ) : succ a + b = succ (a + b)

[boss battle music]

Look in your inventory to see the proofs you have available. These should be enough.

An author can add their own Verso text here, for example a reference to the next level.

On the set of natural numbers, addition is commutative. In other words, if a and b are arbitrary natural numbers, then a + b = b + a.

theorem add_comm (a b : ℕ) : a + b = b + a

We've been adding up two numbers; in this level we will add up three.

What does x+y+z mean? It could either mean (x+y)+z, or it could mean x+(y+z). In Lean, x+y+z means (x+y)+z.

But why do we care which one it means; (x+y)+z and x+(y+z) are equal!

That's true, but we didn't prove it yet. Let's prove it now by induction.

On the set of natural numbers, addition is associative. In other words, if a, b and c are arbitrary natural numbers, we have (a + b) + c = a + (b + c).

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

add_comm b c is a proof that b + c = c + b. But if your goal is a + b + c = a + c + b then rw [add_comm b c] will not work! Because the goal means (a + b) + c = (a + c) + b so there is no b + c term directly in the goal.

Use associativity and commutativity to prove add_right_comm. You don't need induction. add_assoc moves brackets around, and add_comm moves variables around.

Remember that you can do more targeted rewrites by adding explicit variables as inputs to theorems. For example rw [add_comm b] will only do rewrites of the form b + ? = ? + b, and rw [add_comm b c] will only do rewrites of the form b + c = c + b.

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

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