Set.isWF

Stream: mathlib4

[Violeta Hernández]

Does it make sense to keep docs#Set.isWF now that we have docs#WellFoundedLT? Specifically, for s : Set α, the predicates s.isWF and WellFoundedLT s should be completely equivalent.

[Violeta Hernández]

Likewise, we have docs#Set.isPWO, but I've really been wanting a type version of this; partially well-ordered types are precisely the posets for which the poset game is guaranteed to end. Sure, I could write (@Set.univ α).isPWO, but that's somewhat awkward and doesn't really fit with our usual design.

[Violeta Hernández]

@Bhavik Mehta

[Bhavik Mehta]

I think the IsWF spelling is quite a bit more convenient, since it doesn't involve a coercion from sets to types. For instance, WellFoundedLT is reducible and inline, and it seems to me that the rhs WellFoundedLT s isn't even in simp-normal form. So I'd instead say that docs#WellFoundedLT is the one that should change here.

[Bhavik Mehta]

Violeta Hernández said:

Likewise, we have docs#Set.isPWO, but I've really been wanting a type version of this; partially well-ordered types are precisely the posets for which the poset game is guaranteed to end. Sure, I could write (@Set.univ α).isPWO, but that's somewhat awkward and doesn't really fit with our usual design.

I'm in favour of having a typeclass for partially well-ordered types, perhaps defined as (@Set.univ α).isPWO

[Violeta Hernández]

Bhavik Mehta said:

For instance, WellFoundedLT is reducible and inline, and it seems to me that the rhs WellFoundedLT s isn't even in simp-normal form.

Oh yeah, that's a good point. We would end up with the same problem that happened with Subrel, where e.g. WellFoundedLT {x | p x} gets simped into WellFoundedLT {x // p x} which then causes all other simp lemmas to break.

[Violeta Hernández]

Bhavik Mehta said:

I'm in favour of having a typeclass for partially well-ordered types, perhaps defined as (@Set.univ α).isPWO

This seems a bit backwards in design to me, surely we'd want IsPWO to be defined in terms of PartiallyWellOrderedLT instead? But I guess that's a minor concern.

By the way, the typeclass should really be called something like WellQuasiOrderedLT instead. PWO means WQO + partial order.

[Violeta Hernández]

I'll try to get this new typeclass into Mathlib :smile: and I'll leave these existing set predicates alone for the most part

[Bhavik Mehta]

Violeta Hernández said:

By the way, the typeclass should really be called something like WellQuasiOrderedLT

And also partially well-ordered is less standard and more confusing than well quasi-order!

[Violeta Hernández]

I think "well quasi-order" is also confusing, but that ship has already sailed :frown:

[Violeta Hernández]

Question: does it make sense to have the unbundled version docs#Set.PartiallyWellOrderedOn ?

[Violeta Hernández]

Or more generally, an unbundled predicate for a relation being a well quasi-order

[Bhavik Mehta]

Keeping the relative version (ie not univ) is definitely useful

[Violeta Hernández]

Yeah I agree, I'm talking about the version that takes an arbitrary relation instead of a preorder

[Bhavik Mehta]

IMO that's useful too, eg for the divisibility relation on nat or the subset relation on finsets or sets

[Violeta Hernández]

It is a bit annoying that you'd like to prove a wqo is well-founded and has no infinite antichains. But the well-founded relation is < and the no infinite antichains conditions is on ≤ instead!

[Violeta Hernández]

But the definition that is currently in Lean is correct on preorders and needs only one of the two relations, so maybe we don't need to fix anything. Just introduce the necessary API in the preorder case.

[Violeta Hernández]

Violeta Hernández said:

It is a bit annoying that you'd like to prove a wqo is well-founded and has no infinite antichains. But the well-founded relation is < and the no infinite antichains conditions is on ≤ instead!

In fact, the current API has some pretty awkward theorems as a consequence of this

[Violeta Hernández]

Like, docs#PartiallyWellOrderedOn.wellFoundedOn

[Violeta Hernández]

"If r is a preorder and a WQO, then the relation r a b ∧ ¬ r b a is well-founded"
Is this ever going to be useful outside of when r = ≤ and the resulting relation is <?

[Violeta Hernández]

I'm not sure if we have e.g. a strict divisibility relation where this could be used

[Violeta Hernández]

And as for subsets, we could just use ≤ and < in that case

[Violeta Hernández]

And also, what's the deal with docs#partiallyWellOrderedOn_iff_finite_antichains ?

[Violeta Hernández]

This is true - obviously, it's in Lean. But is it really meaningful? The "intended" use case for the predicate is r a reflexive and transitive relation, and if you add the symmetric condition you end up with r being the always true relation, which seems unintended.

[Violeta Hernández]

To me, this reads like a corruption of the statement connection wqos to well-founded orders: if ≤ is a preorder, then it's a wqo iff all antichains are finite and if < is well-founded

[Violeta Hernández]

(which I don't think we currently have in Mathlib!)

[Violeta Hernández]

Violeta Hernández said:

To me, this reads like a corruption of the statement connection wqos to well-founded orders: if ≤ is a preorder, then it's a wqo iff all antichains are finite and if < is well-founded

Judging by the docstring just above docs#Set.PartiallyWellOrderedOn, that seems to be the case.

[Violeta Hernández]

Another theorem I'd classify as nonsense is docs#IsAntichain.finite_of_partiallyWellOrderedOn. A preordered antichain is just a singleton.

[Violeta Hernández]

Is there any interesting about WQOs that aren't preorders, or is this just Mathlib overgeneralization?

[Violeta Hernández]

@Aaron Anderson

[Aaron Anderson]

Violeta Hernández said:

Another theorem I'd classify as nonsense is docs#IsAntichain.finite_of_partiallyWellOrderedOn. A preordered antichain is just a singleton.

You can have antichains of any size in preorders- IsAntichain is defined in terms of pairs of distinct elements being incomparable, so it doesn't matter if you're looking at ≤ or <.

[Aaron Anderson]

That particular theorem is just half of the characterization you want that "if ≤ is a preorder, then it's a wqo iff all antichains are finite and if < is well-founded"

[Aaron Anderson]

Violeta Hernández said:

And also, what's the deal with docs#partiallyWellOrderedOn_iff_finite_antichains ?

I agree this one's weird - essentially this is a theorem about graphs, and it's not used anywhere in the library.

[Aaron Anderson]

Violeta Hernández said:

Is there any interesting about WQOs that aren't preorders, or is this just Mathlib overgeneralization?

My use case working on this stuff was Hahn series, for which we just care about partially ordered monoids, so preorders are definitely a good enough use case as far as I'm concerned.

[Bhavik Mehta]

Aaron Anderson said:

Violeta Hernández said:

Another theorem I'd classify as nonsense is docs#IsAntichain.finite_of_partiallyWellOrderedOn. A preordered antichain is just a singleton.

You can have antichains of any size in preorders- IsAntichain is defined in terms of pairs of distinct elements being incomparable, so it doesn't matter if you're looking at ≤ or <.

Indeed, this theorem is useful, and there are many preordered antichains: just consider the discrete poset on n elements, which is always an antichain.

[Bhavik Mehta]

Violeta Hernández said:

This is true - obviously, it's in Lean. But is it really meaningful? The "intended" use case for the predicate is r a reflexive and transitive relation, and if you add the symmetric condition you end up with r being the always true relation, which seems unintended.

I think this is massively unfair. Firstly, there are reflexive symmetric transitive relations other than the always true relation, for example equality. More generally, any equivalence relation would work, and there are many of these on a given type! As Aaron says, this is essentially a theorem about graphs (notice it doesn't assume transitivity), and it says that the edge relation on a graph is a pwo iff there are no infinite independent sets. To me, this is a meaningful statement!

[Violeta Hernández]

Aaron Anderson said:

You can have antichains of any size in preorders- IsAntichain is defined in terms of pairs of distinct elements being incomparable, so it doesn't matter if you're looking at ≤ or <.

Oh yeah I had something wrong in my logic. But, a preordered antichain should just be the equality relation, right? So I think what we're actually missing is the result that says that, and the result that said relation is wqo.

[Violeta Hernández]

Bhavik Mehta said:

I think this is massively unfair. Firstly, there are reflexive symmetric transitive relations other than the always true relation, for example equality.

Yeah, that's another mistake of mine. I must have been thinking about total orders instead.

[Violeta Hernández]

(glad we have Lean, or people like me could just say whatever :stuck_out_tongue:)

[Bhavik Mehta]

Violeta Hernández said:

But, a preordered antichain should just be the equality relation, right?

Technically yes, but this is kind of missing the point: it's very rare to talk about the entire preorder being an antichain, instead what's usual is to consider subsets which are antichains

[Bhavik Mehta]

In particular the theorem in question here - that you called nonsense - actually plays an important role in my disproof of fishbone mentioned elsewhere! It's half of the proof that the first of the two alternatives fails.

[Violeta Hernández]

Bhavik Mehta said:

Violeta Hernández said:

But, a preordered antichain should just be the equality relation, right?

Technically yes, but this is kind of missing the point: it's very rare to talk about the entire preorder being an antichain, instead what's usual is to consider subsets which are antichains

Fair enough. But since I'm writing the API for the "full preorder" version of this predicate I'm also trying to figure out what lemmas to port and how to port them.

[Violeta Hernández]

Sorry for calling it nonsense! I was misunderstanding the hypotheses.

[Violeta Hernández]

I've got a few more questions about the WQO design. I already have a sorry-free proof of the main characterization of WQOs, i.e.

theorem wellQuasiOrderedLE_iff {α : Type*} [Preorder α] :
    WellQuasiOrderedLE α ↔ WellFoundedLT α ∧ ∀ s : Set α, IsAntichain (· ≤ ·) s → s.Finite :=
  sorry

Question 1: is it worth having the more verbose form for unbundled relations? Namely

theorem wellQuasiOrdered_iff {α : Type*} {r : α → α → Prop} [IsPreorder α r] :
    WellQuasiOrdered r ↔ WellFounded (fun a b ↦ r a b ∧ ¬ r b a) ∧ ∀ s : Set α, IsAntichain r s → s.Finite :=
  sorry

In my opinion, if you're in a preorder where both < and ≤ are relevant, you really should just build an actual Preorder instance.

Question 2: what about the corollary

theorem wellQuasiOrdered_iff_of_isSymm {α : Type*} {r : α → α → Prop} [IsPreorder α r] [IsSymm α r] :
    WellQuasiOrdered r ↔ ∀ s : Set α, IsAntichain r s → s.Finite :=
  sorry

(which is the docs#Set.partiallyWellOrderedOn_iff_finite_antichains lemma I brought up earlier). Surely that's not really worth having, is it?

[Violeta Hernández]

I've decided to open #21008, which defines the new type predicates for WQOs but doesn't yet link them to the existing set predicates in any way. This way, I can parallelize my work on combinatorial games which depends on WQOs, with the work of linking both APIs together.

[Violeta Hernández]

There's some preliminary merging work in #20786, which isn't yet complete but should at least show both APIs are compatible.

[Bhavik Mehta]

For your earlier two questions - I agree for Question 1, for Question 2 note that your version assumes transitivity where the original doesn't. So you don't need to keep it, but the actual "full" version of the lemma is potentially useful