Max instance for order

Stream: Is there code for X?

[Bolton Bailey]

Do we have this?

import Mathlib

instance [Preorder a] : Max (a) := by sorry

[Timo Carlin-Burns]

What would the semantics be? What if I write max x y and x and y are incomparable? (e.g. x y : Set Nat, x := {3}, and y := {5})

[Bolton Bailey]

Well we have this function in the library

variable [Preorder α] [@DecidableRel α (· < ·)] {l : List α} {a m : α}

/-- `maximum l` returns a `WithBot α`, the largest element of `l` for nonempty lists, and `⊥` for
`[]`  -/
def maximum (l : List α) : WithBot α :=
  argmax id l

so I guess the same semantics as that, which I imagine is if a < b then b else a

[Bolton Bailey]

Seems like if we can define a function called maximum, we should be able to define Max

[Bolton Bailey]

Hmm, if I am reading you right, are you saying that this maximum function returns a singleton on [{3},{5}]? That's pretty nonintuitive.

[Bolton Bailey]

Yep, here it is

import Mathlib

open Classical

example : List.maximum (α := Multiset ℕ) [{3}, {5}] = some {3} := by
  unfold List.maximum List.argmax List.argAux
  simp

[Bolton Bailey]

Frankly I am not a fan of Maximum returning a type not the same as the type of the list, I would prefer it require Bot and Max typeclass arguments and return the same type.

[Timo Carlin-Burns]

From a programming point of view, I think it's reasonable to be expected to handle the empty case separately. e.g. a signed 32-bit integer technically has a bottom element in -2,147,483,648, but if I'm taking the minimum of a list of them I probably want to error if it's empty, not produce that bottom element. If we want to draw off of other languages, Rust's Iterator::max returns Option which is the moral equivalent of WithBot here.

[Timo Carlin-Burns]

And it does seem like these functions should mostly be considered from a programming point of view. I think you would always prefer a function with infimum/supremum semantics for mathematics.

[Bolton Bailey]

Well I take your point, but it is mathlib, and I think we are generally oriented toward the more mathy way of doing things. If this were to be moved to Std or Core I would certainly agree it should return an option.

[Bolton Bailey]

Related is that I found this through Polynomial.degree_list_sum_le which looks like it would be cleaner if there was degree on both sides, which seems like it would be easier if there was a maximum function that preserved the type.

[Bolton Bailey]

I am not sure if there is a type common in programming where the above clear strangeness pops up. A bitmask type perhaps?

[Yaël Dillies]

Bolton Bailey said:

Hmm, if I am reading you right, are you saying that this maximum function returns a singleton on [{3},{5}]? That's pretty nonintuitive.

The use case comes from @Mantas Baksys. The point is that docs#List.maximum returns a maximum element for nonempty lists. So unless the list is a chain it doesn't return something that's greater than anything in the list.

[Yaël Dillies]

Bolton Bailey said:

Related is that I found this through Polynomial.degree_list_sum_le which looks like it would be cleaner if there was degree on both sides, which seems like it would be easier if there was a maximum function that preserved the type.

Aren't you looking for docs#Tropical by any chance?

[Timo Carlin-Burns]

Bolton Bailey said:

I am not sure if there is a type common in programming where the above clear strangeness pops up. A bitmask type perhaps?

So the question here is whether there is a type in programming for which comparison is common that is not a linear order? Floating point types are a classic example because NaN is incomparable to every element, including itself. So e.g.

import Mathlib

def Float.nan : Float := 0.0 / 0.0

instance : Preorder Float where
  le_refl := sorry
  le_trans := sorry
  lt_iff_le_not_le := sorry

#eval List.maximum [0.0, Float.nan] -- ↑0.000000
#eval List.maximum [Float.nan, 0.0] -- ↑NaN

[Timo Carlin-Burns]

Bolton Bailey said:

Related is that I found this through Polynomial.degree_list_sum_le which looks like it would be cleaner if there was degree on both sides, which seems like it would be easier if there was a maximum function that preserved the type.

I think this should be restated in terms of a List.supremum like so

def List.supremum {α : Type*} [SemilatticeSup α] [OrderBot α] : List α → α :=
  List.foldr (· ⊔ ·) ⊥

theorem Polynomial.degree_list_sum_le' {S : Type u_1} [Semiring S] (l : List (Polynomial S)) :
  Polynomial.degree (List.sum l) ≤ List.supremum (List.map Polynomial.degree l) := sorry

[Timo Carlin-Burns]

Hmm I see. If List.maximum was stated in terms of Max and Bot, then all we would need is an instance from SemilatticeSup to Max and it would just be a generalization of my List.supremum

[Bolton Bailey]

Yaël Dillies said:

Bolton Bailey said:

Related is that I found this through Polynomial.degree_list_sum_le which looks like it would be cleaner if there was degree on both sides, which seems like it would be easier if there was a maximum function that preserved the type.

Aren't you looking for docs#Tropical by any chance?

Yes I am finally trying to add the structure from this thread and adding an equivalence to lists.

[Bolton Bailey]

Timo Carlin-Burns said:

Bolton Bailey said:

Related is that I found this through Polynomial.degree_list_sum_le which looks like it would be cleaner if there was degree on both sides, which seems like it would be easier if there was a maximum function that preserved the type.

I think this should be restated in terms of a List.supremum like so

def List.supremum {α : Type*} [SemilatticeSup α] [OrderBot α] : List α → α :=
  List.foldr (· ⊔ ·) ⊥

theorem Polynomial.degree_list_sum_le' {S : Type u_1} [Semiring S] (l : List (Polynomial S)) :
  Polynomial.degree (List.sum l) ≤ List.supremum (List.map Polynomial.degree l) := sorry

Supremum seems like a good name. Is there any precedent for this in Finset? - it would be best to keep the names consistent if possible.

[Yaël Dillies]

docs#Finset.sup