Better than Unit Tests? Idris Proofs
In continuing my study of Idris and sharing my progression, I am looking beyond the features of contemporary enterprise languages towards the edge of language design. I wanted to take a look at some of the deeper properties of proofs.
Let’s start with a baseline implementation of Natural numbers, which is a sum type of Zero
or some Successor
to a natural number. We can also define two functions incr and decr to increment or decrement any Nat
.
namespace Numbers data Nat : Type where
Zero : Numbers.Nat
Successor : Numbers.Nat -> Numbers.Nat decr : Numbers.Nat -> Numbers.Nat
decr Zero = Zero
decr (Successor x) = x incr : Numbers.Nat -> Numbers.Nat
incr Zero = Successor Zero
incr (Successor x) = Successor (Successor x)
Then we can add some constants / helpers to make our initial set of tests easier to read:
One : Numbers.Nat
One = Successor ZeroTwo : Numbers.Nat
Two = Successor OneThree : Numbers.Nat
Three = Successor Two
Which allows for these tests proofs / tests. Restating from my last post — the code will not compile if the proofs don’t hold true. These proofs are in the form of the reflexivity tactic.
proofIncrementOne : incr One = Two
proofIncrementOne = ReflproofDecrementOne : decr One = Zero
proofDecrementOne = ReflproofDecrementZero : decr Zero = Zero
proofDecrementZero = Refl
However we could do a little more here by coding up a function to add two numbers and defining an infix operator deferring to that function:
plus : Numbers.Nat -> Numbers.Nat -> Numbers.Nat
plus Zero b = b
plus (Successor a) b = Successor(plus a b)syntax [x] "+" [y] = Numbers.plus x y
plus
is defined by taking two Nat’s
and returning a Nat
. In the event the first Nat
supplied is Zero
the result is the second Nat
supplied. In the second statement where the first Nat
is non-Zero
we deconstruct it into the Successor
of some Nat
a
. The second input b
is still some Nat
(with no constraints). The implementation of this possibility is that we recurs plus
with a
and b
and applying the successor to that value until we hit the first case (the first parameter is Zero
) essentially transferring all the Successor constructors from a
onto b
. The definition for the infix operator should be intuitive to follow even if the style is foreign. plus
gives us the opportunity to define some other types of proofs!
This is a straight proof that Two + One = Three
based on reflexivity:
proofTwoPlusOne : (Two + One) = Three
proofTwoPlusOne = Refl
But we can get more creative and define a proof Zero + n = n
over the full set of Nat
:
proofZeroPlusN : (n : Numbers.Nat) -> (Zero + n) = n
proofZeroPlusN n = Refl
This form is referred to as simplification. The Idris compiler looks at the left hand side of the proof Zero + n
which is de-sugars to plus Zero n
and attempts to find corresponding pattern in the definition of plus which it does plus Zero b
. It then replaces the left hand side of the proof with the right hand side of the corresponding pattern in the definition. Variables are re-termed for equivalency.
In unit tests we could test some function plus with some variable n and zero will in fact equal n in some subset of n. However we cannot test for all possible n. But leveraging features like recursive data types and inductive reasoning we are able to do that in Idris — although it isn’t always simple.
Unfortunately proving n + Zero = n
isn’t as simple. Idris cannot discern a single pattern match in the definition of plus without knowing what n
is. n
could be Zero
and the first match would work or non Zero
and the second match would work. I needed help fully understanding and asked on stack. The simplification method requires Idris to have a perfect match before it substitutes in the proof. We need to rely on the premise of induction:
- prove a base case (in this instance
n = Zero
) some property (p
)holds true. In this instance the property isn + 0 = n
. - prove for some successor to the base case (in this instance
n = Successor k
) the property (p
) also holds true; said another way ifp(n)
holds true thenp(Successor n)
also holds true. - conclude the property holds true for all
Here is the proof for (n + Zero) = n
proofNPlusZero : (n : Numbers.Nat) -> (n + Zero) = n
proofNPlusZero Zero = Refl
proofNPlusZero (Successor k) =
let inductiveNPlusZero = proofNPlusZero k in
rewrite inductiveNPlusZero in Refl
We break the proof into two steps the first where n
is Zero
and that holds true because of reflexivity. In the second case the variable n
in the proof can be replaced with Successor k
so that we have an expanded proof (or target) for this step Successor k + Zero = Successor k
. We type of the recursion (inductiveNPlusZero) is plus k Zero = k
. The rewrite
keyword takes the equation from inductiveNPlusZero and breaks into two components the lhs plus k Zero
and the rhs k
. In that same step it searches the expanded proof for this step (Successor k + Zero = Successor k
) for the lhs (plus k Zero
) and replaces it with the rhs (k
) yielding: Successor k = Successor k
thus proving the step.
The approach is a departure from straight assertions, should syntax and expect syntax. It takes some time.
For exra credit (with myself) I tackled proving plus on natural numbers is commutative. This is a more complex proof with multiple cases { (Zero, Zero), (Zero, k), (k, Zero), (k, j) }
so it made sense to break this into smaller facts (lemmas) to accomplish independently.
lemmaPlusCommutesZeroM : (m: Numbers.Nat) -> m = plus m Zero
lemmaPlusCommutesZeroM (Successor k) =
let inductiveCummativeM = lemmaPlusCommutesZeroM k in
rewrite inductiveCummativeM in RefllemmaPlusCommutesZeroKM : (k, m: Numbers.Nat) ->
Successor (plus m k) = plus m (Successor k)
lemmaPlusCommutesZeroKM k Zero = Refl
lemmaPlusCommutesZeroKM k (Successor j) =
rewrite lemmaPlusCommutesZeroKM k j in ReflproofPlusCommutative : (n, m : Numbers.Nat) -> (n + m) = (m + n)
proofPlusCommutative Zero Zero = Refl
proofPlusCommutative Zero m = lemmaPlusCommutesZeroM m
proofPlusCommutative (Successor n) m =
rewrite proofPlusCommutative n m in lemmaPlusCommutesZeroKM n m
plusCommutative drives the action deferring the more complicated steps for Zero plus m
and n plus m
to subsidiary lemmas. lemmaPlusCommutesZeroM
is very similar to proofNPlusZero
but doesn’t need to handle the Zero
case (it is handled in proofPlusCommutative
). I think I will leave the last lemma for another day — as this article is getting long.