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 🙂