lean-pr-testing-4595

Stream: nightly-testing

[Kim Morrison]

Is one of the authors of Mathlib.Tactic.ToAdditive, @Mario Carneiro, @Yury G. Kudryashov, @Floris van Doorn, @Jon Eugster available to help understand a failure of @[to_additive] on the lean-pr-testing-4595 branch?

(This is an experimental branch changing the proofs that simp generates when using dsimp lemmas, attempting to reduce the occurrence of "unguided" defeq problems in the kernel after simp.)

I am seeing failures in Mathlib.Data.Part, and in Mathlib.RingTheory.OreLocalization, where the @[to_additive] attribute is failing, and I'm not sure why.

Typical errors are:

@[to_additive "A difference is equal to its expansion by a summand from `S`."]
protected theorem expand' (r : X) (s s' : S) : r /ₒ s = s' • r /ₒ (s' * s) :=
  OreLocalization.expand r s s' (by norm_cast; apply SetLike.coe_mem)

producing

application type mismatch
  @Mathlib.Algebra.Group.Subsemigroup.Operations._auxLemma.7 R (AddSubmonoid R) AddZeroClass.toAdd
argument has type
  Add R
but function has type
  ∀ [inst : Mul R] [inst_1 : SetLike (AddSubmonoid R) R] [hA : MulMemClass (AddSubmonoid R) R] (S' : AddSubmonoid R)
    (x y : ↥S'), ↑x * ↑y = ↑(x * y)

and

@[to_additive]
theorem some_mul_some [Mul α] (a b : α) : some a * some b = some (a * b) := by simp [mul_def]

producing

application type mismatch
  mul_def
argument has type
  Add α
but function has type
  ∀ [inst : Mul α] (a b : Part α),
    a * b = do
      let y ← a
      map (fun x ↦ y * x) b

Note this is not a complete failure of @[to_additive], it is working fine still in basic files.

[Floris van Doorn]

See #10830. The issue is that simp generates subterms that don't have enough context to translate. They are lambda-terms quantifying over multiplicative type-classes, but applied to terms. We need to know what the terms are to decide whether we should translate these multiplicative type-classes (currently we do translate them).
Possible solutions:

• adapt simp to not generate applied lambda-terms
• adapt to_additive to beta-reduce the value before translating anything (this might actually be pretty feasible - but we also need to look at generated auxiliary declarations, which will be harder)
• adapt to_additive to be more context-aware during the translation (probably not feasible).
• Live with the status quo: the workaround is to specify the type explicitly in a few simp-rules.

[Kim Morrison]

@Floris van Doorn, could you explain what the workaround would look like here? Which simp rules do I need to look at to fix

@[to_additive]
theorem some_mul_some [Mul α] (a b : α) : some a * some b = some (a * b) := by simp [mul_def]

What type needs to be specified explicitly?

[Floris van Doorn]

This has nothing to do with #10830. It is fixed by adding @[to_additive] to Part.mul_def.

[Floris van Doorn]

I don't know why those lemmas don't have that...

[Floris van Doorn]

I pushed to the branch fixing Data.Part.

[Floris van Doorn]

We just didn't see it on master, since simp [mul_def] created a proof term that doesn't mention mul_def.

[Floris van Doorn]

Do you know the internals of simp?
Given a new declaration (to which we want to add the to_additive attribute) it would be very helpful to know which declarations were automatically generated by this declaration. to_additive needs to (potentially) additivize these declarations as well.
The current heuristic when adding declaration foo it will consider the following declarations that (may) have been added to the environment when elaborating foo:

1. It has to occur in foo (or in a declaration automatically generated by foo)

2. It has to be of one of these forms

   • foo.<something>
   • Mathlib.MyFile._auxLemma.<something>
   • docs#LeanisPrivateName holds
   • docs#Lean.Name.hasMacroScopes holds

[Floris van Doorn]

(ran off to lunch, now I'm back)
The first error in OreLocalization.Basic is a case where simp generates Mathlib.Algebra.Group.Subsemigroup.Operations._auxLemma.7, and to_additive currently doesn't consider additivizing this.

[Kim Morrison]

Why is that?

[Kim Morrison]

Surely this occurs everywhere?

[Kim Morrison]

It wasn't created during expand' (at least according to whatsnew in)

[Kim Morrison]

but presumably that just means that someone had previously used it as simp lemma.

[Kim Morrison]

Oh, when you said "one of these forms": Mathlib.MyFile._auxLemma.<something> did you literally mean that MyFile had to match the current file?

[Floris van Doorn]

Yes

[Floris van Doorn]

I don't recall why we did it this way. We could try to additivize everything that satisfies docs#Lean.Name.isInternalDetail.

[Floris van Doorn]

I think the reason is that there is a problem if files B and C both import file A, and both separately additivize A.something, then you now have two additive translations.

[Kim Morrison]

Ah -- at least for theorems this is allowed now.

[Floris van Doorn]

How does simp deal with this? Can it be the case that two files both generate Mathlib.Algebra.Group.Subsemigroup.Operations._auxLemma.7?

[Kim Morrison]

Yes, and we arrange that lean doesn't complain about the duplication in these cases!

[Kim Morrison]

So hopefully to_additive could take advantage of the same.

[Floris van Doorn]

So simp guarantees that all generated declarations with the name Mathlib.Algebra.Group.Subsemigroup.Operations._auxLemma.7 have exactly the same type?

[Kim Morrison]

That is a good question. I'm not confident there.

[Kim Morrison]

But presumably the answer is yes??

[Floris van Doorn]

Then I'm a bit surprised what the 7 indicates... It somehow must encode for what declaration it is generating an equation lemma.

[Floris van Doorn]

Kim Morrison said:

Surely this occurs everywhere?

to_additive calls docs#Lean.Meta.getEqnsFor? with nonrec := true on all declarations it additivizes. This ensures that most equation lemmas are already generated (and correctly additivized). This is a hack that maybe we can get rid of now...

[Floris van Doorn]

Though I'm still not sure if nonrec := false is the correct default for Mathlib. I expect that for most declarations we will use the equational lemmas multiple times, so it is cheaper to just always compute it once, instead of computing it potentially multiple times. (I can imagine that in other contexts this is the right default behavior.)

[Floris van Doorn]

I believe

Floris van Doorn said:

This is a hack that maybe we can get rid of now...

Probably we cannot (easily). A comment in the source code mentions

/- We need to generate all equation lemmas for `src` and `tgt`, even for non-recursive
definitions. If we don't do that, the equation lemma for `src` might be generated later
when doing a `rw`, but it won't be generated for `tgt`. -/

[Kim Morrison]

Ooh, so I made a hacky change so it will additivize everything, even from different files.

[Kim Morrison]

OreLocalization then succeeds.

[Kim Morrison]

I'll see if the rest of mathlib survives.

[Floris van Doorn]

I expect that in some random file you will get a clash of additivized names. But let's see.

[Kim Morrison]

Somewhat unexpectedly the first error is

error: ././././Mathlib/Algebra/BigOperators/Group/Finset.lean:1712:2: application type mismatch
  @one_ne_zero α inst✝² inst✝¹
argument has type
  Zero α
but function has type
  ∀ [inst : One α] [inst_1 : NeZero 1], 1 ≠ 0

Shouldn't it already know not to touch this?

[Floris van Doorn]

The big issues of simp(/rw) + to_additive interactions that I currently see:

1. If large lambda-terms are generated (that abstract over multiplicative classes), we should beta-reduce these beta-redexes before translation.
2. We should correctly additivize generated auxiliary declarations (and manage if they come from different modules)
3. If we generate an auxiliary declaration that cannot be additivized (maybe for a lemma about Ring) then we should have a mechanism that decides not to additivize it.

I believe the workaround of specifying types explicitly (mentioned in #10830) can work around both issues 1 and 3.
There are probably other issues I'm not seeing at the moment, though.

[Kim Morrison]

This is on branch#to_additive_all if you want to take a look.

[Floris van Doorn]

Well, one_ne_zero doesn't have a to_additive tag, but depending on your implementation you now basically made it have one?

[Kim Morrison]

I think I only changed anything about _auxLemma.

[Kim Morrison]

diff

[Kim Morrison]

Oh

[Kim Morrison]

I see, but as soon as someone uses it manually in simp...

[Floris van Doorn]

Not sure why you get that error on Master. But it is completely expected that to_additive translates One α to Zero α

[Kim Morrison]

Hrmm... is the additive version of OreLocalization even a useful thing? I would be just as happy here to rip out all the to_additives in this file!

[Matthew Ballard]

Algebraic $K_0$ was mentioned by Johan

[Kim Morrison]

Hmm, my hack breaks master pretty thoroughly. :-(

[Floris van Doorn]

Actually, I don't even know when and why Mathlib.Algebra.Group.Subsemigroup.Operations._auxLemma.7 is generated. It looks like the symmetric version of docs#MulMemClass.coe_mul (and not an equational lemma for docs#MulMemClass.mul ). Is that changing in lean4#4595 ?

[Kim Morrison]

lean#4595 is a pretty big change. It actually rewrites by all simp lemmas, even if they are rfl lemmas (previously we just omitted the proof, and this gave the kernel lots of hard defeq problems).

[Kim Morrison]

So yes, we are generating many more auxiliary lemmas (for all the rfl lemmas that we ever rewrite by).

[Floris van Doorn]

Can we generate them the moment that a declaration is tagged simp? (or when a definition is declared)?

[Floris van Doorn]

Though I guess when a definition is declared we already do that in to_additive.

[Floris van Doorn]

Or if we already do... Is there a way to figure out what the name is?

[Floris van Doorn]

Note: there is another hack in to_additive to figure out what lemmas are generated by simp. I expect this hack doesn't survive this change.
If this information is somehow available in the environment after the simp attribute is executed, that would make the behavior of to_additive less hacky, and we might then be able to find (and generate) the newly generated simp-lemmas.

[Floris van Doorn]

See docs#Lean.Meta.Simp.addSimpAttrFromSyntax (which is in Mathlib, despite its name)

[Floris van Doorn]

Looking at the pr-branch.
Mathlib.Algebra.Group.Subsemigroup.Operations._auxLemma.7 is generated the moment that MulMemClass.coe_mul is declared, but not currently caught and additivized by the current implementation of to_additive (probably because of the very hacky Lean.Meta.Simp.addSimpAttrFromSyntax)

[Floris van Doorn]

I have to run now.

[Floris van Doorn]

I'm investigating this a bit further. These declarations are generated by norm_cast. The attribute @[to_additive (attr := norm_cast)] applies the norm_cast attribute to both the multiplicative and additive declaration, creating the lemmas Mathlib.Algebra.Group.Subsemigroup.Operations._auxLemma.7 and Mathlib.Algebra.Group.Subsemigroup.Operations._auxLemma.8. What is missing is that these lemmas should be put in the "multiplicative -> additive" dictionary that to_additive is using.
This is currently done in a very hacky way for the simp and simps attributes specifically, but not for other attributes.
I'm not sure what the best way forward is.
From the perspective of to_additive, it would be nice if every attribute could report "I generated this list of declarations" (in order).
I could try to extend the hack further to norm_cast, but maybe other attributes are also affected.
I could try something else hacky but more general, by comparing the environment before and after executing the command, and collecting the new attributes that way (but then I lose the order in which the declarations were added...)

[Kim Morrison]

Thanks Floris. My suggestoin would be to try extending the hack further to norm_cast for now. Given that we seem to get a fair way into Mathlib before this problem occurs, perhaps we can hope to get lucky.

[Kim Morrison]

Testing out the consequences of #4595 is moderately high priority: if this is something that we can make work we'd really like to.

[Floris van Doorn]

I think I will have time for this today.

[Michael Rothgang]

Kim Morrison said:

Testing out the consequences of #4595 is moderately high priority: if this is something that we can make work we'd really like to.

lean4#4595, right?

[Floris van Doorn]

This was a bit more painful since norm_cast is in Core now, but on branch#to-additive-4595 this issue is now fixed by increasing the hack. RingTheory.OreLocalization builds now.

[Floris van Doorn]

@Kim Morrison would Core be open to decreasing the depth of the hack?
This requires three things:

• have Lean.Meta.addSimpTheorem return an array of declaration names that were generated. Two implementation options are on Mathlib master and on this branch (these are not equivalent, since on master we return the empty array if no declaration was generated, and on the branch we return #[declName], but both work well for me).
• all declarations that use addSimpTheorem (currently, AFAIK: simp and norm_cast) and are used in attributes should also return an Array Name
• The add field of the attributes should be separated out as definitions that also return an Array Name.
• An alternative 3rd thing is that the add field docs#Lean.AttributeImpl have return type Lean.AttrM A for some configurable A and that for simp and norm_cast we have A := Array Name, but that might be too invasive.

[Kyle Miller]

What's the feasibility of avoiding working with _auxLemmas by unfolding them? (And perhaps using an Expr.beta to fold in the arguments?)

[Floris van Doorn]

Another alternative is that we store in the environment all simp lemmas associated to a declaration (separately, somewhere), and that to_additive has access to that.

[Floris van Doorn]

Kyle Miller said:

What's the feasibility of avoiding working with _auxLemmas by unfolding them? (And perhaps using an Expr.beta to fold in the arguments?)

Unclear: some proofs generated by simp that do not use declarations are actually hard to translate, as described in #10830. But maybe both of them can be solved by beta-reducing more.

[Floris van Doorn]

oh wait, that's not the right issue

[Floris van Doorn]

maybe #10830 is also solved by your suggestion... So it's probably worth looking into...

[Floris van Doorn]

branch#to-additive-4595 builds successfully. Feel free to force-push it into lean-pr-testing-4595 (that will remove your last commit).

[Floris van Doorn]

oh, unsuccesfully, but significantly more

[Floris van Doorn]

And it looks like the remaining failures have nothing to do with to_additive.

[Floris van Doorn]

Kyle Miller said:

What's the feasibility of avoiding working with _auxLemmas by unfolding them? (And perhaps using an Expr.beta to fold in the arguments?)

testing on branch#fvd/to_additive_unfold_aux . It seems to work quite well.

[Floris van Doorn]

It works! #14628