is_pow_tower

Stream: general

[Johan Commelin]

Should we multiplicativize is_scalar_tower to is_pow_tower? And thing like smul_comm_class into pow_comm_class?

[Anne Baanen]

I don't see any objection if you think it's worth your time, do you have a mathematical example in mind where this is useful?

[Eric Wieser]

I think we're going to need to_additive to be more clever before we embark on that

[Eric Wieser]

Presumably we want to be able to write is_pow_tower F nat int, which is backwards compared to is_scalar_tower int nat F

[Anne Baanen]

Doesn't it handle pow and smul pretty well nowadays?

[Eric Wieser]

Right now to_additive_reorder only supports adjacent argument swaps, and doesn't actually check that your invocation does what you want

[Eric Wieser]

I've been having a hard time with in in #15478

[Eric Wieser]

In particular, there's no way to additivize prod.mk_pow to prod.smul_mk without having the argument order be unnatural for one of the lemmas

[Johan Commelin]

Have to_additive support would of course be extremely useful. Maybe even a prerequisite.

[Johan Commelin]

Is it worth trying to tackle this before a port to Lean 4?

[Eric Wieser]

By "do what you want" above, I mean that if you do something like

lemma foo_smul : foo (a • b) = a • b := sorry
@[to_additive foo_smul] lemma pow_foo : foo (a ^ b) = a ^ b := sorry

with or without to_additive_reorder, you get no diagonistic for getting it wrong until you actually use the lemma:

-- fails, generating an invalid additive proof
@[to_additive] lemma pow_foo' : foo (a ^ b) = a ^ b := by rw pow_foo

[Yaël Dillies]

Also note that this is the one case I know where it would make sense to additivize twice in a room. Namely, we will want the vadd versions as well eventually.

[Eric Wieser]

We already have the vadd versions of many of these