Proof-Search Friendly Non-Equality Proofs
The Problem
When designing interfaces, you may occasionally find a need to thread
a proof of non-equality through API, and for ergonomics reasons, you
would like that proof to be an auto
implicit so the user
doesn't have to generate the proof manually. Often, these proofs seem
like they really should be trivial for the compiler to generate, but
proof search will adamantly refuse to do so.
I recently came across an instance of this implementing the Brown Benchmark for Table Types1, where I needed to encode a proof that a given value was non-equal to every value currently in a list (much like a FreshList2, but with propositional equality). In many cases, this list is going to be know statically at compile time, so I would like the compiler to just generate the structure when possible to keep the API easy to use.
It may seem natural to use a value of type Not (x = y)
,
but this has a bit of an issue, the compiler will refuse to generate
even seemingly trivial values of this type:
failing
oneIsNotTwo : Not (1 = 2)
oneIsNotTwo = %search
This is because Not x
is an alias for
x -> Void
, a function type. Proof search won't try to
produces values of function types, it only searches for value types.
More generally, it is a lot easier to find positive proof of a statement
than negative proof of a statement.
The Solution
We can sneak around the compiler's limitations here by generating a
positive proof of non-equality instead. One cheeky way that comes to
mind is to use our old friend Data.So
, instead asking for a
So
bearing witness that the result of calling
decEq x y
satisfies the isNo
function.
Lets take a look at it in action, here's an example of a type that
serves as proof that some value x
is unique compared to
every value in some list:
data IsUnique : (value : t) -> List t -> Type where
NotInTheEmptyList : IsUnique value []
NotHere : DecEq t => {x : t} ->
(prf : So (isNo (decEq value x))) -> IsUnique value xs
-> IsUnique value (x :: xs)
This sneaks our proof of non-equality into a value type, as the
argument to So
is a Bool
, not a function,
allowing proof search to generate these values by actively calling the
decEq
and isNo
functions.
This So (isNo (decEq x y))
type is equivalent to
Not (x = y)
. Don't believe me? Here's proof:
soNoIsNot : DecEq t => {x, y : t} -> So (isNo (decEq x y)) -> Not (x = y)
soNoIsNot {x} {y} soPrf with (decEq x y)
soNoIsNot {x} {y} soPrf | Yes prf = absurd soPrf
soNoIsNot {x} {y} soPrf | No contra = contra
We can therefore use this IsUnique v xs
proof to, for
example, produce a proof of Not (Elem v xs)
:
isUniqueMeansNotElem : {v : t} -> IsUnique v xs -> Not (Elem v xs)
isUniqueMeansNotElem (NotHere prf x) Here =
let notPrf = soNoIsNot {x = v} {y = v} prf
in notPrf Refl
isUniqueMeansNotElem (NotHere prf x) (There y) = isUniqueMeansNotElem x y