# 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 `T`

based on reflexivity:**wo + One = Three**

`proofTwoPlusOne : (Two + One) = Three`

proofTwoPlusOne = Refl

But we can get more creative and define a proof

over the full set of **Zero + n = n**`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

pluswith some variablenandzerowill in fact equalnin some subset ofn. However we cannot test for all possiblen. 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

isn’t as simple. Idris cannot discern a single pattern match in the definition of **n + Zero = n****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

keyword takes the equation from **rewrite****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.