noncomputable and to_additive

Stream: mathlib4

[Sebastien Gouezel]

A weird interaction between to_additive and noncomputable. The following works fine

import Mathlib.MeasureTheory.Measure.Haar.Basic
noncomputable section
open MeasureTheory

-- @[to_additive]
instance (α : Type*) [MeasurableSpace α] (G : Type*) [SMul G α] : SMul G (Measure α) :=
{ smul := fun g μ ↦ Measure.map (fun x ↦ g • x) μ }

But if you uncomment the to_additive, then you get a complaint

failed to compile definition, consider marking it as 'noncomputable' because it depends on 'MeasureTheory.Measure.map', and it does not have executable code

Marking it by hand as noncomputable fixes it, so this is not a blocker at all, but still it doesn't seem right. @Floris van Doorn , any idea what could be going wrong?

[Alex J. Best]

I would say this is a core issue. Declarations in noncomputable sections that are not compiled are not currently tagged noncomputable
see

import Mathlib.Tactic


noncomputable section
def t : ℕ := Classical.choose (⟨0, trivial⟩ : ∃ n, True)

end section
noncomputable def t' : ℕ := Classical.choose (⟨0, trivial⟩ : ∃ n, True)


#eval t

open Lean Tactic Elab Meta
#eval show MetaM Unit from do
  dbg_trace isNoncomputable (← getEnv) `t

#eval show MetaM Unit from do --for comparison
  dbg_trace isNoncomputable (← getEnv) `t'

[Alex J. Best]

I'll make a PR to change this later today, and see if it is a desired change or not

[Alex J. Best]

This is now https://github.com/leanprover/lean4/pull/2610

[Sébastien Gouëzel]

I was about to mention a bad interaction between to_additive and noncomputable section that I encountered recently, with the following MWE:

import Mathlib

noncomputable section

@[to_additive]
def myOne (α : Type) [One α] : α := by
  have : ∃ (x : α), x = 1 := ⟨1, rfl⟩
  exact Classical.choose this

where one gets a complaint that the additivized declaration should be marked noncomputable, although one is already in a noncomputable section.

Then I realized that there was already a discussion about this on Zulip, initiated by myself (!) 2 years ago, with a suggested fix. @Kim Morrison, is it something core could consider fixing?

[Kim Morrison]

Yes, definitely. Someone would need to create an issue, however, explaining the problem, ideally something that doesn't need Mathlib at all.

Tagging Cameron Zwarich on such an issue is probably the right thing to do. Everything about noncomputable is in flux at the moment, as we switch everyone over to the new compiler in the near future.

[Sébastien Gouëzel]

There is already an issue and a PR at lean4#2610. @Cameron Zwarich

[Kim Morrison]

An separate issue is probably more likely to get traction than an abandoned broken PR.

[Cameron Zwarich]

Apologies for not replying in detail sooner, although I'm not sure I would've given as good of an answer at the time anyways.

This change is required for correctness, beyond any improvements it would enable for to_additive. We fixed some soundness issues in the noncomputable check (especially when used with native_decide) by moving it earlier, but this relies on the noncomputable attribute, not checking for the existence of IR. We still have a second last-ditch check in the backend, but it's entirely possible that after irrelevant terms are erased, we erroneously optimize away the use of the definition that does not have IR and then fail to catch it at this point.

I'm pretty sure that the approach in the PR won't work after async elaboration, so I'll make a new issue and close the PR. I'm a bit nervous about changing this a few days before we cut a new release, but maybe I'll at least try to test it out tomorrow, now that nightly-testing is green again.

[Cameron Zwarich]

https://github.com/leanprover/lean4/issues/9021