How to prove mathematical induction formulae in LEAN theorem prover?

Question

Can anyone help me understand how to write the proof of a simple result that can be easily obtained by induction, for example the formula for the sum of the first n natural numbers: 1+2+...+n = n(n+1)/2, using the LEAN theorem prover?

Answer 1

Here is my proof. You'll need mathlib for it to work.

import algebra.big_operators tactic.ring

open finset

example (n : ℕ) : 2 * (range (n + 1)).sum id = n * (n + 1) :=
begin
  induction n with n ih,
  { refl },
  { rw [sum_range_succ, mul_add, ih, id.def, nat.succ_eq_add_one],
    ring }
end

range (n + 1) is the set of natural numbers less than n + 1, i.e. 0 to n.

I used the finset.sum function. If s is a finset and f is a function, then s.sum f is $\sum_{x \in s} f(x)$.

The induction tactic does induction. There are then two cases. The case n = 0 can be done with refl since this is nothing more than a computation.

The inductive step can be done with rw. Using a VSCode you can click after each comma in my proof to see what each rw does. This gets it into a form that the ring tactic will solve.