maximum of a list known to be nonempty

Stream: Is there code for X?

[Jared green]

l : List (List a)
l != []
--nat expected
match (List.max? (l.map (fun c => c.dedup.length))) with
    |none => 0
    | some n => n

there should be a way to avoid this 'option' part

[Aaron Liu]

docs#Option.get

[Alfredo Moreira-Rosa]

you can add this to a Utils.lean file :

def List.max {α : Type} [Max α] (l : List α) (h : l ≠ []) : α :=
  match l with
  | [] => False.elim (h rfl)
  | a :: as => as.foldl Max.max a

[Kenny Lau]

I don't think we like partial functions very much (because we would have to carry the proof around all the time)

[Kenny Lau]

def Option.forceGet {α : Type _} [Inhabited α] : Option α → α
  | some x => x
  | none => default

we should have this instead

[Aaron Liu]

docs#Option.get!

[Kenny Lau]

(this is also Option.getD _ default)

[Kenny Lau]

that one panics

[Aaron Liu]

logically does the same thing

[Aaron Liu]

also usually you want to panic

[Aaron Liu]

and if you don't then like you said Option.getD _ default works well

[Yakov Pechersky]

We have docs#List.max? and docs#List.maximum

[Aaron Liu]

uhoh

[Aaron Liu]

that's defeq abuse (in the definition of docs#List.maximum)

[Kenny Lau]

@Yakov Pechersky well they both do the same thing and both bring you to Option which the OP is trying to avoid

[Yakov Pechersky]

No option, hypothesis instead, dealt with by autoparam

def List.max_of_nonempty' {α : Type _} [Max α] : {l : List α} → l ≠ [] → α
| [x], _ => x
| x :: y :: xs, _ => max x (max_of_nonempty' (l := y :: xs) (by simp))

def List.max_of_nonempty {α : Type _} [Max α] (l : List α) (h : l ≠ [] := by decide) : α :=
  max_of_nonempty' h

/-- info: 7 -/
#guard_msgs in
#eval [1, 5, 7].max_of_nonempty

#eval [].max_of_nonempty -- two errors

[Jared green]

why isnt this in mathlib?

[Aaron Liu]

well generally we don't work with lists that much in my experience

[Aaron Liu]

so docs#Finset.sup or docs#Finset.max' instead

[Chris Henson]

Aaron Liu said:

that's defeq abuse (in the definition of docs#List.maximum)

WithBot is a serial offender in this regard, right? I assume this is one of those things the refactor to a structure will handle.

[Kim Morrison]

(If anyone would like to help with that refactor, please contribute to #27918! I would love help here! :-)

[Kenny Lau]

Jared green said:

why isnt this in mathlib?

we don't like partial functions

[Alfredo Moreira-Rosa]

I understand that total functions are nice from a mathematical point of view, but List are more engineering oriented.
And from an engineering point of view, partial functions are totally fine, and can bring way better performance in runtime and memory used.

[Kenny Lau]

@Alfredo Moreira-Rosa but they are asking about mathlib specifically

[Alfredo Moreira-Rosa]

Yes, but maybe, these simple functions could have a place in core or std instead of Mathlib. But yes, it's another subject

[Jared green]

could it be in batteries? any place for it would be fine by me.

[Markus Himmel]

I have this lying around in a abandoned paused personal project:

namespace List

theorem isSome_min?_of_ne_nil [Min α] : {l : List α} → (hl : l ≠ []) → l.min?.isSome
  | x::xs, h => by simp [List.min?_cons']

theorem isSome_max?_of_ne_nil [Max α] : {l : List α} → (hl : l ≠ []) → l.max?.isSome
  | x::xs, h => by simp [List.max?_cons']

protected def min [Min α] : (l : List α) → (hl : l ≠ []) → α
  | a::as, _ => as.foldl min a

theorem min_eq_get_min? [Min α] : (l : List α) → (hl : l ≠ []) →
    l.min hl = l.min?.get (isSome_min?_of_ne_nil hl)
  | a::as, _ => by simp [List.min, List.min?_cons']

protected def max [Max α] : (l : List α) → (hl : l ≠ []) → α
  | a::as, _ => as.foldl max a

theorem max_eq_get_max? [Max α] : (l : List α) → (hl : l ≠ []) →
    l.max hl = l.max?.get (isSome_max?_of_ne_nil hl)
  | a::as, _ => by simp [List.max, List.max?_cons']

theorem min?_eq_some_min [Min α] (l : List α) (hl : l ≠ []) :
    l.min? = some (l.min hl) := by
  simp [min_eq_get_min?]

theorem max?_eq_some_max [Max α] (l : List α) (hl : l ≠ []) :
    l.max? = some (l.max hl) := by
  simp [max_eq_get_max?]

theorem min_le_of_mem [Min α] [LE α] [Std.IsLinearOrder α] [Std.LawfulOrderMin α]
    (l : List α) (a : α) (ha : a ∈ l) :
    l.min (List.ne_nil_of_mem ha) ≤ a :=
  (List.min?_eq_some_iff.1 (List.min?_eq_some_min l (List.ne_nil_of_mem ha))).2 _ ha

theorem le_max_of_mem [Max α] [LE α] [Std.IsLinearOrder α] [Std.LawfulOrderMax α]
    (l : List α) (a : α) (ha : a ∈ l) :
    a ≤ l.max (List.ne_nil_of_mem ha) :=
  (List.max?_eq_some_iff.1 (List.max?_eq_some_max l (List.ne_nil_of_mem ha))).2 _ ha

If someone PRs this to core, adding versions of all the lemmas that exist for min? (there aren't that many), I'll merge the PR :)

[Alfredo Moreira-Rosa]

Thanks markus, i can try. Looks doable for me. I'll have some time this week end.

[Wrenna Robson]

Is List engineering orientated? I must admit I think of it as a structure for theoretical reasoning.

[Alfredo Moreira-Rosa]

I guess everybody has a different perspective on data depending on their field of interrest :)

[Alex Meiburg]

I think the partial function is 'justified' in some sense by the signature for docs#List.head. Because the operation you really want is l.foldl max l.head, which is 'safe' in the sense that foldl has a starting argument, but then you need the head.

[Alfredo Moreira-Rosa]

So i'm trying to do my first contribution to lean core. I followed the docs, build lean 4 using CMake, then make, and opened the project using lean 4 vscode workspace.
But i'm getting this error :
image.png
Any hint from a core team member ?

[Alfredo Moreira-Rosa]

The command that is failing :
image.png

[Markus Himmel]

Did you follow the steps in https://github.com/leanprover/lean4/blob/master/doc/dev/index.md#development-setup ?

[Alfredo Moreira-Rosa]

yes, these ones

[Markus Himmel]

Did you execute the two elan toolchain link commands?

[Alfredo Moreira-Rosa]

oh, good, i missed this one.
Thanks, let me try

[Alfredo Moreira-Rosa]

Nice, it works.

[Alfredo Moreira-Rosa]

PR is here : lean4#11060

I see a pipeline error on changelog label, maybe i missed something ?

[Alfredo Moreira-Rosa]

thanks @Markus Himmel for fixing it.

[Markus Himmel]

You can also comment changelog-library on the PR to have a bot add the label for you.

[Snir Broshi]

If before there was duplication with docs#List.max? and docs#List.maximum, this will cause further duplication with docs#List.maximum_of_length_pos, though it asks for 0 < l.length rather than l ≠ [].
Does this mean docs#List.maximum_of_length_pos will be deprecated?

[Alfredo Moreira-Rosa]

List.max? and List.max is lean core, while List.maximum is Mathlib.

So i think they would serve a different purpose with different properties. WithTop and WithBot really serves a mathematical purpose, List.max don't give such properties, and like i said earlier would serve more in engineering/programming with lean side than mathematical one.

[Snir Broshi]

Maybe but docs#List.maximum_of_length_pos doesn't use WithBot, so what's the advantage of keeping it around?

[Alfredo Moreira-Rosa]

I think it's better distinguish the mathlib discussion from lean core one and let mathlib maintainers decide what they want to do.

[Snir Broshi]

Alfredo Moreira-Rosa said:

I think it's better distinguish the mathlib discussion from lean core one and let mathlib maintainers decide what they want to do.

This thread is about "there should be a way to avoid this 'option' part", including both core and mathlib, to which the answer is docs#List.maximum_of_length_pos.
You're talking about upstreaming this functionality to core, so the mathlib version should be part of the discussion.

I agree that upstreaming this to core is good, so now the question becomes what to do with the old version.

[Alfredo Moreira-Rosa]

I'm not so sure such adherence is necessary.
But indeed if a Mathlib maintainer wants to discuss it here. Do you know who could contribute to the discussion ?