sum_range_id proof

Stream: new members

[Iocta]

I proved Gauss's summation rule but had some issues which I've annotated in comments.

import Mathlib
import Mathlib.Tactic
import Mathlib.Data.Finset.Basic
import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Algebra.Order.Sub.Canonical

open BigOperators Nat Finset

-- Mathlib version

theorem mathlib_sum_range_id_mul_two (n : ℕ) : (∑ i in range n, i) * 2 = n * (n - 1) :=
  calc
    (∑ i in range n, i) * 2 = (∑ i in range n, i) + ∑ i in range n, (n - 1 - i) := by
      rw [sum_range_reflect (fun i => i) n, mul_two]
    _ = ∑ i in range n, (i + (n - 1 - i)) := sum_add_distrib.symm
    _ = ∑ i in range n, (n - 1) :=
      sum_congr rfl fun i hi => add_tsub_cancel_of_le <| Nat.le_sub_one_of_lt <| mem_range.1 hi
    _ = n * (n - 1) := by rw [sum_const, card_range, Nat.nsmul_eq_mul]


theorem mathlib_sum_range_id (n : ℕ) : ∑ i in range n, i = n * (n - 1) / 2 := by
  rw [← mathlib_sum_range_id_mul_two n, Nat.mul_div_cancel _ zero_lt_two]


-- My version

theorem my_sum_range_id_mul_two (n : ℕ) : (∑ i in range n, i) * 2 = n * (n - 1) :=
  calc
    (∑ i in range n, i) * 2 = (∑ i in range n, i) + (∑ i in range n, i) := by rw [mul_two]
    _ = (∑ i in range n, i) + (∑ i in range n, (n - 1 - i)) := by rw [sum_range_reflect (fun i => i) n]
    _ = (∑ i in range n, (i + (n - 1 - i))) := sum_add_distrib.symm
    _ = (∑ i in range n, ((n - 1 - i) + i)) := by simp only [add_comm] -- Why doesn't `rewrite [add_comm]` work?
    _ = (∑ i in range n, (n - 1)) := sum_congr rfl (fun i => by -- Do I really need sum_congr? Does this need to be so complicated?
        intro h
        apply mem_range.1 at h
        apply le_sub_one_of_lt at h
        rw [tsub_add_cancel_of_le h]
      )
    _ = n * (n - 1) := by rw [sum_const, card_range, Nat.nsmul_eq_mul] -- Is this abstract nsmul stuff really necessary - can't I use simpler tools?


theorem my_sum_range_id (n : ℕ) : (∑ i in range n, i) = n * (n - 1) / 2 := by
rw [← my_sum_range_id_mul_two, Nat.mul_div_cancel _ zero_lt_two]

[Matt Diamond]

re: your first question, rw doesn't allow you to rewrite expressions involving bound variables... however, simp_rw will usually work in those cases

[Matt Diamond]

re: your second question, subtraction with natural numbers is tricky because it stops at 0, so n - i + i doesn't always equal n... for example, 1 - 2 + 2 does not equal 1, because 1 - 2 = 0, so 1 - 2 + 2 = 0 + 2 = 2

[Matt Diamond]

so when you're simplifying (n - 1 - i) + i, you need the fact that i ≤ n

[Matt Diamond]

so you have to do a little extra work to get that