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.

Answer 2

I was just going through this exercise while trying to learn Lean 4. Here is my solution (so far, likely lots of room for improvement):

import Mathlib.Tactic.Ring

-- summing 1 + 2 + ... + n
def sum_first_n(n: Nat) : Nat :=
  match n with
  | 0 => 0
  | m + 1 => m + 1 + sum_first_n m

-- summing 1 + 2 + ... + n == n * (n + 1) / 2
theorem sum_first_n_eq_my_definition(n: Nat) : sum_first_n n = n * (n + 1) / 2 := by
  induction n
  . simp [sum_first_n]
  case succ m ih =>
    simp [sum_first_n]
    rw [ih]
    ring_nf
    rw [(by ring: m * 3 = m * 2 + m)]
    rw [(by ring: 2 + (m * 2 + m) = 2 * (m + 1) + m)]
    rw [Nat.add_assoc (2 * (m + 1)) _ _, Nat.add_comm (2 * (m + 1)) _]
    rw [Nat.add_mul_div_left _ _ (by decide : (0 < 2))]
    ring

This should work for the range and sum definition (not the custom sum function), but I am having hard time unrolling the foldr:

theorem sum_n_plus_one(n: Nat) : Nat.sum (List.range (n + 1)) = n + Nat.sum (List.range n) := by
  sorry

theorem sum_first_n_eq(n: Nat) : Nat.sum (List.range (n + 1)) = n * (n + 1) / 2 := by
  induction n
  case zero =>
    simp [Nat.sum, List.range, List.foldr]
  case succ m ih =>
    rw [sum_n_plus_one, ih]
    ring_nf
    rw [(by ring: m * 3 = m * 2 + m)]
    rw [(by ring: 2 + (m * 2 + m) = 2 * (m + 1) + m)]
    rw [Nat.add_assoc (2 * (m + 1)) _ _, Nat.add_comm (2 * (m + 1)) _]
    rw [Nat.add_mul_div_left _ _ (by decide : (0 < 2))]
    ring