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?
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.