Zulip Chat Archive
Stream: general
Topic: is_pow_tower
Johan Commelin (Jul 27 2022 at 11:13):
Should we multiplicativize is_scalar_tower
to is_pow_tower
? And thing like smul_comm_class
into pow_comm_class
?
Anne Baanen (Jul 27 2022 at 11:15):
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 (Jul 27 2022 at 11:15):
I think we're going to need to_additive
to be more clever before we embark on that
Eric Wieser (Jul 27 2022 at 11:16):
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 (Jul 27 2022 at 11:16):
Doesn't it handle pow
and smul
pretty well nowadays?
Eric Wieser (Jul 27 2022 at 11:16):
Right now to_additive_reorder
only supports adjacent argument swaps, and doesn't actually check that your invocation does what you want
Eric Wieser (Jul 27 2022 at 11:17):
I've been having a hard time with in in #15478
Eric Wieser (Jul 27 2022 at 11:18):
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 (Jul 27 2022 at 11:20):
Have to_additive
support would of course be extremely useful. Maybe even a prerequisite.
Johan Commelin (Jul 27 2022 at 11:21):
Is it worth trying to tackle this before a port to Lean 4?
Eric Wieser (Jul 27 2022 at 11:22):
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 (Jul 27 2022 at 16:52):
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 (Jul 27 2022 at 17:22):
We already have the vadd versions of many of these
Last updated: Dec 20 2023 at 11:08 UTC