Proving sum(range n) == n(n+1)/2 without induction

Stream: new members

[Dax Fohl]

My first exposure to Lean was a couple years ago, working my way through this tutorial that proves sum(range n) == n*(n+1)/2.

That worked, but I didn't really "like" the proof because it doesn't correspond to how I pictured it visually in grade school. You stack some blocks up in columns height 1..n to make a triangle, make a second one that's flipped over, stack them on top of each other to make an n by (n+1) rectangle. So I was hoping to make a proof that was more true to that approach.

I figured it'd be easy, but I couldn't figure it out after days of trying. I eventually gave up around here, at over 100 lines that are mostly trial-and-error. I kind of lost interest in Lean at that point too.

Now I'm starting to look at Lean again, I'm curious now, is it even possible to formalize the "stacked triangles of blocks" approach, or is that something that can only be used to "visualize" a proof, whereas the inductive approach is required to formalize it? (Note, i figured out you can visualize the inductive approach too, by flipping the second stack of blocks 90 degrees instead of 180, but I still think the 180 degree version is more intuitive).

[Aaron Liu]

What do you mean by "induction"? You can't really do much of anything without induction.

[Weiyi Wang]

def first_n_nat : (n: Nat) → Vector Nat n
| 0 => Vector.nil
| n + 1 => (n + 1) ::ᵥ first_n_nat n

If the definition is induction like this, the proof will likely have to be by induction as well. And induction is a basic building block in Lean, so it will always be used at some point in the proof.

What you can do following your intuition is that you can use some higher level concept to "hide" induction. For example, if you reformulate the theorem in terms of Fintype / Finset sum ∑, I can imagine there being a proof without obvious induction on the surface

[Kenny Lau]

The proof "without induction" is basically Gauss' trick: you write out the sum 1 + 2 + ... + (n-1) + n, and then reverse it to get n + (n-1) + ... + 2 + 1, and then sum these two to get (n+1) + (n+1) + ... + (n+1) + (n+1), which is n(n+1), but you added it to itself so the answer is n(n+1)/2

(but this isn't really "without induction" as others have said)

[Aaron Liu]

Is this along the lines of what you want?

import Mathlib

-- 0 + 1 + ... + n - 1 = n * (n - 1) / 2
example (n : Nat) : 2 * ∑ i : Fin n, i.val = n * (n - 1) :=
  calc 2 * ∑ i : Fin n, i.val
    _ = ∑ i : Fin n, i.val + ∑ i : Fin n, i.val := by rw [two_mul]
    _ = ∑ i : Fin n, i.val + ∑ i : Fin n, (Fin.revPerm i).val := by rw [Equiv.sum_comp]
    _ = ∑ i : Fin n, (i.val + (Fin.revPerm i).val) := by rw [Finset.sum_add_distrib]
    _ = ∑ i : Fin n, (i.val + i.rev.val) := by simp only [Fin.revPerm_apply]
    _ = ∑ i : Fin n, (i.val + (n - (i.val + 1))) := by simp only [Fin.val_rev]
    _ = ∑ i : Fin n, (i.val + (n - 1 - i.val)) := by simp only [tsub_add_eq_tsub_tsub_swap]
    _ = ∑ i : Fin n, (n - 1) := by simp only [Nat.add_sub_of_le, Fin.isLt, Nat.le_sub_one_of_lt]
    _ = n • (n - 1) := by rw [Fin.sum_const]
    _ = n * (n - 1) := by rw [smul_eq_mul]

[Kenny Lau]

if i had three whole days to spare i could translate the original post into literal areas on R^2!

[Kenny Lau]

(you'll have to prove that the intersection of the boundaries have zero measure :upside_down: )

[Kenny Lau]

actually there might be a very clever way to avoid all those boundary issues, which is if you take the unit square to be [0,1) x [0,1)!

[Kenny Lau]

but then I'll need to convince Dax that [0,1) x [0,1) is the "same" as the unit square

[Kevin Buzzard]

In a formal sense it is not even possible to state the question without some form of induction, because you use induction (or more precisely recursion) to define what that "..." means between the 1 and the n

[Dax Fohl]

Hmm, maybe my foundations aren't good enough to give a proper answer to that question. But in the blog post, the inductive step is core to the proof. Note it's easier to visualize if you double both sides, so 2*sum(range n) == n*(n+1). Visually, you can picture it as proving the n==1 case by stacking a red block on top of a blue one, so 2*range(1) == 1*2. Then for n==2 you can picture it as putting a column of two blue blocks on the right-hand side of that, and then a row of two red blocks on top of each of those stacks. Then for n==3, a column of three blue blocks on the RHS, and a row of three red blocks on top. So each step is a rectangle of n*(n+1) and both the blue and the red blocks form a triangle of 1+2+3+...+n.

Which is fine, but yeah I'm looking for something closer to "Gauss's trick". That approach seems more intuitive. But the proof above, that "trick" isn't used or evident. The red blocks are added horizontally and the blue ones are added vertically. It ends up being the same thing in the end, but the proof doesn't really make use of the column heights like Gauss's trick does.

I guess the other thing is that the inductive approach, when you visualize it, you have to start from n==1 and work your way up, adding columns and rows of blue and red blocks. Which is fine, but with Gauss's trick, it's easier to visualize you're just rotating one stack of blocks, putting it on top of the other one, and done in one step. It feels less technical. It's something I could explain to my third-grader. But maybe that's why it's harder to formalize?

[suhr]

Dax Fohl said:

Which is fine, but yeah I'm looking for something closer to "Gauss's trick".

It's doable if you introduce some list operations in the style of APL.. I actually did this exercise, but working with arithmetic without grind was annoying so I put this aside. It seems like I need to redo it.

[Dax Fohl]

Okay, I see what you mean about induction being formally required. Even in Gauss's approach, you'd need induction to define the stacks of blocks. So maybe that's what I'm imagining; is it possible to externalize the induction, so that it's only involved in the setting-up phase, rather than having it be intertwined with the core logic of the proof?

[suhr]

Keep in mind, that you need induction anyway to work with natural numbers.

[Aaron Liu]

@Dax Fohl Did you take a look at my proof above at #new members > Proving sum(range n) == n(n+1)/2 without induction @ 💬?

[Aaron Liu]

I'd say that the "core logic" of the proof doesn't have any induction

[Aaron Liu]

it's just a calculation

[Dax Fohl]

Okay yeah, @Aaron Liu I just got to it. I haven't combed through the whole thing but I think that looks roughly like what I was imagining. It's not explicitly using induction and I see some rev so I guess that's reversing the components 1..n to n..1, and presumably summing them to n+1 and multiplying by the count, though I'm still learning and haven't quite worked out what each step is doing yet.

[Dax Fohl]

So where is the induction happening in that proof?

[Aaron Liu]

Induction is used to prove the lemmas used, like for example you need induction to prove docs#Finset.sum_add_distrib

[Dax Fohl]

Awesome, this is great! Thanks so much!

[Kenny Lau]

Dax Fohl said:

So where is the induction happening in that proof?

Every step

[Kenny Lau]

I claim that 90% of the steps there use induction