This post is a literate Idris file, so first let’s get some bureaucracy out of the way:

```
module LT
%default total
```

When writing Idris code, we sometimes need a proof as an argument to a function. In many cases, these proofs can be constructed automatically by a decision procedure. Here, I’m using the term "decision procedure" for some property `p`

to refer to a function that returns something in the type `Dec p`

.

An instance of `Dec p`

is either a proof of `p`

or a proof that `p`

is an absurdity. The datatype is defined as follows:

```
data Dec : Type -> Type where
Yes : p -> Dec p
No : (p -> _|_) -> Dec p
```

As an example, take the following type from the Idris library that represents a proof that one natural number is less than or equal to another:

```
data LTE : Nat -> Nat -> Type where
lteZero : LTE 0 m
lteSucc : LTE n m -> LTE (S n) (S m)
```

The first constructor, `lteZero`

, should be interpreted as an assertion that zero is less than or equal to any natural number. The second, `lteSucc`

, is an assertion that if \(n \leq m\), then \(n+1 \leq m+1\). It happens to be the case that, for any two natural numbers, it is decidable whether the first is less than or equal to the second.

To prove this, we start with two simple lemmas. The first states that it is not the case that the successor of any number is less than or equal to zero:

```
notLTESZ : LTE (S k) Z -> _|_
notLTESZ lteZero impossible
```

Additionally, we show that, if \(k \not\leq j\), then \(k+1 \not\leq j+1\):

```
notLTE_S_S : (LTE k j -> _|_) -> LTE (S k) (S j) -> _|_
notLTE_S_S nope (lteSucc x) = nope x
```

We are now in a position to write the decision procedure, by examining each case and using our lemmas to produce the appropriate contents for the `No`

constructor. If the details don’t make sense, then please fire up Idris, replace some right-hand sides with metavariables, and examine the proof context.

```
decLTE : (n,m : Nat) -> Dec (n `LTE` m)
decLTE Z m = Yes lteZero
decLTE (S k) Z = No notLTESZ
decLTE (S k) (S j) with (decLTE k j)
decLTE (S k) (S j) | (Yes prf) = Yes (lteSucc prf)
decLTE (S k) (S j) | (No contra) = No $ notLTE_S_S contra
```

Now that these details are out of the way, we can get to the main point of this blog post: demonstrating various techniques for getting Idris to fill out these proofs for us.

The most straightforward way is to use the interactive editing features to get Idris to construct the proof term directly. For example, if we want to show that \(3 \leq 5\), then we need only create a definition with type `3 `LTE` 5`

:

`ok : 3 `LTE` 5`

We can then use `C-c C-s`

in `idris-mode`

to cause it to become

```
ok : 3 `LTE` 5
ok = ?ok_rhs
```

Using the proof search command `C-c C-a`

on the metavariable gives us

```
ok : 3 `LTE` 5
ok = lteSucc (lteSucc (lteSucc lteZero))
```

and the decision procedure simply isn’t necessary. This approach can make our programs ugly, but it is straightforward and direct. We need not actually show the resulting term, however. In Idris, tactic scripts are allowed as the right-hand side of definitions. So we can simply invoke the `search`

tactic explicitly, rather than using it through the compiler’s editor interface, and the resulting term does not need to occur in the source file. This can also be more robust in the face of changes to the definition of `LTE`

. The tactic-based definition is:

```
okTactic : 3 `LTE` 5
okTactic = proof search
```

Here, `proof`

begins a tactic script, and `search`

is the tactic to be invoked.

Using Idris’s built-in proof search has two major limitations:

- It cannot solve more "interesting" goals, in which a simple recursive application of constructors is insufficient
- It fails to find large goals, as the recursion depth is limited. For example, it cannot solve
`103 `LTE` 105`

.

What we really want to do is use `decLTE`

to find the term.

One non-solution is to have the right-hand side of the definition perform a case analysis on the result of a call to `decLTE`

, and then return the contents of the `Yes`

case. Because we know that three is, in fact, less than five, we will never need the `No`

case:

```
okCase : 3 `LTE` 5
okCase = case decLTE 3 5 of
Yes prf => prf
```

Unfortunately, the Idris compiler needs to be convinced of the fact that `No`

cannot occur. We do this by showing that the `No`

case could cause the empty type to be inhabited, and then use `FalseElim`

. Unfortunately, doing this requires actually proving the property again:

```
okCase : 3 `LTE` 5
okCase = case decLTE 3 5 of
Yes prf => prf
No nope => FalseElim . nope $ lteSucc (lteSucc (lteSucc lteZero))
```

So this method is a non-starter.

The next method is to cause the solver for implicit arguments to execute the decision procedure while filling out an implicit argument for the proof, and then return this implicit argument. The definition `okImplicit`

demonstrates this technique:

```
okImplicit : 103 `LTE` 105
okImplicit = getProof
where getProof : {prf : LTE 103 105} -> {auto yep : decLTE 103 105 = Yes prf} -> 103 `LTE` 105
getProof {prf} = prf
```

All of the work happens in `getProof`

, which is in a `where`

block to keep the type signature of `okImplicit`

clean. In the definition of `getProof`

, the implicit argument `prf`

is the one that will be filled out with the proof, and then returned. The argument `yep`

is an implicit proof that the result of executing the decision procedure will be `Yes prf`

– in other words, that it will succeed, and the thing it succeeds with will unify with `prf`

. The `auto`

keyword causes Idris to fill out the argument with `refl`

, the constructor of proofs of equality.

While the `okImplicit`

technique leads to noisy boilerplate in type signatures, it also tends to cause error messages that are easy to understand. I’ve had a lot of luck using it for embedded DSLs with some kind of side condition (like "these queries must have disjoint schemas").

The final technique that I’d like to demonstrate uses a dependently-typed extractor of proofs from `Dec`

. The *type* of the function `getYes`

does case-analysis on the result of a decision procedure. If the result was `Yes`

, then `getYes`

will return the contents – an instance of `p`

. Otherwise, it returns unit, which contains no interesting information. Note that the result of the case expression is a *type* — either the type parameter to `Dec`

or the unit type.

`getYes : (res : Dec p) -> case res of { Yes _ => p ; No _ => () }`

The body of `getYes`

performs a case analysis on the result of the decision, either returning a proof or a trivial value, in accordance with the type. Note that Idris’s interactive editing features were able to write this code entirely – the only thing I needed to do was tell it to case split on the argument. Agda, which has more advanced interactive editing features, could probably write the entire body by passing Agsy the `-c`

option, which enables case splitting.

```
getYes (Yes prf) = prf
getYes (No contra) = ()
```

Now, `getYes`

can be used on the right-hand side of our definition to extract the proof:

```
okYes : 3 `LTE` 5
okYes = getYes (decLTE 3 5)
```

While this approach is clean, the error messages can be somewhat unpleasant if Idris is asked to prove a falsehood. The following code:

```
oops : 5 `LTE` 3
oops = getYes (decLTE 5 3)
```

results in this unification error:

```
When elaborating right hand side of oops:
Can't unify
case block in getYes (LTE (fromInteger 5) (fromInteger 3)) (decLTE (fromInteger 5) (fromInteger 3)) (decLTE (fromInteger 5) (fromInteger 3))
with
LTE 5 3
Specifically:
Can't unify
case block in getYes (LTE (fromInteger 5) (fromInteger 3)) (decLTE (fromInteger 5) (fromInteger 3)) (decLTE (fromInteger 5) (fromInteger 3))
with
LTE 5 3
```

whereas the error message from

```
badImplicit : 105 `LTE` 103
badImplicit = getProof
where getProof : {prf : LTE 105 103} -> {auto yep : decLTE 105 104 = Yes prf} -> 105 `LTE` 103
getProof {prf} = prf
```

was

```
When elaborating right hand side of badImplicit:
When elaborating argument yep to LT.badImplicit, getProof:
Can't solve goal
decLTE (fromInteger 105) (fromInteger 104) = Yes prf
```

You have now seen a few ways of getting Idris to find proofs. Hopefully, you’ve also gotten a bit more understanding of how Idris works while compiling your source file.

This post sprang out of a discussion on a Github issue with Nicola Botta. The discussion of error messages is improved as the result of a suggestion from Anthony Cowley. Thanks, Nicola and Anthony!