Otter Version of Don Knuth's Hand Proof

July 2005

This page is a continuation of a discussion about finding a first-order proof of a median algebra problem. Click here to go to the median algebra home page.

After studying our first Otter proof of the long form of distributivity, Knuth sent us the following hand proof of the short form of distributivity. The following excerpt is from Knuth's email.

Here is how I think one can boil "median.pf" down to the
shortest purely equational proof of the (short) distributive law
that I know. I will use my angle-bracket notation for the ternary
operator, and I'll freely apply commutative and associative laws.
The associative law will be indicated by writing <xwywz> for
<<xwy>wz> and/or <xw<ywz>>; indeed, <xwywz> is a valid median of five
elements, fully commutative.

1) <<xyz>yz>=<xyz>. (absorption law)
Proof. <<xyz>yz>=<xy<zyz>>=<xyz>.

2) <x<xuv><zuv>>=<xuv>. (case x=y of short distributive law)
Proof (Kolibiar and Marcisov\'a). <x<xuv><zuv>>=<<xuv>xux<zuv>>=
<<xuv>x<zuxuv>>=<x<xuv>u<xuv>z>=<<xuv><xuv>z>=<xuv>.

3) If w=<wxy>=<wxz>=<wyz> then w=<xyz>. (median law; it can obviously
   be converted to purely equational substitutions when I apply it below)
Proof. w=<yxw>=<yxzxw>>=<<yxz>x<zyw>>=<xyz> by (2).

4) <<xuv><yuv><zuv>>=<x<yuv><zuv>>. (equivalence of two distributive laws)
Proof (Otter had this as 21054, but I give my own proof).
  <<xuv><yuv><zuv>>=<<<xuv>x<zuv>><yuv><zuv>>  (by (2))
   =<<<<xuv>x<yuv>>x<zuv>><yuv><zuv>> (by (2))
   =<<<<xuv><zuv>x><yuv>x><yuv><zuv>>
   =<<<xuv><zuv>x><yuv><x<yuv><zuv>>> (associativity)
   =<x<yuv><zuv>> (again (2)).

5) <x<yuv><zuv>>=<<xy<zuv>><yuv><zuv>>. (Otter's first law (7407))
Proof. <x<yuv><zuv>>=<x<y<yuv><zuv>><zuv>>=<x<zuv>y<zuv><yuv>>.

6) <<<xyz>uv>x<yuv>>=<<xyz>uv>. (Otter's second law (24293))
Proof. <x<<xyz>uv><yuv>>
  =<<xy<<xyz>uv>><<xyz>uv><yuv>>  (by (5))
  =<<<xy<<xyz>uv>><<xyz>uv><xyz>><<xyz>uv><yuv>>  (by (2))
  =<<xy<<xyz>uv>><<xyz>uv><<xyz><<xyz>uv><yuv>>>  (associativity)(!)
  =<<xy<<xyz>uv>><<xyz>uv><<xyz>uv>> (by (2))
  =<<xyz>uv>.

7) <<xyz>uv>=<x<yuv><zuv>>. (the short distributive law)
Proof (mine). <<<xyz>uv><yuv><zuv>>=<<<xyz>uv>y<zuv>> by (4),
and this equals <<xyz>uv> by (6). Letting w=<<xyz>uv>, we have therefore
established the equations w=<wx<yuv>>=<wx<zuv>>=<w<yuv><zuv>>. Apply (3). QED

As an exercise for proof sketches, we used Knuth's hand proof as a starting point to find a new Otter proof. Note that while the hand proof omits details such as applications of the commutative and associative laws of median algebra and uses a simplified representation that accounts for associativity, Otter needs to work out all of the details explicitly.

For this exercise, we had to replace sequences of equalities such as t1 = t2 = ... = tn with sets of equality unit clauses. In addition, when combining the 7 steps into a single proof, we had to address the fact that the result of Step 3 is a nonunit and therefore does not naturally change its role from being a separate lemma to a step in a larger proof.

Here are Otter proofs corresponding to Knuth's 7 steps.

f(f(x,y,z),y,z) = f(x,y,z) # label("Step 1"). proof f(x,f(x,u,v),f(z,u,v)) = f(x,u,v) # label("Step 2"). proof f(w,x,y) != w | f(w,x,z) != w | f(w,y,z) != w | f(x,y,z) = w # label("Step 3"). proof f(f(x,u,v),f(y,u,v),f(z,u,v)) = f(x,f(y,u,v),f(z,u,v)) # label("Step 4"). proof f(f(x,y,f(z,u,v)),f(y,u,v),f(z,u,v)) = f(x,f(y,u,v),f(z,u,v)) # label("Step 5"). proof f(f(f(x,y,z),u,v),x,f(y,u,v)) = f(f(x,y,z),u,v) # label("Step 6"). proof
f(x,f(y,u,v),f(z,u,v)) = f(f(x,y,z),u,v) # label("Step 7"). proof

Putting it all together into a single proof ...

f(x,f(y,u,v),f(z,u,v)) = f(f(x,y,z),u,v) # label("Distributivity (short)"). proof

Finally, we used this proof as hints to find a new proof of the long form of distributivity. The new proof is substantially shorter than the first proofs we found.

f(f(x,y,z),f(u,y,z),f(w,y,z)) = f(y,z,f(x,u,w)) # label("Distributivity (long)"). proof