As far as I can tell field for R only supports the power function with nat exponents, but not the powerRZ function. I only know roughly how field works. Would it be possible to extend it to understand powerRZ?

depends which kind of equations you expect `field`

to solve with `powerRZ`

. For easy ones, a preprocessing could be enough

```
Goal forall x, (powerRZ x (-2)) * x * x = 1.
intros.
unfold powerRZ; simpl.
field.
```

but I guess you are looking for something more fancy.

I e.g. have quotients of powers with variable exponent, such that the variable part of the exponent cancels after expansion. This usually requires a bit of manual work.

yep so the problem is already there with usual exponent.

```
Goal forall x n, x ^ (n + 2) = x ^ n * x * x.
intros.
Fail ring.
repeat rewrite pow_add; ring.
```

but I agree it would be good to have this processing already included for `R`

Yes, some automated preprocessing would be helpful.

With short terms the manual preprocessing is straight forward. With terms which span a few lines, it is much harder to control the preprocessing such that things are not messed up in other places of the term.

if the exponents stay in the presburger fragment (+ and multiplication by constant) I think it is relatively easy to get some proper ltac preprocessing.

It is more delicate if you want to handle multiplication too.

Last updated: Sep 30 2023 at 07:01 UTC