min/max definitions non-alignment

Stream: mathlib4

[Yakov Pechersky]

In mathlib3:

lemma min_def (a b : α) : min a b = if a ≤ b then a else b :=
lemma max_def (a b : α) : max a b = if b ≤ a then a else b :=

in mathlib4:

lemma min_def (a b : α) : min a b = if a ≤ b then a else b :=
lemma max_def (a b : α) : max a b = if a ≤ b then b else a :=

@Mario Carneiro you ported the mathlib4 lines. I am running into this clash in trying to (ab)use OrderDual defeq for LinearOrder (OrderDual _). Do we want to prefer the mathlib3 style of swapping the inequality, or the current mathlib4 style of swapping the then-else branches?

[Mario Carneiro]

Those definitions ultimately derive from the lean 4 implementation of max and min, which uses that order deliberately so that (min a b, max a b) can get optimized using common subexpression elimination to only involve one comparison

[Mario Carneiro]

That said, the max/min support in LinearOrder was hacked together without too much thought so it's totally fine if you have a better approach as long as it still allows for custom max/min implementations

[Yakov Pechersky]

OK -- do we want to then align max_def to have a non LinearOrder.max_def .. proof?

[Yakov Pechersky]

basically, naked max_def and LinearOrder.max_def aren't syntactically equal

[Yakov Pechersky]

or, we can change it in both places, and have a smarter autoParam proof?

[Mario Carneiro]

What does mathlib do? We should probably do that

[Mario Carneiro]

seems like we probably want to align max to match lattice join

[Mario Carneiro]

I see, mathlib is using a separate linear_order from lattices because it is mostly in core

[Yakov Pechersky]

In the meantime, here's what the LinearOrder (OrderDual _) proof looks like:

instance (α : Type _) [LinearOrder α] : LinearOrder αᵒᵈ where
  __ := inferInstanceAs (PartialOrder αᵒᵈ)
  le_total := fun a b : α => le_total b a
  decidable_le := inferInstanceAs (DecidableRel fun a b : α => b ≤ a)
  decidable_lt := inferInstanceAs (DecidableRel fun a b : α => b < a)
  min := @max α _
  max := @min α _
  min_def := fun a b => by
    let a' : α := a
    let b' : α := b
    show (@Max.mk α _).max a' b' = if b' ≤ a' then a' else b'
    rw [max_def]
    split_ifs with hab hba
    · exact le_antisymm hba hab
    · simp [*]
    · simp [*]
    · simp only [not_le] at *
      exact absurd (hab.trans ‹_›) (lt_irrefl _)
  max_def := fun a b => by
    let a' : α := a
    let b' : α := b
    show (@Min.mk α _).min a' b' = if b' ≤ a' then b' else a'
    rw [min_def]
    split_ifs with hab hba
    · exact le_antisymm hab hba
    · simp [*]
    · simp [*]
    · simp only [not_le] at *
      exact absurd (hab.trans ‹_›) (lt_irrefl _)

[Mario Carneiro]

those proofs seem unnecessarily long. It should just be an application of max_comm to convert between the two possible interpretations

[Mario Carneiro]

also, isn't there already a proof of this?

[Yakov Pechersky]

so something like:

  min_def := fun a b => by
    let a' : α := a
    let b' : α := b
    show (@Max.mk α _).max a' b' = if b' ≤ a' then a' else b'
    rw [max_comm, max_def]

?

[Mario Carneiro]

https://github.com/leanprover-community/mathlib4/blob/d78a3d45bf33119f21ca18cfd2f822b747cc9a98/Mathlib/Order/Basic.lean#L420-L429

[Yakov Pechersky]

ah, I overwrote it =C. Thanks.

[Yaël Dillies]

seems like we probably want to align max to match lattice join

In fact I have a branch to core that does exactly this, but I guess rather open it to std4 now

[Yaël Dillies]

Oh wait, is LinearOrder in mathlib now?

[Scott Morrison]

It is, but only as an ad-hoc port.

[Mario Carneiro]

The whole order hierarchy is part of mathlib4 now, so these kinds of refactors are presumbably easier (except that we still care about mathlib alignment so we would rather backport something like this if possible)

[Yaël Dillies]

Oh I like that!

[Yury G. Kudryashov]

Should we rename LinearOrder.min to LinearOrder.inf?

[Yury G. Kudryashov]

So that we don't need to rename fields in extends

[Yury G. Kudryashov]

And so that we don't accidentally forget to rename them

[Yaël Dillies]

As I previously said, I don't think we ever need min and max at all.

[Yaël Dillies]

It's quite practical for pedagogical purposes and lemma naming, but those have other solutions than "duplicate a few hundred lemmas for a special case".

[Yaël Dillies]

So I'm happy for you to do whatever you want with those, as I'm hoping I will one day crush their parasitic existence.

[Yury G. Kudryashov]

I'm fine with removing them completely in favor of sup/inf but this (a) needs approval from other maintainers; (b) should not be done before the port is done.

[Jireh Loreaux]

@Yaël Dillies what exactly are those "other solutions" you are contemplating?

[Yaël Dillies]

Here are the solutions I'm aware of, from most radical to least radical:

1. Drop min/max entirely and rename all lemmas.
2. Drop min/max as definitions but keep as a naming convention that inf/sup on a linear order is called min/max.
3. Turn min/max from definitions to input-only notations.
4. Turn min/max from definitions to notations that pretty-print only in the presence of a linear_order instance.
5. Keep the status quo.

2 is my favourite, I would also be happy with 1 and 3, but 4 is IMO past the reasonable in that it tries to be very backwards compatible with an arbitrary core Lean 3 convention.

[Yaël Dillies]

Note that there are ramifications for the corresponding finset declarations, which are also partially duplicated (three way in the case of docs#finset.sup !). For those, I would go for 1 because their limited use doesn't justify an exception to the naming convention.

[Jireh Loreaux]

Yeah, 2 is nice IMO.

[Eric Wieser]

2 seems a bit confusing (compared to 1), because to guess the name of a lemma you have to work out whether your result holds only in linear orders or not

[Yaël Dillies]

That's usually pretty obvious, eg docs#min_le_iff

[Yaël Dillies]

I should point out that 2 is already the solution used in Sup vs cSup. tsub vs sub is quite similar, except that lemmas are purposefully duplicated from the tsub name to the sub precisely to avoid what Eric is complaining about (and because there it's actually quite hard to figure out the correct generality of a lemma).

[Yaël Dillies]

The easiest path to any of those solutions is probably 5 -> 3 -> 4 and 5 -> 3 -> 2 -> 1 (as in, it's no more work to implement those in order rather than implementing the end one directly).

[Eric Wieser]

Things like docs#with_top.coe_infi don't really fit the cInf/Inf rule there

[Yaël Dillies]

They do, in the sense that lemmas that apply to both situations get the simpler name.

[Anne Baanen]

I don't like the "2. inf is called min in theorem names" approach. If we can teach ring theorists the zero ideal is called bot then we can teach them that the minimum is called inf.

[Damiano Testa]

I am a little worried that this change would make Lean much less mathematician-friendly: if I see inf 2 3, my first instinct is "surely you meant min 2 3". I would argue that, just like bot and top, this would add an extra layer of separation between Lean and informal mathematics.

[Reid Barton]

why have a separate definition inf? it's just the product

[Kevin Buzzard]

I have come over to the idea that if mathematicians learn the basic definitions of lattice theory and its notations then they're in a much better position to find theorems in the library in general, so I typically teach this early now