Proving Addition is Commutative in Idris

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