RFC: Ditch WellFounded.min

Stream: mathlib4

[Violeta Hernández]

I've come to the opinion that docs#WellFounded.min is an antipattern we've been falling victim to, and should be removed in favor of docs#WellFounded.has_min

[Violeta Hernández]

Here's my reasoning:

1. This is often not the correct spelling for what we want. If we have a well-order, we can define the stronger docs#ConditionallyCompleteLinearOrderBot instance, and use Inf instead.
2. When we don't have a well-order, choosing an explicit but arbitrary minimal element is basically pointless.
3. The arguments of min, min_mem, and not_lt_min are annoyingly duplicated. Using obtain on has_min solves this issue entirely.

[Violeta Hernández]

@Yaël Dillies what do you think?

[Yaël Dillies]

My biggest complaint is that it's completely unsearchable. Every time I look for it, I search for something like Set.Nonempty.exists_min

[Violeta Hernández]

That could very well be made into an alias

[Violeta Hernández]

I'm not sure if we have examples of theorems where two separate arguments allow for dot notation, though

[Violeta Hernández]

Hypothetically min could be useful in the following, very specific case:

1. A well-founded order that isn't a well-order
2. Under a relation other than <
3. With a single minimal element
4. That can't be defined explicitly

[Violeta Hernández]

The closest thing to that is ZFSet membership, but of course the empty set is perfectly definable

[Violeta Hernández]

If such a specific case did arose... Surely we could just use Classical.some <| WellFounded.has_mem explicitly

[Violeta Hernández]

I'll make the PR tonight if there's no objections

[Violeta Hernández]

Actually, we do have three other definitions depending on WellFounded.min. These are WellFounded.sup, WellFounded.succ, and Function.argmin.

[Violeta Hernández]

These... also have distinct problems

[Violeta Hernández]

WellFounded.sup is very misleading. It's only the supremum in a well-ordered type (in which case we almost definitely should be using Sup instead), and otherwise, it's just some random "minimal upper bound" for the set.

[Violeta Hernández]

Fortunately, it doesn't seem to be used anywhere (not even in the definition of docs#IsWellOrder.conditionallyCompleteLinearOrderBot) so we can just axe it

[Violeta Hernández]

WellFounded.succ has the same problem; it's only valid for a well-order, and a SuccOrder instance exists in the overwhelmingly common case where the order relation is <

[Violeta Hernández]

That one is actually used in another file, namely Order/IsWellOrderLimitElement

[Violeta Hernández]

That file proves theorems for LinearOrder α and IsWellOrder α (· < ·), which is completely equivalent to ConditionallyCompleteLinearOrder α + IsWellOrder α (· < ·)

[Violeta Hernández]

In my view, the "correct" notion of a limit element is that of a SuccOrder, namely a (non-minimal) element that is not a successor

[Violeta Hernández]

So really that whole file is problematic to me

[Violeta Hernández]

Looking at the discussion on #11584, it seems @Junyan Xu agrees with me

[Violeta Hernández]

As for Function.argmin, it does seem to get used a bit more throughout MathLib.

[Violeta Hernández]

(deleted)

[Violeta Hernández]

I'm not quite sure how I feel about it. I think it should probably be made specific to lattices, but it can stay for now, I guess

[Violeta Hernández]

I opened #15863, which should be an initial step towards getting rid of / refactoring IsWellOrderLimitElement.lean

[Violeta Hernández]

You know, I'm beginning to see how WellFounded.min is useful

[Violeta Hernández]

It serves some purpose within nonconstructive definitions, particularly when you're working not with < but with an arbitrary relation

[Violeta Hernández]

In that case, it's useful even in the well-order case

[Violeta Hernández]

Of course, we should avoid working with general well-orders like that, but this is simply how some parts of the library are set up. For instance, ordinals are defined as a quotient of well-ordered types under otherwise arbitrary relations.

[Violeta Hernández]

I think the actual thing to be doing is refactoring the uses of min out whenever possible, if they can be replaced by sInf or obtains _ := WellFounded.has_min. There's few legitimate uses, but that's not zero.