should minimum take an arbitrary relation

Stream: general

[Chris Hughes]

I want to find the minimum of a list (fin m), but not using the standard definition of le on fin, but using a different total order (the lex of a function fin m -> rat and fin m -> fin (m + n)). Would it be better for minimum to take arbitrary relations?

[Mario Carneiro]

that doesn't really sound like a minimum anymore. Maybe some kind of foldl will suffice?

[Chris Hughes]

The proofs that that suffices are not entirely trivial. data.list.min_max is quite a long file.

[Reid Barton]

Do you really mean an arbitrary relation, or an arbitrary total order (not coming from an instance)?

[Chris Hughes]

arbitrary total order.

[Reid Barton]

Haskell has minimumBy as well as minimum, which seems like a sensible arrangement to me

[Simon Hudon]

Maybe foldMap would be a better direction. It maps every objects to an element of a monoid. You can then pick whichever monoid works best.

[Reid Barton]

But minimum has associated theorems (it's an element of the original list, and leq all the other elements) which don't have analogues for a general monoidal operation

[Simon Hudon]

How about we consider a special kind of monoids? A semilattice with a total order? Then we have x * y = x \/ x * y = y from which we can prove that the result is an element of the list.

[Sebastien Gouezel]

What if you register another order with a higher priority? Wouldn't minimum talk about this order? Or use the @ version of min everywhere?

[Chris Hughes]

That's what I did, but it's ugly.

[Scott Morrison]

Or define a type synonym, with the instance you want to use available for that. This seems like the “mathlib canonical” way to do it, once we’ve committed to using typeclasses everywhere.