There is a syntax in Idris which is kind of cool. Apparently it is inspired by a similar facility in Agda called “preorder reasoning”, but I haven’t used Agda, so I don’t know how Agda’s version works. But the idea in Idris is to allow you to prove that a reflexive-transitive relation holds between two particular endpoints by showing that it holds between a bunch of intermediate endpoints. That’s kind of abstract, so for now let’s forget about “reflexive-transitive relations” and just talk about equality (which happens to be reflexive and transitive). So for now we’ll just be using preorder reasoning to prove that two things are equal to each other by proving that a bunch of intermediate states are equal.

The idea is that you’d prove, say, `(a * b) * c = (c * a) * b`

by writing something like this:

(a * b) * c ={ associativity of * }= a * (b * c) ={ commutativity }= a * (c * b) ={ associativity }= (a * c) * b ={ commutativity again }= (c * a) * b QED

where you have a left column in which you write intermediate states and a right column in which you write justifications for transforming each state into the next. So you prove that `(a * b) * c = (c * a) * b`

by transforming the former into the latter, making sure to maintain equality along the way.

Of course, what I’ve written is pseudocode — in particular, the justifications I’ve written in the `={ }=`

s are basically just comments. In the actual Idris code, we’ll have to fill them in with proofs that the corresponding two lines are equal.

We don’t have to fill them in just yet, though: we can use metavariables, the Idris way of saying “I haven’t filled this in yet and I want to leave it for later. Can you just assume I’ve implemented this and typecheck the rest of the file?” You mark a name as a metavariable by prefixing it with a `?`

. So let’s write up a first draft of our proof:

p : (a, b, c : Nat) -> (a * b) * c = (c * a) * b p a b c = (a * b) * c ={ ?assoc }= a * (b * c) ={ ?commute_bc }= a * (c * b) ={ ?unassoc }= (a * c) * b ={ ?commute_ac }= (c * a) * b QED

Let’s run this through Idris and see what the types of our metavariables are…

error: expected: operator (a * b) * c ={ ?assoc }= ^ (idris)

Uh oh. What’s going wrong here?

…well, this took me 10 minutes to figure out, so let’s just skip to the answer. Because the `={ }=`

syntax is defined in the standard library rather than being built in, it doesn’t have the precedence we’d like it to have. The things in our “left column” all have to be simple expressions, which means either a single name or something in parentheses. Also, since it’s defined in the standard library, we don’t have the syntax unless we import the module it’s defined in. So here’s our updated metavariable-using code:

import Syntax.PreorderReasoning p : (a, b, c : Nat) -> (a * b) * c = (c * a) * b p a b c = ((a * b) * c) ={ ?assoc }= (a * (b * c)) ={ ?commute_bc }= (a * (c * b)) ={ ?unassoc }= ((a * c) * b) ={ ?commute_ac }= ((c * a) * b) QED

And now that our code can be loaded into the interpreter, we can ask it for the types of our metavariables.

assoc : a * b * c = a * (b * c) commute_bc : a * (b * c) = a * (c * b) unassoc : a * (c * b) = a * c * b commute_ac : a * c * b = mult (mult c a) b

Two things to note. First, Idris leaves off the parentheses when showing us an expression like `(a * b) * c`

, because their parenthesization is the same as the default association of the `*`

operator. That’s kind of unfortunate since it’s clearer here to explicitly show the parenthesizations we’re working with, but we can deal with it.

Second, the final `commute_ac`

lemma mentions a function called `mult`

. It just so happens that `*`

is a polymorphic function working on any number type (specifically, any type that is a member of the `Num`

typeclass); its implementation for `Nat`

s calls a `Nat`

-specific function called `mult`

. We can basically pretend it’s the same as `*`

here, because Idris will expand the definition of `*`

if that helps it unify something. Again, this is a little annoying, but we can totally work around it.

So, now for our proofs. All of the types we need are basic properties of multiplication proved in the standard library. You can find them using the `:search`

command in the repl (which I won’t go into here, partially because `:search`

command seems to have an unfortunate infinite loop bug that strikes in this case… it would be great to fix the bug and post about it another time). Here they are filled in:

import Syntax.PreorderReasoning p : (a, b, c : Nat) -> (a * b) * c = (c * a) * b p a b c = ((a * b) * c) ={ sym (multAssociative a b c) }= (a * (b * c)) ={ multCommutative b c }= (a * (c * b)) ={ multAssociative a c b }= ((a * c) * b) ={ multCommutative a c }= ((c * a) * b) QED

(The `sym`

is to reverse the equality, turning `x = y`

into `y = x`

, which is what we need in that first justification slot).

But wait! We still get an error:

When elaborating right hand side of p: When elaborating argument x to function Syntax.PreorderReasoning.Equal.step: Can't unify mult c b with a * (c * b)

Remember, `mult`

isn’t the problem — `*`

and `mult`

basically look the same to Idris, so it’ll spit out error messages using whatever expression it happens to have stored. The problem is that our equation, `multCommutative b c`

, equates *subexpressions* of the intermediate steps on either side — it’s a proof that `b * c = c * b`

, but we need to equate the full expressions. We need a proof of `a * (b * c) = a * (c * b)`

. The way to do this is `cong`

, whose type is `(a = b) -> (f a = f b)`

— in other words, “if you take an equation and apply the same function to both sides, your equation is still valid”. We want to apply `cong`

with `f = (a*)`

, but since `f`

is an implicit argument, Idris can usually tell what we mean.

import Syntax.PreorderReasoning p : (a, b, c : Nat) -> (a * b) * c = (c * a) * b p a b c = ((a * b) * c) ={ sym (multAssociative a b c) }= (a * (b * c)) ={ cong (multCommutative b c) }= (a * (c * b)) ={ multAssociative a c b }= ((a * c) * b) ={ cong (multCommutative a c) }= ((c * a) * b) QED

Are we done? …not yet, there’s one more error:

When elaborating right hand side of p: When elaborating an application of function Syntax.PreorderReasoning.Equal.step: Can't unify mult (mult c a) b = mult (mult c a) b with f (mult c a) = mult (mult c a) b

Remember when I said Idris can *usually* tell what we want for our `f`

? In this case, it actually can’t (and yes, this error message doesn’t do a very good job of telling us what’s going on). On line 8, we want to apply `cong`

with `f = (* b)`

, so let’s specify that using implicit-argument curly braces:

import Syntax.PreorderReasoning p : (a, b, c : Nat) -> (a * b) * c = (c * a) * b p a b c = ((a * b) * c) ={ sym (multAssociative a b c) }= (a * (b * c)) ={ cong (multCommutative b c) }= (a * (c * b)) ={ multAssociative a c b }= ((a * c) * b) ={ cong {f = (*b)} (multCommutative a c) }= ((c * a) * b) QED

And… we’re done! Idris accepts this definition as type-correct and total, which means we’ve successfully proved the theorem!