Formalization of Boolean algebra pt. 2

In my previous post I’ve said that to prove that from it follows will be slightly more complicated. That’s what we will do in this post.

Instead of writing the story in a linear order where everything is prepared in advance, I will write it in a hands-on way. We will try to prove the equation right away, and address the roadblocks on the way.

To prove that from it follows , we will have as a given:

xanxoy $a |- ( x * ( ( ~ x ) + y ) ) $.

Next, we just use da (distributivity) and eq to further expand the form. We are doing this because we want to take advantage of . This gets us to :

distr $p |- ( ( x * ( ~ x ) ) + ( x * y ) ) $=
    wx wx wn wy wo wa       $( wff ( x * ( ( ~ x ) + y ) ) $)
    wx wx wn wa wx wy wa wo $( wff ( ( x * ( ~ x ) ) + ( x * y ) ) $)
    wx wy xanxoy            $( |- ( x * ( ( ~ x ) + y ) ) $)
    wx wx wn wy da          $( |- ( x * ( ( ~ x ) + y ) ) = ( ( x * ( ~ x ) ) + ( x * y ) ) $)
    eq $( we have to construct well formed formulas for x and y, and also give the proof that x and x = y $)
$.    

The next thing is to get to . This will be problematic with our equational rule eq.

I turned to ##dependent@freenode and got answers from pgiarrusso and mietek, as usual. Later, the discussion slightly diverged (and touched my (to-be) Masters thesis). Some important topics like implementing lambda calculus in Haskell were discussed, stuff like deciding how much “control” the “parent” language has in our DSL, etc.

Anyway, back to our original topic.

Namely, our rule only supports full replacement of equations instead of replacing subterms within terms. Here’s a quote form Metamath’s wiki article:

All Metamath proof steps use a single substitution rule, which is just the simple replacement of a variable with an expression and not the proper substitution described in works on predicate calculus.

We are hitting exactly this problem.

Along with we will also need . But, then there’s another problem. Metamath works on a very low level, and it does not know of predicates.

There are a few solutions we can take from here. One is implementing subterm substitution, but, as pgiarrusso says, “formalizing capture-avoiding substitution is a major pain”. Another, simpler solution is to encode |- y = z |- y + x = z + x for every operator (*, +). While not the best solution, it’s the one that will allow us to prove the original statement without too much hassle. Note that given the original rules, we cannot deduce this rule, so we have to specify it as an axiom.

Thus, we have the following two new rules in addition to the existing ones:

${
    eqo1 $e |- y = z $.
    eqo  $a |- ( y + x ) = ( z + x ) $.
$}

${
    eqa1 $e |- y = z $.
    eqa  $a |- ( y * x ) = ( z * x ) $.
$}

Now, our proof becomes much simpler.

compl $p |- ( ( x * ( ~ x ) ) + ( x * y ) ) = ( 0 + ( x * y ) ) $=
    wx wy wa     $( wff x * y $)
    wx wx wn wa  $( wff x * ( ~ x ) $)
    wZ           $( wff 0 $)
    wx coa       $( |- x * ( ~ x ) = 0 $)
    eqo          $( in `eqo`, `x` is `x * y`, `y` is `x * ( ~ x)` and `z` is 0 $)
$.

Next, we get to :

zoxay $p |- ( 0 + ( x * y ) ) $=
    wx wx wn wa wx wy wa wo  $( wff ( ( x * ( ~ x ) ) * ( x + y ) ) $)
    wZ wx wy wa wo           $( wff ( 0 + ( x * y ) ) $)
    wx wy distr              $( |- ( ( x * ( ~ x ) ) + ( x * y ) ) $)
    wx wy compl              $( |- ( ( x * ( ~ x ) ) + ( x * y ) ) = ( 0 + ( x * y ) ) $)
    eq 
$.

Further, to get to we simply use co:

xay $p |- ( ( x * y ) + 0 ) $=
    wZ wx wy wa wo     $( wff ( 0 + ( x + y ) ) $)
    wx wy wa wZ wo     $( wff ( ( x * y ) + 0 ) $)
    wx wy zoxay        $( |- ( 0 + ( x * y ) ) $)
    wZ wx wy wa co     $( |- ( 0 + ( x * y ) ) = ( ( x * y ) + 0 ) $)
    eq
$.

Finally, using idoZ we conclude simply :

justZ $p |- ( x * y ) $=
    wx wy wa wZ wo $( wff ( ( x * x ) + 0 ) $)
    wx wy wa       $( wff ( x * y ) $)
    wx wy xay      $( |- ( ( x * y ) + 0 ) $)
    wx wy wa idoZ  $( |- ( ( x * y ) + 0 ) = ( x * y ) $)
    eq
$.

Here’s the table of inference rules:

Rule applied	Formula
	( x * ( ( ~ x ) + y ) )
da	( ( x * ( ~ x ) ) + ( x * y ) )
coa	( ( x * ( ~ x ) ) + ( x * y ) ) = ( 0 + ( x * y ) )
rule 2 and 3 with eq	( 0 + ( x * y ) )
co	( ( x * y ) + 0 )
idoZ	( x * y )

To sum it, building formal systems like this (in an iterative approach) makes me learn a lot about why some rules are needed, and how powerful they are.

Here’s an excerpt from the IRC discussion:

but what’s wrong with Coq? Just don’t use fancy tactics if you want to be low-level. Or just “no tactics”.
– nothing wrong with it, I just feel I should work on a lower level to understand things better. for example how to express П in a language like Metamath. there are so many things I take for granted when writing in Coq. if I find out what those things are I think I’ll learn more