The Coq mailing list

[Tej Chajed <tchajed AT mit.edu>]

I ran into exactly this problem recently. It turns out that the Qc operators are reasonably close to Q, so you might be able to do the preprocessing yourself:

Ltac qc_lra := unfold Qclt, Qcle in *; cbv [Qcanon.this Qcplus Q2Qc] in *; try rewrite -> !Qred_correct in *; lra.




I can't really tell if Frederic's solution is more robust than doing it manually since I don't know how much of an abuse of zify it is.


On Thu, Oct 8, 2020 at 7:52 AM Frédéric Besson <frederic.besson AT inria.fr> wrote:

Hi Elias,

`lra` does not support Qc.
This could probably be done but this requires writing some Ocaml code.

Attached is a solution which exploits `zify` to pre-process operators
in Qc. I say `exploit` because, as the name implies, `zify` has been
designed to pre-process towards Z. So, it kind of works by chance...


Best,
--
Frédéric

On Thu, 2020-10-08 at 11:39 +0000, Elias Castegren wrote:
> Hi all
>
> I have a Coq development which uses the rational numbers from QArith.
> Most arithmetic issues can be nicely solved by the lra tactic:
>
> Require Import QArith.
> Require Import Psatz.
>
> Example q_le_trans :
>   forall q1 q2 : Q,
>     0 <= q1 ->
>     0 <= q2 ->
>     0 <= q1 + q2.
> Proof.
>   intros q1 q2 Hle1 Hle2.
>   lra.
> Qed.
>
> Because rational numbers use their own equivalence rather than
> syntactic equality, I would like to move to the Qc type from
> QArith.Qcanon, which are rational numbers which are know to be
> irreducible. However, when doing that, lra stops working:
>
> Require Import QArith.Qcanon.
>
> Example qc_le_trans :
>   forall q1 q2 : Qc,
>     0 <= q1 ->
>     0 <= q2 ->
>     0 <= q1 + q2.
> Proof.
>   intros q1 q2 Hle1 Hle2.
>   Fail lra.
> Abort.
>
> I understand that this is because addition is now defined as Q2Qc (q1
> + q2), where Q2Qc is a function that takes rational numbers to their
> irreducible counterpart, and I guess that lra does not ”understand"
> this function. However, it feels like any arithmetic result over Q
> should hold for Qc as well. Is there any way of extending lra, or
> some simple preprocessing I can do to the proofs to turn the proof
> context to one that lra can work with?
>
> Thanks
>
> /Elias