# Proving Addition is Commutative in Idris

Posted on 7 September, 2016 by Eric Bailey
Tags: idris, theorem-proving, books

First off, I think Idris is pretty great. Over the past several months, I've been thoroughly enjoying reading and working through Type-Driven Development with Idris, as well as chatting with the community on IRC (#idris on freenode).

For every MEAP book, Manning provides a forum. To be honest, though I've partaken in quite a few MEAPs, I've never really participated in the fora. In the Type-Driven Development with Idris forum, however, I've made a whopping two posts so far. One was a clarifying question about a possible error in the text and the other was an answer to a fellow reader's question. My answer seemed like a good example of how Idris works, so I thought I'd turn it into a blog post. Here goes.

In this example, we're trying to prove that addition of natural numbers is commutative, i.e. $\forall n,m \in \mathbb{N}\ (n + m \equiv m + n)$ … which we can express in Idris as follows:

myPlusCommutative : (n, m : Nat) -> n + m = m + n


The type signature for myPlusCommutative can be read as something like, "For all natural numbers n and m, n plus m is exactly equivalent to m plus n."

Over-simplifying the Curry-Howard correspondence, if we can write a total function that satisfies the type signature, then we've effectively written a proof for the corresponding universal quantification.

Idris has some great interactive editing tools, so I'll try to show those off a bit here too. For a start, we can call idris-add-clause (M-RET d in Spacemacs) to get:

myPlusCommutative : (n, m : Nat) -> n + m = m + n
myPlusCommutative n m = ?myPlusCommutative_rhs


The prefix ? signifies a hole and in this case, the type of that hole is:

  n : Nat
m : Nat
--------------------------------------
myPlusCommutative_rhs : plus n m = plus m n


Next, we can case split (idris-case-split, M-RET c) on n:

myPlusCommutative : (n, m : Nat) -> n + m = m + n
myPlusCommutative  Z    m = ?myPlusCommutative_rhs_1
myPlusCommutative (S k) m = ?myPlusCommutative_rhs_2


For ?myPlusCommutative_rhs_1 we need to prove that $$m = m + 0$$.

myPlusCommutative_rhs_1 : m = plus m 0


Fortunately, the Prelude has a proof that's almost exactly what we want:

plusZeroRightNeutral : (left : Nat) -> left + 0 = left


Since we need to swap the left- and right-hand sides, we can use sym:

sym : (left = right) -> right = left


So the complete definition for the base case of myPlusCommutative is:

myPlusCommutative  Z    m = sym (plusZeroRightNeutral m)


Next, we've got to tackle the inductive step. Since we know we'll need to reduce to the base case, let's define a local variable inductiveHypothesis:

myPlusCommutative (S k) m =
let inductiveHypothesis = myPlusCommutative k m in
rewrite inductiveHypothesis in
?myPlusCommutative_rhs_2


Examining the type of ?myPlusCommutative_rhs_2:

  k : Nat
m : Nat
inductiveHypothesis : plus k m = plus m k
_rewrite_rule : plus k m = plus m k
--------------------------------------
myPlusCommutative_rhs_2 : S (plus m k) = plus m (S k)


… we see we need to prove the successor of $$k$$ plus $$m$$ is exactly equivalent to $$m$$ plus the successor of $$k$$, i.e. $\forall m \in \mathbb{N}\ (S(k + m) \equiv m + S(k))$

Prelude to the rescue, yet again:

plusSuccRightSucc : (left : Nat) ->
(right : Nat) -> S (left + right) = left + S right


Now we can rewrite the hole using plusSuccRightSucc with m as left and k as right:

myPlusCommutative (S k) m =
let inductiveHypothesis = myPlusCommutative k m in
rewrite inductiveHypothesis in
rewrite plusSuccRightSucc m k in
?myPlusCommutative_rhs_2


Eliding the repetitive bits, we get:

myPlusCommutative_rhs_2 : plus m (S k) = plus m (S k)


… which looks like our old friend, Refl:

Refl : x = x


At this point, Idris can fill in the hole for us, via idris-proof-search (M-RET p):

myPlusCommutative (S k) m =
let inductiveHypothesis = myPlusCommutative k m in
rewrite inductiveHypothesis in
rewrite plusSuccRightSucc m k in
Refl


Tidying up a bit for my taste, we arrive at the complete (and total) definition:

||| Addition of natural numbers is commutative.
total
myPlusCommutative : (n, m : Nat) -> n + m = m + n
myPlusCommutative  Z    m = sym (plusZeroRightNeutral m)
myPlusCommutative (S k) m = rewrite myPlusCommutative k m in
plusSuccRightSucc m k


$$\square$$