How to prove Gauss summation of integers with proof assistants using forward reasoning?

Question

As shown in an exercise here, we can prove the Gauss summation (that $\Sigma_{i=0..n}{i} = n \cdot (n + 1)/2$ ) in Isabelle/Isar using mathematical induction, as follows.

theorem
  fixes n::nat
  shows"2 * (∑i=0..n. i) = n * (n + 1)" 
  by (induct n) simp_all

The proof is a one-liner with much details hidden or handled automatically.

However, this seems to be very different from the intuitive proof by Gauss that basically adds the sequence of numbers $1...n$, and a reversed copy of itself. The above Isabelle proof is a backward one, which is perfectly fine and is a textbook example of mathematical induction. But it still differs from the ideas of Gauss's famous proof, which seems to be a forward construction and then verification that it's what is wanted.

I am just wondering:

Is there a way to do a forward style proof that faithfully replicates Gauss's proof in Isabelle or similar proof assistants?

(This example almost changed my perception of which proof style is simpler.)

Answer 1

Like @Bubbler, I think a nice forward proof can be done using a chain of equalities, to spell out each step:

theorem
  fixes n::nat
  shows"2 * (∑i=1..n. i) = n * (n + 1)" 
proof-
  have "2 * (∑i=1..n. i) = (∑i=1..n. i) + (∑i=1..n. i)" by simp
  also have "… = (∑i=1..n. i) + (∑i=1..n. (n + 1 - i))"
    by (subst sum.atLeastAtMost_rev) simp
  also have "… = (∑i=1..n. (i + (n + 1 - i)))"
    using sum.distrib[symmetric].
  also have "… = (∑i=1..n. n + 1)" by simp
  also have "… = n * (n + 1)" by simp
  finally show ?thesis.
qed

I took the liberty to start the summation at 1, not at 0, because I presumptuously expect that that’s how Gauss thought about this list of numbers.

Answer 2

Not exactly sure if Lean counts as "similar proof assistant" to Isabelle, but Lean mathlib has the proof of essentially the same statement, using calc mode which allows to gradually transform the left side of an equality to the right side. (here range n is a range from 0 to n-1 inclusive)

lemma 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 (λ 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 $ λ i hi, add_tsub_cancel_of_le $
  nat.le_pred_of_lt $ mem_range.1 hi
... = n * (n - 1) : by rw [sum_const, card_range, nat.nsmul_eq_mul]

It does not use induction on the surface, but it does use many lemmas which are individually proved with induction under the hood. Also, simplifying (i + (n - 1 - i)) to (n - 1) is rather complicated because, due to the nature of - on nat, one needs to assert that i is at most n - 1 inside the summation. The other three steps correspond to Gauss's three-step proof (twice sum is sum with itself reversed; two sums are zipped so that it becomes a sum of constant; a sum of constant is the constant times length of the sum).