batteries
batteries copied to clipboard
leanprover-community
feat: add type classes for decidable < and <= relations
This means that instead of writing
def f [inst : LT α] [DecidableRel (@LT.lt α inst)] (args ...) := ...
users can write
def f [DecidableLT α] (args ...) := ...
I find this much easier to figure out, and it doesn't impose any extra work on library authors.
This came up while @nomeata and I were writing code examples for a tutorial today.
I think an alternative version that required explicit instances would also serve the goals here, at the cost of a bit more implementation work.
I worry that this is going to just become a trap for new users, who write [PartialOrder X] [DecidableLE X] and now end up with two unrelated ≤ operators.
PartialOrder is not in std4, nor in core Lean. It seems important to me that users using only Std can write if x < y then ... else ... without first understanding dependent types. But fixing this new user papercut should also not make Mathlib worse!
Please help me understand the issue better - why is this worse than if the user had written [PartialOrder X] [LE X], which could easily happen today?
Please help me understand the issue better - why is this worse than if the user had written
[PartialOrder X] [LE X], which could easily happen today?
It's not, really. But I think people are more likely to reach for DecidableLE as a way to say "LE is decidable" rather than "I have a LE and it is decidable", and in the example, the correct solution is [PartialOrder X] [DecidableRel (@LT.lt X _)] which reintroduces exactly the problem we're trying to solve here. This is what I would call a pitfall: the natural option is the wrong one.
Maybe an alternative which solves this issue is to have DecidableLE A just mean the mixin part, meaning that you have to write [LE A] [DecidableLE A] if you just want a decidable LE and nothing more, but this composes better with alternative sources for the LE as in [PartialOrder A] [DecidableLE A].
GHC has an extension ConstraintKinds that if implemented in Lean, could address this.
It lets one wrote constraint synonyms:
type Stringy a = (Read a, Show a)
foo :: Stringy a => a -> (String, String -> a)
foo x = (show x, read)
I'm not sure on the syntax, but it could be something like:
class DecidableLT α := (LT α, DecidableRel (α := α) (· < ·))
def f [DecidableLT α] (x y : α) : Bool := decide (x < y)
I think class abbrev is meant to be Lean's equivalent of ConstraintKinds but the semantics are not quite the same. The notation
class abbrev Stringy α := Read α, Show α
currently expands to
class Stringy α extends Read α, Show α
attribute [instance] Stringy.mk
There is a bit of room for improvement to allow for parametric classes, for example.
Just an update from my side - I've been busy with some other things, but I plan to run some Mathlib builds with a few of the options we've discussed here, then report back on the impact on build times.