well_founded.min

Stream: maths

[Violeta Hernández]

Do we even need docs#well_founded.min?

[Violeta Hernández]

Obviously, docs#well_founded.has_min is super useful as a characterization of well-foundedness, I'm not doubting that.

[Violeta Hernández]

The question is whether being able to select an arbitrary minimal element from a set through choice, instead of just using obtain on an existential, is ever useful.

[Violeta Hernández]

If there is a unique minimal element, then it is nice being able to reference it directly. However, a (nonempty) well-founded order with unique minimal elements is in fact a well-order, and more so a docs#conditionally_complete_linear_order_bot, so in that case you really ought to be using Inf instead.

[Violeta Hernández]

I've golfed a bunch of proofs in the past by simply replacing well_founded.min, well_founded.min_mem, and well_founded.not_lt_min with a single call to well_founded.has_min, so it really seems like the former are but an annoyance. I say we get rid of them, and if we really need to extract data out of this, we simply use classical.some (well_founded.has_min hr s hs) directly.

[Violeta Hernández]

On this note, docs#well_founded.succ and docs#well_founded.sup ought to go too, for the same reasons. I think they're unused, anyways.

[Kyle Miller]

well_founded.min seems to go way back to 2017: https://github.com/leanprover-community/mathlib/commit/49a63b7464df04e216ad1ff353b306ca157119f8 (edit: I missed that I still haven't gotten to the origin, this might be it)

[Kyle Miller]

These don't seem to be harmful API to me, so I'm not sure it's worth worrying too much about them. Maybe it's a bit redundant to have them, but at worst using them adds a constant factor to proof size.

It's not uncommon to create wrappers around classical.some like this, and sometimes it's better because then you can state nicer lemmas than whatever classical.some_spec gives you.

[Violeta Hernández]

Kyle Miller said:

These don't seem to be harmful API to me, so I'm not sure it's worth worrying too much about them.

I wanted to add some boilerplate convenience lemmas for well_founded.has_min, re: #18751. So I need to decide whether I'll port these or not. They add quite a lot of lines to that file.

[Violeta Hernández]

Kyle Miller said:

Sometimes it's better because then you can state nicer lemmas than whatever classical.some_spec gives you.

A generic minimal element of a set is a very broad notion. We really can't say anything about it that isn't just a restatement of the definition, except in the cases I've already brought up.

[Violeta Hernández]

It's telling that the original use case was for ordinals. I believe I was the one who removed it from that file in favor of Inf.

[Kyle Miller]

Why are you defining is_well_founded.min, well_founded_lt.min, well_founded_gt.max in that PR? Are you planning on using them for something? If not, then don't define them -- if they're not convenient then maybe they're not actually convenience lemmas.

[Violeta Hernández]

I'm defining them for symmetry with the existing API.

[Kyle Miller]

Violeta Hernández said:

A generic minimal element of a set is a very broad notion. We really can't say anything about it that isn't just a restatement of the definition, except in the cases I've already brought up.

Right, I get that this is a completely arbitrary element, but min_mem and not_lt_min are epsilon nicer than what classical.some_spec for ∃ a ∈ s, ∀ x ∈ s, ¬ r x a would give you, which is all I'm saying here.

[Kyle Miller]

Violeta Hernández said:

I'm defining them for symmetry with the existing API.

I give you permission not to keep symmetry. It's not symmetric anyway, since the new definitions use instance arguments instead of an explicit one.

[Yaël Dillies]

Violeta Hernández said:

I'm defining them for symmetry with the existing API.

"Maintenance without guidance is the API's perdition" -Someone, I guess?

[Yaël Dillies]

I think you should stop changing API for the sake of it, and set yourself some big goals that will guide your API-writing.

[Violeta Hernández]

This really isn't "for the sake of it". I've worked a bunch with well-founded relations, it's somewhat annoying to do this, and I'm making it less annoying.

[Yaël Dillies]

What's your end goal?

[Violeta Hernández]

This really isn't supposed to be a big project, it's just making some code nicer to work with.

[Violeta Hernández]

Admittedly I do have other big projects to go back to, but that shouldn't invalidate this

[Yaël Dillies]

These kinds of decisions are hard to evaluate without a clear end goal, so I would think that, yes, it does invalidate this.

[Kevin Buzzard]

Randomly adding stuff to mathlib 3 for no clear reason is a step in the wrong direction

[Eric Wieser]

Or at least, randomly adding stuff to the already-ported parts of mathlib3 for no clear reason is

[Eric Wieser]

@Violeta Hernández, I would recommend for now you focus on forward-porting the files you've already changed; there were >10 files out of sync with your name on last time I checked.