coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] solving Qc inequalities

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] solving Qc inequalities
Date: Fri, 8 Jan 2021 12:47:44 -0800
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-io1-f43.google.com
Ironport-phdr: 9a23:ql7+EBYq56U9O5PY7tmqmFz/LSx+4OfEezUN459isYplN5qZr8W7bnLW6fgltlLVR4KTs6sC17OJ9fq8BCdfu96oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCybL9vLhi6txvdu8YWjIdtKKs91AbCr2dVdehR2W5mP0+YkQzm5se38p5j8iBQtOwk+sVdT6j0fLk2QKJBAjg+PG87+MPktR/YTQuS/XQcSXkZkgBJAwfe8h73WIr6vzbguep83CmaOtD2TawxVD+/4apnVAPkhSEaPDM/7WrZiNF/jLhDrR2upxJxzY3abpyLOvViZa7SZ88WSHBbU8pNSyBMAIWxZJYPAeobOuZYqpHwqkcVohu+BAmsH+PvxSFLhnTrwaA61f4uEQfb0wc9GN8Bqm/brNX0NKcJUeC60qrIwS/ZYPNQwzj97pXHfgogofGNQbJwftHcyUYqFwzfj1WQrZbpMC+S1uQIqmWW6fdrWu2zhWA9sQ5xviSvydk2ionPno8Y1FDK+DtkzYs6KtO1VVB3bNC6HJZTqyyXOYt4Tt0tTmxsuis2178LtIO7cSYKypkqxBzSZ+CZf4SW4R/uV+icLDFlj3xrf7K/ggy98UmmyuDkSsa010xKrixbndnIsnABzQLc5dWaSvZ740yv2i6P2hjN5u1YJU04j6nWJp47zrItl5cesF7PEyD4lUjwkaSYbF8r+vKy5OTierjmpoGTN4tzigzmN6QhgM2/AeAhPggPWGiX5P2w1LPs8ED3WrlKgfo2kq7WsJDeO8sXvLK2AwhQ0oo76ha/CSmp0MgAkHUZMF5IfAiLgovpNl3UPfz1DPayj06jnTpl3/zGO6fuApTJLnjNirfherN95lZGxwUozdBf5olUCrEfL/LwQEP+rtrYAQU/MwOp2ernCdR91p8RWW+UDa+ZNbndsV6M5u41P+aMY4oVtC7nK/c5//7ukWM5mVgFcKa12psXcWm0EehiI0WEenXhmcwBEGcPvgomVuPmklyCUThJZ3azRa0w/D87CJj1RbvEE4uqmfmK2DqxVsldYXkDAVSRG1/pcZ+FUrECcnTBDNVml2ktX7igUI8s1lmHsgb8x/IzJ+DU+zYYuJGl3d584eGVlBAu+hR7Cs2c1yeGSGQizTBAfCM/wK0q+R818VyEy6Ut26UER+wW3OtAV0IBDbCZ1/ZzUomgVQfIf9PPQ1GjEI3/UGMBC+kpytpLWH5TXtCrjxTNxS2vWuZHmLmCBZhy+aXZjSGoepRNjk3e3axktGEIB8tCMWr82/x6/gnXQo/OygCXy/3seqMb0yrAsmyEyDjWsQ==

I see that there is a field instance for Qc.

Is there a psatz/lra like tactic for Qc?

If not, is there a tactic to preprocess a Qc goal to Q, something like what zify does? (Thanks Frédéric for solving the problem in the other thread.)

Thanks,

-- Abhishek

http://www.cs.cornell.edu/~aa755/

[Coq-Club] solving Qc inequalities, Abhishek Anand, 01/08/2021
- Re: [Coq-Club] solving Qc inequalities, Frédéric Besson, 01/08/2021
- Re: [Coq-Club] solving Qc inequalities, Elias Castegren, 01/22/2021