coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Elias Castegren <eliasca AT kth.se>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Getting lra to work with canonical rationals
Date: Thu, 8 Oct 2020 11:39:22 +0000
Accept-language: sv-SE, en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=eliasca AT kth.se; spf=Pass smtp.mailfrom=eliasca AT kth.se; spf=Pass smtp.helo=postmaster AT smtp-4.sys.kth.se
Ironport-phdr: 9a23:U9DADBIYTVio4GDia9mcpTZWNBhigK39O0sv0rFitYgeKvvxwZ3uMQTl6Ol3ixeRBMOHsq0C17ud6vyocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmTiwbal9IRiyogndq8YbipZ+J6gszRfEvmFGcPlMy2NyIlKTkRf85sOu85Nm7i9dpfEv+dNeXKvjZ6g3QqBWAzogM2Au+c3krgLDQheV5nsdSWoZjBxFCBXY4R7gX5fxtiz6tvdh2CSfIMb7Q6w4VSik4qx2ThLjlSUJOCMj8GzPisJ+kr9VoA6vqRJ8wo7bfI6aOeFkca/BeNMXX3ZNUtpTWiFHH4iyb5EPD+0EPetAoIf9o1oOogGlBQKxGu7g0CRIhmPo0q01yeQuDwfG1xEnEt0QtHTUrc/6NLwOXu+v16TIzinDb/NM1Tfm9ofFaxYsquyDUrxsa8Te01UvFx/bgVWKr4zoJzOY2+oOvmWU7+dtUf+jhm86pg9/rDWj2sMhh4rKi48Lyl7J6Tl0zYUpKdC8RkB3fcCoHZhQuiyEM4Z6XMMvTWFutS0nybMGoYa2cDUExZg73RLTdfKKfoqS7h/sV+udOyp0iXZrdb6nhBu//1KsxvP8W8WqylpHrTdJnsPIu30Lyhfd8NKISuFn8UekwTuP1x7c6uVDIU0sjqrbLoIhwqYpmpccq0jDBS/3mF7sgK+VakUk+vKk6//5bbn+p5+cMZF7ih3mP6gzlMGzHf40PhYAUmWZ4+ix277u8VfkTLhOgPA6iqzZv4rbJcQfqK65GQhV0oM75hmhCzem0c4XnWIbI11fYx+HjJTpO1HULPDjE/izm06snytzx/DaIr3hBY3AIWTEkLf4ZLpy90pcyBcowt1E/JJVCrQBIOrpVUPrtdzYCAU5Mw2uzOr9BtV9zNBWZWXaSKSeKebZtUKCzuMpOeiFIoEP8n6pIP88ovXqkHURmFkHfKDv04FBO16iGfEzDkGYaGGkqd4aDWoFpAc4BLjnjFyLSjVaT3WuX+Qn62doW8qdEY7fS9X10/S61yChE8gOPzEUOhW3CX7tMr68dbIJYSOWLNVml2xWVqShDZQsh0j36V3KjoF/J++RwRU28JLu0N8str/IkA0qsGAyFNWGlWKRTydvkzFRHmNk7OVEuUV4j2y7/+1gmfUIR99P57VSX1ViOA==

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

[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