Preorder on Option

Stream: Is there code for X?

[Wrenna Robson]

Does Option have any kind of preorder relationship defined (assuming the underlying type does)? I've run myself into a mild pickle through assuming it did but I'm not sure it does.

[Mario Carneiro]

See docs#WithTop and docs#WithBot

[Mario Carneiro]

depending on whether you want none to be at the top or bottom

[Eric Wieser]

I guess you could put an order on Option X that has none as incomparable?

[Wrenna Robson]

Yeah, that's what I was assuming.

[Wrenna Robson]

Or hoping for.

[Wrenna Robson]

Oddly there is an LT instance defined? But it isn't much use.

[Wrenna Robson]

But what I want is
instance (priority := 10) le [LE α] : LE (Option α) := ⟨Option.Rel (. ≤ .)⟩
instance (priority := 10) lt [LT α] : LT (Option α) := ⟨Option.Rel (. < .)⟩

(and then ideally a preorder...)

[Wrenna Robson]

Wait no. I want that for LE, for LT I don't because obviously Bot should not be LT itself as then you can't make a Preorder

[Wrenna Robson]

Urrrgh. That might be a day's work buggered if this is a challenge. I assumed (given that < worked!) that it would just nicely inherit the structure.

[Yaël Dillies]

Just define a < b ↔ a ≤ b ∧ ¬ b ≤ a

[Wrenna Robson]

Sure, that's what I want.

[Wrenna Robson]

But obviously if it doesn't already exist there will be lots of fiddly lemmas to sort.

[Wrenna Robson]

Also, instLTOption exists by default, and makes none lt everything else - which I don't particularly want. But also trying to move to WithBot or WithTop means parts of the Option API don't work - I want to retain that.

[Wrenna Robson]

That instance is in Init.Data.Option.Basic

[Eric Wieser]

docs#instLTOption

[Yaël Dillies]

Oh that's ancient

[Wrenna Robson]

Indeed, but because it already exists it somewhat gets in the way for me/was a footgun because < worked, but actually it didn't really have any way of using it properly.

[Eric Wieser]

< is defined correctly, isn't it?

[Eric Wieser]

Oh wait, no it isn't

[Eric Wieser]

It declares none as a bottom element

[Wrenna Robson]

It uses Option.lt, so, no.

[Eric Wieser]

I think we should remove it, if you want that behavior you should use WithBot

[Wrenna Robson]

Yes, I agree.

[Eric Wieser]

Eric Wieser said:

I guess you could put an order on Option X that has none as incomparable?

I think this is a good idea though

[Wrenna Robson]

Yep.

[Wrenna Robson]

I think what you do is

• define <= as Option.Rel (le)
• Define < as Yaël says above, the standard a < b if a <=b and not (b <= a) thing.

[Wrenna Robson]

I believe that will also give a Preorder if your base type has one. I assume you also get PartialOrder and LinearOrder as appropriate too?

[Yaël Dillies]

Actually if you want to make none incomparable you can just define ¬ none < none, ¬ none < some b, ¬ some a < none and some a < some b ↔ a < b and that will give you nice definitional properties

[Wrenna Robson]

Well, yeah - that also looks great. Just would like the inheriting thing really!

[Wrenna Robson]

I don't have time today (or honestly the mental space - I'm not in a good place with the stres right now) to put a PR together, but it seems like honestly it would be good. And this feels like the "right" order to have on Option as opposed to WithBot or WithTop.

[Wrenna Robson]

(We don't have a notation for none and some x, right? You just write that?)

[Yaël Dillies]

some is also the coercion

[Eric Wieser]

Wrenna Robson said:

I believe that will also give a Preorder if your base type has one. I assume you also get PartialOrder and LinearOrder as appropriate too?

Not a linear order, because none is incomparable and therefore le_total isn't true

[Wrenna Robson]

Oh yes ofc

[Wrenna Robson]

Eric Wieser said:

Wrenna Robson said:

I believe that will also give a Preorder if your base type has one. I assume you also get PartialOrder and LinearOrder as appropriate too?

Not a linear order, because none is incomparable and therefore le_total isn't true

Oh yes. But I think it would be a perfectly good PartialOrder?

[Eric Wieser]

Wrenna Robson said:

I don't have time today (or honestly the mental space - I'm not in a good place with the stres right now) to put a PR together

A middle ground that maybe we should encourage more is to create a github issue to track the idea

[Eric Wieser]

Heck, this might even be a "good first issue"

[Wrenna Robson]

example {α : Type*} [Preorder α] : Preorder (Option α) where
  lt a b := match a, b with | some a, some b => a < b | _, _ => False
  le a b := match a, b with | none, none => True | some a, some b => a ≤ b | _, _ => False
  le_refl a := match a with | none => sorry | some a => sorry
  le_trans a b c := sorry

Not actually sure how you fill the sorries here. Also I get some kind of weird error:

type mismatch
  HEq.rfl
has type
  HEq ?m.92552 ?m.92552 : Prop
but is expected to have type
  a✝ < b✝ ↔ a✝ ≤ b✝ ∧ ¬b✝ ≤ a✝ : Prop

But I assume this is something to do with the existing LT instance interfering? IDK.

[Wrenna Robson]

It seems like there are two, maybe three PRs here:

• kill the existing Option instance (That is in Init.Data.Option.Basic - is that Mathlib? Deeper?)
• Add in a new instance for Option (where should this go?)
• Add the Preorder and Partial Order results.

[Wrenna Robson]

Wow yeah it looks like that instance is in the actual Lean 4 repo. I don't even know if they accept PRs.

[Wrenna Robson]

Is there a way to supress an existing instance? I wonder if that instance is actually used by anything.

[Eric Wieser]

The weird error is coming from the lt_iff_le_not_le field that you omitted

[Wrenna Robson]

aha

[Wrenna Robson]

It didn't list that as a missing field so I didn't think to.

[Eric Wieser]

Here's a full proof:

example {α : Type*} [Preorder α] : Preorder (Option α) where
  lt
    | some a, some b => a < b
    | _, _ => False
  le
    | none, none => True
    | some a, some b => a ≤ b | _, _ => False
  le_refl
    | none => trivial
    | some a => le_refl a
  le_trans
    | none, none, none, _, _ => trivial
    | some a, some b, some c, hab, hbc => le_trans hab hbc
  lt_iff_le_not_le a b :=
    ⟨(match a, b, · with | some a, some b, h => lt_iff_le_not_le.1 h),
     (match a, b, · with
      | none, none, ⟨_, hn⟩ => hn trivial
      | some a, some b, h => lt_iff_le_not_le.2 h)⟩

[Wrenna Robson]

Aha. Thanks, I was trying to use rfl where you have trivial but I see now the issue.

[Eric Wieser]

The last one is a fun golfing challenge

[Yaël Dillies]

Is there not some existing inductive proposition to lift α → β → Prop to Option α → Option β → Prop?

[Eric Wieser]

Yes, but that only works for le

[Wrenna Robson]

Yes, Option.Rel.

[Yaël Dillies]

Surely you don't need iff_iff_implies_and_implies ?

[Wrenna Robson]

Yes you can't lift < using that.

[Yaël Dillies]

Wrenna Robson said:

Yes, Option.Rel.

Yeah but without the none case

[Wrenna Robson]

Oh I see. I haven't found one!

[Eric Wieser]

I guess we could adjust docs#Option.Rel to take the none value too

[Eric Wieser]

Or define Option.StrictRel

[Wrenna Robson]

Option.lt imposes the "none is least" condition and is a bit of a trap imo.

[Wrenna Robson]

You would possibly want to consider nixing it at the same time as nixing instLTOption, and add Option.StrictRel as you say.

[Eric Wieser]

Wrenna Robson said:

Wow yeah it looks like that instance is in the actual Lean 4 repo. I don't even know if they accept PRs.

You could make a draft PR that deletes the instance and sees what breaks (or just do this in a fork)

[Wrenna Robson]

Having experimented with deleting it, the answer seems to be: not much. If it builds OK I might well actually submit a PR if that's in line with the lean4 contribution guidance.

[Wrenna Robson]

Looks like I should open an issue first.

[Eric Wieser]

My process has been 1) open a draft PR, check it compiles, discuss on zulip 2) write the issue, linking the zulip thread 3) promote the draft PR to a real PR

[Eric Wieser]

The draft PR is nice because it also tests Std and mathlib for you

[Wrenna Robson]

https://github.com/leanprover/lean4/issues/3100

[Wrenna Robson]

Their contribution guidelines say "make an issue before making a PR". I am not sure how to distinguish between a draft PR and a real PR.

[Eric Wieser]

When you make a PR the "open PR" button has a "draft" dropdown

[Wrenna Robson]

Oh interesting. Perhaps if it compiles fine locally I will do that.

[Wrenna Robson]

Interestingly it couldn't even successfully detect the Lean version in the file when I opened it, I assume because it's just running at the bottom of the stack and a project isn't set up? Idk.

[Wrenna Robson]

How do I link to commits in repos other than mathlib?

[Yaël Dillies]

Eg YaelDillies/LeanAPAP#3

[Wrenna Robson]

Ta

[Wrenna Robson]

leanprover/lean4#3102 and leanprover/std4#473 may be of interest then

[Eric Wieser]

neat, everything is green with the core change

[Wrenna Robson]

Yep, it seems to genuinely break nothing. So I am hoping it will be an easy decision for them.

[Wrenna Robson]

What is the theorem for like - so I have Option.Rel. I know Option.Rel r (some a) (some b). So I can conclude that r a b.

[Eric Wieser]

That's Option.Rel.rec

[Eric Wieser]

Or just cases h

[Wrenna Robson]

Aye, cases h worked fine, just was trying to do it as a term. I was using Option.Rel.casesOn and it wasn't really working.

[Wrenna Robson]

Incidentally, there is an argument that there shouldn't be any kind of ordering on Option at all, and we have a third synonym for the incomparable ordering. What do you think?

[Wrenna Robson]

Personally I like the idea of Option having an ordering and it being that one, because to me it's the best "default".

[Wrenna Robson]

inductive StrictRel (r : α → β → Prop) : Option α → Option β → Prop
  /-- If `a ~ b`, then `some a ~ some b` -/
  | some {a b} : r a b → StrictRel r (some a) (some b)

instance instLTOption' [LT α] : LT (Option (α)) := ⟨StrictRel (· < ·)⟩
instance instLEOption [LE α] : LE (Option (α)) := ⟨Rel (· ≤ ·)⟩

@[simp]
lemma none_le_none {α : Type*} [LE α] : (none : Option α) ≤ none := Rel.none
@[simp]
lemma not_none_le_some {α : Type*} [LE α] {a : α} : ¬ none ≤ some a := fun ha => by cases ha
@[simp]
lemma not_some_le_none {α : Type*} [LE α] {a : α} : ¬ some a ≤ none := fun ha => by cases ha

lemma some_le_some_of_le {α : Type*} [LE α] {a b : α} (hab : a ≤ b) :
    some a ≤ some b := Rel.some hab
lemma le_of_some_le_some {α : Type*} [LE α] {a b : α} (hab : some a ≤ some b) :
    a ≤ b := by cases hab; assumption
@[simp]
lemma some_le_some_iff {α : Type*} [LE α] {a b : α} : some a ≤ some b ↔ a ≤ b :=
  ⟨le_of_some_le_some, some_le_some_of_le⟩

@[simp]
lemma not_none_lt_none {α : Type*} [LT α] : ¬ (none : Option α) < none := fun ha => by cases ha
@[simp]
lemma not_none_lt_some {α : Type*} [LT α] {a : α} :
    ¬ (none : Option α) < some a := fun ha => by cases ha
@[simp]
lemma not_some_lt_none {α : Type*} [LT α] {a : α} :
    ¬ some a < (none : Option α) := fun ha => by cases ha
lemma some_lt_some_of_lt {α : Type*} [LT α] {a b : α} (hab : a < b) :
    some a < some b := StrictRel.some hab
lemma lt_of_some_lt_some {α : Type*} [LT α] {a b : α} (hab : some a < some b) :
    a < b := by cases hab; assumption
@[simp]
lemma some_lt_some_iff {α : Type*} [LT α] {a b : α} : some a < some b ↔ a < b :=
  ⟨lt_of_some_lt_some, some_lt_some_of_lt⟩

instance {α : Type*} [Preorder α] : Preorder (Option α) where
  le_refl a := a.casesOn Rel.none (fun _ => Rel.some (le_refl _))
  le_trans a b c hab hbc := by
    cases' hab with _ _ hab
    · cases' hbc with _ _ hbc
      exact Rel.some (hab.trans hbc)
    · cases hbc
      exact Rel.none
  lt_iff_le_not_le a b := Iff.intro (fun hab => by
    cases' hab with _ _ hab
    simp_rw [some_le_some_iff]
    exact le_not_le_of_lt hab)
    (fun ⟨hab, hba⟩ => by
      cases' hab with _ _ hab
      · simp_rw [some_le_some_iff] at hba
        exact some_lt_some_of_lt (lt_iff_le_not_le.mpr ⟨hab, hba⟩)
      · exact (hba none_le_none).elim)

instance {α : Type*} [PartialOrder α] : PartialOrder (Option α) where
  le_antisymm a b hab hba := by
    cases' hab with _ _ hab
    · exact (some.injEq _ _).symm ▸ (le_antisymm hab (le_of_some_le_some hba))
    · exact rfl

[Wrenna Robson]

Now, where in Mathlib should this go? We don't seem to import any order files in the basic Option/Data/* files. @Yaël Dillies, should it go in Order/Basic.lean?

[Yaël Dillies]

Either there or in a new Data.Option.Order file

[Wrenna Robson]

That has something to commend it.

[Wrenna Robson]

There are various other things - some is an order embedding, I guess some results about Option.get, that sort of thing - that really are very Option-flavoured and might need other order imports.

[Wrenna Robson]

Data/Option/Order.lean would seem reasonable

[Wrenna Robson]

Incidentally we should probably remove Option.rel from Mathlib.

[Wrenna Robson]

Give it is identical to Option.Rel in Standard

[Kim Morrison]

I'm skeptical about this being the "default". It would not have occurred to me as being better than the WithBot interpretation, which for me is the obviously correct one. :-)

[Kim Morrison]

(Just like false < true for everyone, right!? :-)

[Wrenna Robson]

Yeah, I think that's a valid way to feel. I also think it's legitimate to simply not have an ordering on Option itself. Do you have a good name for, uh, the incomparable space, I don't know what to call it?

[Kim Morrison]

IncomparableNoneOption? :-)

[Wrenna Robson]

That feels a little long to me.

[Yaël Dillies]

I think the incomparable order is a decent default.

[Wrenna Robson]

Fundamentally I was in a context where None just had no meaning, a partial function sort of thing, and in that context I don't want theorems to be accidentally true without caveating for good inputs. To me, that's the appropriate place to use the incomparable one - and it's the closest to the semantic meaning of Option in my head.

[Wrenna Robson]

Option = "I've added an element, and literally it represents nothing except that it exists and is distinct to all things that correspond to a value, and I want to have a partial order on this if I can and to do that I guess it needs to have minimal relations"

[Wrenna Robson]

"WithBot = all of that but it's less than everything"

[Wrenna Robson]

So that's I think why it's the default for me - it's a kind of "minimal property", the closure in a sense.

[Kim Morrison]

I asked ChatGPT for whimsical options for a name for an incomparable type synonym. Most were not that great, but I did like WildCard α.

[Wrenna Robson]

That's fun.

[Wrenna Robson]

It also somewhat represents having a default or error value, so WithDefault is not bad.

[Wrenna Robson]

Better yet it fits the naming convention.

[Wrenna Robson]

It would be ideal if the API for this was as straightforward to use as possible. Once you create a synonym that does create a debt of lots of fiddly little bits you want to do.

[Wrenna Robson]

I also suspect there's a bunch of places we currently use Option where semantically WithDefault is more appropriate.

[Yaël Dillies]

I really don't think there's any point bothering with a type synonym here.

[Wrenna Robson]

I mean that would be my wish! But clearly there's differing views.

[Mario Carneiro]

I'm concerned about the programming use case though, I don't think we want to make people use a type synonym to be able to put options in map keys

[Wrenna Robson]

What's the requirement for that?

[Wrenna Robson]

It needs to be ordered?

[Mario Carneiro]

Option T should have a total order if T does

[Wrenna Robson]

Right. I mean that wasn't the case already so we're going to need to add something. (Indeed the problem was that Option T actually didn't have anything really.)

[Wrenna Robson]

If Option T has to have a total order if T does, I don't really see how you can avoid having it be one of WithBot or WithTop. In which case, why have them?

[Wrenna Robson]

Personally I think it should be the case that it has a partial order (or at the very least a preorder) if T does. It's entirely clear that for the most part of it that is just T wearing a hat you know what the order should be. There's just this other element you need to stick on.

[Eric Wieser]

Mario Carneiro said:

I'm concerned about the programming use case though, I don't think we want to make people use a type synonym to be able to put options in map keys

Would a solution be to have maps use [Trunc (LinearOrder X)] as a typeclass instead of LinearOrder X?

[Wrenna Robson]

@Mario Carneiro arrrrguably if I want to create a map with Option as its keys, that should be better thought of as an Option (map). Like in the sense that I'm uncomfortable with the idea that you could create a map such that putting None in gave data out.

[Eric Wieser]

There are cases where there is obviously an order, but while the exact choice of order isn't clear, it's not actually relevant to the implementation

[Mario Carneiro]

Eric Wieser said:

Mario Carneiro said:

I'm concerned about the programming use case though, I don't think we want to make people use a type synonym to be able to put options in map keys

Would a solution be to have maps use [Trunc (LinearOrder X)] as a typeclass instead of LinearOrder X?

No.

[Wrenna Robson]

Like kinda what Option wants is to be able to use it as monadically as possible, where essentially I chunter along using it but if at any point a None appears everything after it is None too.

[Eric Wieser]

(this also feels a bit like the Repr (Multiset X) problem, where on X = Prod A B we want to print in a lexicographic order, even though it's not as canonical as the standard order)

[Mario Carneiro]

Wrenna Robson said:

Mario Carneiro arrrrguably if I want to create a map with Option as its keys, that should be better thought of as an Option (map). Like in the sense that I'm uncomfortable with the idea that you could create a map such that putting None in gave data out.

That's not what a map with option keys is though, a HashMap (Option K) V is isomorphic to Option V x HashMap K V

[Eric Wieser]

What's the story for HashMap (Prod X Y) Z right now? Do you have to use HashMap (Lex (Prod X Y)) Z?

[Mario Carneiro]

Quotients make printing and lots of other things difficult. Consider the Repr Real instance which cannot be made safe

[Mario Carneiro]

No hashmaps of products work fine

[Wrenna Robson]

Mario Carneiro said:

Wrenna Robson said:

Mario Carneiro arrrrguably if I want to create a map with Option as its keys, that should be better thought of as an Option (map). Like in the sense that I'm uncomfortable with the idea that you could create a map such that putting None in gave data out.

That's not what a map with option keys is though, a HashMap (Option K) V is isomorphic to Option V x HashMap K V

Hang on, why isn't it V x HashMap K V?

[Eric Wieser]

Because the none key could be absent

[Wrenna Robson]

For that matter why is it prod and not sum - ah!

[Wrenna Robson]

Right yes of course

[Eric Wieser]

Mario Carneiro said:

I'm concerned about the programming use case though, I don't think we want to make people use a type synonym to be able to put options in map keys

I think I'm missing something; where is the order requirement coming from for map keys? docs#Std.HashMap doesn't have one

[Wrenna Robson]

Was trying to work out where that extra state came from. Still think it seems more like a sum though.

[Mario Carneiro]

For hashmaps actually everything is fine, these types already have derived hash and eq impls

[Mario Carneiro]

it's order-based maps that require ord impls

[Mario Carneiro]

like RBMap

[Eric Wieser]

Maybe we should have a HasLexicographicOrder X Y typeclass which provides a map from a type X to an outparam linearly-ordered type Y?

[Eric Wieser]

Though maybe LinearOrder (Lex X) is sufficient for that and we should just put the with_bot order on Lex Option

[Mario Carneiro]

that would also be bad in the programming use case, it adds an additional computationally relevant operation on the hot path

[Eric Wieser]

Is an identity function computationally relevant?

[Mario Carneiro]

only if it's the identity function

[Eric Wieser]

Or is the point that the compiler can't see its an identity function?

[Mario Carneiro]

it may not be the identity

[Mario Carneiro]

and in the derived impls it won't be

[Mario Carneiro]

even if it is Prod.map id id I don't think the compiler will know it is the identity, but I expect some of these to also be genuinely non-identity maps

[Wrenna Robson]

And all these problems are solved if none < some k?

[Mario Carneiro]

yes, at least for option

[Eric Wieser]

In the cases where it's a non-identity map, aren't we just choosing between baking that map into the comparator vs storing it separately?

[Mario Carneiro]

I think a better approach would be HasWeirdOrd X which has derived total ordering impls

[Eric Wieser]

The latter is arguably more efficient because you can avoid recomputing the embedding in the linear order when doing multiple comparisons

[Wrenna Robson]

Mario Carneiro said:

I think a better approach would be HasWeirdOrd X which has derived total ordering impls

What's the weird ord here?

[Mario Carneiro]

none < some k in this case

[Wrenna Robson]

Right

[Mario Carneiro]

it might not even be a LT implementation, I think RBMap uses compare

[Eric Wieser]

Maybe the answer here is docs#compare gets to have the weird order

[Wrenna Robson]

compare is interesting. Does it need total ordering?

[Eric Wieser]

Since it can't agree with le / lt anyway unless the order is linear

[Mario Carneiro]

if we do that though then a lot of LawfulOrd instances go out the window

[Mario Carneiro]

(and it might also be confusing)

[Eric Wieser]

Do they? docs#LawfulOrd is never true on a non-linear order ,is it?

[Mario Carneiro]

right, but if we put a linear order whenever there is a cmp then of course it will be lawful

[Wrenna Robson]

Yeah, one of the odd things here is that baked into the very definition of Ordering is an assumption of totality

[Wrenna Robson]

One could imagine a type that had INC along with LT, EQ, and GT.

[Mario Carneiro]

you would not have a LawfulOrd instance unless you have a cmp anyway

[Wrenna Robson]

... Option (Ordering), if you will

[Eric Wieser]

Mario Carneiro said:

if we do that though then a lot of LawfulOrd instances go out the window

I don't think this typeclass even exists?

[Mario Carneiro]

no it doesn't, our metatheory around this area is in shambles in part because of the issues being discussed here

[Eric Wieser]

LinearOrder is a candidate for it, which has the compatibility requirements

[Wrenna Robson]

Incidentally Option Ordering is a great example, perhaps the prototypical example, of somewhere where the incomparable ordering is appropriate.

[Mario Carneiro]

I think the main relevant issue is lean4#1777

[Eric Wieser]

This solution looks like it works to me:

• On linearly ordered types, Lt, Le, cmp all agree (and we have a lawful instance that declares this)
• On partially-ordered types, cmp is the "most canonical" lexicographic linear order, which is independent of < and <=

[Eric Wieser]

Sure, it's a bit confusing that cmp can disagree with le/lt, but that seems like precisely the design requirement to put things with a partial order in an rbmap

[Mario Carneiro]

might be nice to have at least some partial agreement like x <= y -> (cmp x y).isLE

[Eric Wieser]

I think that one is fairly easy to keep

[Eric Wieser]

Mario Carneiro said:

I think the main relevant issue is lean4#1777

I don't know if I agree with this feature request; this feels like a problem for downstream code (std/mathlib) to deal with, not a core issue

[Wrenna Robson]

Would this mean that Option was free to have the incomparable ordering without breaking things?

[Mario Carneiro]

well it's in core in part because Ord is in core

[Mario Carneiro]

I think we could just remove it?

[Mario Carneiro]

and relocate it to std

[Eric Wieser]

Well, OfNat is in core and so is HAdd, but that doesn't mean we need core to enforce 0 + x = x

[Wrenna Robson]

Presumably the rationale for things being in core is "this really is necessary to even have a programming language at all".

[Mario Carneiro]

well some of those things are in std too

[Wrenna Robson]

I'm not entirely sure I understand the user who would not use std4 but.

[Eric Wieser]

So why do we need it to enforce lawfulness of Ord and LT? To me, keeping Ord as the raw notation class seems sensible, and Std should be building lawfulness on top of the notation classes

[Mario Carneiro]

not lawfulness, it just provides both operations

[Eric Wieser]

Wrenna Robson said:

Presumably the rationale for things being in core is "this really is necessary to even have a programming language at all".

My interpretation of this is "this is really necessary to _write_ the programming language itself"

[Mario Carneiro]

that way you have a one stop shop for assuming you have an ordered type

[Mario Carneiro]

mathlib understands the value of this very well but in lean4 programming mode we have 3 to 6 different ways to assume ordering on a type used in various combinations

[Wrenna Robson]

Ghastly.

[Eric Wieser]

Mario Carneiro said:

mathlib understands the value of this very well but in lean4 programming mode we have 3 to 6 different ways to assume ordering on a type used in various combinations

Does mathlib have any typeclasses that provide a bundle of data with no lawfulness?

[Mario Carneiro]

from what I can tell Ord is used exactly 0 times in lean core for reasons other than deriving Ord instances

[Mario Carneiro]

No, but that's not the point. In math mode of course you want lawfulness, in programming mode the lawfulness is in our hearts

[Mario Carneiro]

the point is that in mathlib you write LinearOrder and get < and <= and compare and min and max, etc, rather than having that as 5 different typeclass arguments

[Wrenna Robson]

"the lawfulness is in our hearts" is very funny to me

[Wrenna Robson]

It do be like that

[Eric Wieser]

Ah, so the compromise you're proposing is that the lawfulness in our hearts become the weaker x <= y -> (cmp x y).isLE and x = y -> (cmp x y).isEQ, and then the operators can always coexist?

[Eric Wieser]

(that is, lawfulness means that cmp always describes an order at least as strong as </<=)

[Mario Carneiro]

yeah, there would be two LawfulOrd like typeclasses in this case

[Mario Carneiro]

but Ord itself would just give you the whole bundle

[Eric Wieser]

... and a warning that it is likely to not be quite as lawful as you might expect

[Mario Carneiro]

and it would be used for both linear and partial order cases

[Eric Wieser]

I think we still want a separate typeclass for compare alone, to let you define things one piece at a time

[Mario Carneiro]

Usually when defining things one piece at a time it suffices to just have a standalone Foo.compare function and use that as part of the construction

[Mario Carneiro]

it's often a good idea to do that anyway even if the typeclass just wraps it

[Eric Wieser]

The main downside in that approach is that if you state any lemmas about it, you have to state them again when you assemble the typeclass

[Wrenna Robson]

As I alluded to above, you could have a cmp? which mapped into Option Ordering.

[Wrenna Robson]

Like in a sense that might be what a partial order needs.

[Wrenna Robson]

Incidentally have submitted #9178 which is another small and easy PR around this issue.

[Wrenna Robson]

Is there a way to make a mathlib commit depend on a std4 commit?

[Eric Wieser]

Yes, you update the lake manifest to point at your std branch

[Mario Carneiro]

we should have a tag to track PRs which do that so that we don't accidentally merge them

[Eric Wieser]

Could we just have CI fail on anything other than master in the lakefile?

[Mario Carneiro]

no, because we want these PRs to pass CI to justify merging the things they depend on

[Mario Carneiro]

We could have CI fail for the master/staging branch only, that would make bors reject it

[Wrenna Robson]

@Eric Wieser I wonder if there's a way to make a class that contains WithBot, WithTop, and whatever it is we call the thing with the incomparable whatsit, which might just be Option.

[Wrenna Robson]

It occurs that there's lemmas that are always true for all of them - e.g.

lemma some_le_some_iff {a b : α} : some a ≤ some b ↔ a ≤ b :=
  ⟨le_of_some_le_some, some_le_some_of_le⟩

Where the proof is essentially the same for all of them.

[Wrenna Robson]

Wheras there are things that are only true in one of them.

[Wrenna Robson]

This to me feels like the kind of thing that a class is meant to handle.

[Yaël Dillies]

More like "some is an OrderEmbedding"

[Eric Wieser]

Note that each of WithBot, WithTop, and Option have a different some anyway, so what Yael describes is exactly the bit that is actually generalizable

[Wrenna Robson]

Sure.

[Wrenna Robson]

But the point is, there's a common structure there.

[Wrenna Robson]

Incidentally, why does OrderEmbedding.subtype require Preorder

[Yaël Dillies]

because we don't really care about things weaker than preorders

[Wrenna Robson]

Ye-es.

[Wrenna Robson]

But it could just require LE, right? It's just a notational truth.

[Yaël Dillies]

In that case, yes

[Wrenna Robson]

Essentially, I can say this:

def optionIsSomeOrderIso (α : Type*) [LE α] : { x : Option α // x.isSome } ≃o α where
  toFun o := Option.get _ o.2
  invFun x := ⟨some x, rfl⟩
  left_inv _ := Subtype.eq <| Option.some_get _
  right_inv _ := Option.get_some _ _
  map_rel_iff' := get_le_get_iff_le _ _

Obviously I can do something similar with the embedding of some. But in a sense it would be good to derive the latter from the former. Unfortunately for that...

def someOrderEmbedding (α : Type*) [Preorder α] : OrderEmbedding α (Option α) :=
RelEmbedding.trans (optionIsSomeOrderIso α).symm.toOrderEmbedding (OrderEmbedding.subtype _)

[Wrenna Robson]

You need Preorder.

[Wrenna Robson]

If you look at WithBot.some_le_some, the WithBot version of what I cited above, it just needs LE. So clearly you would want to do the same thing here.

[Eric Wieser]

This is in general a problem; if you make your morphisms assume any lawful structure, then you find that you can't use the morphisms to pull back / push forward structure

[Wrenna Robson]

Aye. Because this is the bit where their structure is in agreement I had hoped this wouldn't be an issue

[Wrenna Robson]

And you know, things like MulEquivClass seem magic to me

[Eric Wieser]

(but if your morphisms don't assume any structure, then often you end up needing way more fields; group morphisms and monoid morphisms are the same, but one/mul/inv morphisms and one/mul morphisms are different)

[Wrenna Robson]

Partially I just think it's things having differing levels of generality across the library - in this case, Monotone is only defined on Preorders, even though it makes sense as a sentence (even if it has less meaning) for LE.

[Wrenna Robson]

But you could change it.

[Wrenna Robson]

Personally I think definitions should always be made with minimal assumptions.

[Eric Wieser]

So should we have separate MonoidHom and GroupHom in order to permit that? That creates massive amounts of extra boilerplate...

[Wrenna Robson]

I'm not sure I understand what that has to do with Monotone...

[Wrenna Robson]

Always here should be understood to mean "not always, but often".

[Wrenna Robson]

I am not sure you would need GroupHom? That's actually an example of the kind of generality I think is good.

[Eric Wieser]

Always here should be understood to mean "not always, but often".

I don't think defining X in terms of not X is particularly transparent...

[Wrenna Robson]

?

[Wrenna Robson]

Oh I see - I mean I'm just being colloquial I guess.

[Wrenna Robson]

As a rule of thumb, one should always bend towards minimal assumptions for things, but sometimes that isn't necessary.

[Wrenna Robson]

In this case I was asking "can we have less boilerplate here somehow".

[Yaël Dillies]

And I would think this is pretty minimal in terms of boilerplate already.

[Wrenna Robson]

Also pointing out that it is mildly absurd that the assumptions for defining an OrderEmbedding are in fact less than that needed to define an OrderHom.

[Yaël Dillies]

Agreed. I'm happy to merge a PR to change it to Preorder!

[Wrenna Robson]

Ha!

[Wrenna Robson]

But presumably not to go in the other direction?

[Yaël Dillies]

No, I wouldn't really see the point

[Wrenna Robson]

Hmm.

[Wrenna Robson]

I think in my view they're equally pointless - so I don't really understand why you'd be happy to do one but not the other.

[Wrenna Robson]

(I am perfectly content for pointless things to happen.)

[Wrenna Robson]

And, indeed, if I look at, say, the structure of WithBot.lean, I can see a clear distinction between LE and LT assumptions and Preorder ones.

[Wrenna Robson]

I have PR'd #9181, just to get something in there. But the core issue of what the solution should be is not resolved.

[Wrenna Robson]

I have also summarised the above discussion - @Mario Carneiro I haven't gone into all the detail you gave but I've tried to represent your position fairly. Of course, if you feel there are important points to add, please do do so.

[Wrenna Robson]

@Joe Hendrix if you're interested in the context of that PR to std, it's here.

[Wrenna Robson]

#9181 tries to summarise the situation. Unfortunately there are a few moving parts.

[Wrenna Robson]

If we end up removing Rel and not putting StrictRel into standard, I suspect I will add them to #9181!

[Wrenna Robson]

Amused that we are solving all the issues with this being spread across three places by just adding everything into Mathlib.

[Mario Carneiro]

I feel like that has historically been the solution to quite a lot of problems

[Wrenna Robson]

And the cause!

[Wrenna Robson]

It's interesting because presumably these were deliberately added to std4? But I agree they taste more mathsy.

[Mario Carneiro]

they were part of the initial mathlib import of these basic files

[Wrenna Robson]

Right.

[Wrenna Robson]

Well, Rel and StrictRel would fit well into Data/Option/Order when it exists though we still haven't entirely resolved this issue of what should actually happen to Option by default.

[Mario Carneiro]

they may not be defined like that though

[Mario Carneiro]

best wait until we have the rest of it together

[Patrick Massot]

Wrenna Robson said:

Amused that we are solving all the issues with this being spread across three places by just adding everything into Mathlib.

This strategy served us extremely well in the past. Now we are trying to move away from this. There are good reasons to do that, but the cost is huge.

[Eric Wieser]

Mario Carneiro said:

best wait until we have the rest of it together

Is there any reason not to have (in mathlib) Rel, StrictRel, and the lemmas saying that if R is transitive then so is Rel R etc? I think the contention in this thread is about canonical orders, not arbitrary relations

[Mario Carneiro]

I think those are fine theorems to have in mathlib

[Mario Carneiro]

without a use case in std they are just dead weight

[Eric Wieser]

Ah, so you mean "wait until the rest is together before upstreaming anything to std"?

[Mario Carneiro]

we should have a coherent strategy for how all these theorems are to be used together to improve the general usability of lean qua programming language

[Wrenna Robson]

Indeed.

[Eric Wieser]

But this isn't a prerequisite for (partial?) inclusion in mathlib

[Eric Wieser]

(maybe it is a prerequisite for the global instance being proposed)

[Mario Carneiro]

indeed not, the mathlib bar is a bit closer to "it's true and potentially useful"

[Wrenna Robson]

As I say, this all started because I had some function I'd defined to Option (Fin n), because having it defined to Fin n with junk values was giving me a need to have NeZero n everywhere. Semantically, Option is correct. But then I wanted certain ordering theorems to be true - essentially think "this is a partial function, but when it has values, these nice inequalities are true".

[Wrenna Robson]

This was in the context of my real actual work I've been doing (well - actually it was in a refactor to SuccAbove I was looking at that had come from that - the point is it was me actually using Lean for a real purpose - at the end of the day, trying to verify this particular subroutine in some cryptography - so I am here wearing the hat, partially, of Real Actual User).

[Mario Carneiro]

right, that sounds like sufficient grounds to get it in mathlib

[Eric Wieser]

I think you should split #9181 into the bit that doesn't conflict with the core instance, and the bit that does

[Wrenna Robson]

Indeed. And I'd quite like this default order to be on Option, because for the interpretation of Option as "partial function codomain", if you see what I mean, you kinda really don't want none to accidentally mean anything.

[Wrenna Robson]

Ah, so just the LE instance, and then the LT part and beyond?

[Mario Carneiro]

I think by std standards this mainly motivates not having a LE or LT instance on Option at all

[Wrenna Robson]

That's reasonable. As I say I do think having the core instance is not unreasonable - it is just unfortunate that a) it has zero API, b) we re-implement that as WithBot.

[Mario Carneiro]

let downstream users decide what they want to do with it

[Wrenna Robson]

Yes, I think that would be the correct choice for std.

[Eric Wieser]

As a reminder Mario, the problem is that core has already decided for us

[Mario Carneiro]

that one seems to be on its way out, I don't think anyone has objected to that

[Wrenna Robson]

From a mathlib point of view you know my view.

[Wrenna Robson]

But I'm in total agreement also that this is a better choice for maths than for programmers.

[Mario Carneiro]

it was added in very early lean 4, if it's not used by now then I doubt anyone will defend it

[Eric Wieser]

Mario Carneiro said:

that one seems to be on its way out, I don't think anyone has objected to that

I think the context for lean4#3100 has grown so large there's a serious chance of the core PR being ignored because the benefit is not worth reading this zulip thread to work out what the consensus is

[Wrenna Robson]

2018 I think?

[Joe Hendrix]

@Wrenna Robson Thanks for mentioning this thread. If your code is publicly is available, I'd be interested in taking a look to get more context.

[Wrenna Robson]

It is. #9181 contains a summary of the relevant PRs and the discussion so you don't have to read scrollback.

[Wrenna Robson]

I was trying to obey the contribution guidelines of "don't expect everyone to have to read Zulip" <_<

[Joe Hendrix]

@Wrenna Robson Oh, I meant the crypto code.

[Wrenna Robson]

Oh!

[Wrenna Robson]

Well, that's a whole other thing. Technically my project is not cryptography per se - I've been working on a verification of Classic McEliece's representation of permutations as bitvectors, extending prior work by DJB. In particular this necessitated some annoying to prove theorems about succAbove and predAbove (... which I think might actually be the simplicial identities...) and that prompted an attempt at a refactor of that.

[Joe Hendrix]

Perhaps BitVec n (or some other type than Option (Fin n) would be useful). I think the downside of a type of like Option is that none can mean virtually anything.

[Wrenna Robson]

It's the XKCD sharks comic.

[Wrenna Robson]

In this case, Option (Fin n) is being used in the sense of, I have a map from pairs of Fin (n + 1) to Fin n, but it only really applies to distinct pairs.

[Wrenna Robson]

It's actually precisely the existing docs#finSuccEquiv'

[Wrenna Robson]

Which you'll note maps to Option.

[Wrenna Robson]

I agree that none can mean virtually anything, but the interpretation of Option I favour, the one we all learn metaphorically on our grandmother's knee, right, is "computations that might fail".

[Wrenna Robson]

BUT - other choices are available, I get that.

[Joe Hendrix]

Thanks for the context. It's being used as something like a set with at most one element.

[Wrenna Robson]

Yes - bit like how List can mean "computations which can have a variable number of outputs".

[Joe Hendrix]

I think keeping the definitions and theorems in Mathlib makes sense to me, but the context is helpful.

[Wrenna Robson]

Indeed. The debate has been about whether or not there should be any kind of order on Option at all and if so what it should be.

[Wrenna Robson]

@Eric Wieser I'm not sure about splitting that PR until we've obtained some consensus about the holistic plan.

[Wrenna Robson]

Unfortunately I don't really know how to rework my core issue or PR so that the maintainers will spend any time on it. I would hope it would be an easy choice for them.

[Wrenna Robson]

But that requires them to actually look at it.