simp/ring/other should work here?

Stream: new members

[Newell Jensen]

Hey all, I am confused on why simp, ring etc. don't work here. This seems like something that should be easy for the tactics to figure out. Yes I am aware that lean already has finset.sum_range_id but I wanted to play around with actually summing over the first n positive integers.

import tactic -- import all tactics

import data.nat.basic
import data.finset.basic

open_locale big_operators

example : ∀ (n : ℕ), (∑ i in finset.range (n + 1), i) = (n * (n + 1)) / 2 :=
begin
    intro n,
    induction n with n hn,
    dec_trivial,
    change (∑ i in finset.range (n + 2), i) = (n + 1) * ((n + 1) + 1) / 2,
    have h1 : (∑ i in finset.range (n + 2), i) = (∑ i in finset.range (n + 1), i) + (n + 1),
    exact finset.sum_range_succ (λ (x : ℕ), x) (n + 1),
    rw [h1, hn],
    -- all manner (at least what I tried) of rw, simp, ring, ring_nf etc. doesn't seem
    -- to work here... which is confusing so think there is something more going on here
    sorry,
end

[Damiano Testa]

My guess, untested, is that if you coerce the inner n to ℚ, some tactic may work...

[Newell Jensen]

Would have thought the tactics would handle that. Thanks for the suggestion.

[Damiano Testa]

No, since, if the statement you wrote is true as stated, it is a fluke of how associativity works with multiplication and division. Note that you have nat-division, not actual division

[Newell Jensen]

Yeah understood. Need to dig into the tactics more to understand how they work as well so I am not just assuming what they should or should not be doing.

[Damiano Testa]

@Newell Jensen working with ℕ, somewhere along the way, a proof of the fact that n*(n+1) is even should have appeared with nat-division. This is not something any of those tactics would do.

[Damiano Testa]

When working with ℚ, division is the usual one and the need for evenness is no longer required. In fact, even is not really well-defined/meaningful for rational numbers.

[Damiano Testa]

Here is a proof using rational numbers:

example : ∀ (n : ℕ), (∑ i in finset.range (n + 1), (i : ℚ)) = (n * (n + 1)) / 2 :=
begin
  intro n,
  induction n with n hn,
  { simp },
  { rw [finset.sum_range_succ, hn],
    field_simp,
    ring },
end

[Damiano Testa]

Here you can see where division by 2 shows up, continuing your approach:

example : ∀ (n : ℕ), (∑ i in finset.range (n + 1), i) = (n * (n + 1)) / 2 :=
begin
    intro n,
    induction n with n hn,
    dec_trivial,
    change (∑ i in finset.range (n + 2), i) = (n + 1) * ((n + 1) + 1) / 2,
    have h1 : (∑ i in finset.range (n + 2), i) = (∑ i in finset.range (n + 1), i) + (n + 1),
    exact finset.sum_range_succ (λ (x : ℕ), x) (n + 1),
    rw [h1, hn],
    --  keep massaging a little the equation
    rw [add_assoc, mul_add _ _ (1 + 1), nat.add_div_of_dvd_left, nat.mul_div_cancel],
    { ring_nf },  -- now `ring` works
    { exact zero_lt_two },  -- clean up the mess
    { exact dvd_mul_left _ _ },  -- division by 2!!
end