Pattern Matching Proofs
In this section, we will provide a proof of plus_commutes
directly,
by writing a pattern matching definition. We will use interactive
editing features extensively, since it is significantly easier to
produce a proof when the machine can give the types of intermediate
values and construct components of the proof itself. The commands we
will use are summarised below. Where we refer to commands
directly, we will use the Vim version, but these commands have a direct
mapping to Emacs commands.
Command 
Vim binding 
Emacs binding 
Explanation 
Check type 


Show type of identifier or hole under the cursor. 
Proof search 


Attempt to solve hole under the cursor by applying simple proof search. 
Make new definition 


Add a template definition for the type defined under the cursor. 
Make lemma 


Add a top level function with a type which solves the hole under the cursor. 
Split cases 


Create new constructor patterns for each possible case of the variable under the cursor. 
Creating a Definition
To begin, create a file pluscomm.idr
containing the following type
declaration:
plus_commutes : (n : Nat) > (m : Nat) > n + m = m + n
To create a template definition for the proof, press \a
(or the
equivalent in your editor of choice) on the line with the type
declaration. You should see:
plus_commutes : (n : Nat) > (m : Nat) > n + m = m + n
plus_commutes n m = ?plus_commutes_rhs
To prove this by induction on n
, as we sketched in Section
Inductive Proofs, we begin with a case split on n
(press
\c
with the cursor over the n
in the definition.) You
should see:
plus_commutes : (n : Nat) > (m : Nat) > n + m = m + n
plus_commutes Z m = ?plus_commutes_rhs_1
plus_commutes (S k) m = ?plus_commutes_rhs_2
If we inspect the types of the newly created holes,
plus_commutes_rhs_1
and plus_commutes_rhs_2
, we see that the
type of each reflects that n
has been refined to Z
and S k
in each respective case. Pressing \t
over
plus_commutes_rhs_1
shows:
m : Nat

plus_commutes_rhs_1 : m = plus m Z
Similarly, for plus_commutes_rhs_2
:
k : Nat
m : Nat

plus_commutes_rhs_2 : (S (plus k m)) = (plus m (S k))
It is a good idea to give these slightly more meaningful names:
plus_commutes : (n : Nat) > (m : Nat) > n + m = m + n
plus_commutes Z m = ?plus_commutes_Z
plus_commutes (S k) m = ?plus_commutes_S
Base Case
We can create a separate lemma for the base case interactively, by
pressing \l
with the cursor over plus_commutes_Z
. This
yields:
plus_commutes_Z : (m : Nat) > m = plus m Z
plus_commutes : (n : Nat) > (m : Nat) > n + m = m + n
plus_commutes Z m = plus_commutes_Z m
plus_commutes (S k) m = ?plus_commutes_S
That is, the hole has been filled with a call to a top level
function plus_commutes_Z
, applied to the variable in scope m
.
Unfortunately, we cannot prove this lemma directly, since plus
is
defined by matching on its first argument, and here plus m Z
has a
concrete value for its second argument (in fact, the left hand side of
the equality has been reduced from plus Z m
.) Again, we can prove
this by induction, this time on m
.
First, create a template definition with \d
:
plus_commutes_Z : (m : Nat) > m = plus m Z
plus_commutes_Z m = ?plus_commutes_Z_rhs
Now, case split on m
with \c
:
plus_commutes_Z : (m : Nat) > m = plus m Z
plus_commutes_Z Z = ?plus_commutes_Z_rhs_1
plus_commutes_Z (S k) = ?plus_commutes_Z_rhs_2
Checking the type of plus_commutes_Z_rhs_1
shows the following,
which is provable by Refl
:

plus_commutes_Z_rhs_1 : Z = Z
For such immediate proofs, we can let write the proof automatically by
pressing \s
with the cursor over plus_commutes_Z_rhs_1
.
This yields:
plus_commutes_Z : (m : Nat) > m = plus m Z
plus_commutes_Z Z = Refl
plus_commutes_Z (S k) = ?plus_commutes_Z_rhs_2
For plus_commutes_Z_rhs_2
, we are not so lucky:
k : Nat

plus_commutes_Z_rhs_2 : S k = S (plus k Z)
Inductively, we should know that k = plus k Z
, and we can get access
to this inductive hypothesis by making a recursive call on k, as
follows:
plus_commutes_Z : (m : Nat) > m = plus m Z
plus_commutes_Z Z = Refl
plus_commutes_Z (S k)
= let rec = plus_commutes_Z k in
?plus_commutes_Z_rhs_2
For plus_commutes_Z_rhs_2
, we now see:
k : Nat
rec : k = plus k Z

plus_commutes_Z_rhs_2 : S k = S (plus k Z)
So we know that k = plus k Z
, but how do we use this to update the goal to
S k = S k
?
To achieve this, Idris provides a replace
function as part of the
prelude:
Main> :t replace
Builtin.replace : (0 rule : x = y) > p x > p y
Given a proof that x = y
, and a property p
which holds for
x
, we can get a proof of the same property for y
, because we
know x
and y
must be the same. Note the multiplicity on rule
means that it’s guaranteed to be erased at run time.
In practice, this function can be
a little tricky to use because in general the implicit argument p
can be hard to infer by unification, so Idris provides a high level
syntax which calculates the property and applies replace
:
rewrite prf in expr
If we have prf : x = y
, and the required type for expr
is some
property of x
, the rewrite ... in
syntax will search for all
occurrences of x
in the required type of expr
and replace them with y
. We want
to replace plus k Z
with k
, so we need to apply our rule
rec
in reverse, which we can do using sym
from the Prelude
Main> :t sym
Builtin.sym : (0 rule : x = y) > y = x
Concretely, in our example, we can say:
plus_commutes_Z (S k)
= let rec = plus_commutes_Z k in
rewrite sym rec in ?plus_commutes_Z_rhs_2
Checking the type of plus_commutes_Z_rhs_2
now gives:
k : Nat
rec : k = plus k Z

plus_commutes_Z_rhs_2 : S k = S k
Using the rewrite rule rec
, the goal type has been updated with plus k Z
replaced by k
.
We can use proof search (\s
) to complete the proof, giving:
plus_commutes_Z : (m : Nat) > m = plus m Z
plus_commutes_Z Z = Refl
plus_commutes_Z (S k)
= let rec = plus_commutes_Z k in
rewrite sym rec in Refl
The base case of plus_commutes
is now complete.
Inductive Step
Our main theorem, plus_commutes
should currently be in the following
state:
plus_commutes : (n : Nat) > (m : Nat) > n + m = m + n
plus_commutes Z m = plus_commutes_Z m
plus_commutes (S k) m = ?plus_commutes_S
Looking again at the type of plus_commutes_S
, we have:
k : Nat
m : Nat

plus_commutes_S : S (plus k m) = plus m (S k)
Conveniently, by induction we can immediately tell that
plus k m = plus m k
, so let us rewrite directly by making a
recursive call to plus_commutes
. We add this directly, by hand, as
follows:
plus_commutes : (n : Nat) > (m : Nat) > n + m = m + n
plus_commutes Z m = plus_commutes_Z
plus_commutes (S k) m = rewrite plus_commutes k m in ?plus_commutes_S
Checking the type of plus_commutes_S
now gives:
k : Nat
m : Nat

plus_commutes_S : S (plus m k) = plus m (S k)
The good news is that m
and k
now appear in the correct order.
However, we still have to show that the successor symbol S
can be
moved to the front in the right hand side of this equality. This
remaining lemma takes a similar form to the plus_commutes_Z
; we
begin by making a new top level lemma with \l
. This gives:
plus_commutes_S : (k : Nat) > (m : Nat) > S (plus m k) = plus m (S k)
Again, we make a template definition with \a
:
plus_commutes_S : (k : Nat) > (m : Nat) > S (plus m k) = plus m (S k)
plus_commutes_S k m = ?plus_commutes_S_rhs
Like plus_commutes_Z
, we can define this by induction over m
, since
plus
is defined by matching on its first argument. The complete definition
is:
total
plus_commutes_S : (k : Nat) > (m : Nat) > S (plus m k) = plus m (S k)
plus_commutes_S k Z = Refl
plus_commutes_S k (S j) = rewrite plus_commutes_S k j in Refl
All holes have now been solved.
The total
annotation means that we require the final function to
pass the totality checker; i.e. it will terminate on all possible
welltyped inputs. This is important for proofs, since it provides a
guarantee that the proof is valid in all cases, not just those for
which it happens to be welldefined.
Now that plus_commutes
has a total
annotation, we have completed the
proof of commutativity of addition on natural numbers.