Proving equations with divisions?

Stream: new members

[Fernando Chu]

I was trying the following example:

import Mathlib

example (n : ℕ) : (∑ k ∈ Finset.range (n), k) = n*(n-1)/2 := by
  induction' n with n ih
  · simp
  · ring_nf
    rw [Finset.sum_range_add (fun x ↦ x) 1 n, Finset.sum_add_distrib, ih]
    simp
    sorry

Is there a nice way to close the goal?

[Aaron Liu]

what's your reasoning for why this should be true

[Aaron Liu]

note that it's not completely trivial because (2 * n + 1) / 2 = n so division doesn't always distribute over addition

[Fernando Chu]

Interesting point, that made me think that I should continue on with

    have : n = 2 * n / 2 := by simp
    nth_rw 1 [this]

So that the goal is now

2 * n / 2 + n * (n - 1) / 2 = (n * n + n) / 2

I had hoped that maybe ring would solve this but seems not

[Fernando Chu]

Ah, I think the problem is n * (n - 1)? Maybe ring doesn't know about negation when working on a semiring?

[Robin Arnez]

- on Nat isn't working with negation, it's instead truncated subtraction (e.g. 3 - 4 = 0)

[Kevin Buzzard]

I would claim that you're trying to prove the wrong thing. n*(n-1)/2 doesn't mean what you think it means because neither natural subtraction nor natural division are what mathematicians expect them to mean.

[Ruben Van de Velde]

I was writing "as Kevin would say, this isn't what you want to prove...", but there we go :)

[Ruben Van de Velde]

It's possible to prove this form, but sort of only by accident and not with tools that assume well-behaved subtraction like ring. In fact, the ring_nf you started with only makes things harder for you

Proof

import Mathlib

example (n : ℕ) : (∑ k ∈ Finset.range (n), k) = n*(n-1)/2 := by
  induction' n with n ih
  · simp
  · simp only [add_tsub_cancel_right]
    rw [Finset.sum_range_add, Finset.sum_add_distrib, ih]
    simp
    trans ((n * (n - 1)) + n * 2) / 2
    · grind
    congr
    rw [← mul_add, mul_comm n]
    cases n with
    | zero => simp
    | succ n => simp

[Kevin Buzzard]

Note how much easier it is to prove the mathematically correct statement -- I coerce to the rationals and then subtraction and division have their correct meaning.

import Mathlib

example (n : ℕ) : (∑ k ∈ Finset.range (n), (k : ℚ)) = n*(n-1)/2 := by
  induction n with
  | zero => simp
  | succ n IH => rw [Finset.sum_range_succ, IH]; grind

[Aaron Liu]

Using grind is cheating

[Kevin Buzzard]

import Mathlib

example (n : ℕ) : (∑ k ∈ Finset.range n, (k : ℚ)) = n*(n-1)/2 := by
  induction n with
  | zero => simp
  | succ n IH => rw [Finset.sum_range_succ, IH]; push_cast; ring

[Aaron Liu]

Fine you win

[Fernando Chu]

Thanks for the answers!

[Yannick Seurin]

Note that MIL has a similar example in Section 5.2:

import Mathlib

theorem sum_id (n : ℕ) : ∑ i ∈ Finset.range (n + 1), i = n * (n + 1) / 2 := by
  symm; apply Nat.div_eq_of_eq_mul_right (by norm_num : 0 < 2)
  induction' n with n ih
  · simp
  rw [Finset.sum_range_succ, mul_add 2, ← ih]
  ring

Quoting:

The first step of the proof clears the denominator. This is generally useful when formalizing identities, because calculations with division generally have side conditions. (It is similarly useful to avoid using subtraction on the natural numbers when possible.)

[Yannick Seurin]

For the original statement, it can be adapted as follows:

import Mathlib

theorem sum_id (n : ℕ) : ∑ i ∈ Finset.range n, i = n * (n - 1) / 2 := by
  symm; apply Nat.div_eq_of_eq_mul_right (by norm_num : 0 < 2)
  induction' n with n ih
  · simp
  rw [Finset.sum_range_succ, mul_add 2, ← ih]
  cases n with
  | zero => simp
  | succ n => simp; ring