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

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] ring tactic: boolean rings and completeness when supplied with equalities
Date: Thu, 14 Apr 2016 22:00:09 -0400
Authentication-results: mail2-smtp-roc.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-yw0-f177.google.com
Ironport-phdr: 9a23:9f2hNxIwX9OrIHg8PtmcpTZWNBhigK39O0sv0rFitYgUL/TxwZ3uMQTl6Ol3ixeRBMOAu6IC1rWd7vCocFdDyKjCmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TWM5DIfUi/yKRBybrysXNWC34LqiKvvq9X6WEZhunmUWftKNhK4rAHc5IE9oLBJDeIP8CbPuWZCYO9MxGlldhq5lhf44dqsrtY4q3wD86Fpy8kVWqLjOq88ULYQWD8hKiU+4NDhnRjFVwqGoHUGBDY4iB1NViHP7BDhXpry+gL8v+xxkH2TN833VrA5WnKr6a5tRFnpiTsIHzE8+WDTzMd3ifQI81qauxVjztuMM8muP/1kc/aFcA==

Thanks, Daniel.

I was overlooking the fact that the boolean ring in my application is not an integral domain.

So I cannot use nsatz.

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.

-- Abhishek

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

On Thu, Apr 14, 2016 at 8:47 PM, Daniel Schepler <dschepler AT gmail.com> wrote:

On Thu, Apr 14, 2016 at 5:17 PM, Abhishek Anand
<abhishek.anand.iitg AT gmail.com> wrote:
> Context {R:Type}`{Rid:Integral_domain R}.

I thought many boolean rings of interest were not integral domains.
For example, in a classical universe, the boolean ring corresponding
to the boolean algebra P(X) is an integral domain only if X is empty
or a singleton.
--
Daniel

[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, 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, Assia Mahboubi, 04/19/2016