The Coq mailing list

[Frédéric Besson <frederic.besson AT inria.fr>]

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
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.

Require Import QArith.Qcanon.

Require Import ZifyClasses.
Declare ML Module "zify_plugin".

Program Instance InjQc : InjTyp Qc Q :=
  mkinj _ _ this (fun q => (Qred q) = q) canon.
Add Zify InjTyp InjQc.

Program Instance InjQ : InjTyp Q Q :=
  mkinj _ _ (fun x => x) (fun q => True) (fun _ => I).
Add Zify InjTyp InjQ.


Instance Op_le : BinRel Qcle :=
  {| TR := Qle; TRInj := (fun n m : Qc => iff_refl (n <= m)%Q) |}.
Add Zify BinRel Op_le.

Program Instance Op_plus : BinOp Qcplus :=
  {| TBOp := fun x y => Qred (Qplus x y); TBOpInj := fun n m : Qc => eq_refl|}.
Add Zify BinOp Op_plus.

Program Instance Op_Q2Qc : UnOp Q2Qc :=
  {| TUOp := fun x => Qred x ; TUOpInj := _ |}.
Add Zify UnOp Op_Q2Qc.


Ltac qify :=
  Zify.zify ; repeat rewrite Qred_correct in *.

Example qc_le_trans :
  forall q1 q2 : Qc,
    0 <= q1 ->
    0 <= q2 ->
    0 <= q1 + q2.
Proof.
  intros q1 q2 Hle1 Hle2.
  qify.
  lra.
Qed.