ring_exp with integer powers

Stream: general

[Yury G. Kudryashov]

Here is an #mwe:

import tactic.ring_exp

example {k : Type*} [field k] {x : k} (hx : x ≠ 0) (m : ℤ) : x ^ m * x ^ m = x ^ (2 * m) :=
by ring_exp -- fails

[Yury G. Kudryashov]

Do I understand correctly that ring_exp only works with natural powers? Is it hard to make it work for integer powers?

[Yury G. Kudryashov]

Of course, the actual expression where I wanted to use ring_exp is much longer.

[Eric Rodriguez]

docs#ring_exp mentions that it is; from a glance through the code, I think it'd just be a looot of special casing but I'm not too sure

[Yury G. Kudryashov]

I see a few problems with supporting fpow (without looking at the code):

• we have two different lemmas, e.g., for x ^ (m + n) = x ^ m * x ^ n, see docs#gpow_add and docs#fpow_add;
• for the fpow case we need to prove x ≠ 0 here and there;
• need to deal with, e.g., x ^ m * x ^ n, where m : int, n : nat.

[Yakov Pechersky]

Can one case on m as nonneg and neg, and use field_simp first?

[Yury G. Kudryashov]

field_simp won't deal with x ^ m * x ^n

[Yury G. Kudryashov]

And you can have many ms and ns

[Yury G. Kudryashov]

I don't want the proof to be exponentially large (and exponentially slow) in the number of exponents in the formula.

[Yakov Pechersky]

Of course. The forcing to nat via a case is just a possible stopgap for a two exponents. It's the "brute force" tactic that you can use as the baseline for comparing performance :-)