# 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.NatOne = Successor ZeroTwo : Numbers.NatTwo = Successor OneThree : Numbers.NatThree = 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 = TwoproofIncrementOne = ReflproofDecrementOne : decr One = ZeroproofDecrementOne = ReflproofDecrementZero : decr Zero = ZeroproofDecrementZero = 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.Natplus Zero b = bplus (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) = ThreeproofTwoPlusOne = 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) = nproofZeroPlusN 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) = nproofNPlusZero Zero = ReflproofNPlusZero (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.

A 25 year software industry veteran with a passion for functional programming, architecture, mentoring / team development, xp/agile and doing the right thing.

## More from Todd Brown

A 25 year software industry veteran with a passion for functional programming, architecture, mentoring / team development, xp/agile and doing the right thing.