Instead of proving everything by hand, sometimes we would like to produce proofs of certain propositions automatically. It seems reasonable to think that we can do this for any class of propositions for which a decision procedure exists. However, we don’t necessarily want to extend the language itself — errors in our extension could mess everything up.

Proof by reflection is one way to write a verified procedure within the language itself. Reflection lets us convert a piece of the program into a data structure in Idris itself; we can manipulate it like we would any other (this is very similar to Lisps in some regard). By analyzing the structure of the proof goal itself, we can automatically derive a term of the goal’s type.

LTE m n is a relatively simple type which represents less-than-or-equal-to propositions. It would be great to be able to produce a value of, say, LTE 10 15 at compile time! Traditionally, if the value is computed automatically, it will be wrapped in a type like Dec or Maybe, which you then have to do case analysis on. You can always write out the value manually, but who wants to write LTESucc (LTESucc (LTESucc ...))? Below, I’ll detail two different methods for producing these proofs automatically.

Method 1

We already have a decision procedure isLTE for computing whether LTE m n is inhabited or not in the standard library, so we just need a way to safely unpack this value.

data IsYes : Dec p -> Type where
  ItIsYes : IsYes (Yes prf)

getYes : (x : Dec p) -> IsYes x -> p
getYes (Yes prf) ItIsYes = prf
getYes (No _) ItIsYes impossible

By providing only a constructor for the Yes case, the IsYes type lets us pack up a proof that we indeed have a value of form Yes x for some x and getYes lets us extract x itself.

%reflection
reflectLTE : (P : Type) -> Dec P
reflectLTE (LTE m n) = isLTE m n

The %reflection annotation tells Idris to treat the arguments to this function as syntax rather than as values. This lets us pattern match on the syntax itself. The actual meat of this function is rather simple! Note that this function is not total.

syntax LTEProof = quoteGoal x by id in
	getYes (reflectLTE x) ItIsYes

quoteGoal foo by f in bar takes the quoted goal, applies f to it, and then introduces it as foo in the expression bar. Since we don’t need to do anything special to the quoted form, we just apply id.

By calling getYes on our result and passing in ItIsYes, we are forcing the typechecker to try and figure out that our term is actually in the form we want. If the typechecker cannot figure it out, then this will fail at compile-time. We can use our new syntax as follows:

lte5_10 : LTE 5 10
lte5_10 = LTEProof

And trying to construct a proof of proposition gives an error like so:

When elaborating right hand side of lte10_5:
When elaborating an application of function Main.getYes:
        Can't unify
                IsYes (Yes prf)
        with
                IsYes (reflectLTE x)

        Specifically:
                Can't unify
                        Yes prf
                with
                        No (succNotLTEzero . fromLteSucc . fromLteSucc .
                            fromLteSucc .
                            fromLteSucc .
                            fromLteSucc)

Error messages with this approach are not very friendly! Maybe with David Christiansen’s Reflect on Your Mistakes! this can be made better, but unfortunately I haven’t investigated that yet.

Method 2

The second approach is inspired by section 4.1 in Paul van der Walt’s Reflection in Agda. We construct an LTE predicate which is either the unit or empty type if the proposition is true or false, respectively.

lte' : Nat -> Nat -> Type
lte' Z k         = ()      -- 0 ≤ k
lte' (S k) Z     = Void    -- ¬(k + 1 ≤ 0)
lte' (S k) (S l) = lte k l -- k ≤ l → k + 1 ≤ l + 1

If lte' n o maps to the empty type, then a value x : lte' n o can produce anything we want via false elimination. Using this allows us to write the approach with a normal function:

LTEProof' : (m, n : Nat) -> lte' m n -> LTE m n
LTEProof' Z     k     ()  = LTEZero
LTEProof' (S k) Z     prf = absurd prf
LTEProof' (S k) (S l) prf = LTESucc $ LTEProof' k l prf

But this method is a little annoying as-is; we have to pass in all of our arguments, including the proof lte' m n, explicitly. This is where implicit arguments come in handy. By specifying the type signature as:

LTEProof' : {m, n : Nat} -> {auto prf : lte' m n} -> LTE m n

We can force the type-checker to figure out these arguments for us. The auto keyword tells the compiler to try and produce a value using the trivial tactic. After the necessary modifications, our function ends up looking like this:

LTEProof' : {m, n : Nat} -> {auto prf : lte' m n} -> LTE m n
LTEProof' {m=Z}   {n=k}         = LTEZero
LTEProof' {m=S k} {n=Z}   {prf} = absurd prf
LTEProof' {m=S k} {n=S l} {prf} = LTESucc $ LTEProof' {m=k} {n=l} {prf}

Using LTEProof' is identical to the first approach:

lte5_10 : LTE 5 10
lte5_10 = LTEProof'

However, error messages look a little nicer this time around:

When elaborating argument prf to function Main.LTEProof':
        Can't solve goal
                lte' 10 5

Conclusion

Both methods are effective at producing proofs automatically. The first approach takes more footwork to write and has unforgiving error messages upon failure. However, the ability to inspect the quoted syntax is far more powerful than the technique used in the second approach, and will likely come in handy for more complicated examples. Think about your problem domain before you decide which to use!