Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities

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: Fri, 15 Apr 2016 11:39:12 +0200


It seems that I now have the complete decision procedure (for boolean
rings) that I was looking for, except that I may have run into a bug in
nsatz.
I have illustrated it in the lemma nsatzNotComplete below, where nsatz
fails unexpectedly and succeeds if I reorder a hypothesis.
Is this a known limitation of nsatz, or just a bug?


It looks like a bug. I look into it.


> I can use the ring tactic with the additional equations for all
> variables, but I was hoping for a complete decision procedure for
> unquantified equations in a boolean ring.

Maybe I am missing something here but as

x = y can be encoded as x + y + 1
and
x -> y as x * y + y + 1

can you just turn your equational problem into a tautology checking that can be solved by ring plus the basic equations x * x = x and x + x = 0 on variables?

--
Laurent



Archive powered by MHonArc 2.6.18.

Top of Page