coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- 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+.