remove decidable fields from LinearOrder?

Stream: mathlib4

[Matthew Ballard]

Splitting off the discussion from #mathlib4 > set_option maxSynthPendingDepth 2 about this since there appears to be support on both sides of the question.

It might be too early for a poll but please register your sentiments about dropping the Decidable fields from LinearOrder.

[Matthew Ballard]

Personally I also found this strange compared to the rest of mathlib when I first encountered it. I would lean yes

[Eric Wieser]

I don't think "strange" is that good a reason; Field.nnqsmul is certainly also strange, but it is also useful!

[Eric Wieser]

I think your this proposal would amount to replacing

variable [LinearOrder X]

with

variable [LinearOrder X]
variable [Ord X] [DecidableEq X] [DecidableLT X] [DecidableLE X] [Batteries.LawfulOrd X]

which is rather a mouthful

[Matthew Ballard]

Perhaps "inconsistent" is better language. I hesitate to call this "mine" :) The previous thread had people responding with exclamation points! and did have an actual problem that was currently hidden under the cutoff for depth.

I really just want people to convince me one way or the other while I focus on grading for bit. But I do think further discussion is merited either way.

[Eric Wieser]

I think the actuall problem was a weird typeclass argument, not the fields within LinearOrder. I think pulling decidable fields out of LinearOrder is likely to increase the prevalence of such weird arguments (chosen from the mouthful above)

[Matthew Ballard]

Certainly a mouthful of typeclass assumptions is a solid reason against

[Matthew Ballard]

But we already have default values for some don't we?

[Eric Wieser]

I think splitting it also means we need to re-separate min and inf

[Eric Wieser]

Otherwise either docs#minOfLe creates an instance diamond, or we still need all the decidable instances to define LinearOrder anyway

[Eric Wieser]

Matthew Ballard said:

But we already have default values for some don't we?

We already have default values for the fields in LinearOrder. Did you mean default instances? I think default Decidable instances is just reverting back to the (global) open scoped Classical approach that we've moved away from

[Kevin Buzzard]

that we've moved away from

...and for good reason, as it used to cause diamonds when Lean found the actual decidable order instances on e.g. Nat. So this is where it differs from the [DecidableEq (Ideal R)] situation where there are literally no instances in mathlib.

[Martin Dvořák]

Eric Wieser said:

I don't think "strange" is that good a reason; Field.nnqsmul is certainly also strange, but it is also useful!

It is a good reason. If possible, we should avoid "strange things" in definitions. Imagine somebody comes with a new shiny theorem about linear orders. Whoëver comes to check whether the theorem holds really for all linear orders will be puzzled with the complicated definition, making them wonder whether some linear orders (according to their personal understanding of what linear order is) are excluded. In my case, I have struggled both with nnqsmul and with what OP mentions.

However, I also understand the reasons why it shouldn't be changed.

[Jireh Loreaux]

1 / 0 = 0 is strange to many mathematicians, and we could avoid it. But we don't because strange is not the primary metric we should minimize / optimize for. It's much more useful to allow 1 / 0 = 0.

[Martin Dvořák]

Philosophically, it is the same kind of issue, but in practice, division by zero has different trade-offs.

[Jovan Gerbscheid]

Could there be some comment at LinearOrder explaining why these fields are there?

I think the mouthful of typeclass assumptions isn't a good objection, because we can define ComputableLinearOrder to extend LinearOrder and also contain all of [Ord X] [DecidableEq X] [DecidableLT X] [DecidableLE X] [Batteries.LawfulOrd X].

[Eric Wieser]

Certainly we should document the status quo

[Eric Wieser]

I think if you had that second typeclass, you'd just annoy a bunch of mathematicians who don't like typing the word "computable" because they don't care about it, and then mathlib would end up being less computable as a result.

[Eric Wieser]

Which is a loss both for the mathematicians who were made to think about it more than they currently do, and a loss for the people who like using #eval.

[Yury G. Kudryashov]

Note: we had linear_order and decidable_linear_order in Lean 3, then decided to merge them.

[Yury G. Kudryashov]

Semi-offtopic: I think that default fields is a footgun. IMHO, we should use something like ofMinimalAxioms instead.

[Yury G. Kudryashov]

BTW, doesn't docs#minOfLe create a diamon for Min (Nat × Nat)?

[Jovan Gerbscheid]

Yes, it does:

import Mathlib

#eval min (0,1) (1,0) -- (0,0)

attribute [instance high] minOfLe

#eval min (0,1) (1,0) -- (1,0)

[Jovan Gerbscheid]

I think nobody would ever use minOfLe on Nat × Nat, because it only really makes sense on a linear order, while × is given the pairwise order.

[Yury G. Kudryashov]

Is it possible that someone will use it by accident?

[Yury G. Kudryashov]

(probably, yes, but how easy is to shoot yourself in the foot with this?)

[Jovan Gerbscheid]

It's not an instance, so I don't think so.

[Yury G. Kudryashov]

Ah, indeed!

[Kevin Buzzard]

Aha, so it's on a par with that non-instance which makes $A\otimes_R B$ into a $B$-algebra, which gives a diamond if $A=B$.