Michael Soegtrop (May 30 2022 at 09:43): Michael Soegtrop (May 30 2022 at 09:43):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?
Laurent Théry (Jun 01 2022 at 14:02):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.
Michael Soegtrop (Jun 01 2022 at 16:10):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.
Laurent Théry (Jun 01 2022 at 21:54):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
Michael Soegtrop (Jun 02 2022 at 07:47):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.
Laurent Théry (Jun 02 2022 at 11:24):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: Oct 13 2024 at 01:02 UTC