Any infimum based version of `OmegaCompletePartialOrder`?

Stream: general

[Pierre Quinton]

I am trying to build some framework about lattices (or Boolean algebras) where the suprema and infima of any countable collection exist.
If we have a Lattice that is also an OmegaCompletePartialOrder, then for any countable collection, we can take the chain of finite supremas, this has a supremum which is exactly the supremum of the original collection.

My problem is that I cannot find any infimum based version of OmegaCompletePartialOrder, it feels like it would therefore make sense to create it. This would mimic CompleteSemilatticeSup and CompleteSemilatticeInf that are combined to give CompleteLattice. But this feels like a problem as OmegaCompletePartialOrder should probably be the name of the combination of some OmegaCompletePartialOrderSup and OmegaCompletePartialOrderInf.

I'm not sure how to achieve this without either picking names that are not nice or redefining OmegaCompleteSemilattice to be a closed under suprema and infima of countable chains.

One last thing, the definition of a OmegaCompletePartialOrder.Chain is ([ℕ](https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Nat) [→o](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Hom/Basic.html#OrderHom) α) which makes it complicated to take infima meaningfully (compared to a definition of chain as a totally ordered subset of a partial order).

Any idea or suggestion would be welcome.

[Violeta Hernández]

I wonder why ωSup wasn't defined as ωSup : (s : Set α) → s.Countable → α, or something similar. Or is the existence of suprema for things that aren't chains not guaranteed?

[Violeta Hernández]

If only countable chains have suprema, perhaps its easier to redefine OmegaCompletePartialOrder.Chain s as IsChain (· ≤ ·) s ∧ s.Countable. I think that should be the same condition you want for the infimum.

[Pierre Quinton]

@Violeta Hernández The existence of arbitrary countable sets (non-chains) is guaranteed only in a Omega complete lattice which is simply a Lattice that is also Omega Complete.

I like this definition of chain better than the current one as it doesn't restrict them to have a minimal element. Otherwise you would need a dual concept to chains and that can get messy, I will try to see how hard it is to replace.

Note that with this definition, then ωSup is in some sense a sSup that is LUB. In ConditionallyCompleteLattice, sSup is defined on all s : Set α and IsLUB s (sSup s) is guaranteed if s is bounded above and non-empty. Similarly, we could replace defining ωSup by inheriting from SupSet, thereby defining sSup, and guaranteeing that IsLUB s (sSup s) whenever IsChain (· ≤ ·) s ∧ s.Countable. If we do that, then defining OmegaCompleteLattice only requires us to inherit from Lattice, OmegaCompletePartialOrder and its dual counterpart (which would give sInf). Finally, we can show that this must be closed under countable supremum and infimum.

[Violeta Hernández]

Does this mean we'd get rid of ωSup and simply make use of sSup but with a different set of axioms?

[Violeta Hernández]

I like that approach.

[Pierre Quinton]

@Violeta Hernández That is an option. I can see several pros such as getting iSup and associated notations for free. I can see one con which is that we force users to define sSup even on set that cannot have a supremum, I'm not sure of how much this is a problem.

[Violeta Hernández]

I don't think it should be any more of a problem than it is for ConditionallyCompleteLattice. As long as your type is inhabited you can always provide some convenient dummy value.

[Yaël Dillies]

I doubt this is a problem in practice: One can always do if blah then decent_sSup else junk_value

[Yaël Dillies]

You could even wrap this into a constructor that requires the user to merely provide decent_sSup

[Pierre Quinton]

Yaël Dillies said:

You could even wrap this into a constructor that requires the user to merely provide decent_sSup

That would indeed be helpful, I might add this to ConditionallyCompleteLatticeindependently if it does not exist

[Pierre Quinton]

Okay then I will explore that direction. I am still unsure about naming, I would vouch for something like

• OmegaCompletePartialOrderSup is the equivalent of the current OmegaCompletePartialOrder
• OmegaCompletePartialOrderInf its dual notion with sInf
• OmegaCompletePartialOrder extends both classes above.

I think that doing this might be problematic for users that construct some OmegaCompletePartialOrder as they would need to provide the dual notion with sInf. But in any case they might lose ωSup so there will be some work for them.

[Aaron Liu]

Do we have a typeclass for (∃ x, IsLUB s x) → IsLUB s (sSup s) (and its dual)?

[Pierre Quinton]

Aaron Liu said:

Do we have a typeclass for (∃ x, IsLUB s x) → IsLUB s (sSup s) (and its dual)?

IMO we should, and any subclass of SupSet should inherit from it. I think this means that we should add this in SupSet. Also this would make the default constructor easy (and not depend on inhabited). I'm tempted to do a PR with that, any objection?

[Violeta Hernández]

I think this is a much better way to define sSup than what we have right now. So then a complete lattice is one where every set has LUB and GLB, a conditionally complete lattice is one where every bounded set has a LUB and GLB, and an omega complete lattice is one where every countable chain has LUB and GLB.

[Violeta Hernández]

And as a bonus we don't need ConditionallyCompleteLinearOrderBot as a separate structure! The condition sSup ∅ = bot follows directly from this typeclass + the existence of a bottom element.

[Violeta Hernández]

We can also have constructors that simply require proofs of existence for the LUB and GLB, and construct the sup/inf nonconstructively. In nearly all cases sSup and sInf are noncomputable anyways.

[Pierre Quinton]

All very nice indeed, I'm still unsure on how to proceed as SupSet is part of SetNotation, and I think this goes beyond set notations and deserves its own type class. But then we do need SupSet to define sSup to be able to define iSup in SetNotation, so I am not sure what is the best way to proceed.

[Violeta Hernández]

Yeah, this shouldn't be part of sSup, that typeclass should be purely notational. We can define a typeclass like e.g. LawfulSup with the condition IsLUB s x -> sSup s = x.

[Violeta Hernández]

I think that should initially go in a new file, and then we can work on subsequent PRs that redefine the existing lattice typeclasses to extend LawfulSup / LawfulInf.

[Violeta Hernández]

Tag me in these PRs and I'll be sure to review them!

[Violeta Hernández]

(deleted)

[Aaron Liu]

Violeta Hernández said:

Oh, I'm wrong about ConditionallyCompleteLinearOrderBot. The theorem sSup ∅ = bot just assigns a convenient junk value, it's not really a mathematical condition.

no?

[Aaron Liu]

We have IsLUB ∅ x ↔ IsBot x

[Violeta Hernández]

Oh

[Violeta Hernández]

You're right, it's sInf ∅ that doesn't exist

[Violeta Hernández]

The docstring is a bit misleading then, sSup ∅ = bot isn't a convention, it's a theorem!

[Aaron Liu]

But it's unfortunately not provable from the axioms of a ConditionallyCompleteLinearOrderBot

[Aaron Liu]

unless you add it in explicitly

[Aaron Liu]

which is what has been done here

[Violeta Hernández]

Yeah, but it is provable from the axiom of LawfulSup!

[Violeta Hernández]

So the typeclass will be redundant after the refactor

[Violeta Hernández]

And I'm glad! It's awful having to write it down

[Aaron Liu]

Violeta Hernández said:

Yeah, this shouldn't be part of sSup, that typeclass should be purely notational. We can define a typeclass like e.g. LawfulSup with the condition IsLUB s x -> sSup s = x.

This means LawfulSSup would not be preserved under order equivalences, which I don't like

[Aaron Liu]

I think instead we should have the slighly weaker version IsLUB s x -> IsLUB s (sSup x)

[Violeta Hernández]

Sure. The stronger version is satisfied by any partial order, anyways.

[Pierre Quinton]

A lot of results in CompleteLattice, ConditionallyCompleteLattice and later OmegaCompleteLattice are in essence the same result. They typically have a proof of existence of some sSup s, then it proves some fact and then the existence of a new sSup. As an example, if IsLUB s (sSup s) then for any a, we have IsLUB {a ⊔ b | b ∈ s } (a ⊔ (sSup s)), then we combine this fact with the a proof of the first to get the second one and finally a proof that {a ⊔ b | b ∈ s } has LUB sSup {a ⊔ b | b ∈ s }. The end result would prove sSup {a ⊔ b | b ∈ s } = a ⊔ sSup s given appropriate assumptions to prove the existence of both.

But if we work and the level of Lattice and we can provide sSup for any Lattice with a constructor of LawfulSup, then we can provide a proof of IsLUB s (sSup s) → IsLUB {a ⊔ b | b ∈ s } (a ⊔ (sSup s)). Then in all subclass we can use assumptions to deduce existence.

[Yaël Dillies]

Apologies if I am stating the obvious, but if you really are interested in rewriting complete lattices, have you thought of looking at how (co)complete categories are dealt with in mathlib?

[Pierre Quinton]

I know very little of category theory and have not started browsing the Category folder. If you have a good entry point, I would be glad to take it.

[Pierre Quinton]

In Lattice, we will get sSup s and sInf s whenever s is finite quite naturally. That's nice.

[Wrenna Robson]

I think this all sounds really good and I'm interested.

[Pierre Quinton]

In OmegaCompleteLattice, should we provide a constructor for a LawfulSupInf rather than extending it?

[Pierre Quinton]

In #27534 I have a problem:

open Classical in
noncomputable def Preorder.toLawfulSup [Preorder α] [Inhabited α] :
    LawfulSup α where
  sSup s := if hs : ∃ x, IsLUB s x then Classical.choose hs else default
  isLUB_sSup_of_exists_isLUB s := by
    intro ⟨x, hs⟩
    rw [dif_pos]
    exact Classical.choose_spec ⟨x, hs⟩

Seems to be fine, but adding a docstring in front of it makes the open unhapy:

unexpected token 'open'; expected 'lemma'

Note that this was not a problem with instance instead of def but it feels like this should work.

EDIT: This could be fixed by using:

/-- Defines `sSup` so as to return an arbitrary LUB when it exists, and a default element otherwise.
-/
-- open Classical in
noncomputable def Preorder.toLawfulSup [Preorder α] [Inhabited α]
    {_ : ∀ s : Set α, Decidable (∃ x, IsLUB s x)} : LawfulSup α where
  sSup s := if hs : ∃ x, IsLUB s x then Classical.choose hs else default
  isLUB_sSup_of_exists_isLUB s := by
    intro ⟨x, hs⟩
    rw [dif_pos]
    exact Classical.choose_spec ⟨x, hs⟩

It is also possible to have [∀ s : Set α, Decidable (∃ x, IsLUB s x)] but I think that the first one is prefered. Those two approaches make the def heavy, but would be trivial when using Classical.
Not sure what is preferable and if the previous behavior is wrong and should be reported.

[Aaron Liu]

You have to put the docstring after open

[Aaron Liu]

Since open ... in expands to a section ... end

[Violeta Hernández]

Decidability should be reserved to two circumstances:

• you need it for your statement to even type check
• you want computability

Here you're getting neither, so it's better to just use Classical.choice instead.

[Aaron Liu]

You can never have such a decidability hypothesis anyways since it would decide the halting problem

[Aaron Liu]

Just use classical

[Pierre Quinton]

Okay, so what is the next step here? @Violeta Hernández it feels like you had in mind changing axioms of all class that currently inherit from SupSet and InfSet to provide existential statements (and therefore not inheriting from SupSet and InfSet?). So for instance, in Conditionally CompleteLattice, we currently have this definition:

class ConditionallyCompleteLattice (α : Type*) extends Lattice α, SupSet α, InfSet α where
  /-- `a ≤ sSup s` for all `a ∈ s`. -/
  le_csSup : ∀ s a, BddAbove s → a ∈ s → a ≤ sSup s
  /-- `sSup s ≤ a` for all `a ∈ upperBounds s`. -/
  csSup_le : ∀ s a, Set.Nonempty s → a ∈ upperBounds s → sSup s ≤ a
  /-- `sInf s ≤ a` for all `a ∈ s`. -/
  csInf_le : ∀ s a, BddBelow s → a ∈ s → sInf s ≤ a
  /-- `a ≤ sInf s` for all `a ∈ lowerBounds s`. -/
  le_csInf : ∀ s a, Set.Nonempty s → a ∈ lowerBounds s → a ≤ sInf s

Now I think that le_csSup and csInf_le might now be irrelevant as we would want to prove that BddAbove implies that there exists an element above the set (trivial). Therefore I think this all can be simplified to

class ConditionallyCompleteLattice (α : Type*) extends Lattice α where
  exists_isLUB_of_nonempty_bounded : ∀ s, Set.Nonempty s → BddAbove s → ∃ a, IsLUB s a
  exists_isGLB_of_nonempty_bounded : ∀ s, Set.Nonempty s → BddAbove s → ∃ a, IsGLB s a

And then we can make a constructor for LawfulSupInf.

Is that an oversimplification?

[Yaël Dillies]

All you say makes sense to me

[Pierre Quinton]

some git question. If I branch the PR with Lawful stuff, as bors squashes the commits that I made, will there be any problem if I git rebase my branch on master later on? Or is there another way to do that?

[Yaël Dillies]

No, there will no problem. Personally my git commits look like

feat: first PR
some more
fix
fix
fix
bleh
feat: second PR
fix
whoops
fix
feat: third PR
etc...

Then when the first PR gets merged, I rebase the second PR onto master by dropping

feat: first PR
some more
fix
fix
fix
bleh

and then rebase the third PR onto the second PR's branch by dropping

feat: first PR
some more
fix
fix
fix
bleh

again.

[Pierre Quinton]

oh so when you rebase you do it interactively and you drop the commits, makes sense. Thanks!

[Yaël Dillies]

Yes, I was inspired by the "stacked diffs" philosophy. The workflow I just described above is seemingly the closest you get from true stacked diffs if you want to stick with github

[Pierre Quinton]

Most (if not all) of the csSup and csInf results in ConditionallyCompleteLattice will now take one of [LawfulSup α], [LawfulInf α] or [LawfulSupInf α]. In CompleteLattice, we can define an instance of LawfulSupInf α rather than a def as we do not need Classical. For this reason, I don't think we will need to condition the sSup and sInf results on the lawful results.

Some of the results in both of those can now be factorized in Latticeor even Preorder as if we condition on LawfulSup, we have e.g.

theorem le_sSup [Preorder α] [LawfulSup α] {s : Set α} {a : α} (hs : ∃ b, IsLUB s b) (ha : a ∈ s) :
    a ≤ sSup s :=
  sorry

I am not certain that those results are important, but maybe results that are more involved proofwise will be useful to factorize some proofs from all Complete kind of partial orders (CompleteLattice, ConditionallyCompleteLattice, OmegaCompletePartialOrder, ComplettePartialOrder, etc..).

[Pierre Quinton]

For the last part, it is probably better to have hs : IsLUB s (sSup s) rather than hs : ∃ b, IsLUB s b as the former does not necessitate Classical and both are equivalent under LawfulSup

[Aaron Liu]

Pierre Quinton said:

For the last part, it is probably better to have hs : IsLUB s (sSup s) rather than hs : ∃ b, IsLUB s b as the former does not necessitate Classical and both are equivalent under LawfulSup

what?

[Aaron Liu]

can you give an example?

[Pierre Quinton]

Sorry, that's astupid mistake

[Violeta Hernández]

Pierre Quinton said:

Okay, so what is the next step here? Violeta Hernández it feels like you had in mind changing axioms of all class that currently inherit from SupSet and InfSet to provide existential statements (and therefore not inheriting from SupSet and InfSet?).

I think the lattice classes should extend SupInfSet as well. They would not provide any extra information, mathematically, but I think most people would expect that CompleteLattice α should enable sSup and sInf.

[Violeta Hernández]

Pierre Quinton said:

Some of the results in both of those can now be factorized in Latticeor even Preorder as if we condition on LawfulSup

I think you can build the API like this. First, take all of the basic results on suprema/infima that are provable on LawfulSup/LawfulInfand prove them there. All of the most basic stuff like le_sSup, lt_sSup_iff, etc. should have a LawfulSup version, for instance. Then prove the results for conditional/complete/etc. lattices as special cases of these.

We probably need to find better names for the LawfulSup/LawfulInf theorems, so that they don't clash with the theorems on conditional lattices. I propose le_lsSup (where the l stands for lawful, kind of like the c in le_csSup stands for conditional). It's not pretty, but I find it preferable to spamming primes.

[Pierre Quinton]

How about using namespaces?

[Violeta Hernández]

Hm. Is there ever a situation where we'd want to use the lawful theorems over the more specific theorems for different kinds of lattices?

[Violeta Hernández]

I imagine that won't be a very common occurence, save for when we're proving the more specific theorems themselves.

[Pierre Quinton]

I don't think so but then this is a good reason to put them in a namespace right?

[Violeta Hernández]

I guess we could put everything in a LawfulSupInf namespace.

[Pierre Quinton]

BTW, I feel weird about having supset and infset in lattices

[Pierre Quinton]

Especially if they don't give meaning to the symbols

[Violeta Hernández]

In lattices? Yeah we shouldn't have them in lattices, but in complete lattices!

[Violeta Hernández]

I think I misspoke

[Pierre Quinton]

No I got that, subtypes of lattice that have some logic on sups and infs

[Pierre Quinton]

The thing is, if we use existantial definitions, for instqnce in complete lattice, every set has a LUB, then sSup is not constrained at all

[Violeta Hernández]

I mean, we wouldn't just have SupSet.

[Violeta Hernández]

Maybe I misread what you said earlier. What I mean is that complete/conditionally complete/omega complete lattices should all inherit from LawfulSup and LawfulInf.

[Pierre Quinton]

So we would have that sSup s is the LUB of s?

[Pierre Quinton]

My bad

[Pierre Quinton]

Okay I get it, but still feels weird as this will typically force people to use Classical

[Pierre Quinton]

(which is typically the case anyway)

[Violeta Hernández]

Mathlib is by and large a library for classical logic. And nearly all instances of complete lattices are noncomputable/defined through choice, anyways.

[Violeta Hernández]

(in fact, you can't compute a supremum or infimum except for trivial cases, since the type Set α = α → Prop carries no meaningful data)

[Pierre Quinton]

Right, but it makes sense to avoid it if it doesn't make the structure anoying. In any case I don't see a good way to avoid it.

[Violeta Hernández]

I disagree. If CompleteLattice didn't extend LawfulSupInf the vast majority of theorems would have to write [CompleteLattice α] [LawfulSupInf α], which benefits no one.

[Pierre Quinton]

Violeta Hernández said:

(in fact, you can't compute a supremum or infimum except for trivial cases, since the type Set α = α → Prop carries no meaningful data)

Yeah I think you are right, even if you had a sigma algebra, then knowing when a collection of measurable sets has measurable union is not possible.

[Pierre Quinton]

Violeta Hernández said:

I disagree. If CompleteLattice didn't extend LawfulSupInf the vast majority of theorems would have to write [CompleteLattice α] [LawfulSupInf α], which benefits no one.

Agreed

[Violeta Hernández]

As a maybe analogous example, docs#Ring extends docs#NatCast even though you can define the map ℕ → R using the other data provided.

[Violeta Hernández]

In that case it's more about giving nice definitional equalities, but the point of "sometimes it's fine to have redundant data" stands.

[Wrenna Robson]

So what is the currently planned design? Could you recap?

[Wrenna Robson]

Just been reading up :)

[Violeta Hernández]

Basically, the plan is to redefine the complete/conditional/omega lattice types. We defined a new typeclass LawfulInfSup which states that IsLUB s x -> IsLUB s (sSup s), and likewise for the infimum. Then, instead of the lattice typeclasses placing different constraints on Sup and Inf, they'd inherit from this typeclass, and place constraints on which sets have a LUB/GLB.

[Violeta Hernández]

This has various nice side effects, with the one I'm happiest about being the overly verbose docs#ConditionallyCompleteLinearOrderBot now getting subsumed by it's slightly slimmer sibling docs#ConditionallyCompleteLinearOrder

[Violeta Hernández]

(the sSup ∅ = bot condition follows from OrderBot + LawfulSup)

[Wrenna Robson]

I assume you mean IsLUB s x -> IsLUB s (sSup s) instead.

[Violeta Hernández]

Whoops

[Wrenna Robson]

It might get odd if you're not in a partial order (as then you can have multiple LUBs than aren't equal I think?)

[Violeta Hernández]

All the types we care about are partial orders. I think this definition was chosen for generalizing slightly better to preorders.

[Aaron Liu]

Wrenna Robson said:

It might get odd if you're not in a partial order (as then you can have multiple LUBs than aren't equal I think?)

There is another version that was proposed IsLUB s x -> sSup s = x and I objected because this one implies partial order and therefore is evil from a category theory point of view

[Yaël Dillies]

Stupid question: Why keep sSup as notation? Wouldn't it be better to define sSup s := if h : \exists x, IsLUB s x then h.choose else Classical.arbitrary? My reasoning is that defeqs for sSup/iSup are actually always bad, and therefore it's not a loss to throw them away.

[Yaël Dillies]

What I mean by bad defeq is for example that sSup/iSup don't commute definitionally with projections from a product or pi type. And generally I've never seen them commute definitionally with anything interesting

[Violeta Hernández]

Counterpoint: we want sSup on sets to be def-eq to the union.

[Violeta Hernández]

(and presumably you can make sSup x = ∅ def-eq for an empty type, which is at least something)

[Pierre Quinton]

There seem to be three possibilities, each with pros and cons, I might be missing a fourth that is a strict improvement over all three:
1) Have sSup s defined as if h : \exists x, IsLUB s x then h.choose else Classical.arbitrary. Con: No def-eq for unions of sets.
2) Have some PartialOrders inherit from Lawful such as Complete*, OmegaComplete*, ConditionallyComplete*. Con: If this is a good idea, then why is it a bad idea to have all PartialOrder inherit from Lawful stuff? For instance Lattice is in essence a FinitelyCompleteLattice where we can prove that sSup is well defined on finite collections, so I think this would require us to justify what makes an order inherit lawfulsupinf or not.
3) Have some PartialOrders (same as in 2) provide proof of existence of LUB and provide constructors to build lawful orders from those (def for all, instance for CompleteLattice). Con: We would have to carry some [LawfulSup α], [LawfulInf α] or [LawfulSupInf α] around. Maybe this approach also breaks def-eq?

It would be nice to settle this before proceeding.

[Violeta Hernández]

I'd rather go with 2.

[Violeta Hernández]

As for why lattices don't use Sup, I think that's just the max/sup argument again. We have some amount of duplication, but not enough to warrant going against mathematical convention.

[Violeta Hernández]

(in any case, if we wanted, we could prove Sup s = Finset.sup s for finite sets in a LawfulSupInf lattice)

[Pierre Quinton]

So if I understand you correctly, the role of those complete (or partially complete) type classes are to provide sSup and/or sInf operations and so they should inherit from lawful. If we want to have say a FinitelyCompleteLattice, then we could make it inherit from Lattice and LawfulSupInf and provide meaningful definition to sSup s and sInf s when s is finite?

[Violeta Hernández]

Yes to the first part, though I don't really think we'll ever need FinitelyCompleteLattice.

[Aaron Liu]

Would [FinitelyCompleteLattice α] be equivalent to [Lattice α] or [Lattice α] [BoundedOrder α]?

[Violeta Hernández]

Good question

[Aaron Liu]

empty sets are certainly finite

[Pierre Quinton]

Violeta Hernández said:

Yes to the first part, though I don't really think we'll ever need FinitelyCompleteLattice.

me neither, but it is an example of things that we should be able to decide on.

[Pierre Quinton]

Aaron Liu said:

Would [FinitelyCompleteLattice α] be equivalent to [Lattice α] or [Lattice α] [BoundedOrder α]?

Like OmegaComplete I guess it must be bounded.

[Violeta Hernández]

I like the idea of continuing to use Sup where we already use it, and not introduce it elsewhere, at least not until a subsequent refactor

[Pierre Quinton]

I like it too. Are there any other strong opinions?

[Yaël Dillies]

And the reason I pointed out category theory earlier

Violeta Hernández said:

Counterpoint: we want sSup on sets to be def-eq to the union.

But how do you define sUnion? Why can't it be the same definition as sSup?

[Yaël Dillies]

Violeta Hernández said:

As for why lattices don't use Sup, I think that's just the max/sup argument again. We have some amount of duplication, but not enough to warrant going against mathematical convention.

I actually think the refactor we're discussing here would be a great opportunity to get rid of all the clutter around Finset.sup, Finset.sup', Finset.max. I think the definitions can stay, for computation, but the API could be transferred to sSup of a finite set, meaning that we could finally use the \Sup notation

[Aaron Liu]

Yaël Dillies said:

And the reason I pointed out category theory earlier

Violeta Hernández said:

Counterpoint: we want sSup on sets to be def-eq to the union.

But how do you define sUnion? Why can't it be the same definition as sSup?

We want x ∈ ⋃₀ S to be defeq to ∃ s ∈ S, x ∈ s

[Aaron Liu]

for sets

[Yaël Dillies]

I get the point, but x \in iUnion f is already not defeq to \exists i, x \in f i. How do you explain this disconnect to a beginner?

[Aaron Liu]

it's still something you can rintro or obtain and get a nice goal state out of

[Aaron Liu]

I use this a lot

[Aaron Liu]

finsets are more difficult

[Pierre Quinton]

Is ∃ a fundamental of the language or is it defined somewhere? (Just out of curiosity)

[Aaron Liu]

docs#Exists

[Violeta Hernández]

Yaël Dillies said:

I get the point, but x \in iUnion f is already not defeq to \exists i, x \in f i. How do you explain this disconnect to a beginner?

It isn't? How come?

[Violeta Hernández]

I think the point still stands though. Surely we at the very least want the supremum of say, subgroups, to be def-eq to the supremum of sets?

[Violeta Hernández]

Again, this all reminds me of NatCast, which can always be defined for certain structures, but which can often be defined nicely.

[Aaron Liu]

Violeta Hernández said:

Yaël Dillies said:

I get the point, but x \in iUnion f is already not defeq to \exists i, x \in f i. How do you explain this disconnect to a beginner?

It isn't? How come?

It's defeq to ∃ s ∈ Set.range f, x ∈ s, which is the same as ∃ s, (∃ i, f i = s) ∧ x ∈ s.

[Aaron Liu]

Violeta Hernández said:

I think the point still stands though. Surely we at the very least want the supremum of say, subgroups, to be def-eq to the supremum of sets?

Unfortunately they're not even propositionally equal, so I don't know how you plan to make them defeq.

[Violeta Hernández]

Aaron Liu said:

Violeta Hernández said:

I think the point still stands though. Surely we at the very least want the supremum of say, subgroups, to be def-eq to the supremum of sets?

Unfortunately they're not even propositionally equal, so I don't know how you plan to make them defeq.

Sorry, not the supremum, the infimum

[Pierre Quinton]

Yaël Dillies said:

Stupid question: Why keep sSup as notation? Wouldn't it be better to define sSup s := if h : \exists x, IsLUB s x then h.choose else Classical.arbitrary? My reasoning is that defeqs for sSup/iSup are actually always bad, and therefore it's not a loss to throw them away.

I think that this is actually orthogonal to some of the steps that @Violeta Hernández was suggesting. This idea would just have an impact on the proofs that we provide but not on the structure that we are building. If I am right about this, then we can proceed with refactoring some of the Complete orders classes. We could then have a discussion once this is done, I think we will have better information and understanding at that time.

[Violeta Hernández]

I agree. I'm not entirely opposed to that refactor, but we should do things one step at a time.

[Pierre Quinton]

@Violeta Hernández I added some OrderDual material to the PR if you want to take a look. I realized that CompleteLattice.lean was the place where the dual of SupSet and InfSet were defined, now LawfulSupInf takes that responsibility.

[Pierre Quinton]

In terms of theorems for Lawful orders, what do you think of having namespace of the type class with the least assumptions needed to prove things? Let me illustrate, we could have in LawfulSupInf.lean the following:

variable {s : Set α} {a : α}

namespace Preorder

theorem isLUB_sSup [LawfulSup α] (hs : ∃ b, IsLUB s b) : IsLUB s (sSup s) :=
  LawfulSup.isLUB_sSup_of_exists_isLUB s hs

theorem isGLB_sInf [LawfulInf α] (hs : ∃ b, IsGLB s b) : IsGLB s (sInf s) :=
  isLUB_sSup (α := αᵒᵈ) hs

theorem le_sSup [LawfulSup α] (hs : ∃ b, IsLUB s b) (ha : a ∈ s) : a ≤ sSup s :=
  (isLUB_sSup hs).1 ha

theorem sInf_le [LawfulInf α] (hs : ∃ b, IsGLB s b) (ha : a ∈ s) : sInf s ≤ a :=
  le_sSup (α := αᵒᵈ) hs ha

theorem sSup_le [LawfulSup α] (hs : ∃ b, IsLUB s b) (ha : ∀ b ∈ s, b ≤ a) : sSup s ≤ a :=
  (isLUB_sSup hs).2 ha

theorem le_sInf [LawfulInf α] (hs : ∃ b, IsGLB s b) (ha : ∀ b ∈ s, a ≤ b) : a ≤ sInf s :=
  sSup_le (α := αᵒᵈ) hs ha

end Preorder

namespace PartialOrder

variable [PartialOrder α]

theorem sSup_eq_of_isLUB [LawfulSup α] (hs : IsLUB s a) : sSup s = a :=
  IsLUB.unique (Preorder.isLUB_sSup ⟨a, hs⟩) hs

theorem sInf_eq_of_isGLB [LawfulInf α] (hs : IsGLB s a) : sInf s = a :=
  sSup_eq_of_isLUB (α := αᵒᵈ) hs

end PartialOrder

So all results that are always provable go in the namespace Preorder, then if we need PartialOrder, it goes in there, then we can have Lattice and all sort of namespace we would like.

[Wrenna Robson]

Hmm. I am not sure it's usual to use namespaces rather than sections here.

[Pierre Quinton]

Yes but the problem is that we can have many theorems with the same name as we will adapt the conditions, for instance isLUB_sSup is in CompleteLattice, isLUB_csSup is in ConditionallyCompleteLattice, etc...

[Wrenna Robson]

Ah I see the issue.

[Wrenna Robson]

Yes good point.

[Pierre Quinton]

My thinking is that LawfulSupInf is in some sense private content that helps structure all those type classes that are public, but I don't think that a user would use them directly.

[Violeta Hernández]

It's an interesting idea, though why not just have everything in a LawfulSup/LawfulInf/LawfulSupInf namespace?

[Pierre Quinton]

It would look something like this:

variable {s : Set α} {a b : α}

namespace LawfulSup

variable [LawfulSup α]

theorem isLUB_sSup (hs : IsLUB s a) : IsLUB s (sSup s) :=
  LawfulSup.isLUB_sSup_of_exists_isLUB s ⟨a, hs⟩

theorem le_sSup (hs : IsLUB s b) (ha : a ∈ s) : a ≤ sSup s :=
  (isLUB_sSup hs).1 ha

theorem sSup_le (hs : IsLUB s b) (ha : ∀ c ∈ s, c ≤ a) : sSup s ≤ a :=
  (isLUB_sSup hs).2 ha

theorem sSup_eq_of_isLUB [PartialOrder α] (hs : IsLUB s a) : sSup s = a :=
  (isLUB_sSup hs).unique hs

end LawfulSup

namespace LawfulInf

variable [LawfulInf α]

theorem isGLB_sInf (hs : IsGLB s b) : IsGLB s (sInf s) :=
  LawfulSup.isLUB_sSup (α := αᵒᵈ) hs

theorem sInf_le (hs : IsGLB s b) (ha : a ∈ s) : sInf s ≤ a :=
  LawfulSup.le_sSup (α := αᵒᵈ) hs ha

theorem le_sInf (hs : IsGLB s b) (ha : ∀ c ∈ s, a ≤ c) : a ≤ sInf s :=
  LawfulSup.sSup_le (α := αᵒᵈ) hs ha

theorem sInf_eq_of_isGLB [PartialOrder α] (hs : IsGLB s a) : sInf s = a :=
  LawfulSup.sSup_eq_of_isLUB (α := αᵒᵈ) hs

end LawfulInf

namespace LawfulSupInf

variable [LawfulSupInf α]

theorem sInf_le_sSup (hs : s.Nonempty) (ha : IsGLB s a) (hb : IsLUB s b) :
    sInf s ≤ sSup s :=
  isGLB_le_isLUB (LawfulInf.isGLB_sInf ha) (LawfulSup.isLUB_sSup hb) hs

end LawfulSupInf

I like it too.

[Wrenna Robson]

Normally I don't think we tend to have hypotheses of the form hs : ∃ b, IsGLB s b, because this can be replaced by {b} (hs : IsGLB s b) which is somehow more natural.

[Pierre Quinton]

Makes sense, it is better

[Wrenna Robson]

i.e. implicitly we use exists_imp.

[Wrenna Robson]

Basically you prove the exists by providing a witness.

[Pierre Quinton]

Now I think that we need to think hard about what we should do about iSup results. The first one I have encountered in CompleteLattice.Defs while working on translating the old way to the new is this one:

theorem le_iSup_iff {s : ι → α} : a ≤ iSup s ↔ ∀ b, (∀ i, s i ≤ b) → a ≤ b := by
  simp [iSup, le_sSup_iff, upperBounds]

The only way that we have to prove this in LawfulSup is by assuming that the range of s has a LUB. This is doable but is rather different from the condition I had in mind for OmegaCompleteLattice that ι is Countable.

Any thoughts are welcome.

[Aaron Liu]

well countable sets have least upper bound in omega complete lattice and docs#Set.countable_range will say your range is countable

[Pierre Quinton]

I know, but it gets very nasty with iSup2 results

[Aaron Liu]

oh ok

[Pierre Quinton]

Sorry, let me rephrase, I think we should discuss about iSup₂ results such as

theorem le_iSup₂ {f : ∀ i, κ i → α} (i : ι) (j : κ i) : f i j ≤ ⨆ (i) (j), f i j :=
  sorry

It might be annoying to require as an assumption that for all i, the range of f i has a LUB. We clearly can't have assumptions on κ or ι. For most of those results, it would be enough to have a condition on the existence of a LUB of {f i j | (i : ι) (j : κ i)}, but maybe this would make most of those results useless.

[Pierre Quinton]

Actually, I think it makes sense to have ```
{f : ∀ i, κ i → α} {g : ι → α} (h₁ : ∀ i, IsLUB (Set.range (f i)) (g i)) (h₂ : IsLUB (Set.range g) a)

And to leave the responsibility of proving those to the instances, especially since the proof will typically be the same for all theorems involving `iSup₂`.

[Violeta Hernández]

@Yaël Dillies could you elaborate on what you were saying about secret suprema?

[Violeta Hernández]

I don't really get what the problem you're talking about is

[Yaël Dillies]

Say you want to deduce results about OmegaCompletePartialOrder from LawfulSupInf: You cannot, as there are possibly sets which are not chains or not countable that have suprema anyway

[Violeta Hernández]

Why is that an issue? Results on LawfulSupInf would presumably be of the form "if this set has a LUB/GLB, then X". Results on OmegaCompletePartialOrder would look like "for every countable chain, then X". Since every countable chain has a LUB/GLB, the result would follow from the LawfulSupInf version.

[Violeta Hernández]

If some other set happens to have a supremum that isn't accounted for by the typeclass assumptions, then yeah, the typeclass assumptions won't say anything about it. LawfulSupInf might, though.

[Yaël Dillies]

So now you're suggesting to not prove anything about OmegaCompletePartialOrder but instead OmegaCompletePartialOrder + LawfulSupInf? That's strictly less general of course, and I do not know how you will instantiate this combo of typeclasses in practice, except by taking the sSup s := if hs : ∃ b, IsGLB s b then hs.choose else junk approach I explained above

[Violeta Hernández]

I thought the idea was to make the existing typeclasses extend LawfulSupInf.

[Yaël Dillies]

Yes then again I do not know how you will instantiate them except for my approach to defining sSup

[Violeta Hernández]

That will be by far the most common approach to instantiate them, that's true. But as I mentioned earlier I do think there's some situations where you can have nice def-eqs, and I think we should preserve that.

[Pierre Quinton]

Would instances with proper priority solve part of our dilemma? If we have a low priority instance for @Yaël Dillies construction of ssup and higher one for say powerset?

[Yaël Dillies]

Tweaking priorities doesn't solve diamonds sadly, so no

[Violeta Hernández]

I have a very good reason to not define sSup through choice - we lose the def-eqs between sSup on an order and sInf on the order dual, and viceversa. oh nevermind, I think we would still have that, actually

[Kenny Lau]

how else would you define sSup, the fact that you're pulling data from Prop means that you require choice

[Kenny Lau]

(oops, I just realised that I have completely no idea of the context of this discussion)

[Pierre Quinton]

@Yaël Dillies I am currently rather stuck on this matter. I think I'm missing a point and maybe you can help me. What would be the main advantages of having defined sSup in the way you suggest? You mentioned on github that in the case of an OmegaCompleteLattice that is actually complete, we could not deduce LawfulSup for all elements of the family from the axioms of OmegaCompleteLattice only. But still, if we make OmegaCompleteLattice satisfy LawfulSup, then the user defined sSup must be a LUB whenever there exists one. So for a coutnable collection, you can deduce facts by combining existence from OmegaCompleteLattice and facts from IsLawfulSup. But still, if you have for instance the collection of all elements of your lattice, then you can deduce that its sSup is the maximal element by using IsLawfulSup right?
Am I missing something?

[Jozef Mikušinec]

Aaron Liu said:

Violeta Hernández said:

Yaël Dillies said:

I get the point, but x \in iUnion f is already not defeq to \exists i, x \in f i. How do you explain this disconnect to a beginner?

It isn't? How come?

It's defeq to ∃ s ∈ Set.range f, x ∈ s, which is the same as ∃ s, (∃ i, f i = s) ∧ x ∈ s.

Sorry if I'm taking this discussion a bit off topic (I find the thread hard to follow), but wouldn't it be better to use ∃ i, x ∈ f i for iUnion and iSup? I find the current definition quite clumsy and don't see any advantages.

[Yaël Dillies]

The advantage is that it's defeq to docs#iSup, and therefore you can use results about iSup when proving results about docs#Set.iUnion.