lean 4: minimal by

Stream: Is there code for X?

[Thomas Murrills]

Is there something which could be called minimalBy or minBy for either arrays or lists in lean4, std4 or mathlib4? This would be a function such that a.minimalBy f would return an array or list of the elements in a which attained a minimal value under f.

If it doesn't exist, I'll be making one for use in a mathlib4 tactic (unless plans change). What should it be named and where in mathlib4 should it go?

[Yaël Dillies]

There's docs#list.argmin, which returns one of them.

[Thomas Murrills]

hmm, I need all of them, or at least to know if there are multiple

[Thomas Murrills]

I did wind up writing a few related functions to this end for arrays, so I can just put them anywhere in Mathlib. Would it be alright to create a file Mathlib.Array.Order? Seems like arrays are new, so it doesn’t hit any ported files.

[Thomas Murrills]

(Hmm, maybe I should move this question to #mathlib4 . I’ll revisit it tomorrow.)

[Yaël Dillies]

Whatever you end up writing, it would be nice to connect it to list.argmin somehow. In particular, I would do an implementation in terms of list (and why not one in terms of array).

[Thomas Murrills]

my heart says it ought to be named minimalBy (etc.), but my head says it ought to be named argmins for consistency with the preexisting argmin… :)

[Thomas Murrills]

My instinct is to stay away from ported files under the assumption that we shouldn’t change ported files unless we backport the changes. Is that a fair assumption? And if so what would be a good spot for the List versions? For Array I can simply make a new file, but I think List is all ported files.

[Yaël Dillies]

Oh I'm sure you can add it to data.list.argmin without bnackporting, so long as you don't change existing theorems