Bundled sets/functions with even more classes

Stream: mathlib4

[Moritz Doll]

I recently ran once again into the hell that is function coercion for bundled maps. While @Yury G. Kudryashov 's idea to fix this seems to be 'get rid of FunLike and SetLike` my idea was to use even more classes (in particular define operations on functions/sets using classes). Example is here: https://gist.github.com/mcdoll/0060646e3f6a413f3401cf9f62e3afe5
It is clear that this design immediately loses dot-notation and I have no idea whether performance would be an issue.
I am very much not an expert on these things, so there might be a very obvious reason why this idea is a bad idea.

@Anne Baanen (congrats on the PhD) @Eric Wieser

Yury's proposal: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/RFC.3A.20bundled.20sets.20.236442

[Yury G. Kudryashov]

I tried a similar approach with functions in Lean 3. It didn't work but this is not an argument because typeclasses work differently in Lean 4.

[Moritz Doll]

Do you remember what exactly did not work?

[Yury G. Kudryashov]

I don't remember, Lean failed to find some instances. But you can try with Lean 4.

[Yury G. Kudryashov]

Also, we had way too many FunLike superclasses back then.

[Moritz Doll]

In my example code all instances are found without any problems

[Yury G. Kudryashov]

An obvious con of your approach is that we can no longer define generic functions (e.g., Submonoid M → Subsemigroup M)

[Yury G. Kudryashov]

But I don't know if this is an issue.

[Moritz Doll]

There is a funny thing happening: all the operators lose definitional equality, but retain proposition equality. A priori [Inter S1 S2 S3 M] and [Inter S2 S1 S3 M] give two different intersections if S1 = S2, but of course they are propositonally equal:

import Mathlib.Data.SetLike.Basic
import Mathlib.Data.Set.Basic

namespace Zulip

/-- `a ∩ₛ b` is the intersection of `a` and `b`. -/
class Inter (S1 S2 S3 : Type*) (M : outParam (Type*)) [SetLike S1 M] [SetLike S2 M] [SetLike S3 M] where
  inter : S1 → S2 → S3
  inter_coe (s1 : S1) (s2 : S2) : (inter s1 s2 : Set M) = (s1 : Set M) ∩ s2

/-- `a ∩ₛ b` is the intersection of `a` and `b`. -/
infixl:70 " ∩ₛ " => Inter.inter

variable {M S1 S2 S3 : Type*}

variable [SetLike S1 M] [SetLike S2 M] [SetLike S3 M] [Inter S1 S2 S3 M] [Inter S2 S1 S3 M]

theorem inter_comm (s1 : S1) (s2 : S2) : (s1 ∩ₛ s2 : S3) = s2 ∩ₛ s1 := by
  apply SetLike.coe_injective
  simp only [Inter.inter_coe]
  exact Set.inter_comm _ _

[Moritz Doll]

and I start to see why it does not work with Lean3

[Moritz Doll]

variable [i1 : Inter S1 S2 S3 M] [i2 : Inter S1 S2 S3 M]

theorem inter_eq (s1 : S1) (s2 : S2) :
    Inter.inter (self := i1) s1 s2 = Inter.inter (self := i2) s1 s2 := by
  apply SetLike.coe_injective
  rw [Inter.inter_coe (self := i1), Inter.inter_coe (self := i2)]

[Moritz Doll]

:ping_pong:

[Yury G. Kudryashov]

I mentioned both my and your approach in my talk yesterday. Didn't work to attract attention.

[Anne Baanen]

Thanks for trying to push this forward! It's on my todo list to make this happen, and I'm reserving time next week to try this out and write up my experiences.

[Anne Baanen]

Moritz Doll said:

I recently ran once again into the hell that is function coercion for bundled maps. While Yury G. Kudryashov 's idea to fix this seems to be 'get rid of FunLike and SetLike` my idea was to use even more classes (in particular define operations on functions/sets using classes). Example is here: https://gist.github.com/mcdoll/0060646e3f6a413f3401cf9f62e3afe5
It is clear that this design immediately loses dot-notation and I have no idea whether performance would be an issue.
I am very much not an expert on these things, so there might be a very obvious reason why this idea is a bad idea.

I think we should see this as a gradual process rather than an all in one refactor. Here's how I see the steps:

• Current SetLike setup.
• Define a highly parametrized Inter class (Only in @Moritz Doll's proposal. Should be totally independent from what follows, although defining instances would be a hassle).
• Separating out Is___Mem predicates from the current bundled structures.
• Separating out Is___Mem predicates from the current bundled classes. (Not done in @Moritz Doll's proposal; unnecessary in @Yury G. Kudryashov's proposal.)
• Using the typeclass system to infer relations between the Is___Mem predicates. (Only in @Yury G. Kudryashov's proposal.)
• Replacing all traces of SetLike with the bundled approach.

[Anne Baanen]

Going all out from SetLike to BundledSet would be an enormous headache, from my experience of originally setting up SetLike.

[Yury G. Kudryashov]

Do you have opinion about which proposal should we aim for?

[Moritz Doll]

Anne Baanen said:

• Separating out Is___Mem predicates from the current bundled classes. (Not done in Moritz Doll's proposal; unnecessary in Yury G. Kudryashov's proposal.)

I tried that and it was quite messy, I ran into problems unifying

@[reducible] def IsOneMem {M : Type*} [One M] (s : Set M) : Prop :=
  1 ∈ s

@[reducible] def IsOneMem' (M S : Type*) [One M] [SetLike S M] : Prop :=
  ∀ s : S, (1 : M) ∈ s

class OneMemClass (S : Type*) (M : outParam (Type*)) [One M]
  extends SetLike S M where
  one_mem : IsOneMem' M S

structure OneMem (M : Type*) [One M] where
  carrier : Set M
  one_mem' : IsOneMem carrier

The problem is that one is A -> Prop and the other one is Prop.

[Moritz Doll]

@Anne Baanen is moving theorems from FoobarMap to FoobarMapClass a good idea at the moment? I continue to run into these problems where a theorem is stated for a : FoobarMap, but my use case is either a type synonym or a more specialized type. At the moment I only want to move theorems about 'internal' properties (properties of a single a) of FoobarMap, as opposed to my proposal above to also move external properties (stuff about the space FoobarMap, such as linearity)

[Moritz Doll]

To give an example: we have lots of really weird projections such as ContinuousLinearMap -> LinearMap and my proposal would be to replace them by adding a ContinuousLinearMapClass.toContinuousLinearMap etc and use that ContinuousLinearMap has an instance for LinearMapClass (automatically since it has an instance for ContinuousLinearMapClass).
Then if you have a type synonym on ContinuousLinearMap you get the instance by def-eq abuse and all the projections are already there, whereas without classes there is more boilerplate.

[Anne Baanen]

In general it is a very good idea to move from FoobarMap to FoobarMapClass if you are expecting to consume, rather than produce, a foobar map. So docs#LinearMapClass is no good for stating that e.g. the endomorphisms of a vector space form a monoid, since there is nothing in LinearMapClass F R M M stating that F is closed under compositions. But if the theorem is given some linear map f, then the right thing to do is to say [LinearMapClass F R M N] (f : F).

[Anne Baanen]

(There are some caveats to this general statement: going to FoobarMapClass loses dot notation support, and leanprover/lean4#3107 means that for semilinear maps specifically we need to restate certain @[simp] lemmas.)

[Yury G. Kudryashov]

I have 2 more use cases for this:

• generalize ae_mono, ae_zero etc to OuterMeasureClass;
• generalize translation number to AddConstMapClass F Real Real 1 1 and lemmas about it to the same class + monoid/group structure with mul=comp.

[Yury G. Kudryashov]

For the first use case, @Yaël Dillies argues that I'm overengineering in #10721.

[Yury G. Kudryashov]

@Moritz Doll @Anne Baanen What do you think?

[Yury G. Kudryashov]

Ping here

[Yury G. Kudryashov]

Ping here...

[Yury G. Kudryashov]

@Sébastien Gouëzel What do you think?

[Yury G. Kudryashov]

Ping here... I understand that this topic may seem unimportant but I don't see a way to generalize theorems like docs#CircleDeg1Lift.translationNumber_pow to a *Class without making a decision here.

[Yury G. Kudryashov]

And I want to generalize them so that we can have one translationNumber (defined for any map f : Real -> Real) and a bunch of theorems that apply to

• the lifts of monotone circle maps (now docs#CircleDeg1Lift, to be migrated to AddConstOrderHom once I add it);
• the lifts of orientation-preserving circle homeomorphisms (now Units CircleDeg1Lift, to be migrated to AddConstEquivs from #9726)
• the lifts of continuous monotone circle maps;
• the lifts of $C^r$ smooth monotone circle maps with finitely many critical points;
• the lifts of $C^r$ circle diffeomorphisms;
• the lifts of $C^r$ smooth monotone cirlce maps with finitely many break points.
• probably more classes.

[Yaël Dillies]

Sorry, Yury, did you mean to ping https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/RFC.3A.20bundled.20sets.20.236442 instead? I'm failing to understand what you're asking opinion on

[Yury G. Kudryashov]

I think that migrating to "common data structure for bundled maps + generic instances for this type" is difficult, because (a) sometimes we want, e.g., a different order; (b) I don't see how to fit *Equivs, so I'm talking about going forward with #10721 and, more generally, @Moritz Doll 's proposal above (add Pointwise* classes).

[Yury G. Kudryashov]

In particular, I want to have

• PointwiseLE for ae_mono;
• CompMulClass + IdOneClass for *End types

or some other way to get generic ae_mono, coe_mul_eq_comp, and coe_one_eq_id.

[Yury G. Kudryashov]

Personally, I would prefer to have a common data type so that these lemmas become rfl but I failed to come up with a design that works for (a) *Homs and *Equivs; (b) special cases like *Hom type with non-pointwise order.