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 Zero
Two : Numbers.Nat
Two = Successor One
Three : 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 = Refl
proofDecrementOne : decr One = Zero
proofDecrementOne = Refl
proofDecrementZero : 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 is n + 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 if p(n) holds true then p(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 Refl
lemmaPlusCommutesZeroKM : (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 Refl
proofPlusCommutative : (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.