coq-club AT inria.fr
Subject: The Coq mailing list
List archive
Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities
Chronological Thread
- From: Laurent Thery <Laurent.Thery AT inria.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities
- Date: Wed, 13 Apr 2016 22:50:44 +0200
On 04/13/2016 09:54 PM, Abhishek Anand wrote:
A few months ago, I was happy to find in the manual
<https://coq.inria.fr/refman/Reference-Manual028.html> that the ring
tactic can be supplied with
additional ring equalities using the ring [...] syntax.
However, it seems that the ring tactic is NOT complete w.r.t the
supplied equalities. This is illustrated in the example below, which was
checked with Coq 8.5.
maybe the documentation is not clear about this:
the mechanism provided by the equation is very naive (no knuth-bendix like completion), it was meant to be used for cancellation (when a monomial can be expressed in terms of "simpler" ones like y^2 = x + y).
Your example would of course work with the "canonical" H : y = 0.
Is there some other tactic (for unquantified ring equations) that is
complete w.r.t the supplied (unquantified) ring equalities and the ring
laws? It need not be complete w.r.t. definitional equalities.
You can use the nullstellensatz tactic nsatz but of course the complexity of the procedure is much higher:
Require Import Nsatz.
Section test.
Context {R:Type}`{Rid:Integral_domain R}.
Lemma nsatz_test1 : forall (y:R), (1 + 1) * y == y -> y + y == 0.
Proof.
Time nsatz.
Qed.
End test.
Also, is there a similar tactic for boolean rings (where forall x,
x*x=x), instead of regular rings?
Not that I remember of, but calling ring with the equations x * x = x
for all the boolean variables of your expression should do the trick.
--
Laurent
- [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Abhishek Anand, 04/13/2016
- Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Laurent Thery, 04/13/2016
- Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Laurent Thery, 04/13/2016
- Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Abhishek Anand, 04/15/2016
- Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Daniel Schepler, 04/15/2016
- Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Abhishek Anand, 04/15/2016
- Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Daniel Schepler, 04/15/2016
- Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Pierre-Marie Pédrot, 04/15/2016
- Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Abhishek Anand, 04/15/2016
- Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Laurent Thery, 04/15/2016
- Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Laurent Thery, 04/15/2016
- Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Abhishek Anand, 04/16/2016
- Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Daniel Schepler, 04/16/2016
- Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Abhishek Anand, 04/16/2016
- Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Laurent Thery, 04/15/2016
- Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Daniel Schepler, 04/15/2016
- Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Abhishek Anand, 04/15/2016
- Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Laurent Thery, 04/13/2016
- Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities, Laurent Thery, 04/13/2016
Archive powered by MHonArc 2.6.18.