Stream: Coq users

Topic: field and powerRZ


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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: Mar 29 2024 at 09:02 UTC