Ord ɑ from LinearOrder ɑ?

Stream: mathlib4

[Thomas Murrills]

Should we have

instance [LinearOrder α] : Ord α where
  compare a b := compareOfLessAndEq a b

somewhere in mathlib4? if so where?

[Thomas Murrills]

(Context: existing minimizing functions on Arrays rely on Ord, and since I'm writing more such functions, I wanted to stay consistent with that. But analogous existing minimizing functions for lists rely on LinearOrder, so I figured there should be a way to move between them in at least one direction. Then we can have theorems about these functions on arrays which depend on LinearOrder.)

[Gabriel Ebner]

We should definitely not have an instance because that creates diamonds, but a def would be good.

[Eric Wieser]

What types would it create diamonds on?

[Eric Wieser]

So far the only existing instance that isn't implemented as compareOfLessAndEq seems to be Fin, and that could easily be changed

[Gabriel Ebner]

Indeed, the extra Ord class isn't really used (yet). Notably, Bool has a different implementation as well.

[Eric Wieser]

I guess I can see the appeal for String or Lex ..., where likely it can be computed more efficiently

[Eric Wieser]

So in the long run a compare field of LinearOrder probably makes sense

[Eric Wieser]

But in the short term just making the above instance global (and adjusting the instances forFin and Bool) is probably more useful than doing nothing

[Eric Wieser]

If we have no theorems about Ord then diamonds don't matter anyway

[Thomas Murrills]

Hmm, would it be any harm to jump straight to the long run and have LinearOrder extend Ord with the above as a default field value? (afaict structure instances prefer typeclass synthesis of substructures to optparams for their field values, so I don’t think this would interfere with any Ord instances that were already defined, and so any diamonds should be defeq…)

[Eric Wieser]

I guess as a default it probably won't interfere with porting

[Thomas Murrills]

Now that I think about it, though, if we’re going to add compare to LinearOrder it should be lawful—namely we should add fields compare_lt_iff_lt and compare_eq_iff_eq (we can prove the would-be remaining field as a theorem)

[Thomas Murrills]

(These ofc can also have default proofs so that it doesn’t affect porting)

[Eric Wieser]

Or you could just ask the user to prove that compare a b = compareOfLessAndEq a b to save a field

[Thomas Murrills]

true! fields are at a premium, I gather?

[Eric Wieser]

I'd probably go for the single-field approach until we actually know what specialized instances to expect and which ones will be annoying to prove. Right now, almost every instance will just have rfl in that field, whereas proving your fields is very marginally harder.

[Thomas Murrills]

Exploring this on !4#2858 (have yet to supply the lawfulness field for Fin)

[Thomas Murrills]

!4#2858 is green; I've tentatively put it out for review, in case we decide to go with it.