From 106d46cc3cb4e63954aa4ef3ed259599f79ac01f Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Sat, 5 Jul 2025 23:53:41 -0400 Subject: [PATCH] Proof-Search Friendly Non-Equality Proofs --- db/posts/8.json | 16 +++++ db/series/1.json | 3 +- projects/Idris/Idris.ipkg | 1 + .../ProofSearchAndNonEquality.md | 66 +++++++++++++++++++ 4 files changed, 85 insertions(+), 1 deletion(-) create mode 100644 db/posts/8.json create mode 100644 projects/Idris/src/TipsAndTricks/ProofSearchAndNonEquality.md diff --git a/db/posts/8.json b/db/posts/8.json new file mode 100644 index 0000000..a28f529 --- /dev/null +++ b/db/posts/8.json @@ -0,0 +1,16 @@ +{ + "edited-at": [ + ], + "hidden": false, + "idris": true, + "ipkg": "/home/nathan/Projects/Blog/projects/Idris/Idris.ipkg", + "posted-at": "2025-07-05T22:48:03.372522-04:00", + "slugs": [ + ], + "source": "/home/nathan/Projects/Blog/projects/Idris/src/TipsAndTricks/ProofSearchAndNonEquality.md", + "special": false, + "tags": [ + "idris", + "tip" + ] +} \ No newline at end of file diff --git a/db/series/1.json b/db/series/1.json index 994b5cf..d4def3e 100644 --- a/db/series/1.json +++ b/db/series/1.json @@ -1,7 +1,8 @@ { "desc": "Introductions to the building blocks of dependently typed programs.

The posts in this series are 'living posts', they will be referenced as library modules by future posts, and will be updated as needs change.", "post-ids": [ - 7 + 7, + 8 ], "title": "Dependent Nuggets" } \ No newline at end of file diff --git a/projects/Idris/Idris.ipkg b/projects/Idris/Idris.ipkg index ce522e4..20285d8 100644 --- a/projects/Idris/Idris.ipkg +++ b/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 = diff --git a/projects/Idris/src/TipsAndTricks/ProofSearchAndNonEquality.md b/projects/Idris/src/TipsAndTricks/ProofSearchAndNonEquality.md new file mode 100644 index 0000000..3619616 --- /dev/null +++ b/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]: + +[^2]: [FreshLists: Containers That Only Accept "Fresh" Elements](/posts/by-slug/freshlists-containers-that-only-accept-fresh.html)