A quadratic scaling problem

Stream: mathlib4

[Kenny Lau]

Consider the situation where we have a function being applied to a constructor (think Polynomial.eval and X).

The functions can have several forms depending on the generalisation (e.g. a plain function, a linear map, a ring map; and also specialisation e.g. Localization vs. Localization.Away vs. Localization.AtPrime).

The constructors can also have several forms.

Given that these are all valid simpNFs, that means that if we have m forms of the function and n forms of the constructor, then we would need m * n simp lemmas.

[Kenny Lau]

Is there any way to make this scaling easier?

[Kenny Lau]

90% of the time we can assume that the constructor and the function are in the same level of generalisation, which makes it linear, but that makes it harder 10% of the time where for some reason they have to be different

[Yury G. Kudryashov]

We simplify applications of bundled versions of functions to the unbundled versions.

[Yury G. Kudryashov]

See, e.g., Polynomial.coe_evalRingHom

[Kenny Lau]

hmm i thought we didn't do that for some reason but i can't remember what the reason was so maybe you're right

[Kenny Lau]

yep I think I'm convinced that this is right, with the caveat that we still want a different constructor for a different type (e.g. Localization.Away is an abbrev for Localization but it should have its own constructor); now it's not clear whether we want a simp lemma for e.g. map (Away.mk x s)

[Kenny Lau]

or Away.map (mk x s)

[Kenny Lau]

I think reasonably map, Away.map, mk, and Away.mk should all be simpNF

[Andrew Yang]

We simplify applications of bundled versions of functions to the unbundled versions.

I'm not sure if this is universally true/better. If we were to use evalRingHom as normal form, we would avoid the need of eval_add eval_mul eval_finsetSum eval_pow eval_finsetProd eval_finprodSum eval_zero etc. which might be way more than the n * m lemmas above.

[Yury G. Kudryashov]

For functions that can be bundled without extra typeclass assumptions, we can just replace the functions with the minimally bundled versions.

[Kenny Lau]

Andrew Yang said:

eval_add eval_mul eval_finsetSum eval_pow eval_finsetProd eval_finprodSum eval_zero

maybe we can have something like "RingHomClass" but instead of the whole type we just register it for one thing?

[Kenny Lau]

oh maybe that would be impossible to infer...

[Yury G. Kudryashov]

We used to have is_*_hom in Lean 3 and moved to *_hom_class because with these classes, Lean has DFunLike.coe to match lemmas / call inference.

[Kenny Lau]

yeah, i just tested that my idea is impossible to infer:

import Mathlib

class IsAddHom {α β : Type*} [Add α] [Add β] (f : α → β) : Prop where
  map_add (x y : α) : f (x + y) = f x + f y

def double : ℕ → ℕ := fun n ↦ 2 * n

instance : IsAddHom double := ⟨by unfold double; grind⟩

example (m n : ℕ) : double (m + n) = sorry := by
  rw [IsAddHom.map_add]

[Kenny Lau]

Invalid rewrite argument: The pattern to be substituted is a metavariable (`?m.12 (?x + ?y)`) in this equality
  ?m.12 (?x + ?y) = ?m.12 ?x + ?m.12 ?y

[Kenny Lau]

but I definitely want a way to avoid having to prove eval_sum for every additive function that I define...

[Kenny Lau]

what if:

@[generate_hom_lemmas] instance : IsAddHom eval  := sorry

[Kenny Lau]

what if I have an attribute generate_hom_lemmas that works like @[simps!] and automatically generates all of the lemmas about add homs?

[Aaron Liu]

there are a lot of lemmas about addhoms

[Aaron Liu]

not all of which may be imported at the moment

[Kenny Lau]

the addhom lemmas can be extended by an attribute, and we will only generate the lemmas that have been imported, (which is already what is happening with functions like eval)

[Kenny Lau]

e.g. eval_finset_sum is proved in the same file as the definition of eval

[Kenny Lau]

in my proposal, this lemma would be autogenerated

[Kenny Lau]

and the lemma exists anyway so it isn't like we're generating more lemmas than needed

[Kenny Lau]

@loogle "multiset_sum"

[loogle]

:search: map_multiset_sum, AddMonoidHom.map_multiset_sum, and 60 more

[Kenny Lau]

has 62 hits

[Yury G. Kudryashov]

I think that this should be an attribute on evalRingHom. It should specialize some lemmas to whatever DFunLike.coe (evalRingHom ..) simplifies to.

[Kenny Lau]

in any case do you think this is a good idea?

[Yury G. Kudryashov]

I think that this is a good idea but I suspect there are some design decisions to make here, and I'm too sleepy to think it through rn.

[Kenny Lau]

here's the full proposal:

import Mathlib

set_option autoImplicit false

class IsAddHom {α β : Type*} [Add α] [Add β] (f : α → β) : Prop where
  map_add (x y : α) : f (x + y) = f x + f y

@[add_lemma]
lemma IsAddHom.multiset_sum {α β : Type*} [AddCommMonoid α] [AddCommMonoid β]
    (f : α → β) [IsAddHom f] : ∀ m : Multiset α, f m.sum = (m.map f).sum := sorry

def double : ℕ → ℕ := fun n ↦ 2 * n

@[generate_lemma]
instance : IsAddHom double := ⟨by unfold double; grind⟩

#check double_multiset_sum -- ∀ m : Multiset ℕ, double m.sum = (m.map double).sum
/-
(secretly, it does this:)
lemma double_multiset_sum : ∀ m : Multiset ℕ, double m.sum = (m.map double).sum :=
  IsAddHom.multiset_sum double
-/

[Kenny Lau]

I think even without the tactics, just this one IsAddHom.multiset_sum might already be good

[Kenny Lau]

like, look at this file:

@[simp, norm_cast]
theorem cast_list_sum (s : List ℚ) : (↑s.sum : α) = (s.map (↑)).sum :=
  map_list_sum (Rat.castHom α) _

@[simp, norm_cast]
theorem cast_multiset_sum (s : Multiset ℚ) : (↑s.sum : α) = (s.map (↑)).sum :=
  map_multiset_sum (Rat.castHom α) _

@[simp, norm_cast]
theorem cast_sum (s : Finset ι) (f : ι → ℚ) : ∑ i ∈ s, f i = ∑ i ∈ s, (f i : α) :=
  map_sum (Rat.castHom α) _ s

@[simp, norm_cast]
theorem cast_list_prod (s : List ℚ) : (↑s.prod : α) = (s.map (↑)).prod :=
  map_list_prod (Rat.castHom α) _

[Kenny Lau]

imagine if these 4 lemmas were auto generated

[Aaron Liu]

I don't like IsAddHom

[Kenny Lau]

I think this allows us to generate those lemmas without first haivng defined the bundled map

[Aaron Liu]

lest we also get IsAddSubmonoid etc.

[Kenny Lau]

but it's also possible to i guess start from the bundled lemma and either 1. tell it which unbundled function it should use, or 2. just simp the LHS and make it a simp lemma (oh wait, this wouldn't work because it would simp f 0 to 0)

[Kenny Lau]

so, proposal 2, the four lemmas above would be autogenerated by:

/-- Coercion `ℚ → α` as a `RingHom`. -/
@[generate_hom_lemmas (↑)]
def castHom : ℚ →+* α where
  toFun := (↑)
  map_one' := cast_one
  map_mul' := cast_mul
  map_zero' := cast_zero
  map_add' := cast_add

[Yury G. Kudryashov]

If you use @[simps -fullyApplied] on the same def, then it won't simplify myFunHom 0 to 0, because it will simplify DFunLike.coe myFunHom to myFun first.

[Yury G. Kudryashov]

(not 100% sure if it will work w/o -fullyApplied)

[Kenny Lau]

Yury G. Kudryashov said:

For functions that can be bundled without extra typeclass assumptions, we can just replace the functions with the minimally bundled versions.

let's take a concrete example which is PolynomialModule.single, which I believe should be simped to PolynomialModule.lsingle? As in, should we make lsingle the simpNF?

[Kenny Lau]

actually maybe we should even delete single?

[Yury G. Kudryashov]

If the function can be bundled under the same assumptions, then we should drop the unbundled version.

[Kenny Lau]

@George McNinch do you want to try this?

[Kenny Lau]

precise task: delete single and replace it with lsingle (and also make sure the other definitions in the file have API, as we've been discovering that they lack)

[Kenny Lau]

i mean perhaps in a different PR maybe we should also make PolynomialModule a one-param strcuture just like docs#Polynomial ?

[Yury G. Kudryashov]

AFAIK, there is a plan to make docs#AddMonoidAlgebra a 1-field structure, then turn Polynomial into a def. So, I would change PolynomialModule right now.

[Kenny Lau]

i'm not sure i follow, how do the two sentences relate to each other (PolynomialModule is not an algebra), and are you saying you would change the PolynomialModule into a one-param structure or some other def?

[Yury G. Kudryashov]

:man_facepalming:

[Yury G. Kudryashov]

I'm not the one turning MonoidAlgebra into a structure. I saw this discussion somewhere on Zulip. I think that it makes sense to coordinate the effort even if the refactor does not apply directly.

[Kenny Lau]

when should we have def and when should we have 1-param structs?

[Jovan Gerbscheid]

@Yaël Dillies is working on #25273 to make MonoidAlgebra into a 1 field structure. The reasoning is that it defined in terms of M →₀ R, i.e. Finsupp. We want to have a better separation between these two types, because Finsupp doesn't have any of the algebraic structure that we are putting on MonoidAlgebra.

[Yaël Dillies]

Both G →₀ R and R[G} have the same AddCommGroup structure, but as Jovan points out, they have a different Mul: G →₀ R is pointwise and R[G} is convolution

[Eric Wieser]

Yury G. Kudryashov said:

If the function can be bundled under the same assumptions, then we should drop the unbundled version.

This isn't the full picture; if a function can be bundled in two different ways for which there is no type bundling both, then I'd argue that rather than picking between the bundlings you should not bundle.

[Eric Wieser]

And more tenously, I'd argue that therefore we should avoid bundled definitions in simpNF API as much as possible, as these make the API unstable under availability of new bundlings combined with the rule above.

[Eric Wieser]

(another more minor reason to keep bundling out of simpNF API is because foo x is a much smaller term than @DFunLike.coe X Y (@instFunLikeFooHom X Y ...) x)

[Yury G. Kudryashov]

Then we need a way to specialize map_sum etc lemmas to those unbundled functions.

[Eric Wieser]

I think the reality is that we copy the API over

[Eric Wieser]

But at least prove it using the bundled version, theorem foo_sum ... := map_sum fooHom ... etc

[Yury G. Kudryashov]

I meant something like @[homLemmas] def fooHom := ...

[Eric Wieser]

That can only do so much; lemmas like map_dfinsuppSum likely won't exist at the point the def is created, and I'm not sure how you'd add them latter

[Eric Wieser]

Maybe we can register map_ as an autogeneration prefix like equation lemmas, such that the lemmas are generated on the fly when used

[Robert Maxton]

Kenny Lau said:

what if I have an attribute generate_hom_lemmas that works like @[simps!] and automatically generates all of the lemmas about add homs?

I had a similar but more general idea in another thread, which was that simps could be extended so that custom 'projection' lemmas that aren't actually referencing true projections could be registered
this would then also apply to things like (at least attempting to) generate ι_comp comp_lift etc lemmas in category theory

[Kenny Lau]

Eric Wieser said:

That can only do so much; lemmas like map_dfinsuppSum likely won't exist at the point the def is created, and I'm not sure how you'd add them latter

see my proposal way above, we would make it an environment extension

[Kenny Lau]

@Robert Maxton that is a good idea, was there any objection the last time you mentioned it? (also could you link to the thread?)

[Robin Carlier]

@Kenny Lau I think @Robert Maxton is referring to this message: #general > "Missing Tactics" list @ 💬. I also have a bunch of wishes for extending/improving @[simps] that makes me think it would be good to start a thread discussing this and coordinating with interested maintainers.

[George McNinch]

Kenny Lau said:

George McNinch do you want to try this?

Whoops - not sure why I didn't see this message the other day (!). Sure, I 'm happy to take a shot at it (though I probably can't look at it until tomorrow).

[Kenny Lau]

so, to summarise this thread finally, according to Eric's guidelines (no i didn't use LLM):

Let's look at a concrete example.

• Minimally bundled function: DirectSum.decompose : M ≃ ⨁ i, ℳ i
• Bundled functions:
  • DirectSum.decomposeLinearEquiv
  • DirectSum.decomposeAddEquiv
• Minimally bundled constructor: DirectSum.of : β i →+ ⨁ i, β i
• Bundled constructor: DirectSum.lof: M i →ₗ[R] ⨁ i, M i

According to Eric, the simpNF of the applied forms of the function and the constructor are the minimally bundled version, and to balance this cost, we need to copy over all the hom lemmas to the unbundled version of both. In effect, there is no difference between how we treat constructors and how we treat functions (because a constructor is just a special function).

[Kenny Lau]

And on top of that we're (me and Robin) trying to see if the "copy over" step could be automated by extending @[simps]

[Kenny Lau]

Eric Wieser said:

That can only do so much; lemmas like map_dfinsuppSum likely won't exist at the point the def is created, and I'm not sure how you'd add them latter

there are two situations:

• if DFinsupp.sum is not defined at the current point, then right now we wouldn't have the map_dfinsuppSum lemma anyway
• if we have access to DFinsupp.sum, then according to my proposal the map_dfinsuppSum lemma would be automatically generated

my proposal is this:

-- at the definition of RingHom
structure RingHom ...

@[hom_lemma] theorem RingHom.map_add (f : R →+* S) {x y} : f (x + y) = f x + f y := ...

-- in another file

def foo : R → S := ...
@[hom_lemma foo] def fooRingHom : R →+* S := ...
#check foo_add -- foo (x + y) = foo x + foo y

-- at the definition of DFinsupp

@[hom_lemma] theorem RingHom.map_dfinsuppSum (f : R →+* S) : ...

-- in another file

def bar : R → S := ...
@[hom_lemma bar] def barRingHom : R →+* S := ...
#check bar_dfinsuppSum -- bar (x.sum f) = x.sum fun a b ↦ bar (f a b)

[Kenny Lau]

@Robin Carlier what do you think about my proposal?

[Kenny Lau]

also, should we include my summary above somewhere in the official guidelines?

[Eric Wieser]

In the past I've considered that docs#DirectSum.of should not be bundled at all, but gave up on the PR trying to make the change

[Eric Wieser]

(I think it might have been motivated by broken unification in lean 3, which might no longer be relevant)

[Kenny Lau]

Polynomial.C is bundled so this should be fine

[Artie Khovanov]

Polynomial.C isn't good design imo

[Yury G. Kudryashov]

What's wrong with it?

[Eric Wieser]

One problem is that it fights with algebraMap for simpNF

[Eric Wieser]

Probably there's some issue with both relating to polynomials over non-unital rings too, but I haven't thought about that in any depth.

[Kenny Lau]

algebraMap is a problem on its own, i can never tell if it's meant to be simpNF or not, take for example the map from R to Localization (w : Submonoid R)

[Yury G. Kudryashov]

My guess is that algebraMap should not be a simpNF because in many cases we have special names for it (Nat.cast, Polynomial.C, Complex.ofReal etc).

[Eric Wieser]

@Anne Baanen tried to unify these all under one name in Lean 3, but it got swept away by the port

[Eric Wieser]

Essentially the algebraic version of DFunLike.coe

[Yury G. Kudryashov]

Where can I find more details?

[Artie Khovanov]

@Yury G. Kudryashov I disagree with this approach because it leads to API duplication

[Artie Khovanov]

Needs a reusable solution

[Yuyang Zhao]

Yury G. Kudryashov said:

Where can I find more details?

#general > "has canonical morphism" class
#general > Should `algebra_map` be a coercion?
#general > Please stop adding generalized API around coercions

[Yury G. Kudryashov]

Artie Khovanov said:

Yury G. Kudryashov I disagree with this approach because it leads to API duplication

I see 2 other options:

• resurrect Lean3-time coe function and add typeclasses saying that coe is a morphism;
• make discrimination trees match some lemmas like coe_add on symbols marked with @[coe].

[Kenny Lau]

I thought we deprecated "is a morphism"

[Kenny Lau]

Kenny Lau said:

my proposal is this:

-- at the definition of RingHom
structure RingHom ...

@[hom_lemma] theorem RingHom.map_add (f : R →+* S) {x y} : f (x + y) = f x + f y := ...

-- in another file

def foo : R → S := ...
@[hom_lemma foo] def fooRingHom : R →+* S := ...
#check foo_add -- foo (x + y) = foo x + foo y

-- at the definition of DFinsupp

@[hom_lemma] theorem RingHom.map_dfinsuppSum (f : R →+* S) : ...

-- in another file

def bar : R → S := ...
@[hom_lemma bar] def barRingHom : R →+* S := ...
#check bar_dfinsuppSum -- bar (x.sum f) = x.sum fun a b ↦ bar (f a b)

What do you guys think about my proposal here?

[Andrew Yang]

Artie Khovanov said:

Polynomial.C isn't good design imo

Which problem are you referring to? The existence of the ring hom R ->+* R[X]? Or the fact that it is the simpNF for constant polynomials? Or the fact that the simpNF for $aX^n$ is C a * X ^ n instead of a • X ^ n?

[Yury G. Kudryashov]

It feels like this thread turned into discussion of several (related, but different) issues, with many posts not specifying which issue they're trying to solve. It would be nice if one of the participants writes a summary of what issues were discussed, what are the options, and how these issues are related to each other. My guess is that the issues are too Mathlib-specific to ask an AI, but I haven't tried yet.

[Kenny Lau]

I think the central thread is "how best to define a function" where:

• bundled functions have built-in hom lemmas, but are uncanonical so they fight for simpNF
• unbundled functions need hom lemmas proven, but should be the default

And then afterwards we started to discuss several bundled functions that are currently the simpNF and how they are suboptimal, such as Polynomial.C and algebraMap

(I did ask LLM but i'm too afraid to trust it)

[Yury G. Kudryashov]

There is also a discussion of whether we should use bundled maps for stuff like Polynomial.C or MvPolynomial.eval at all.

[Anne Baanen]

Kenny Lau said:

What do you guys think about my proposal [here]?

What happens if map_dfinsuppSum and barRingHom are defined in files that don't know about each other? If we later import both in one file, would the lemmas be generated there?

[Kenny Lau]

Anne Baanen said:

What happens if map_dfinsuppSum and barRingHom are defined in files that don't know about each other? If we later import both in one file, would the lemmas be generated there?

no, you would miss the lemma; but right now in this set up there is no way to have bar_dfinsuppSum anyway.

[Anne Baanen]

I disagree with "there is no way to have bar_dfinsuppSum.

From a current user's perspective: we want to apply bar_dfinsuppSum, find it doesn't exist, define a new lemma bar_dfinsuppSum := map_dfinsuppSum barRingHom and find/create a file where it fits in the import hierarchy.

With autogenerated declarations: we want to apply bar_dfinsuppSum, find it doesn't exist, and then we are out of luck?

[Kenny Lau]

@Anne Baanen no, in that situation you would also do lemma bar_dfinsuppSum := map_dfinsuppSum barRingHom. What I meant by "right now anyway" is that right now you would also have to state the theorem manually anyway, and this wouldn't change after my proposal

[Kenny Lau]

i'm not removing the map_xxx lemmas; i'm tagging them with @[hom_lemma]

[Yury G. Kudryashov]

I think that it should be possible to call hom_def (the attribute that specializes hom_lemmas; I think that we should use a different name) when some of the lemmas are already there. E.g., it's possible that bar_mul is defined in non-commutative settings while bar_prod needs a CommMonoid instance. The code should skip the pre-existing lemmas, possibly checking that they auto imply the new version. As a side effect, it will be possible to write attribute [hom_def] barHom later to generate the missing lemmas.

[Kenny Lau]

I agree

[Yury G. Kudryashov]

Of course, this could lead to multiple definitions of the same lemma. I'm not sure what to do about it.

[Kenny Lau]

we can just look at the names and skip if there's already a lemma with the name

[Yury G. Kudryashov]

I mean, if B and C import A and we call hom_def on a definition from A in both B and C, they can generate conflicting lemmas.

[Yury G. Kudryashov]

Also, it's important to copy attributes like @[simp] from the original hom_lemmas.

[Kenny Lau]

Yury G. Kudryashov said:

I mean, if B and C import A and we call hom_def on a definition from A in both B and C, they can generate conflicting lemmas.

maybe we should ban calling hom_def on a later file, and only permit more specialised lemmas such as:

generate_hom_lemmas barRingHom -> bar: [dfinsuppSum, prod]

This should be more maintainable in the long term (consider once again the argument that in the current setup you could also have someone write theorem bar_dfinsuppSum twice in the file B and then the file C that both import A)