to_additive questions and issues

Stream: mathlib4

[Adam Topaz]

I'm looking at the mathport file GroupTheory.GroupAction.Prod and I have some questions and issues around to_additive.

First, we have

variable [SMul M α] [SMul M β] [SMul N α] [SMul N β] (a : M) (x : α × β)

@[to_additive Prod.hasVadd]
instance : SMul M (α × β) :=
  ⟨fun a p => (a • p.1, a • p.2)⟩

@[simp, to_additive]
theorem smul_fst : (a • x).1 = a • x.1 :=
  rfl
#align prod.smul_fst Prod.smul_fst

Should the line

#align prod.vadd_fst Prod.vadd_fst

be added under the align command above?

In general, what's the procedure for handling align commands in conjunction with to_additive?

Now for the issue. The following results in an error

@[to_additive SMul]
instance hasPow : Pow (α × β) E where pow p c := (p.1 ^ c, p.2 ^ c)
#align prod.has_pow Prod.hasPow

with the following error

application type mismatch
  { smul := fun p c ↦ (c • p.fst, c • p.snd) }
argument has type
  α × β → E → α × β
but function has type
  (α × β → E → E) → SMul (α × β) E

Is this an issue with Mathlib4's to_additive?

[Floris van Doorn]

Yes, please duplicate the #align for the additive versions. It would be nice if mathport could do this automatically, but currently it can't.

[Mario Carneiro]

Mathport can do this automatically, although I think the PR is blocked on something

[Adam Topaz]

@Floris van Doorn what about other automatically generated lemmas, like those generated by simps for example? (This isn't an issue for this file, I'm just thinking ahead)

[Mario Carneiro]

mathport#209

[Floris van Doorn]

I think we want to align those too. They won't be written down very often, so it doesn't matter too much if they're missing, but it would be nice if they could be given automatically by mathport.

[Mario Carneiro]

That PR doesn't support simps, and the general case is quite hard because we don't have any information about what environment declarations correspond to what syntax

[Adam Topaz]

ooohh.... maybe I'll just wait until that PR gets merged before porting this file (since literally every single lemma in this file is tagged with to_additive)

[Adam Topaz]

@Mario Carneiro @Floris van Doorn any advice regarding the error I mentioned?

[Mario Carneiro]

it looks like we need to swap the lambdas in the smul argument

[Mario Carneiro]

did lean 3 handle this?

[Floris van Doorn]

@Mario Carneiro I could try to make an attribute (or some other information) in the Lean 3 environment that contains the information which lemmas are generated by simps. E.g. I could make simps automatically give an attribute, e.g. generated_by_simps [equiv.prod_coe, equiv.prod_symm_coe] for equiv.prod

[Floris van Doorn]

Both Lean 3 and Lean 4 should handle swapping arguments.

[Adam Topaz]

Mario Carneiro said:

did lean 3 handle this?

I guess it did?

[Mario Carneiro]

swapping arguments to a function, yes, but I don't remember anything about swapping lambdas

[Adam Topaz]

actually I'm confused. the mathlib3 file has both

@[to_additive prod.has_vadd] instance : has_smul M (α × β) := ⟨λa p, (a • p.1, a • p.2)⟩

and

@[to_additive has_smul] instance has_pow : has_pow (α × β) E :=
{ pow := λ p c, (p.1 ^ c, p.2 ^ c) }

[Mario Carneiro]

that sounds like it didn't do this automatically

[Yaël Dillies]

Oh, it's missing a to_additive_reorder attribute.

[Floris van Doorn]

Lean 4 since recently also swaps lambdas, but only of the outermost function. Maybe Lean 4 can do this automatically now.

[Floris van Doorn]

Did the Lean 3 version have a to_additive_reorder attribute?

[Adam Topaz]

no the lean3 version is above

[Floris van Doorn]

The new syntax is @[to_additive (reorder := ...)] and that should take care of swapping lambdas.

[Adam Topaz]

I don't understand what the lean3 version is actually doing!

[Floris van Doorn]

In Lean 3 the to_additive is doing basically nothing, except recording that the two declarations you gave are a multiplicative,additive pair

[Adam Topaz]

I see

[Adam Topaz]

So what's the way forward with Lean4?

[Floris van Doorn]

If you don't give an SMul version in Lean 4, it will actually try to generate an smul version, which is of course harder.

[Adam Topaz]

Just to add to the confusion: the mathlib3 version has

@[simp, to_additive] theorem smul_fst : (a • x).1 = a • x.1 := rfl
@[simp, to_additive] theorem smul_snd : (a • x).2 = a • x.2 := rfl

and

@[simp, to_additive smul_snd, to_additive_reorder 6]
lemma pow_fst (p : α × β) (c : E) : (p ^ c).fst = p.fst ^ c := rfl
@[simp, to_additive smul_snd, to_additive_reorder 6]
lemma pow_snd (p : α × β) (c : E) : (p ^ c).snd = p.snd ^ c := rfl

[Mario Carneiro]

Floris van Doorn said:

Mario Carneiro I could try to make an attribute (or some other information) in the Lean 3 environment that contains the information which lemmas are generated by simps. E.g. I could make simps automatically give an attribute, e.g. generated_by_simps [equiv.prod_coe, equiv.prod_symm_coe] for equiv.prod

Yes that will work (although it is blocked on the same thing as mathport#209)

[Adam Topaz]

the fact that smul_snd appears twice in the second code block is not a typo

[Adam Topaz]

I suppose the to_additive smul_snds don't actually do anything here either?

[Mario Carneiro]

Floris van Doorn said:

The new syntax is @[to_additive (reorder := ...)] and that should take care of swapping lambdas.

I guess that needs to be reflected in mathport? I don't recall writing something like that, so it's probably still generating uses of the to_additive_reorder attribute

[Floris van Doorn]

currently the to_additive_reorder attribute gives a warning message asking you to change it to @[to_additive (reorder := ...)]
Since this attribute only occurs occasionally, I don't think it's high priority to implement this in mathport.

[Adam Topaz]

the reorder attribute isn't the heart of the issue I'm having.

[Floris van Doorn]

I think something is wrong with the invocation attribute [to_additive (reorder := 1 4)] Pow.pow in Algebra.Group.Defs. I'll investigate and try to fix.

[Adam Topaz]

Thanks!

[Floris van Doorn]

The reorder attribute is at the heart of your issue: I think another declaration has the wrong reorder attribute, or there is a bug in the implementation of to_additive.

[Adam Topaz]

well, in this case Prod.SMul is defined by hand, while Prod.Pow has a to_additive attribute

[Mario Carneiro]

presumably the relevant function is has_pow.mk

[Floris van Doorn]

I think you're right

[Floris van Doorn]

@Adam Topaz the easiest thing for now is to just port both the Pow and SMul instances (which I think you already do), and then use @[to_additive <name_of_SMul_instance>].

[Floris van Doorn]

The different thing you're trying to do compared to Lean 3 is that you're auto-generating the SMul instance, because the name of the SMul instance has changed.

[Floris van Doorn]

I think to_additive could automatically generate the SMul instance in Lean 4, but to_additive might need a new feature for that.

[Floris van Doorn]

Adam Topaz said:

I suppose the to_additive smul_snds don't actually do anything here either?

It will only generate the dictionary entry. In particular this will mean that additivizing any lemma that using pow_fst will fail, since it will try to replace it by smul_snd and then you'll get a type mismatch.

[Adam Topaz]

What's the porting procedure for naming instances such as this?

[Adam Topaz]

the automatically generated name is Prod.instSMulProd.

[Adam Topaz]

Floris van Doorn said:

I think to_additive could automatically generate the SMul instance in Lean 4, but to_additive might need a new feature for that.

The issue with this is that the to_additive tag for SMul makes the VAdd instance, so SMul does need to be defined by hand.

[Floris van Doorn]

I don't know. I think we can keep the automatically generated names.

[Floris van Doorn]

Adam Topaz said:

The issue with this is that the to_additive tag for SMul makes the VAdd instance, so SMul does need to be defined by hand.

Not necessarily. For some declarations we now use the following to generate pow_lemma, smul_lemma and vadd_lemma

@[to_additive (reorder := ...)] pow_lemma ...
attribute [to_additive] smul_lemma

(and we could of course make this easier to type if we want)

[Floris van Doorn]

Mario Carneiro said:

Yes that will work (although it is blocked on the same thing as mathport#209)

Ok, I'll put that on my todo list (though no promises it will happen this year).

[Adam Topaz]

ruuuuuuggghhhh this file has other issues...
The def

@[to_additive instSMulProd]
instance : Pow (α × β) E where pow p c := ...

has the following context:

M: Type ?u.5487
N: Type ?u.5490
P: Type ?u.5493
E: Type u_1
α: Type u_2
β: Type u_3
inst✝⁵: SMul M α
inst✝⁴: SMul M β
inst✝³: SMul N α
inst✝²: SMul N β
a: M
x: α × β
inst✝¹: Pow α E
inst✝: Pow β E
p: α × β
c: E
⊢ α × β

[Floris van Doorn]

It uses all variables? I wonder why... Is it because of the where syntax?

[Adam Topaz]

oh nevermind the additional instances are removed once the definition is completed.

[Adam Topaz]

By the way, does Lean4's to_additive support the following syntax? to_additive (reorder := 6) foobar?

[Adam Topaz]

it seems that it does not!

[Mario Carneiro]

It does, the reorder argument comes second

[Mario Carneiro]

I think that should be changed BTW, the usual convention is for config args to come first

[Adam Topaz]

oh I see

[Adam Topaz]

yes that's confusing

[Floris van Doorn]

ok, I can change that

[Adam Topaz]

Adam Topaz said:

the fact that smul_snd appears twice in the second code block is not a typo

In the meantime: #17930

[Floris van Doorn]

Mario Carneiro said:

Floris van Doorn said:

Mario Carneiro I could try to make an attribute (or some other information) in the Lean 3 environment that contains the information which lemmas are generated by simps. E.g. I could make simps automatically give an attribute, e.g. generated_by_simps [equiv.prod_coe, equiv.prod_symm_coe] for equiv.prod

Yes that will work (although it is blocked on the same thing as mathport#209)

#17964 adds this information to an attribute (if useful I can change the presentation, e.g. to a single cache).

[Floris van Doorn]

Also, mathport#209 should be unblocked now.

[Mario Carneiro]

I think mathlib is still on 3.49.1, since the 3.50.0 release got yanked, see #17591.