## Stream: new members

### Topic: How do I improve this terrible proof?

#### Dan Piponi (Dec 19 2021 at 17:05):

Here's my first attempt at proving a non quite trivial theorem about numbers in Lean.

import data.set data.int.basic

def mysum : (ℕ → ℕ) → ℕ → ℕ
| f 0       := 0
| f (n + 1) := f n + mysum f n

theorem lemma1 (n : ℕ) : 2 * mysum id (n + 1) = n * (n + 1) → 2 * mysum id (n + 2) = (n + 1) * (n + 2) :=
assume h, (calc
2 * mysum id (n + 2) = 2 * (id (n + 1) + mysum id (n + 1)) : rfl
... = 2 * id (n + 1) + 2 * mysum id (n + 1) : by rw left_distrib
... = 2 * id (n + 1) + n * (n + 1) : by rw h
... = 2 * (n + 1) + n * (n + 1) : rfl
... = 2 * n + 2 * 1 + (n * n + n * 1) : by rw [left_distrib, left_distrib, add_assoc]
... = (2 * 1 + (n * n + n * 1)) + 2 * n: by rw [add_assoc, add_comm]
... = n * n + n * 1 + 2 * 1 + 2 * n: by rw add_comm (2 * 1)
... = n * n + 1 * n + 2 * 1 + 2 * n: by rw mul_comm n 1
... = n * n + 1 * n + (2 * 1 + 2 * n): by rw add_assoc
... = n * n + 1 * n + (2 * n + 2 * 1): by rw add_comm (2 * 1)
... = n * n + 1 * n + (n * 2 + 1 * 2) : by rw [mul_comm n 2, mul_comm 2 1]
... = (n + 1) * n + (n * 2 + 1 * 2) : by rw right_distrib
... = (n + 1) * n + (n + 1) * 2 : by rw ←right_distrib
... = (n + 1) * (n + 2) : by rw ←left_distrib)

theorem young_gauss : ∀ (n : ℕ), 2 * mysum id (n + 1) = n * (n + 1)
| 0 := rfl
| (n + 1) := lemma1 n (young_gauss n)


It's a bit long. What should I be learning next to improve it? Can I use the simp tactic or similar to eliminate that long calculation?

#### David Renshaw (Dec 19 2021 at 17:12):

The ring tactic can do a lot of those things automatically.

import data.set data.int.basic

import tactic.ring

def mysum : (ℕ → ℕ) → ℕ → ℕ
| f 0       := 0
| f (n + 1) := f n + mysum f n

theorem lemma1 (n : ℕ) : 2 * mysum id (n + 1) = n * (n + 1) → 2 * mysum id (n + 2) = (n + 1) * (n + 2) :=
assume h, (calc
2 * mysum id (n + 2) = 2 * (id (n + 1) + mysum id (n + 1)) : rfl
... = 2 * id (n + 1) + 2 * mysum id (n + 1) : by rw left_distrib
... = 2 * id (n + 1) + n * (n + 1) : by rw h
... = 2 * (n + 1) + n * (n + 1) : rfl
... = (n + 1) * (n + 2) : by ring)

theorem young_gauss : ∀ (n : ℕ), 2 * mysum id (n + 1) = n * (n + 1)
| 0 := rfl
| (n + 1) := lemma1 n (young_gauss n)


#### Patrick Johnson (Dec 19 2021 at 17:15):

lemma lemma1 (n : ℕ) :
2 * mysum id (n + 1) = n * (n + 1) →
2 * mysum id (n + 2) = (n + 1) * (n + 2) :=
by simp_rw [mysum, id]; exact (λh, by linarith)


Last updated: Dec 20 2023 at 11:08 UTC