Proof-Search Friendly Non-Equality Proofs

projects/Idris/Idris.ipkg

@@ -20,6 +20,7 @@ modules = Idris
         , Posts.HelloWorld
         , LessMacrosMoreTypes.Printf
         , DependentNuggets.FreshLists
+        , TipsAndTricks.ProofSearchAndNonEquality
 
 -- main file (i.e. file to load at REPL)
 -- main =

projects/Idris/src/TipsAndTricks/ProofSearchAndNonEquality.md

@@ -0,0 +1,66 @@
+# Proof-Search Friendly Non-Equality Proofs
+
+```idris hide
+module TipsAndTricks.ProofSearchAndNonEquality
+
+import Data.List.Elem
+import Data.So
+import Decidable.Decidable
+import Decidable.Equality
+```
+
+## 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.
+
+I recently came across an instance of this implementing the _Brown Benchmark for Table Types_[^1], 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_[^2], 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:
+
+```idris
+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:
+
+```idris
+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:
+
+```idris
+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)`:
+
+```idris
+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
+```
+
+
+[^1]: <https://github.com/brownplt/B2T2>
+
+[^2]: [FreshLists: Containers That Only Accept "Fresh" Elements](/posts/by-slug/freshlists-containers-that-only-accept-fresh.html)