troubleshooting to_additive

Stream: mathlib4

[Jireh Loreaux]

I got the following error from to_additive on a declaration:

application type mismatch
  Group.toDivisionMonoid
argument has type
  AddGroup E
but function has type
  [inst : Group E] → DivisionMonoid E

This makes me think that there is some declaration missing a to_additive tag or else an improper translation. However, the translation Group.toDivisionMonoid → AddGroup.toSubtractionMonoid already exists, so it seems like a translation error on a different declaration. How do I get to_additive to give me more information so I can see exactly where things went wrong? I tried to_additive?, and it told me what it generated, but I didn't see Group.toDivisionMonoid anywhere in the output with set_option pp.explicit true

[Jireh Loreaux]

Also, @Floris van Doorn I noticed that you can write attribute [to_additive non_existent_add_decl] existent_decl and Lean is happy, which seems undesirable and prone to typos making to_additive unexpectedly fail. Is there a way to get it to at least complain if the additive declaration isn't in the environment? If not, we should probably have a linter for this.

[Alex J. Best]

Can you link to a mwe or something? What you said, using ? and pp all is normally how you would debug such things

[Jireh Loreaux]

Have a look at what is currently the first error in !4#2400 (line 265). The inv' field can be fixed by switching rw to simp_rw, but the issue is really with to_additive.

[Jireh Loreaux]

Ah, with pp.all I found something. I think before I just did pp.explicit

[Jireh Loreaux]

I think it's the 1 in the map_one' field not getting converted into a 0.

[Floris van Doorn]

Jireh Loreaux said:

Also, Floris van Doorn I noticed that you can write attribute [to_additive non_existent_add_decl] existent_decl and Lean is happy, which seems undesirable and prone to typos making to_additive unexpectedly fail. Is there a way to get it to at least complain if the additive declaration isn't in the environment? If not, we should probably have a linter for this.

The command attribute [to_additive non_existent_add_decl] existent_decl is very much allowed and widely used, and to_additive will generate the the declaration non_existent_add_decl automatically for you. You can use [to_additive? non_existent_add_decl] to see what declaration to_additive generated. Note however that !4#1881 will make the syntax different, forcing you to write [to_additive existing foo] if foo is a declaration that already exists (which is the less common case).

[Jireh Loreaux]

Aha, I didn't realize it would still translate the declaration if it was added later. I thought that could only be applied to existing declarations. Thanks.

[Floris van Doorn]

Ok, I investigated the error, and the issue is quite subtle.
The proof contains a few occurrences of (0 : ℝ), which are encoded as OfNat.ofNat _ 0 ... to_additive notices that this is a numeral in the real numbers, so it doesn't change it (note: it would only change the numeral if it was 1 anyway, but it looks at this before looking at what the actual numeral is), and leaves this term unchanged.
This is a problem, since simp_rw produces a term OfNat.ofNat .. where the first argument is not syntactically ℝ. Instead, it is (fun x : E => ℝ) (1 : E). And if we don't translate this, Lean will now complain that
(1 : E) is not a valid term anymore in the additive version.

[Floris van Doorn]

Fixed in !4#2419

[Floris van Doorn]

For to_additive (and most/all other attributes), there is no difference in behavior between

@[some_attr] def foo ...

and

def foo ...
attribute [some_attr] foo

[Jireh Loreaux]

@Floris van Doorn bad news: that didn't seem to fix the issue. I stole your fix from !4#2419 but I'm getting the same error.

[Floris van Doorn]

I pushed again. Hopefully the new behavior really fixes it.

[Jireh Loreaux]

Success! Thanks!

[Jireh Loreaux]

@Floris van Doorn I ran into a few other issues in that PR (!4#2400), but I just added the instances by hand for now. If you want to see where I had issues have a look at the porting notes.

[Jireh Loreaux]

There was another one that was an issue with numerals and then also a place where it tried to convert SMul into VAdd

[Floris van Doorn]

The issue with numerals is because norm_num is inserting raw numerals inside the proof term. I can fix that.
The other issue with converting SMul to VAdd was something to_additive also couldn't do in Lean 3 (the additive version of that instance was already in the file before porting). It will require a major rewrite of to_additive to support this. You have arguments [SMul R R'] [IsScalarTower R R' ℝ], and when looking at the argument [SMul R R'] it seems reasonable to additivize it: everything in sight is a variable that can be additivized. Only when looking at [IsScalarTower R R' ℝ] we realize we cannot actually additivize anything (since ℝ is a fixed type).

[Floris van Doorn]

Another issue with GroupSeminormClass is that the additivized version AddGroupSeminormClass is not really an "additive" type. What I mean by this is that we want to additivize One and SMul instances on GroupSeminormClass to One and SMul instances on AddGroupSeminormClass, and not to Zero or VAdd instances.
I'm collecting some ideas of improving to_additive on this branch, that can deal with these kinds of operations.

[Moritz Doll]

I think I have a very similar problem in !4#2499. The definition smul_def in

@[to_additive]
instance : SMul M (Completion X) :=
  ⟨fun c => Completion.map ((· • ·) c)⟩

@[to_additive]
theorem smul_def (c : M) (x : Completion X) : c • x = Completion.map ((· • ·) c) x :=
  rfl

fails with the error

application type mismatch
  instSMulCompletion M X
argument has type
  VAdd M X
but function has type
  [inst : SMul M X] → SMul M (Completion X)

[Moritz Doll]

it seems that the translation of the instance already fails

[Floris van Doorn]

This is lean4#2077. Use the following instead:

@[to_additive]
noncomputable instance : SMul M (Completion X) :=
  ⟨fun c => Completion.map ((· • ·) c)⟩

[Floris van Doorn]

If you define a noncomputable declaration, but don't mark it as noncomputable (because you're in a noncomputable section), then attributes that are executed after compilation (like simp and to_additive are ignored).

[Floris van Doorn]

If @[to_additive?] gives no output at all, it is safe to assume this is the issue. @[to_additive?] is always supposed to show some output.

[Jireh Loreaux]

@Floris van Doorn I have yet another to_additive numeral issue for you. In !4#2736, on line 532 there is the declaration:

@[to_additive zero_lt_one_add_norm_sq]
theorem zero_lt_one_add_norm_sq' (x : E) : 0 < 1 + ‖x‖ ^ 2 :=
  by positivity

(actually, when you look at the file I have provided a workaround proof for the time being), which fails to to_additive-ize the declaration with the error:

application type mismatch
  Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
argument has type
  Mathlib.Meta.NormNum.IsNat 1 1
but function has type
  Mathlib.Meta.NormNum.IsNat 1 0 → Nat.ble 1 0 = true → 0 < 1

This came up several times in this file, and I just worked around each of them by providing an explicit proof instead of using positivity, but it would be good to have an actual fix.

[Kevin Buzzard]

what the heck is the additivised version of 0 < 1 + ‖x‖ ^ 2 supposed to be?

[Yaël Dillies]

0 < 1 + ‖x‖ ^ 2 but where x is valued in an additive normed group rather than a multiplicative one.

[Reid Barton]

Kevin you will have no doubt guessed already that the norm on E satisfies $||x * y|| \le ||x|| + ||y||$

[Reid Barton]

(btw what even is the purpose of this lemma, considering the norm is real-valued?)

[Kevin Buzzard]

There are times when I feel we go a bit too far :-)

[Floris van Doorn]

to_additive is indeed known incompatible with positivity, because of the way numerals are represented. !4#2726 should solve this in a systematic way, by handling numerals differently.

[Floris van Doorn]

It now works: !4#2758