well-founded lt

Stream: general

[Violeta Hernández]

Is it just me, or do we have some quite glaring design flaws when it comes to well-founded relations?

[Violeta Hernández]

It's a lot of things, really

[Violeta Hernández]

First, the fact that well_founded isn't a typeclass is a bit of a minor annoyance

[Violeta Hernández]

What really bothers me most is that we don't have a clear way of spelling out "a type is well-ordered under <"

[Violeta Hernández]

The obvious spelling is linear_order α + well_founded (<), but it turns out this isn't the most convenient spelling because the latter isn't a typeclass

[Violeta Hernández]

A more convenient spelling is linear_order α + is_well_order α (<), which is certainly awkward but gives you all that cool typeclass functionality (though you usually still need to name the latter and call h.wf)

[Violeta Hernández]

Except, if you know that nonempty α, what you really want is conditionally_complete_linear_order_bot α, which is not at all obvious

[Violeta Hernández]

So what we've ended up with is a bunch of disjointed API using these three different spellings

[Violeta Hernández]

Oh and also, we don't have any API on preorder α + well_founded (<), which means that a lot of lemmas that would naturally be stated in terms of ≤ are instead written in terms of the negation of a general relation

[Violeta Hernández]

Here's my proposal: we make well_founded into a typeclass is_well_founded, but only use it sparingly, the same way we use typeclasses like is_refl or is_trans

[Kevin Buzzard]

I'm not at all an expert in this sort of thing, but one flaw in your proposal is that well_founded is in core Lean, which means that Lean itself is using it to do stuff (e.g. make inductive types work? who knows, I guess someone here will), which means that changing it in any way might not be an option.

[Yaël Dillies]

Isn't that exactly what is_well_order is?

[Violeta Hernández]

Well-orders are linear well-founded orders

[Violeta Hernández]

Not the same thing

[Yaël Dillies]

Ah so you want to fill up that gap with another rel class? I think that makes sense, because bundling linearity is unexpected from mathlib's point of view (I know it very well and yet I got tricked just here and now once again).

[Yaël Dillies]

Do we even want is_well_order (as opposed to just the well-foundedness rel class)? What is it used by?

[Violeta Hernández]

I do think we want is_well_order, since it's used with generic relations here and there. But its uses with < and > should be put into new typeclasses instead.

[Yaël Dillies]

My question is whether we use the linearity that comes with it or not.

[Violeta Hernández]

I believe we do

[Violeta Hernández]

Excluding those lemmas about is_well_order _ (<), the API for is_well_order seems to consist of only two kinds of things

[Violeta Hernández]

Typeclass lemmas of the sort you'd expect for one of the unbundled order relation classes, like is_well_order α r → is_irrefl α r and the like

[Violeta Hernández]

And some sporadic uses in the ordinal library

[Violeta Hernández]

Sporadic but important uses, like for instance docs#ordinal.type

[Violeta Hernández]

I don't think this needs to be removed

[Violeta Hernández]

But yeah, my idea is to fill the gap with one or maybe two new order classes, one for preorder α with well-founded <, and another for linear_order α with well-founded <

[Violeta Hernández]

Not very sure about the second one, since as mentioned previously, it's just conditionally_complete_linear_order_bot + empty types

[Yaël Dillies]

This sounds like a mixin's job. We do not want those in the main spine of the order hierarchy.

[Reid Barton]

conditionally_complete_linear_order_bot is weaker, consider $[0, \infty) \subseteq \mathbb{R}$, or $[0,1]$

[Violeta Hernández]

Oh darn, you're right

[Violeta Hernández]

Rather, a nonempty linear_order with well-founded < is equivalent to a conditionally_complete_linear_order_bot with well-founded <

[Violeta Hernández]

Also, since well_founded is on core, we might want to keep it around, but prefer using a new is_well_founded typeclass

[Violeta Hernández]

Kind of how we have the reflexive predicate but prefer using is_refl for the typeclass inference

[Violeta Hernández]

Or actually I don't know, what's our opinion on the unbundled typeclasses?

[Violeta Hernández]

I like them, but I also hear they were part of an abandoned refactor, so maybe I shouldn't be using them?

[Eric Wieser]

It might be worth looking at what Lean4 does here, if it does anything

[Yaël Dillies]

I think an is_well_founded rel class is the way to go. That's whay I did for docs#is_directed.

[Violeta Hernández]

By the way, part of my reason for mentioning this is my annoyance with docs#well_founded.succ

[Violeta Hernández]

I don't think we should have that definition in its current form

[Violeta Hernández]

As the docstring states, it just gives "some" successor, instead of the successor as you really want in almost all cases

[Violeta Hernández]

I've started working on the idea of both an is_well_founded class and a well_founded_lt / well_founded_gt mixin. It's going great!

[Violeta Hernández]

Many of the theorems in order/well_founded.lean now have much nicer spellings

[Violeta Hernández]

Also, I only now realized that is_well_order has a redundant field :fear:

[Violeta Hernández]

is_well_founded implies is_irrefl, as I proved surprisingly recently

[Violeta Hernández]

Speaking of redundant fields, what's the deal with docs#is_strict_total_order'? I know that we don't like to touch core much, but surely one could just remove the redundant field from docs#is_strict_total_order and PR that?

[Violeta Hernández]

Another question, do we not have a predicate for a minimal element of a set? Not a least one, nor a lower bound

[Violeta Hernández]

I made a PR at #15023, but I'm very far from done

[Violeta Hernández]

Doing this as a mixin was definitely the right approach

[Junyan Xu]

class well_founded_lt (α : Type*) [has_lt α] extends is_well_founded α (<) : Prop

Why do you need extend? Are there any precedents? What's wrong about

abbreviation well_founded_lt (α : Type*) [has_lt α] := is_well_founded α (<)

?

[Yaël Dillies]

Violeta Hernández said:

Another question, do we not have a predicate for a minimal element of a set? Not a least one, nor a lower bound

docs#minimals

[Violeta Hernández]

I'm really only using extend because of the convenience of having is_well_founded a (lt) automatically inferred

[Violeta Hernández]

Also, I think minimals is not quite what I want, that seems to assume a reflexive relation when I'm really working with an irreflexive one

[Yaël Dillies]

I know it should be changed to {a ∈ s | ∀ ⦃b : α⦄, b ∈ s → r b a → r a b}, but apart from that I don't see what you mean.

[Violeta Hernández]

Maybe I'm just confused

[Violeta Hernández]

I'm trying to figure out how to spell docs#well_founded.has_min without writing down all the bare predicates

[Violeta Hernández]

I think it would be equivalent but not def-eq to nonempty (minimals r s), since r here is asymmetric

[Violeta Hernández]

Assuming that change you mention

[Junyan Xu]

You want {a ∈ s | ∀ ⦃b : α⦄, b ∈ s → r b a → false} right?
For irreflexive r, r b a → false is equivalent to r b a → a = b, and if r is moreover transitive or well-founded, it's also equivalent to r a b → r b a.

[Violeta Hernández]

Oh yeah, you're right

[Violeta Hernández]

I just realized three things

[Violeta Hernández]

1) every well founded relation has an ordinal-valued height function
2) this coincides with typein in the well-ordered case
3) this coincides with the birthday function on pgame

[Violeta Hernández]

So that's another cool refactor we could do, eventually

[Violeta Hernández]

Oh and also, this is in simple correspondence with grade on a grade_order

[Violeta Hernández]

By the way, do we have that a grade_order graded by a well-founded type is well-founded?

[Yaël Dillies]

Nope. Should be easy however.

[Violeta Hernández]

Don't do it yet though, or I'll have to modify whatever you write in the refactor :P

[Wrenna Robson]

Violeta, I've nothing to say other than I think you're right that there's some grognuts with how we currently do this and you're doing the good work by addressing them. I've run into them a few times. (Also, yes, surprisingly hard to say things like "this is a minimal element of this set" and suchlike.)

[Violeta Hernández]

Oh, speaking of that, it's a bit weird how we have the minimum of a set, but in practice, almost always refer to the minimum of a whole type

[Violeta Hernández]

This leads to mem_univ awkwardness

[Violeta Hernández]

I left a to-do to remedy that in a followup refactor

[Violeta Hernández]

I've noticed that is_well_founded isn't quite like the other unbundled classes

[Violeta Hernández]

Because you can prove much more elaborate theorems on well foundedness that you can on say, irreflexibility

[Violeta Hernández]

So I'm wondering what our policy on the well_founded predicate should be

[Violeta Hernández]

I've tried doing what we do with the other unbundled classes, which is using the class for inferred arguments, and the predicate on non-instance theorems

[Violeta Hernández]

And I've tried putting almost all of the theorems on the typeclass

[Violeta Hernández]

But it turns out that we do sometimes need to talk about minimums of random well-ordered relations that can't easily made into instances

[Violeta Hernández]

On one extreme I could just tank the @ and state all the cool theorems in terms of is_well_founded

[Violeta Hernández]

On another extreme, I could duplicate the entire API on is_well_founded in terms of well_founded

[Violeta Hernández]

A middle ground solution I'm gravitating towards is having only the basic theorems, like well_founded.has_min and such, stated for general well founded orders, and having everything else use the typeclass

[Violeta Hernández]

I'd like a second opinion here though

[Violeta Hernández]

By the way, status update on the refactor: it's going quite well, a bunch of cool theorems on well founded orders can now be upgraded to instances, and pretty much the issue I've encountered is the aforementioned

[Violeta Hernández]

No end in sight yet btw, I'm still editing quite basic files and we're at 800 lines of diff

[Violeta Hernández]

Hey question, what's the difference between well_founded.recursion and well_founded.fix?

[Violeta Hernández]

They have almost the same signature

[Violeta Hernández]

well_founded.recursion doesn't guarantee anything about its output as far as I can tell though

[Violeta Hernández]

While of course there's well_founded.fix_eq

[Junyan Xu]

I'm really only using extend because of the convenience of having is_well_founded a (lt) automatically inferred

I asked whether there's precedent because I've only seen mathlib use @[reducible] def in such situation (e.g. src#finite_dimensional) and never seen extends with a single class without adding any field.

[Eric Wieser]

The problem with using extend like that is you have to duplicate all existing instances. With reducible def you're providing a nicer spelling that has access to all the same instances as the verbose spelling

[Violeta Hernández]

What's up with this?

[Violeta Hernández]

docs#well_founded.eq_iff_not_lt_of_le

[Violeta Hernández]

Obviously this should be moved, but where to?

[Violeta Hernández]

Core?

[Violeta Hernández]

I would be surprised if it didn't exist elsewhere in the library

[Eric Wieser]

I think it's hard to argue that anything should move to core unless it needs C++ support

[Violeta Hernández]

Do we have some file for very basic results on orders other than the one on core?

[Violeta Hernández]

Preferably a really really early import

[Violeta Hernández]

Or should I just leave that result awkwardly lying around in the well-founded file?

[Violeta Hernández]

Or is there any way I can prove/use this result easily?

[Yaël Dillies]

file#order/basic

[Violeta Hernández]

Oh thanks

[Violeta Hernández]

Actually I'm just going to restate the result

[Violeta Hernández]

It's a bit dumb to have the conclusion be m ≤ x → x = m instead of just ¬ x < m

[Violeta Hernández]

I'm facing another slight annoyance. Ideally you'd want an instance linear_order α + well_founded_lt α → is_well_order α (<), but the latter implies is_well_founded α (<) which implies well_founded_lt α, so this doesn't work.

[Violeta Hernández]

I did declare this as a definition well_founded_lt.is_well_orderthough, so it's not a major setback

[Violeta Hernández]

Just something to keep in mind

[Violeta Hernández]

Yaël Dillies said:

Do we even want is_well_order (as opposed to just the well-foundedness rel class)? What is it used by?

On an unrelated note, after scouring the library throughout this refactor, I've seen that we do use is_well_order in its full strength. In fact, I've only found a few theorems that can be generalized to is_well_founded. That said, this class has still been really useful thanks to all the instances you get, on things like subrelations or inverse images.

[Violeta Hernández]

Here's something fun

[Violeta Hernández]

docs#set.is_wf is def-eq to well_founded_lt s

[Violeta Hernández]

I've had to heavily modify this file as a result of this refactor anyways, should I just go ahead and ditch that predicate?

[Violeta Hernández]

Actually, I'll just leave it as a reducible def for now, golf all the theorems, and leave a to-do note to kill that predicate in the future

[Violeta Hernández]

Now here's a harder question

[Violeta Hernández]

docs#set.is_well_founded_on is def-eq to is_well_founded_on s (subrel r s)

[Violeta Hernández]

Does that mean I should treat it like a typeclass argument? It's moved around and rewritten a lot in proofs, so I don't know

[Violeta Hernández]

And what aboud docs#set.partially_well_ordered_on and docs#set.is_pwo? Those don't look typeclassy at all

[Violeta Hernández]

If we are going to make is_well_founded into a typeclass, maybe we should do the same with is_pwo?

[Yakov Pechersky]

No, please don't. Why should they be typeclasses? They're statements about a term, not a type

[Violeta Hernández]

That's the thing, they don't need to be statements about a term

[Violeta Hernández]

You can talk about partially well-ordered types just fine

[Violeta Hernández]

Then, the current definition would just be the assertion that the subtype is partially well ordered

[Yakov Pechersky]

And golfing proofs to use some underlying implementation might make the proofs take fewer characters. But it makes the library much more brittle to later rework. Because if you change the implementation of the thing again, all your proofs break

[Yakov Pechersky]

Please take a look at where is_pwo is used. It's used directly on sets, not on types or subtypes. It's what makes Hahn series work

[Violeta Hernández]

You're right, all current usage of is_pwo in mathlib involves a support set

[Violeta Hernández]

What's to be done about set.is_wf and set.is_well_founded_on though? It's set.is_wf that makes me feel particularly uneasy

[Violeta Hernández]

In any case, my refactor will redefine it as well_founded_lt ↥s, because that's what it is. The question is whether we should take the extra step and use it in typeclass inference as we do for well_founded_lt.

[Violeta Hernández]

This feels like fintype vs set.finite, except this time there's no data involved!

[Yakov Pechersky]

What will be the benefit of relying on typeclass inference for discharging proof goals of set.is_wf?

[Violeta Hernández]

I can find out myself, I'll disable my typeclass experiment and see if anything becomes tangibly more convenient

[Violeta Hernández]

It seems I very quickly found the answer: not a lot

[Yakov Pechersky]

I think the sequence of tactics, in terms of symbols written by a user, might become more convenient, as measured by the number of symbols. But it might be less convenient in terms of elaboration and proof construction time, because you're punting the proof obligation to the implicit tactic of typeclass inference. TC is in general weaker than explicit term construction (the most powerful in assisting elaboration, but often the least user-convenient) or just a user-invoked tactic (that isn't apply_instance).

[Violeta Hernández]

You do sometimes want some of the instances well_founded_on and is_wf are equivalent to, but that can be dealt to with a single auxiliary lemma and haveI

[Violeta Hernández]

For instance here:

lemma is_well_founded_on.induction {s : set α} {r : α → α → Prop} (h : s.is_well_founded_on r)
  {x : α} (hx : x ∈ s) {P : α → Prop} (hP : ∀ (y ∈ s), (∀ (z ∈ s), r z y → P z) → P y) :
  P x :=
begin
  let Q : s → Prop := λ y, P y,
  change Q ⟨x, hx⟩,
  haveI := h.is_well_founded,
  refine is_well_founded.induction (subrel r s) ⟨x, hx⟩ _,
  rintros ⟨y, ys⟩ ih,
  exact hP _ ys (λ z zs zy, ih ⟨z, zs⟩ zy),
end

is_well_founded_on.is_well_founded is actually just id

[Violeta Hernández]

But that's pretty much the only spot where having this be typeclass searchable could have been remotely convenient

[Yakov Pechersky]

(deleted)

[Yakov Pechersky]

I think that if a part of the library relies in proofs with tactic bodies that utilize haveI, introI, repeatedly, there's some weird api bleedover. I'm not making a judgment call on the category theory portion of the library because I admittedly don't understand it. But for proof discovery, either by guessing a name, or knowing that one had to do introI or haveI to make the rest of the API work for some lemmas, it doesn't work so well with other tactics we have for discovery, like suggest, library_search, or relying on simp.

[Yakov Pechersky]

This assertion of mine is from my experience working on constructing various partial orders on a fixed type, which relied on a lot of letI. I made the questionable choice of relying on separate explicitly specified instances instead of type synonyms.

[Violeta Hernández]

I've had to use haveI very little, actually

[Violeta Hernández]

It seems like the lemmas that it's used for subsume other potential uses

[Violeta Hernández]

Alright, I'm done refactoring that file. I think I've managed to use my new code advantageously without being destructive.

[Violeta Hernández]

If someone could review it, that would be awesome: https://github.com/leanprover-community/mathlib/pull/15023/files#diff-885226e6f133825031006afbcd1e5b3cc826941500c61a4f21967571feaf9766

[Violeta Hernández]

Almost all other files on this refactor should be easier to review

[Reid Barton]

The main purpose of well_founded is to support well-founded recursion. Often one will want different orderings on the same type for use in different definitions/proofs. For example, we could put a lot of different orders on list nat. The type class mechanism seems like it would just get in the way here (and type synonyms would be even worse).

[Violeta Hernández]

What's this in reference to?

[Violeta Hernández]

The whole refactor?

[Violeta Hernández]

It's true that there's many possible orderings on a given type, but we usually only care about a handful - that's the reason we have things like has_lt to begin with.

[Violeta Hernández]

So I'm not sure how the type class mechanism would get in the way

[Violeta Hernández]

The thing is, we already have tons of theorems and definitions for things that have a well founded < or > specifically. We already employ the typeclass system for this, though in an ineffective manner, since we have to apply theorems for general well founded relations, which we need to keep providing the proof of, and then convert them into theorems on preorders or partial orders or whatnot.

[Violeta Hernández]

We definitely need predicates for well founded < and well founded >, that's clear to me by now. We use this all throughout mathlib, from finsets to ordinals to linear algebra to category theory. I can't see the problem with taking it one step further and making this inferrable by the typeclass system.

[Violeta Hernández]

This is subjective, but I feel like my refactor has so far alleviated more problems than it's caused

[Violeta Hernández]

(deleted)

[Violeta Hernández]

I do appreciate the opinions though

[Violeta Hernández]

(deleted)

[Violeta Hernández]

It's just hard to work on 1500 lines of code for 3 days straight and not get attached, haha

[Violeta Hernández]

(deleted)

[Reid Barton]

Violeta Hernández said:

Here's my proposal: we make well_founded into a typeclass is_well_founded, but only use it sparingly, the same way we use typeclasses like is_refl or is_trans

This one I don't think is a good idea.

[Reid Barton]

If it's only about whether (<) is well-founded then it's okay to use a type class, because (<) is already associated to the type by a type class.

[Violeta Hernández]

I'm not sure what makes this different from the other unbundled typeclasses

[Violeta Hernández]

Or more specifically, the is_well_order typeclass

[Violeta Hernández]

That one has a decent amount of use for relations other than (<) and (>), this wouldn't be any different

[Violeta Hernández]

I should probably mention

[Violeta Hernández]

I've been working into splitting off the largest parts of this refactor into different files

[Violeta Hernández]

#15069 #15071 #15073

[Violeta Hernández]

And also #14707 I guess

[Violeta Hernández]

Would be super cool if someone could check those out

[Violeta Hernández]

My refactor builds!!!!!!!!!

[Violeta Hernández]

Almost, some IMO file broke lol

[Violeta Hernández]

Final diff clocks in at 2k lines :skull:

[Violeta Hernández]

I'll attempt to make more offshoot PRs before this huge one

[Yaël Dillies]

This looks like a bit much for just introducing an is_well_founded typeclass. Did you scope-creep?

[Violeta Hernández]

Only in a few files that got their own PRs already

[Violeta Hernández]

I didn't just introduce the typeclass, I ported the existing theorems on well-founded relations to use said typeclass

[Violeta Hernández]

And I redefined a few other classes that were just specific cases of said typeclass

[Violeta Hernández]

If you look at the diff you'll see it's mostly just changing well_founded.min to is_well_founded.min and such throughout almost 60 files

[Violeta Hernández]

Just a few extra files that had some more drastic changes, and I'm working on documenting and assessing that

[Violeta Hernández]

Yep, I just went through all my work, and save for the basic files on well-founded relations that I very heavily modified, the whole PR is just a bunch of renames and the occasional golf with the new API.

[Violeta Hernández]

I think the diff will drop by like 500 lines or so when my other spinoff PRs are merged