coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
- [Coq-Club] Getting lra to work with canonical rationals, Elias Castegren, 10/08/2020
- Re: [Coq-Club] Getting lra to work with canonical rationals, Frédéric Besson, 10/08/2020
- Re: [Coq-Club] Getting lra to work with canonical rationals, Tej Chajed, 10/08/2020
- Re: [Coq-Club] Getting lra to work with canonical rationals, Raphaël Cauderlier, 10/09/2020
- Re: [Coq-Club] Getting lra to work with canonical rationals, Théo Zimmermann, 10/09/2020
- Re: [Coq-Club] Getting lra to work with canonical rationals, Raphaël Cauderlier, 10/09/2020
- Re: [Coq-Club] Getting lra to work with canonical rationals, Théo Zimmermann, 10/09/2020
- Re: [Coq-Club] Getting lra to work with canonical rationals, Raphaël Cauderlier, 10/09/2020
- Re: [Coq-Club] Getting lra to work with canonical rationals, Tej Chajed, 10/08/2020
- Re: [Coq-Club] Getting lra to work with canonical rationals, Frédéric Besson, 10/08/2020
Archive powered by MHonArc 2.6.19+.