Zulip Chat Archive

Stream: mathlib4

Topic: Specific typeclasses alternative

Martin Dvořák (Oct 01 2023 at 06:33):

I would like to have a nontrivial alternative to LinearOrderedAddCommMonoid + CompleteLattice, i.e., some typeclasses A and B such that:

(LinearOrderedAddCommMonoid + CompleteLattice ≤ A + B) ∧
( ¬(LinearOrderedAddCommMonoid ≤ A) ∨ ¬(CompleteLattice ≤ B) )

Do you know about anything? You can use more than two typeclasses if it makes sense.

Yaël Dillies (Oct 01 2023 at 06:35):

Hmm, what's the motivation?

Martin Dvořák (Oct 01 2023 at 06:36):

#7404

Yaël Dillies (Oct 03 2023 at 18:50):

And in words?

Martin Dvořák (Oct 03 2023 at 19:39):

The objective is to minimize functions D^n → C where [LinearOrderedAddCommMonoid C] and D can be anything.
In this general setting, the infimum lies in WithTop (WithBot C).
If we have[Inhabited D] then we can search for the infimum in WithBot C.
If we furthermore restrict D to be a finite type or to "behave" as a finite set, we can search for the infimum in C.
The function for infimum of a Set that you recommended me
https://github.com/leanprover-community/mathlib4/blob/68c7277eb809a743588fe39cd21737944bf8e6c6/Mathlib/Order/CompleteLattice.lean#L61-L62
requires [CompleteLattice C] so I didn't even try to incorporate the additional assumptions into my definition.
However, I would like to refine my definition a bit.
As a start, cannot I just enhance [LinearOrderedAddCommMonoid C] with [HasTop C] and [HasBot C] and ask for the infimum on C itself, without going for the [CompleteLattice C] overkill?

Yaël Dillies (Oct 03 2023 at 19:47):

Are you looking for docs#LinearOrderedAddCommMonoidWithTop

Martin Dvořák (Oct 03 2023 at 19:52):

It seems that we don't have docs#LinearOrderedAddCommMonoidWithBot sadly. The latter would actually be useful — I don't mind restricting the main definition to nonempty domains, but restricting it to finite domains might be premature here. At the same, I don't feel like rephrasing everything to maximization just because a certain typeclass exists in Mathlib. Would you approve adding the complementary typeclass to Mathlib if I PRed it?

Yaël Dillies (Oct 03 2023 at 19:55):

I mean, what typeclasses would you instantiate it with?

Martin Dvořák (Oct 03 2023 at 19:56):

You mean what structures would satisfy it?

Martin Dvořák (Oct 03 2023 at 20:10):

Nat? NNRat? NNReal?

Have I overlooked an issue there?

Yaël Dillies (Oct 03 2023 at 20:21):

Then maybe you rather want docs#CanonicallyOrderedAddMonoid ?

Martin Dvořák (Oct 03 2023 at 20:30):

Did you mean docs#CanonicallyLinearOrderedAddMonoid ?

Yaël Dillies (Oct 03 2023 at 20:32):

or docs#CanonicallyOrderedSemiring, whichever one is best for you

Martin Dvořák (Oct 03 2023 at 20:53):

If I understand it right, the existing docs#CanonicallyLinearOrderedAddMonoid is basically the non-existing docs#LinearOrderedAddCommMonoidWithBot with the additional assumption that ⊥ is the neutral element.

Bolton Bailey (Oct 04 2023 at 02:11):

As I recall the rationale is that we don't want changes to the simp set to potentially break untouched files. Is it possible for a nonterminal simp like this which is immediately closed by rfl to do so?

Sorry wrong thread

Martin Dvořák (Oct 04 2023 at 07:05):

CanonicallyLinearOrderedAddMonoid is commutative and total, but conversion to LinearOrderedAddCommMonoid is missing. Why?

Yaël Dillies (Oct 04 2023 at 07:07):

Indeed. That's just an oversight.

Martin Dvořák (Oct 04 2023 at 07:07):

If I PR it, will you approve it?

Martin Dvořák (Oct 04 2023 at 07:09):

When we are at it, is it intentional that "Comm" is no longer a part of its name?

Yaël Dillies (Oct 04 2023 at 07:11):

Not really. This small corner of the library is a bit of a mess because there are very little concrete types we care about that instantiate those typeclasses.

Martin Dvořák (Oct 04 2023 at 07:12):

Can I rename it in the same PR?

Martin Dvořák (Oct 04 2023 at 07:37):

When looking at the diff (wip), I'll rather do it as two PRs.

Martin Dvořák (Oct 04 2023 at 16:13):

First the renaming: @Yaël Dillies
https://github.com/leanprover-community/mathlib4/pull/7503

Martin Dvořák (Oct 04 2023 at 18:11):

Martin Dvořák said:

Did you mean docs#CanonicallyLinearOrderedAddMonoid ?

Would it be possible to derive [InfSet C] from [CanonicallyLinearOrderedAddMonoid C] if I added some canonical conversions?

Martin Dvořák (Oct 04 2023 at 18:13):

Or maybe [InfSet (WithTop C)] to account for infimum of the empty set...

Yaël Dillies (Oct 04 2023 at 18:17):

No, because

  1. How would you do it? NNRat is a CanonicallyLinearOrderedAddMonoid but not a conditionally complete lattice.
  2. That would be constructing data out of a hat, which is bad.

Martin Dvořák (Oct 04 2023 at 18:26):

Yeah (1) was stupid. I still don't know what's wrong with (2).

Martin Dvořák (Oct 04 2023 at 18:32):

Is there any notion of "infimum of nonempty set" in Mathlib that would require only LinearOrder and Bot please?

Martin Dvořák (Oct 04 2023 at 18:48):

It seems that sInf and iInf require more (InfSet in particular) because they need to allow for an infimum over the empty set / function from empty domain. I would be fine with having to prove that every infimum is for a non-empty set; I would like to relax the typeclass requirements.

Martin Dvořák (Oct 04 2023 at 18:53):

Is the InfSet even tied to the operations on given type?

Yaël Dillies (Oct 04 2023 at 19:11):

The infimum of a set is a purely order theoretic operation, if that's what you're asking

Yaël Dillies (Oct 04 2023 at 19:13):

Martin Dvořák said:

Is there any notion of "infimum of nonempty set" in Mathlib that would require only LinearOrder and Bot please?

That's nonsense. Most linear orders don't have infima.

Martin Dvořák (Oct 04 2023 at 19:27):

Bot would be the infimum of the "full set".

Yaël Dillies (Oct 04 2023 at 19:34):

Okay but what's the infimum of {x : NNRat | x^2 > 2}?

Martin Dvořák (Oct 04 2023 at 19:46):

Yaël Dillies said:

Okay but what's the infimum of {x : NNRat | x^2 > 2}?

Yeah, it was really stupid of me...

Martin Dvořák (Oct 04 2023 at 19:48):

If I have both [InfSet C] and [CanonicallyLinearOrderedAddMonoid C], are InfSet.sInf and CanonicallyLinearOrderedAddMonoid.min guaranteed behave consistently with each other?

Yaël Dillies (Oct 04 2023 at 20:12):

InfSet is just a notation typeclass, so no.

Martin Dvořák (Oct 04 2023 at 20:25):

I think I need to get back to my original question but better.

I have [LinearOrderedAddCommMonoid C]. What is the least additional assumption that will allow me to consider (needn't be computable) infimum of any nonempty Set C such that the infimum will respect the LinearOrderedAddCommMonoid.le please?

Yaël Dillies (Oct 04 2023 at 21:18):

What concrete structures do you care about?

Martin Dvořák (Oct 05 2023 at 10:05):

Martin Dvořák said:

When looking at the diff (wip), I'll rather do it as two PRs.

Second: #7515

Martin Dvořák (Oct 06 2023 at 14:35):

Yaël Dillies said:

What concrete structures do you care about?

I changed my mind about what I want:
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Minimum.20of.20a.20finite.20set

Last updated: Dec 20 2023 at 11:08 UTC