RFC: bundled sets #6442

Stream: mathlib4

[Yury G. Kudryashov]

In #6442, I started implementing #2202 for sets (not maps yet). Generic definitions are in Data/BundledSet/*. I adjusted parts of docs#Subsemigroup to the new API, then stopped for now. Before I put more work into this, I would prefer to get some feedback about design choices.

[Eric Wieser]

I'm not yet convinced that things like

class BotPred (α : Type*) (p : Set α → Prop) (b : outParam (Set α)) : Prop where
  bot : p b
  bot_subset {t} : p t → b ⊆ t

are the right design, and am a bit worried about asking Lean to find a typeclass indexed by a function type. But I need to think about this more probably

[Yury G. Kudryashov]

Note that p will be always something like IsSubsemigroup or IsOpen, not something you can unfold.

[Eric Wieser]

I do think that the part of your design that changes

structure Submonoid where
   carrier : Set M
   one_mem : 1 \mem carrier

to something analogous to

structure Submonoid where
   carrier : Set M
   isSubmonoid : IsSubmonoid carrier

is a good idea (in particularly, that design works much better with @Tomas Skrivan's fprop-like tactics than what we have today)

[Eric Wieser]

I don't know if it's worth trying to go through this intermediate state first

[Yury G. Kudryashov]

There is an exception for instances designed to automatically prove SetInterPred for algebraic subobjects but we can move them to a deriving handler.

[Yury G. Kudryashov]

Do you suggest

structure Submonoid where
  carrier : Set M
  isSubmonoid : IsSubmonoid carrier

as you write above or

structure BundledSet (α : Type*) (p : Set α → Prop) where
  carrier : Set α
  prop : p carrier

@[to_additive (attr := reducible)]
def Submonoid (M : Type*) [OneMulClass M] := BundledSet M IsSubmonoid

as I use?

[Yury G. Kudryashov]

With my approach, you can prove generic theorems like mem_weaken or weaken_weaken that argue about different predicates.

[Eric Wieser]

I think your version is a more ambitious version of what I write above, and as such comes with more potential pitfalls to think about.

[Yury G. Kudryashov]

That's why I decided to take a pause and ask for feedback.

[Eric Wieser]

Note that for my suggestion above to work with dot notation, you actually need to write

import Mathlib

namespace Zulip

structure WithCarrier (α : Type _) where
  carrier : Set α

structure IsSubmonoid {α : Type _} [Monoid α] (s : Set α) where
  one_mem : 1 ∈ s
  mul_mem {x y} : x ∈ s → y ∈ s → x * y ∈ s

-- `WithCarrier` is a hack to make `mul_mem` dot notation work;
-- we need the `IsSubmonoid ` to be seen as a parent structure,
-- not just a field; and so `carrier` needs to come before the extends
structure Submonoid (M : Type*) [Monoid M] extends WithCarrier M, IsSubmonoid carrier

variable (M : Type*) [Monoid M] (S : Submonoid M)

#check S.mul_mem  -- works

[Yury G. Kudryashov]

My goal is to replace docs#SetLike with a single structure and docs#MulMemClass etc with [BundledSet.Implies _ _] so that we can have generic theorems and don't search for SetLike every time.

[Eric Wieser]

The main concern I have right now is that this doesn't work for things like SetLike Finset (which admittedly I think we currently don't use); or in general, any set-like objects that carry extra computational data

[Eric Wieser]

But you should take my comments above as skepticism/hesitation, and not as an objection

[Yury G. Kudryashov]

I think that having common data for all algebraic subobjects is already a big improvement.

[Yury G. Kudryashov]

My goal is to have it for algebra and topology.

[Yury G. Kudryashov]

Indeed, Finset won't fit this scheme.

[Yury G. Kudryashov]

This issue becomes more important for functions because we want to cover Equivs.

[Yury G. Kudryashov]

I'm OK with having a common structure for *Hom and a different structure for Finsupp but I want to have map_add that works for Homs and Equivs.

[Yury G. Kudryashov]

Of course, this is what I am OK with. I will need to convince more people to push this change.

[Yury G. Kudryashov]

I think that this is a sufficiently large and important refactor to tag all @maintainers here.

[Anne Baanen]

I'm excited to see you take this forward! Finding a uniform representation is a good step towards taming the complexity of the current subobject setup.

[Anne Baanen]

Yury G. Kudryashov said:

so that we can have generic theorems and don't search for SetLike every time.

Is this really an issue in Lean 4? As far as I can tell, since there are very few classes extending SetLike (I believe the actual number is 0) and everything is handled with "unbundled inheritance", keyed matching will reject most instances almost directly. That is the main motivation for #8386.

[Anne Baanen]

Eric Wieser said:

The main concern I have right now is that this doesn't work for things like SetLike Finset (which admittedly I think we currently don't use); or in general, any set-like objects that carry extra computational data

This could be fixed by relaxing the predicate from Set α → Prop to Set α → Sort*. Although I suppose we'd lose the properties deriving from SetLike.coe_injective. So maybe it should look like:

structure BundledSet (α : Type*) (p : Set α → Sort*) [∀ x, Subsingleton (p x)] where
  carrier : Set α
  prop : p carrier

(I can't say if the typeclass system would work well with the ∀, or whether we should have an EverywhereSubsingleton p := ∀ x, Subsingleton (p x) class instead, like docs#DecidablePred corresponds to docs#Decidable.)

[Eric Wieser]

I'm also somewhat worried about the consequence of losing the Submonoid / Subring etc namespaces to put declarations under; it's great when we can unify a bunch of things as a single declaration under BundledSet, but things will become messy when we can't

[Yury G. Kudryashov]

We can still have Submonoid/Subring namespaces.

[Yury G. Kudryashov]

DecidablePred is reducible, so it doesn't matter.

[Yury G. Kudryashov]

So, is there any conclusion?

[Yaël Dillies]

I just came up with an interesting remark: docs#Subgroup won't be eligible for your BundledSet approach once we have refactored it to work over monoids

[Yaël Dillies]

Currently, the definition is

structure Subgroup (G : Type*) [Group G] extends Submonoid G where
  inv_mem' {x} : x ∈ carrier → x⁻¹ ∈ carrier

which is one data field (carrier : Set G) and many Prop fields (which for BundledSet purposes would be merged into a single prop : IsSubgroup carrier field). If we want to generalize subgroups to monoids in a defeq-sensible way, we need something along the lines of

structure Subgroup (G : Type*) [Monoid G] extends Submonoid G where
  inv : carrier → carrier
  mul_left_inv (a) : (inv a : G) * a = 1

[Yaël Dillies]

Since most bundled sets in algebra build on Subgroup, your BundledSet approach (as currently proposed, at least) would apply to barely anything. And in turn merging your current BundledSet approach would make refactoring Subgroup much harder later. I think this is a pretty serious concern.

[Yaël Dillies]

I am mentioning Subgroup here, but the same argument applies to subobjects of any structure that has Type-valued fields which can be uniquely determined by the other ones (I offer we call these "propositionally redundant fields"), eg docs#Sublattice, whose two data fields can be recovered from ≤ alone.

[Jireh Loreaux]

Do we have intentions to refactor Subgroup to be apply to Monoids?

[Yury G. Kudryashov]

Current docs#Sublattice doesn't have any extra data fields.

[Yury G. Kudryashov]

BTW, the Subsingleton approach mentioned above covers this.

[Yury G. Kudryashov]

Though we won't have nice SetInterPred etc.

[Yaël Dillies]

Jireh Loreaux said:

Do we have intentions to refactor Subgroup to be apply to Monoids?

This has been discussed before, see https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Multiplicative.20subgroups.20of.20a.20ring

[Yury G. Kudryashov]

Do we really care about definitional equalities?

[Yaël Dillies]

Yury G. Kudryashov said:

Current docs#Sublattice doesn't have any extra data fields.

No my point is that it technically makes sense to talk about sublattices of a preorder (well, maybe partial order to ensure unicity).

[Yaël Dillies]

Yury G. Kudryashov said:

Do we really care about definitional equalities?

I would think for cases like docs#circle we do, at least remotely.

[Yury G. Kudryashov]

What's wrong with having Inv.inv defined using Classical.choice on a Subgroup? Do we (plan to) have dependent types that need this definitional equality?

[Eric Wieser]

That sounds pretty annoying to me; I don't want the additive subgroup of ℕ × ℤ for .fst = 0 to have non-computable negation

[Yury G. Kudryashov]

Note that basic operations like docs#Sup.sup will lead to noncomputable inverse for subgroups of monoids.

[Yury G. Kudryashov]

So, is there any conclusion about bundled sets?

[Yury G. Kudryashov]

Let me cross-link an alternative proposal: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Bundled.20sets.2Ffunctions.20with.20even.20more.20classes

[Anne Baanen]

Anne Baanen said:

Eric Wieser said:

The main concern I have right now is that this doesn't work for things like SetLike Finset (which admittedly I think we currently don't use); or in general, any set-like objects that carry extra computational data

This could be fixed by relaxing the predicate from Set α → Prop to Set α → Sort*. Although I suppose we'd lose the properties deriving from SetLike.coe_injective. So maybe it should look like:

structure BundledSet (α : Type*) (p : Set α → Sort*) [∀ x, Subsingleton (p x)] where
  carrier : Set α
  prop : p carrier

(I can't say if the typeclass system would work well with the ∀, or whether we should have an EverywhereSubsingleton p := ∀ x, Subsingleton (p x) class instead, like docs#DecidablePred corresponds to docs#Decidable.)

This change seems indeed to work well:

universe u v

structure BundledSet (α : Type u) (p : Set α → Sort v) [∀ x, Subsingleton (p x)] :
    Type (max u v) where
  carrier : Set α
  protected prop : p carrier

[Anne Baanen]

Some experiments later and it looks like Finset can be practically implemented with the Sort-valued BundledSet as well.

[Anne Baanen]

This seems like a very big proposal, so IMO we should cut it into separate steps to see which ones are worth it.

• What I'll call the first step: I see no reason that replacing structure Submonoid with @[reducible] def Submonoid := BundledSet IsSubmonoid won't work. This would essentially reintegrate the deprecated unbundled subobjects into the main hierarchy. On the other hand, we shouldn't expect too many gains from this switch, and it will be quite disruptive (although we'd be able to switch over each definition one by one). Perhaps automation/tactics are helped by the uniformity of BundledSet.
• Simultaneously we could redefine MulMemClass M S as ∀ (s : S), IsMulMem M s. I expect that this brings some deduplication but otherwise is not too exciting.
• Then we can define new classes such as Implies to make generic operators such as the empty set and intersection. This seems like an obvious advantage in expressivity, so if it works correctly (which I believe it likely will), this would make the previous step pay off.
• The next step is to use the Implies class to automate generic declarations, instead of the current variety of ___MemClasses. I don't see why "so that we can have generic theorems and don't search for SetLike every time" is a convincing argument for this: the discrimination tree matching makes this very fast (just like #8386 did for FunLike). If anything, it seems like the search will be more expensive since Implies IsMulMem _ _ =?= Implies IsOneMem _ _ is slower to fail than not considering IsOneMem at all.

[Anne Baanen]

So in conclusion: I am cautiously optimistic that going ahead with the first three steps will prove to be worth it. I am not convinced about the last one, but I'd like very much to be proven wrong!

[Yury G. Kudryashov]

We can use generic Implies only for forgetful functors.

[Timo Carlin-Burns]

Anne Baanen said:

This could be fixed by relaxing the predicate from Set α → Prop to Set α → Sort*. Although I suppose we'd lose the properties deriving from SetLike.coe_injective. So maybe it should look like:

structure BundledSet (α : Type*) (p : Set α → Sort*) [∀ x, Subsingleton (p x)] where
  carrier : Set α
  prop : p carrier

I wonder if that typeclass parameter would cause performance issues since it would mean that inferInstance : ∀ x, Subsingleton (p x) appears in the definitions of so many abbrevs, e.g. abbrev Submonoid M [Monoid M] := @BundledSet M IsSubmonoid inferInstance.

Would any of these alternatives be an improvement?

• Using Trunc:

structure BundledSet (α : Type u) (p : Set α → Sort v) :
    Type (max u v) where
  carrier : Set α
  prop' : Trunc (p carrier)

variable {α : Type u} {p : Set α → Sort v} [∀ s, Subsingleton (p s)]

def BundledSet.prop (s : BundledSet α p) : p s.carrier :=
  Trunc.recOnSubsingleton (C := fun _ ↦ p s.carrier) s.prop' id

• Using a Subsingleton field:

structure BundledSet (α : Type u) (p : Set α → Sort v) :
    Type (max u v) where
  carrier : Set α
  prop : p carrier
  [subsingleton : Subsingleton (p carrier)]

• Adding the [∀ s, Subsingleton (p s)] hypothesis only when you need the coercion to Set α to be injective.

[Antoine Chambert-Loir]

I was up to asking why not having bundled functions, as well as bundled sets, and I'd probably ask the question in the other direction—Why not copying for set the funlike classes? (So there would be SubmonoidClass, SubgroupClass, SubmoduleClass, etc.)

[Yury G. Kudryashov]

We have docs#MulMemClass

[Yury G. Kudryashov]

I think about ways to reduce code duplications without loss of generality/speed.

[Yury G. Kudryashov]

Also, it would be nice to have polymorphic lemmas like map_map for any compatible FunLikes and SetLikes.

[Antoine Chambert-Loir]

What do people do in other proof assistants?

[Mario Carneiro]

this seems like a bit of a lean-specific problem, so it's difficult to compare with other systems

[Yury G. Kudryashov]

Let me come back to this and https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Bundled.20sets.2Ffunctions.20with.20even.20more.20classes

What issues I want to be solved

• code duplication between various SetLike and DFunLike objects;
• unpredictable holes in API;
• inconsistent names;
• no way to talk about a type which is an AddMonoidHomClass with pointwise addition; the actual example I want to have is "an outer measure-like type with pointwise bottom and order"

Possible approaches

Uniform structures with generic instances

... as described above and in #2202

The main disadvantage of this approach is that in some cases, a bundled homomorphism/bundled set may need to use different order or multiplication.
E.g., 1 can be the bundled version of "cons _ 1 or id`, but there are more examples, see https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Order.20on.20measures for examples about order

While this is the approach I originally suggested, I see no way to accomodate for these special cases.

[PointwiseAdd] etc classes

Suggested by @Moritz Doll in https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Bundled.20sets.2Ffunctions.20with.20even.20more.20classes

Instead of imposing any restrictions on the types, we define typeclasses saying that various operations (order, algebraic operations, inf/sInf for bundled sets) agree with pointwise operations.

I see two disadvantages compared to status quo:

1. Generic lemmas are never dsimp, even if they are dsimp for 95% of the actual types.
   Thus, if we care about dsimp lemmas, then we need to formulate them for all types anyway;

2. If we add generic instances like [FunLike F α M] [Monoid M] [Mul F] [One F] [SMul Nat F] [PointwiseOne F] [PointwiseMul F] [PointwiseSMul Nat F] : Monoid F, then we may get huge instance terms, especially once we start talking about types like (E →L[K] F) →L[K] (F →L[K] G) →L[K] (E →L[K] G). I have no data here.

Meta programming

We can have a meta program that specializes some generic theory to each bundled hom/set type. Maybe we can even build some kind of "hierarchy builder" that takes a file with all morphisms we care about and declares the corresponding types, theorems, and projections.

The main advantage of this approach is that we can get consistent naming and we can have autogenerated dsimp lemmas.

The main disadvantages I see:

1. This approach requires a lot of careful meta-programming, so fewer people can implement it and fewer people will understand how it works.
2. We still don't get a way to generalize docs#MeasureTheory.Measure.ae to outer measures and have lemmas like ae_mono without code duplication.

[Yury G. Kudryashov]

@Anne Baanen @Moritz Doll What do you think?
@Yaël Dillies You may be interested since you're working on dropping some generic instances
@Mario Carneiro Are my concerns about blowup of the size of instances seem valid? If yes, any ideas how to avoid it?

[Johan Commelin]

I think it would be interesting to investigate the third approach in more detail. And maybe we should even see if we can use actual Hierarchy Builder to help with this job.

[Antoine Chambert-Loir]

Does @Cyril Cohen have some opinion about this question?

[Yury G. Kudryashov]

@Johan Commelin How would you formulate a lemma about any OuterMeasure-like bundled map with pointwise order/addition/... (depending on a lemma)?

[Yury G. Kudryashov]

Assuming that meta code can build us a hierarchy with basic stuff.

[Johan Commelin]

Ooh, I don't claim that I can address any of the disadvantages you point out in any of your suggested approaches.

[Yury G. Kudryashov]

Of course, we can create "generic" instances + autodeclare all relevant instances for each specific class to speed up search.