The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

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