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: Daniel Schepler <dschepler 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: Fri, 15 Apr 2016 17:08:26 -0700
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=dschepler AT gmail.com; spf=Pass smtp.mailfrom=dschepler AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi0-f43.google.com
  • Ironport-phdr: 9a23:HH8v3B2CPfCkYTQtsmDT+DRfVm0co7zxezQtwd8ZsegRK/ad9pjvdHbS+e9qxAeQG96Lu7QZ26GN6ejJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd6CyZnnnLvos7ToICx2xxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cYk7sb+sVBSaT3ebgjBfwdVWx+cjN92Mq+nh7aBSCL+3FUBm4Ri19DBxXPxBD8RJb49CXg4LlTwi6faOH/S7E5XXyZ5KdmUBvlkm9TOyUy8GzPjsFqpK1eqROl4Rd4xtiHM8muKPNic/aFLpshTm1bU5MUDnQZDw==

On Fri, Apr 15, 2016 at 4:36 PM, Abhishek Anand
<abhishek.anand.iitg AT gmail.com>
wrote:
> Thanks, Daniel, Pierre-Marie, and Laurent.
>
> I am missing one piece of the puzzle.
> My boolean ring (say B) has infinitely many elements.
> How do I justify changing the types of the variables from B to bool, or to
> Z/2Z?

Basically, for a finite set A (e.g. the atoms of the identity you want
to prove), the free boolean ring with generators in A is isomorphic to
∏ [S ⊆ A] Z/2Z - with a generator a ∈ A corresponding to λ S . χ(a ∈
S) where χ is the characteristic function T ↦ 1, F ↦ 0. Given any
other boolean ring B with map f : A -> B, the morphism ∏ [S ⊆ A] Z/2Z
-> B is given by g ↦ ∑ [S ⊆ A] { g(S) · ∏ [ a ∈ S ] f(a) · ∏ [ a ∈ A ∖
S ] (1 - f(a)) }.

Now, if you construct a boolean ring equivalent of a truth table for
some expression in terms of the variables in A, then each column of
the truth table corresponds to an element of ∏ [S ⊆ A] Z/2Z. So, if
the final column of the "truth table" reads all zeros, then the
corresponding element of the free boolean ring is equal to 0.
Therefore, it maps to 0 under the morphism ∏ [S ⊆ A] Z/2Z -> B, and
expanding the homomorphism property will give you the identity you
wanted. (On the other hand, each row of the "truth table" corresponds
to an assignment of values in Z/2Z to the variables in A, and the
resulting values of subterms.)
--
Daniel Schepler



Archive powered by MHonArc 2.6.18.

Top of Page