Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Getting lra to work with canonical rationals

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Getting lra to work with canonical rationals


Chronological Thread 
  • From: Frédéric Besson <frederic.besson AT inria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Getting lra to work with canonical rationals
  • Date: Thu, 08 Oct 2020 14:51:46 +0200
  • Organization: Inria

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.



Archive powered by MHonArc 2.6.19+.

Top of Page