Batteries.OrientedCmp et al

Stream: batteries

[Kim Morrison]

There are a number of typeclasses in Batteries about comparators which are now duplicates of the same typeclasses in Std, e.g. OrientedCmp.

Is anyone available to deprecate these, and identify what if any functionality Batteries is still adding here?

[François G. Dorais]

batteries#1306

[François G. Dorais]

That was a big job @Kim Morrison ! Fortunately, I was looking for something to get me back to speed after a long months of overwhelming daytime jobs...

I'm on the final stretch and I think I need additional direction as to where Std is going. In batteries#1306, I moved all the old Batteries classes stuff to Batteries.Classes.Deprecated and I only kept stuff that is missing from Std in Batteries.Classes.Order. Since there is a lot more than I expected, I tried to be comprehensive rather than editorial. I did leave a few notes and I gave absurdly long name for things that I don't think should be in Std. (I still need to do the Mathlib adaptation but that doesn't look like a difficult one so far.)

Anyway, I would appreciate your input before moving further. No rush!

[Paul Reichert]

Thanks for your effort! Sorry, I hadn't seen this thread until now. I am working exactly on overhauling the order-related typeclasses in Std this quarter, so there will be changes and improvements. I am still figuring out the details, though.

Do you mean by "additional direction as to where Std is going" whether Std is going to support the missing lemmas in the foreseeable future, or were you thinking of something different?

[François G. Dorais]

My question was vague (which reflected my ambivalence) so let me clarify.

Kim's request suggested that there wasn't much, if anything, in Batteries that wasn't already in Std. There was in fact quite a few things in the difference: the classes LawfulLECmp, LawfulLTCmp, LawfulBCmp, LawfulCmp, their Ord aliases, and some associated lemmas. I think these could go in Std but it's fine for them to stay in Batteries.

[Paul Reichert]

I see! I agree that it makes sense to have them in Std now that similar classes are also living there. I'll keep this in mind and try upstreaming the remaining classes/lemmas at a later point in the coming weeks, okay?

[François G. Dorais]

@Paul Reichert let me mention a lingering issue that can only be solved by fixing in core.

For historical reasons, the default way for constructing an Ordering-valued comparison from LE or LT instances is compareOfLessAndEq. This choice has some defects:

1. It requires both DecidableLT and DecidableEq.
2. The definition if x < y then .lt else if x = y then .eq else .gt doesn't work unless .eq really means equality.
3. Proving anything about this comparison requires a priori knowing a bunch of facts about the relation between < and =.

This was partly fixed by adding compareOfLessAndBEqwhich requires BEq instead of DecidableEq. This is a bit better for 1 and 2 but it actually makes 3 worse in many ways.

There are better alternatives! For example:

def compareOfLT [LT α] [DecidableLT α] (x y : α) : Ordering :=
  if x < y then .lt else if y < x then .gt else .eq

def compareOfLE [LE α] [DecidableLE α] (x y : α) : Ordering :=
  if x ≤ y then if y ≤ x then .eq else .lt else .gt

Both of these are optimal for 1 and 2 and are much better for 3 as well.

We may be too far down the rabbit hole to fix this but we can't lose hope!

[Paul Reichert]

Is TransCmp.compareOfLessAndEq (and its usages) a good example where these problems play out?

[François G. Dorais]

Yes, exactly.

[Paul Reichert]

I find your arguments for compareOfLT/compareOfLE quite plausible, but assuming that the standard library is comprehensive enough (which may not always be the case), I think the definition of Ord instances of stdlib shouldn't even be relevant downstream, at least at some point in the future.

For example, let's consider LawfulOrd Nat. This instance is currently defined using LawfulCmp.compareOfLessAndEq_of_irrefl_of_trans_of_not_lt_of_antisymm.

If the standard library provided convenient lemmas to derive TransOrd, LawfulEqOrd and other instances in the presence of (say) LE or LT satisfying certain axioms, or perhaps proved that its Ord instances are propositionally equal to compareOfLE, a LawfulOrd Nat instance could be defined without reliance on the definitional nature of the Ord instances . I'm open to adding the lemmas to the standard library that make it convenient to do so.

Is my reasoning sound or do you think projects downstream of the standard library really need to rely on the definition of stdlib's Ord instances?

[Mario Carneiro]

The whole point of those theorems like TransCmp.compareOfLessAndEq is to establish that a given Ord instance is in fact a LawfulOrd

[Mario Carneiro]

if the definition was different, you would prove LawfulOrd in a different way

[Mario Carneiro]

holy shit the new names are terrible

[Mario Carneiro]

I thought that was an instance name

[François G. Dorais]

@Mario Carneiro The awful names are my fault, to some extent, "I gave absurdly long name for things that I don't think should be in Std" to quote myself from earlier.

[François G. Dorais]

Paul Reichert said:

Is my reasoning sound or do you think projects downstream of the standard library really need to rely on the definition of stdlib's Ord instances?

They already do! This is the "rabbit hole" I mentioned earlier. It's a weed that needs to be uprooted.

[François G. Dorais]

FWIW when compareOfLessAndEq was introduced about four years ago, my thought was that this was a bad choice, but I thought just as you that this choice is irrelevant downstream and core would eventually fix it. I have since regretted many times not doing anything to change it back then...

[François G. Dorais]

Also remember that Ord instances are data and therefore subject to diamond issues, regardless of propositional equality.

[Paul Reichert]

Mario Carneiro said:

The whole point of those theorems like TransCmp.compareOfLessAndEq is to establish that a given Ord instance is in fact a LawfulOrd

I understand, but my point is that TransOrd/LawfulOrd instances can be proved without the underlying definition by relying on theorems such as (in the Nat case) Nat.le_trans, Nat.le_total, Nat.le_antisymm, Nat.compare_eq_lt and Nat.compare_eq_gt. These theorems are provided by the standard library and they are independent of the intensional definition of the Ord instance.

So if these theorems were used, the proof of LawfulOrd wouldn't change if the definition was different (but still propositionally equal). Of course, the standard library's lemmas would need different proofs when the definition is changed, but my point is that this would not affect downstream users.

[Paul Reichert]

François G. Dorais said:

Paul Reichert said:

Is my reasoning sound or do you think projects downstream of the standard library really need to rely on the definition of stdlib's Ord instances?

They already do! This is the "rabbit hole" I mentioned earlier. It's a weed that needs to be uprooted.

With "they already do", do you mean that they rely on the intensional definition or that they need to? I think that for most standard library types and their Ord instances, the standard library provides enough lemmas to fully characterize the instances propositionally.

(As I said, I'm happy to provide more/better lemmas if it's too inconvenient right now.)

François G. Dorais said:

Also remember that Ord instances are data and therefore subject to diamond issues, regardless of propositional equality.

Yet this is only a problem if there are non-canonical Ord instances. Why would one create a second non-definitionally-equal Ord instance while hoping that it's definitionally equal to the stdlib one? Mathlib doesn't need to redefine the Ord instances because classes such as LinearOrder extend Ord (forgetful instance principle).

[François G. Dorais]

I'm confused. I don't think we're talking about the same thing anymore.

Lean provides two default comparison constructors: compareOfLessAndEq and compareOfLessAndBEq. There could be just one like compareOfLE, to pick one. Not only is compareOfLE propositionally equal to the two existing constructors in all use cases, it's easier to use. For example, compareOfLE does not require DecidableEq nor BEq. Furthermore, proving TransCmp for compareOfLE only needs two facts (le_trans : ∀ x y z : α, x ≤ y → y ≤ z → x ≤ z and le_total : ∀ x y : α, x ≤ y ∨ y ≤ x) whereas proving TransCmp for compareOfLessAndEq requires three or four facts.

[Paul Reichert]

Okay, let me try to get us aligned again...

• The problem I took away from your earlier post is that in Batteries, there seems to be the need to derive properties such as TransOrd directly from the definition of the Ord instances defined in stdlib. The way these instances are defined is annoying to use.
• Can we add compareOfLE and compareOfLT to the standard library, and perhaps lemmas for stdlib types stating that the Ord instances are propositionally equal to compareOfLE? I think so!
• Should we change the Ord instances in the standard library, such as Ord Nat, such that they are definitionally equal to compareOfLE? As long as users rely on the exact definition of these instances, as Batteries currently does, it would be a breaking change (in other words, changing this is affected by the weeds you were mentioning?).

Regarding the third point, what I don't understand is why Batteries is unfolding the definition of the instances and relying on definitional equality at all. Are there lemmas missing that make this necessary? Or is there some reason why proving LawfulOrd instances without relying on definitional equality isn't nice either?

(Side note: Actually, the standard library already provides TransOrd instances for most types, including Nat. But a similar point holds for LawfulOrd. Here, stdlib at least provides Nat.compare_eq_lt etc.)

Let me give an ad-hoc example in Lean pseudocode:

-- LawfulOrd.ofAxioms doesn't exist right now
instance : LawfulOrd Nat := LawfulOrd.ofAxioms Nat.le_antisymm Nat.le_trans
    Nat.le_total Nat.compare_eq_lt Nat.compare_eq_gt Nat.compare_eq_eq
    Nat.isLE_compare Nat.isGE_compare

All the suffering w.r.t. compareOfLessAndEq is then limited to stdlib authors.

Not sure whether this already helps to clear up misunderstandings, but at least I hope so.

[François G. Dorais]

Ah! We were definitely on two different pages. I think I understand the disconnect.

You view compareOfLessAndEq and compareOfLessAndBEq as implementation details for Ord instances in stdlib. I wish that were true! Unfortunately, they are used downstream and that makes them "weeds" to me as a Batteries maintainer. That is: compareOfLessAndEq and compareOfLessAndBEq are the "weeds", not individual uses thereof.

While working on batteries#1306, I was concerned by how many theorems like LawfulCmp.compareOfLessAndEq_of_irrefl_of_trans_of_not_lt_of_antisymm there were in Batteries. I don't think these belong in stdlib, at least not for public use. I then got worried since matching theorems for compareOfLessAndBEq are missing...

My original suggestion is perhaps better phrased like this:

If stdlib is to provide a compareOfBlah for public use, with accompanying theorems, please let that be something more reasonable like compareOfLT or compareOfLE. And, ideally, remove compareOfLessAndEq and compareOfLessAndBEq from public view.

[Paul Reichert]

I see! Indeed, I thought you were mainly concerned with the Ord instances in stdlib that rely on compareOfBlah. Thanks for clarifying.

[Mario Carneiro]

The reason I originally wrote these lemmas was because there were a ton of Ord instances which were not proved lawful (indeed at the time there wasn't even a LawfulOrd class) in std. So I was saddled with the task of proving a bunch of messy lemmas about how std internals work, which I never like to do. It should have been upstream to begin with

[Mario Carneiro]

if LawfulOrd and compareOfLessAndEq are upstream, then LawfulOrd.compareOfLessAndEq should be upstream too.

[François G. Dorais]

@Kim Morrison batteries#1306 was a lot of work and it is subject to quick rotting. I think we should aim to merge soon.

[Kim Morrison]

I agree. I'm happy to merge asap.

[Kim Morrison]

There's currently a merge conflict in RBMap. I've been holding off adding deprecations to RBMap (in favour of Std.Data.TreeMap) as we won't have parity with the Stream interface until Q4. However it's unused in Mathlib, and I'm unaware of any users of the Stream interface elsewhere (but would appreciate knowing about any, to help inform the Q4 work on TreeMap).

[François G. Dorais]

I hadn't noticed. Fixed now!

[Kim Morrison]

(Update; in a separate thread, I'm convinced there's no need to deprecate RBMap, and it serves a different purpose than TreeMap.)

[François G. Dorais]

??? There's nothing in batteries#1306 that deprecates RBMap.

[Kim Morrison]

This was just in reference to my (retracted) comment above that I wanted to deprecate RBMap in future. I said that in response to your statement above that preparing batteries#1306 was a lot of work -- it would have been less work if the changes to RBMap hadn't had to be part of it.

[Kim Morrison]

@Mario Carneiro, do you want to have a look at the changes in batteries#1306 to RBMap files?

[Mario Carneiro]

I didn't see any changes that were not cosmetic

[François G. Dorais]

The changes to RBMap are entirely superficial.

[Mario Carneiro]

a lot of things got longer, I'm not super happy about that, but not enough to block it

[Mario Carneiro]

I imagine that the added Std. everywhere will go away once the deprecation is removed

[Mario Carneiro]

did these get upstreamed?

instance : Batteries.TransOrd String := .compareOfLessAndEq
  String.lt_irrefl String.lt_trans String.lt_antisymm

instance : Batteries.LTOrd String := .compareOfLessAndEq
  String.lt_irrefl String.lt_trans String.lt_antisymm

instance : Batteries.BEqOrd String := .compareOfLessAndEq String.lt_irrefl

[Mario Carneiro]

I'm not quite clear on why we don't need these yet we do need

instance : Std.LawfulLTOrd String :=
  Std.LawfulLTCmp.compareOfLessAndEq_of_irrefl_of_trans_of_antisymm
    String.lt_irrefl String.lt_trans String.lt_antisymm

[François G. Dorais]

Yes, a lot of the added crud is expected to disappear once deprecations run through. The absurdly long names are my bad and intentional as I mentioned above.

I also just noticed that some instances were redundant. I'll fix those in a few of hours -- I have some non-lean I need to deal with until then :/

[Mario Carneiro]

Also, is there a reason dot notation doesn't work above?

[François G. Dorais]

Std.LawfulLTOrd is not upstreamed yet.

Mario Carneiro said:

Also, is there a reason dot notation doesn't work above?

Where?

[Mario Carneiro]

Mario Carneiro said:

I'm not quite clear on why we don't need these yet we do need

instance : Std.LawfulLTOrd String :=
  Std.LawfulLTCmp.compareOfLessAndEq_of_irrefl_of_trans_of_antisymm
    String.lt_irrefl String.lt_trans String.lt_antisymm

[Mario Carneiro]

note that the code it replaces was using dot notation

[Mario Carneiro]

François G. Dorais said:

Std.LawfulLTOrd is not upstreamed yet.

Right, but it wasn't being proved before, so I assume it followed from the other classes

[Mario Carneiro]

or is this just a new theorem?

[Mario Carneiro]

oh wait, this is the equivalent of the LTOrd instance. What do you mean it is not upstreamed, it has Std namespace?

[François G. Dorais]

Dot notation does work, that was a "typo".

LawfulLTCmp, LawfulLECmp are still in batteries after this PR but they are in the Std namespace. They should be upstreamed to core eventually.

[Mario Carneiro]

@Paul Reichert said:

Let me give an ad-hoc example in Lean pseudocode:

-- LawfulOrd.ofAxioms doesn't exist right now
instance : LawfulOrd Nat := LawfulOrd.ofAxioms Nat.le_antisymm Nat.le_trans
    Nat.le_total Nat.compare_eq_lt Nat.compare_eq_gt Nat.compare_eq_eq
    Nat.isLE_compare Nat.isGE_compare

All the suffering w.r.t. compareOfLessAndEq is then limited to stdlib authors.

Not sure whether this already helps to clear up misunderstandings, but at least I hope so.

Let me try to address this again. There should be no need to use Nat.compare_eq_lt in a theorem such as this, because that is literally the content of the LawfulLTOrd class, and similarly for the others. A LawfulOrd Nat instance follows directly from LawfulLTOrd, LawfulLEOrd and some others, although it can sometimes be convenient to prove LawfulOrd first and get the others as a result. Either way, you ultimately need to reduce to things not involving compare because this is supposed to be the first theorem one proves about compare on the type, and also (for a core type like Nat) this theorem should be in std to begin with. When it appears in Batteries that's because Std was lacking the lemma and it should be upstreamed.

For types not in Std/Init, obviously some proof work has to be left for the downstream library, and Std should provide lemmas to make this as easy as possible. The best thing would be to have a deriving handler, but this seems to be difficult, so until then lemmas like LawfulCmp.compareOfLE are used when the Ord instance is pre-existing or otherwise defined using compareOfLE. When the Ord instance is derived and recursive, right now I think the proof is basically impossible, and I've been avoiding the issue thus far and ensuring that such instances are just avoided altogether.

[François G. Dorais]

Mario Carneiro said:

When the Ord instance is derived and recursive, right now I think the proof is basically impossible, and I've been avoiding the issue thus far and ensuring that such instances are just avoided altogether.

Yet another way that weeds propagate... I hope we can fix this!

With the new module system, it should be possible to hide things like compareOfLessAndEq and make something better instead!

[Mario Carneiro]

I'm not sure that hiding solves the problem here

[Mario Carneiro]

in fact, hiding is part of the reason that the derived Ord instance is difficult to work with

[François G. Dorais]

My opinion is that compareOfLE (or something like that) should be made default, have lots of lemmas and should be used in derive handlers (when that makes sense). There should also be derive handlers for LawfulOrdBlah that work without unnecessary requirements...

[François G. Dorais]

@Mario Carneiro I checked all the instances you mentioned. They were all upstreamed. I also removed a few redundant instances that I had missed. I also fixed your additional comments on GitHub.