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 Types¹, where I needed to encode a proof that a given value was non-equal to every value currently in a list (much like a FreshList², 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 Sobearing 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