Finset argmax

Stream: Is there code for X?

[Daniel Weber]

I have a nonempty Finset (Finset (Fin 31)), and I want to get the largest set in it (I don't care how ties are broken, but I want it to be computable). What's the best way to do that? I could map them to lists using Finset.sort, give them the shortlex order and then take the maximum, for instance, but that seems really unwieldy

[Yaël Dillies]

What about docs#List.argmax of Finset.sort?

[Yaël Dillies]

What about docs#List.argmax of Finset.sort?

[Yaël Dillies]

If you don't care about safety, you can instead unquot the finset and feed it to argmax

[Daniel Weber]

Yaël Dillies said:

What about docs#List.argmax of Finset.sort?

Hmm, it requires a total order on Finset (Fin 31), but it is better

[Daniel Weber]

Yaël Dillies said:

If you don't care about safety, you can instead unquot the finset and feed it to argmax

I need safety, sadly

[Violeta Hernández]

In order for this operation to be computable, you need a definite way to break ties. I think your approach of using the shortlex order is probably the best one.

[Violeta Hernández]

I've ran into this issue of "needing literally any computable linear order" before. It'd be nice if there were some tactic to automatically generate one.

[Daniel Weber]

Perhaps there could be an instance

[Violeta Hernández]

But there's already a partial order defined on Finset (Fin 31), and the linear order wouldn't be compatible with it

[Daniel Weber]

It doesn't have to extend LE, it can just be

class HasLinearOrder (α : Type*) where
  r : α -> α -> Prop
  linear: IsLinearOrder α r

[Violeta Hernández]

That'd be nice. You can then have a tactic for deriving this relation for simple inductive types, and combine that with some other mechanism to turn it into a LinearOrder proper.

[Kevin Buzzard]

You'd get a diamond

[Daniel Weber]

I settled on ((p.image (fun a ↦ toLex (a.card, Finset.Colex.toColex a))).max' sorry).2.ofColex, I think that's good enough

[Eric Wieser]

Violeta Hernández said:

I've ran into this issue of "needing literally any computable linear order" before. It'd be nice if there were some tactic to automatically generate one.

I claim we should use the Ord typeclass for this (or rather, a strengthened version of it that says ≤ is weaker than it)

[Eric Wieser]

This would also solve the Repr Multiset problem computably

[Eric Wieser]

(deleted)