Design of `List.min?` / `Array.min?`

Stream: batteries

[Kim Morrison]

Currently in Lean we have List.min? [Min α] : List α → Option α, and in Batteries we have Array.min? [Ord α] : Array α → Option α (which is in turn defined in terms of minD [Ord α] : Array α → α → α and minWith [Ord α] : Array → α → α).

I would like to make these uniform, and would like to solicit input on the design.

1. I could "weaken" List.min? to require an Ord α instance instead: the use cases I know of would survive fine.

2. We could add an instance from Ord to Min, and then switch the existing Array functions to only require Min.

   • This would require some care with the semantics, but I think works out.
   • The Array functions produce the "first minimal element", i.e. if they encounter a comparison of Ordering.eq they prefer the first one.
   • If we make the default Min instance from Ord behave the same way (which would be consistent with all our existing definitions of min) then there will be no change in behaviour.
   • Expanding the doc-string could clarify what happens if you provide a Min instance with different behaviour.

I have a preference for 2. (it generalizes rather than restricts) but I'm happy to have input, particularly if I'm wrong about preserving the semantics or efficiency.

As far as I can see this won't affect Mathlib, hence posting here.

[François G. Dorais]

Although archaic, lean4#1777 is relevant here.

[Kim Morrison]

Yes. We need to punt on big decisions about Ord, and just deal with this question in the context of the status quo.

[Violeta Hernández]

I like 2, but I think we need to consider what Ord is supposed to be accomplishing. Is it a mechanism for defining an ordering on a type, or is it somehow independent from it?

[Violeta Hernández]

If the intention is the former, then yeah, I think lean4#1777 should get approved, and defining Array.min? in terms of Min is the way to go

[Kim Morrison]

To clarify: we are not discussing the design of Ord here, and lean4#1777 is not under consideration today. :-)

[Kim Morrison]

(I hope eventually, but a redesign of Ord is not on the agenda now.)

[François G. Dorais]

Kim Morrison said:

Yes. We need to punt on big decisions about Ord, and just deal with this question in the context of the status quo.

I agree with the sentiment but that seems idealistic. Both options implicitly propose a definition of what it means to have a lawful combination of Min and Ord, with 1 being slightly less prescriptive. This is of course contributing to the problem that lean4#1777 aims to resolve. To really punt the issue, 1 and providing both left and right variants works, but this is silly since the distinction is irrelevant in the vast majority of applications.

[François G. Dorais]

How about 2 with just saying that the definition is foldl min or foldr min (whichever one you pick) to make the outcome clear. The user is left to figure out the implications.

[François G. Dorais]

I guess that's actually just 2... It seems that I just convinced myself that I'm on board with 2. :smirk:

[François G. Dorais]

Actually, I think the most important invariant should be [a, b].min? = some (min a b), so 2 is better in that sense too.

[Eric Wieser]

Am I right in saying that Mathlib hijacks Min for docs#Sup ? Or do we only attempt that on linear orders?

[Mario Carneiro]

I don't think we enable Min on lattices

[Eric Wieser]

Violeta Hernández said:

I think lean4#1777 should get approved,

Without wanting to hijack this thread, I haven't seen any objections yet so thought I should note I have some - I left some comments there.