search

leanprover / lean4

Lean 4 programming language and theorem prover
https://lean-lang.org
Apache License 2.0
4.69k stars 421 forks source link

Make `Ord` extend `BEq`, `LE`, `LT`, `Max`, `Min` #1777

Open gebner opened 2 years ago

gebner commented 2 years ago

As discussed in the dev meeting.

The general rule should be: if there is a noncanonical fooOfBar instance, then we should probably always make Bar extend Foo.

I'd also prefer to have properties defining the derived operations like a < b ↔ compare a b = .lt be part of Ord. Additional "lawful" classes like LinearOrder should then contain stronger properties like ¬ a < a. (But I believe Sebastian preferred a different split.)

fgdorais commented 1 year ago

Since there hasn't been any comments here in two months, should this be approved by no contest? I, for one, am looking forward to this.

Regarding the last paragraph: I can't think of a compelling situation where one would want a type with instances of LT, LE and Ord that disagree but it's probably best for Lean core to remain agnostic about this. There might then be a need for a LawfulOrd class that ensures basic coherence laws like a < b ↔ compare a b = .lt, but that could be delegated to Std, along with stronger laws like TransOrd and LinearOrd.

fgdorais commented 1 year ago

For what it's worth, I did the basic change to make Ord extend BEq, LT, LE, Min, Max on a fork of mine: https://github.com/fgdorais/lean4/tree/ord_refactor

I won't submit a PR since I had to update stage0 after modifying the Ord derive handler and there's also a few small changes to Lake. I also didn't add any "lawful" classes. In any case, maybe this will save someone some work...

eric-wieser commented 1 month ago

Regarding the last paragraph: I can't think of a compelling situation where one would want a type with instances of LT, LE and Ord that disagree

One argument would be that Ord α, since constrained to a linear order, should represent a canonical extension of the order provided by LE and LT, not necessarily the same order. So if x ≤ y then ord x y = .le, but the converse isn't required to hold.

This lets Ord (α × β) safely be the lexicographic order, rather than not existing at all; which in turn makes it easier to print Finset etc in a a friendly order.