How to improve my proof?

Stream: new members

[Viliam Vadocz]

I am trying to get some practice with Lean so I proved that two functions are equivalent. This took me quite a while and it still looks very messy (to my eyes). Surely there is some tactic that would simplify all the algebra so I can just focus on the main ideas. I tried using the ring tactic but I could not get it to work. I also found myself just replacing rw by simp and removing things by trial and error to remove steps.

• How could I prove this more elegantly?
• When and how to use simp?
• Is there a way to nth_rewrite inside the square brackets of some rw?

import Mathlib.Algebra.BigOperators.Group.List

def f n := List.sum (List.range n)

def g n := n * (n - 1) / 2

lemma square_gt (n : Nat): n ≤ n * n := by
  induction n with
  | zero => decide
  | succ k ih => simp [Nat.mul_succ]

theorem f_equals_g (n : Nat): f n = g n := by
  induction n with
  | zero => rfl
  | succ k ih => calc f (k + 1)
    _ = f k + k := by simp [f, List.range_succ, List.sum_append]
    _ = g k + k := by rw [ih]
    _ = k * (k - 1) / 2 + k := by rw [g]
    _ = (k * (k - 1) + 2 * k) / 2 := by rw [← Nat.add_mul_div_left _ _ (by decide)]
    _ = (k + 1) * k / 2 := by rw [Nat.mul_sub, Nat.add_mul,
      Nat.two_mul, Nat.mul_one, Nat.one_mul,
      ← Nat.add_assoc, Nat.sub_add_cancel (square_gt k)]
    _ = g (k + 1) := by simp [g]

[Kevin Buzzard]

Your definition of g is pretty horrible because it is using Nat.sub and Nat.div which are not mathematical subtraction or division (e.g. 1 - 0 = 0, 5 / 2 = 2). Hence you can fully expect some pain. I would even go so far as to argue that the definition of g is not actually what you mean it to be. If you coerce to the rationals then your definition agrees with what a mathematician would mean by the definition:

import Mathlib.Tactic

def f n := List.sum (List.range n)

def g (n : ℕ) : ℚ := n * (n - 1) / 2

and the proof will be much simpler (and automation will be more helpful).

[Viliam Vadocz]

That is a good point. I'll try with that definition to see if it is easier.

[Kevin Buzzard]

by simp [f, List.range_succ] -- `List.sum_append` is already a `simp` lemma

is pretty much the only comment I have on your code; that's a fine time to use simp. As for the gnarly bit at the end, it's hard to get automation to help you because your goal has this Nat.div in it, I think in your case I would have bashed it out like you did. Great effort getting it out by the way!

[Viliam Vadocz]

Wow that was much easier (or maybe I improved since my last attempt?):

import Mathlib.Algebra.BigOperators.Group.List
import Mathlib.Tactic

def f n := List.sum (List.range n)

def g (n : ℕ) : ℚ := n * (n - 1) / 2

theorem f_equals_g (n : Nat): f n = g n := by
  induction n with
  | zero => simp [f, g]
  | succ k ih => calc ↑(f (k + 1))
    _ = ↑(f k + k) := by simp [f, List.range_succ]
    _ = g k + k := by simp [ih]
    _ = k * (k - 1) / 2 + k := by rw [g]
    _ = (k + 1) * k / 2 := by ring
    _ = g (k + 1) := by simp [g]

[Ilmārs Cīrulis]

My attempt at original statement with natural numbers only (with n * (n - 1) / 2 changed to (n * n - n) / 2).

import Mathlib

def f n := List.sum (List.range n)

def g (n: ℕ) := (n * n - n) / 2

lemma aux (n : Nat): 2 * f n + n = n * n := by
  induction n with
  | zero => rfl
  | succ k ih =>
    simp [f, List.range_succ] at *
    ring_nf at *
    omega

theorem f_equals_g (n : Nat): f n = g n := by
  have H := aux n
  have H0 := Nat.le_mul_self n
  simp [g]
  omega

[Viliam Vadocz]

omega seems pretty powerful! Definitely something to keep in mind for future problems.

[Kevin Buzzard]

theorem f_equals_g (n : Nat): f n = g n := by -- this is with g Rat-valued
  induction n with
  | zero => simp [f, g]
  | succ k ih =>
      simp [f,g] at ih
      simp [f,g, List.range_succ, ih]
      ring