8
$\begingroup$

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.)

$\endgroup$
1
  • 1
    $\begingroup$ To use Gauss' method, you need three inductions: One to prove that you can reverse a summation, one to prove that two summations can be added term by term, one to prove that a summation with constant terms is a multiplication. $\endgroup$
    – Trebor
    Feb 18, 2022 at 3:38

2 Answers 2

10
$\begingroup$

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.

$\endgroup$
4
  • $\begingroup$ I haven’t touched Isabelle in a while, so if something I am doing here is (no longer) idiomatic Isabelle, feel free to refine $\endgroup$ Feb 18, 2022 at 11:11
  • $\begingroup$ This porting phenomenon also occurs on codegolf stackexchange. We might want to look at the policies there? $\endgroup$
    – Trebor
    Feb 18, 2022 at 11:12
  • 3
    $\begingroup$ Hmm, I wouldn’t have thought of repeating his answer in Isabelle if the original question wasn’t explicitly talking about Isabelle and tagged [isabelle]; this wasn’t just porting for porting’s sake, but merely trying to give an answer that the OP might find more useful. $\endgroup$ Feb 18, 2022 at 13:18
  • $\begingroup$ Yeah, so I agree that it's not applicable in this particular case. But for the general case I think it's worth asking on meta. $\endgroup$
    – Trebor
    Feb 18, 2022 at 13:57
5
$\begingroup$

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).

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.