lean4
lean4 copied to clipboard
leanprover
fix: remove `Option.lt` and related components
This is a draft PR implementing the minimal changes required to fix #3100.
- ❗ Mathlib CI will not be attempted unless you rebase your PR onto the 'nightly' branch. (2023-12-20 17:44:12)
- ✅ Mathlib branch lean-pr-testing-3102 has successfully built against this PR. (2023-12-20 20:02:59) View Log
- ✅ Mathlib branch lean-pr-testing-3102 has successfully built against this PR. (2023-12-20 21:21:25) View Log
I'm personally in favour of Mathlib having the incomparable order as the default on Option - in some ways it's going to be quite useful to have something on it - but that's a discussion to have elsewhere. Point is it's a downstream choice anyway.
Don't you need at least some order on Option if you need to put data types with option in it into, say, a RBTree or some other ordered data structure? Or if you want to sort arrays of them?
Yes, precisely so. And the incomparable order is the most neutral of the "obvious" choices I think.
(I don't know if it should be in std4 or mathlib4. Clearly any order hierarchy stuff should be in the latter but I can see computer science applications needing the basic order on Option defined for the reasons you mention.)
Sorry, I should have said total order I guess, so incomparable doesn't help. If you need to put Option String into a search tree, you need to be able to totally order all the values (but as a user care less about the precise order).
E.g. what do you pass as lt to
def Array.qsort {α : Type u_1} (as : Array α) (lt : α → α → Bool) : Array α
when α is Option String? This is basic programming functionality (woudn’t even call it “computer science”).
Well, for the function you've given there, it seems like it "makes sense" if any input that involves none outputs false. It probably then depends how qsort is written.
(If it is written assuming totality, it should really have that as a hypothesis in some form, as a typeclass or something else.)
You have high expectations for how programming APIs are structured :-D
Most ordering based data structures will break of the passed lt isn't a linear order, without telling you.
It may make sense to have different type classes for programming (total, canonical instances for common data type) and mathematics?
Btw the none < some _ order on Option is very common in programming, like false < true and [] < _ :: _, so less arbitrary than it maybe looks like from the math point of view.
I should say that I'm as much as programmer as a mathematician. But yes, it makes some sense to make that choice - most implementations of sorting algorithms seem to basically assume totality and that's as good as anything and not without precedent. Though to me false < true is more obvious somehow (because in some sense it's 0 < 1).
Right, and from false < true it's a small step to “empty before filled” order for container types like option and list, if one associates “false” with “no value” or “value”.
So it's rather defensible to have this order, the question is more how to make sure it doesn't get in the way when you want to do math. (but wouldn't you then use WithBot and WithTop?)
I certainly feel that WithTop < Incomparable and WithTop < WithBot - in a sense I personally don't care about the difference between Incomparable and WithBot too much. BUT: not all the API for Option exists on With*. So the other day when I tried to switch them out it broke more things than I was hoping.
not all the API for Option exists on With*.
It kinda does, because WithTop α = Option α, but some of the convenience features (dot notation, type class inference) probably doesn’t work out of the box.
But that’s more a reason to improve the With* APIs?
I don't disagree with that! I was surprised that it didn't Just Work TM tbh.