to_additive and noncomputable

Stream: mathlib4

[Yakov Pechersky]

The plain @[to_additive] decorator does not properly transmit noncomputable to the derived definition. It works fine if the tagging is done after the fact:

import Mathlib.Tactic.ToAdditive

@[to_additive Bar]
def Foo (a : α) : α := a

@[to_additive Bar.bar] -- this does not work
noncomputable def Foo.foo (h : ∃ _ : α, True) : α := Classical.choose h

noncomputable def Foo.foo2 (h : ∃ _ : α, True) : α := Classical.choose h
noncomputable def Bar.baz (h : ∃ _ : α, True) : α := Classical.choose h

attribute [to_additive Bar.baz] Foo.foo2 -- this works

[Alex J. Best]

mathlib4#625

[Jovan Gerbscheid]

I have run into this issue again. The following doesn't work

import Mathlib.Data.Finsupp.SMul

noncomputable section

variable (k G : Type) [Semiring k]

@[to_additive]
def MonoidAlgebra : Type :=
  G →₀ k

@[to_additive]
def MonoidAlgebra.single (a : G) (b : k) : MonoidAlgebra k G := Finsupp.single a b
/-
failed to compile definition,
compiler IR check failed at 'AddMonoidAlgebra.single._redArg'.
Error: depends on declaration 'Finsupp.single',
which has no executable code;
consider marking definition as 'noncomputable'
-/

[Junyan Xu]

Just add noncomputable?

@[to_additive]
noncomputable def MonoidAlgebra.single (a : G) (b : k) : MonoidAlgebra k G := Finsupp.single a b

apparently works.

[Eric Wieser]

This is the workaround we currently use I think

[Junyan Xu]

Finsupp.single is noncomputable so even without to_additive you need to write noncomputable for any def depending on it. (or use noncomputable section)

[Jovan Gerbscheid]

Yes, I used noncomputable section. But for some reason that doesn't work, and noncomputable does work.

[Kenny Lau]

i guess the auto gen can't see noncomputable section

[Junyan Xu]

I wonder how good LLMs (e.g. Claude) are at producing working code that fixes this ...

[Kenny Lau]

LLM needs data, and we don't have a lot of meta code

[Yaël Dillies]

@Jovan Gerbscheid, are you heavily modifying Algebra.MonoidAlgebra.Defs? If so, please be aware that we'll get monster conflicts with #25273

[Jovan Gerbscheid]

I am :sweat_smile:

But I'm also doing this in order to test the new to_additive heuristic. So it might make more sense to merge your change first, and then use @[to_additive] in the file afterwards?

[Thomas Murrills]

(Note: currently fixing the noncomputable section issue in to_additive, unless someone has beaten me to it :) )

[Thomas Murrills]

Oops, maybe I spoke too soon. The flag set by noncomputable section lives in the CommandElabM state (namely, the scopes) but we seem to only have access to CoreM when adding attributes. Hmm.

[Thomas Murrills]

(Hopefully we can access the noncomputability indirectly through the decl if we're careful—let me see if I can get this to work.)

[Thomas Murrills]

Huh, turns out that we don't ever mark the definitions in a noncomputable section noncomputable in the noncomputable extension—we just refrain from logging errors when compiling (hence why the current approach in to_additive doesn't work)! I wonder if this ought to be changed. (I'll see if I can detect whether compilation has occurred or not, regardless.)

[Yaël Dillies]

If we merge your changes first, then my changes are half as short!

[Thomas Murrills]

I've got it working by checking for executable code, but this has the slightly unfortunate side effect of successfully adding a generated noncomputable definition even when the original is loudly failing to compile (due to being outside of noncomputable section)—hence, the original declaration has no executable code, but to_additive has no way of telling that it "should". (We can't look for messages in the log or anything in the infotree, since these are reset before running add.)

I think this is generally fine as a workaround, though, since we will never have an error in final code.

Ideally, I think everything noncomputable in a noncomputable section should get marked noncomputable, but this is a core change I don't think we should wait for.

#28610