List.argMax

Stream: Is there code for X?

[Eric Wieser]

Do we have something like this, and would it be useful?

import Mathlib

def List.argMax {α β} [PartialOrder β] [@DecidableRel β (· < ·)] (f : α → β) (l : List α) : Option α :=
  match l with
  | [] => none
  | [x] => some x
  | x :: xs =>
    match xs.argMax f with
    | some y => if f y < f x then some x else if f x < f y then some y else none
    | none => none

-- unrelated: this is missing!
instance {α β} [PartialOrder α] [PartialOrder β]
    [@DecidableRel α (· < ·)] [@DecidableRel α (· ≤ ·)]
    [@DecidableRel β (· < ·)] [@DecidableRel β (· ≤ ·)] : @DecidableRel (α × β) (· < ·) :=
  fun x y => decidable_of_iff' _ <| Prod.lt_iff


#eval [(1, 2), (2, 1)].argMax id  -- `none`, as the elements are not comparable
#eval [(1, 2), (2, 3)].argMax id   -- `some (2, 3)`
#eval [(1, 2), (1, 3)].argMax (·.1)  -- `none`, as there is a tie

[Eric Wieser]

I suppose

def List.argMax {α β} [PartialOrder β] [@DecidableRel β (· < ·)] (f : α → β) (l : List α) : List α :=

would be another choice, returning all incomparable or tied maximums

[Yakov Pechersky]

docs#List.argmax

[Yakov Pechersky]

Am I missing some difference?

[Eric Wieser]

The handling of ties I guess; the one that exists doesn't lift to a finset.