# Proving Addition is Commutative in Idris

Eric Bailey

Posted on 7 September, 2016

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