Closed-expression of a sum with proof in Idris

One well known fact is the sum $1 + 2 + \ldots + n = \frac {n(n + 1)} {2}$. Let’s try to prove this fact in Idris.

We start intuitively by defining our recursive sum function:

total sum : Nat -> Nat
sum Z     = Z
sum (S n) = (S n) + sum n


Testing it a few times:

Idris> sum 3
6 : Nat
Idris> sum 4
10 : Nat


Looks good.

Next, we will come up with out dependently typed function to prove the fact.

theorem_1_firsttry : (n : Nat) -> sum n = divNat (n * (n + 1)) 2
theorem_1_firsttry Z     = ?a
theorem_1_firsttry (S n) = ?b


The base case that we need to prove is of type 0 = divNat 0 2. Looks a bit tricky. Let’s try to use divNatNZ along with a proof that 2 is not zero:

theorem_1_secondtry : (n : Nat) -> sum n = divNatNZ (n * (n + 1)) 2 (SIsNotZ {x = 1})
theorem_1_secondtry Z     = ?a
theorem_1_secondtry (S n) = ?b


Now the base case is just Refl. Let’s put an inductive hypothesis as well:

theorem_1_secondtry : (n : Nat) -> sum n = divNatNZ (n * (n + 1)) 2 (SIsNotZ {x = 1})
theorem_1_secondtry Z     = Refl
theorem_1_secondtry (S n) = let IH = theorem_1_secondtry n in ?b


Idris tells us that we now need to prove:

b : S (plus n (sum n)) =
ifThenElse (lte (plus (plus n 1) (mult n (S (plus n 1)))) 0)
(Delay 0)
(Delay (S (Prelude.Nat.divNatNZ, div' (S (plus (plus n 1) (mult n (S (plus n 1)))))
1
SIsNotZ
(plus (plus n 1) (mult n (S (plus n 1))))
(minus (plus (plus n 1) (mult n (S (plus n 1)))) 1)
1)))


Woot.

Let’s take a slightly different route by doing a few algebraic tricks to get rid off division. Instead of proving that $1 + 2 + \ldots + n = \frac {n(n + 1)} {2}$, we will prove $2 * (1 + 2 + \ldots + n) = n(n + 1)$.

total theorem_1 : (n : Nat) -> 2 * sum n = n * (n + 1) -- sum n = n * (n + 1) / 2
theorem_1 Z     = Refl
theorem_1 (S n) = ?b


Now we need to show that b : S (plus (plus n (sum n)) (S (plus (plus n (sum n)) 0))) = S (plus (plus n 1) (mult n (S (plus n 1)))).

total theorem_1 : (n : Nat) -> 2 * sum n = n * (n + 1) -- sum n = n * (n + 1) / 2
theorem_1 Z     = Refl
theorem_1 (S n) = let IH = theorem_1 n in
rewrite (multRightSuccPlus n (plus n 1)) in
rewrite sym IH in
rewrite (plusZeroRightNeutral (sum n)) in
rewrite (plusZeroRightNeutral (plus n (sum n))) in
rewrite (plusAssociative n (sum n) (sum n)) in
rewrite (sym (plusSuccRightSucc (plus n (sum n)) (plus n (sum n)))) in
rewrite plusCommutative (plus n 1) (plus (plus n (sum n)) (sum n)) in
rewrite sym (plusSuccRightSucc n Z) in
rewrite plusZeroRightNeutral n in
rewrite (sym (plusSuccRightSucc (plus (plus n (sum n)) (sum n)) n)) in
rewrite (sym (plusAssociative (n + sum n) (sum n) n)) in
rewrite plusCommutative (sum n) n in Refl


Looks a bit big, but it works! With line 4 and 5 we get rid off multiplication and then all we need to do is some algebraic re-ordering of plus to show that both sides are equivalent.

Now that we proved it, you can use this fact in your favorite programming language 🙂