More equality proofs with instantiated definitions (Mathematical Methodology)

More equality proofs with instantiated definitions

We quote from the chapter "The design of a proof of equality" the following about the maximum operator ↑ and the minimum operator ↓ . For all real $w,x,y$

(0) ${x}^{ \uparrow }y \leq w \equiv \times \leq w \land y \leq w$ (1) $w \leq x \uparrow y \equiv w \leq x \vee w \leq y$ (2) $w \leq x \downarrow y \equiv w \leq x \land w \leq y$ (3) ${x}^{2}{y}^{2}{w}^{2} \equiv x{y}^{2} + y{x}^{2}$

and in the proof of the above, essential use was made of the antisymmetry $\sigma f\leq$ , i.e

$p = q \Leftrightarrow p \leq q \land q \leq p$ for all $p,q$ .

Remark In predicate calculus, the antisymmetry of the implication, i.e.

$$ [ X \equiv Y ] \Leftarrow [ X \Rightarrow Y ] \land [ Y \Rightarrow X ] $$

is often used similarly; it is there known as "a proof by mutual implication". Also the somewhat more general term "ping-pong argument" is in use: an appeal to (4) leads to a ping-pong argument but not to a proof by mutual implication. (End of Remark.)

Sometimes the ping-pong argument is entirely appropriate, for instance, when the ping part is totally independent of the pong part: in such a case, the ping-pong argument embodies a laudable disentanglement of the proof. The avoidable ping-pong argument, however, has a bad name because of its (avoidable) case analysis.

At first sight, one might expect equality proofs based on (0) through (3) to take the form of ping-pong arguments, but fortunately there is an alternative: for all real $p,q$ ,

(5) $p = q \Leftrightarrow \left( {\underline{A}w : p \leq w \equiv q \leq w}\right)$ and (6) $p = q \Leftrightarrow \left( {\underline{A}w : w \leq p \equiv w \leq q}\right)$

Proof of (5)

$$ \begin{array}{l} (\underline {{A}} w: p \leq w \equiv q \leq w) \ \Leftrightarrow \quad {w i t h w := q; w i t h w := p } \ (p \leq q \equiv q \leq q) \land (p \leq p \equiv q \leq p) \ = {\leq r e f l e x i v e, t r u e i s i d e n t i t y e l e m e n t o f \equiv } \ p \leq q \land q \leq p \ \Leftrightarrow {(- 1) } \ p = 9 \ \end{array} $$

(End of Proof of (5).)

On account of the above proof of (5), one might be lead to believe that an appeal to (5) for proving $p = q$ is extremely wasteful: why establishing $p \leq w \equiv q \leq w$ for any $w$ , whereas the equivalence is only needed for the two special cases $w = p$ and $w = q$ ? The first remark is that, instead of (5), we could have written

$$ p = q \equiv (\underline {{A}} w: p \leq w \equiv q \leq w) $$

• since, on account of Leibniz's Principle, the left-hand side implies the right-hand side -, so proving the equivalence for any $w$ is, logically at least, no extra burden. The second remark is that proving $psw \equiv qsw$ for any $w$ absorbs the case analysis of proving it for $w = p$ and $w = q$ separately. The third remark is that proving the equivalence for any $w$ is easier than proving it for special values, because in the proof for arbitrary $w$ we are forced to ignore what makes those special values special.

By way of illustration we shall prove a number of little theorems

Theorem 0:Operator ↑ is idempotent,i.e.for any $x$ (7)

Proof On account of (5), it suffices to observe

for any $x,w$

$$ x \uparrow x \leq w $$

$\left{ \left( 0\right) \text{ with }y = x\right}$

$$ x \leq w \wedge x \leq w $$

$= \left{ {\text{pred. calc. in particular idempotence of } \land }\right}$

$$ x \leq w $$

(End of Proof.)

Theorem 1 Operator $\uparrow$ is symmetric, i.e. for any $x,y$

(8) ${x}^{ \uparrow }y = {y}^{ \uparrow }x$

Proof. On account of (5), it suffices to observe

$$ \begin{array}{l} x ^ {\uparrow} y \leq w \ = {\langle 0 \rangle } \ \end{array} $$

$x \leq w \land y \leq w$ $y \leq w \land x \leq w$ $= \left{ {\left( 0\right) \text{ with }x,y = y,x}\right}$

$$ y ^ {\uparrow} x \leq w \quad (\mathrm {E n d o f P r o o f .}) $$

Theorem 2 Operator ↑ is associative, i.e. for any $x, y, z$

$\left( 9\right) \;{\left( x \uparrow y\right) }^{ \uparrow }z = x \uparrow \left( {y \uparrow z}\right)$

Proof on account of (5), it suffices to observe

Mathematical Methodology

$$ \begin{array}{l} (x \uparrow y) \uparrow z \leq w \ = {0) w i t h x, y := (x \uparrow y), z } \ (x \uparrow y) \le w \land z \le w \ = {() } \ (x \leq w \land y \leq w) \land z \leq w \ = {\mathrm {p r e d . c a l c . , i n p a r t i c u l a r a s s o c i a t i v i t y o f} \wedge } \ x \leq w \land (y \leq w \land z \leq w) \ = {(0) \mathrm {w i t h} x, y := y, z } \ x \leq w \land (y \uparrow z) \leq w \ = {0) w i t h y := (y \uparrow z) } \ x \uparrow (y \uparrow z) \ \end{array} $$

Theorem 3 Operator $\downarrow$ distributes over $\uparrow$ ,i.e. for

$$ a n y x, y, z $$

$$ (1 0) \quad (x \uparrow y) \downarrow z = (x \downarrow z) \uparrow (y \downarrow z) $$

Proof In view of (5), it suffices to observe for

$$ \begin{array}{l} a n y x, y, z, w \ (x \uparrow y) \downarrow z \leq w \ = {(3) \mathrm {w i t h} x, y := (x \uparrow y), z } \ (x \uparrow y) \leq w \quad \lor \quad 2 \leq w \ = {0 } \ (x \leq w \land y \leq w) v z \leq w \ = {\mathrm {p r e d . c a l c . , i n p a r t i c u l a r} v \mathrm {d i s t r i b u t e s o v e r} \wedge } \ (x \leq w \lor z \leq w) ^ {\prime} \land (y \leq w \lor z \leq w) \ = {(3) \mathrm {w i t h} y := 2; (3) \mathrm {w i t h} x, y := y, z } \ (x \downarrow z) \leq w \land (y \downarrow z) \leq w \ \end{array} $$

(End of Proof.)

$$ \begin{array}{l} = {(0) \mathrm {w i t h} x, y := (x \downarrow z), (y \downarrow z) } \ (x \downarrow z) \uparrow (y \downarrow z) \ \end{array} $$

The reader who has followed the above proofs in detail must have become high

suspicious: for the real numbers, the operator pair $(\uparrow ,\downarrow)$ - or the other way roundl $(\downarrow ,\uparrow)$ - is very much like the operator pair $(v,\wedge)$ for the boolean domain. The pursuit of such analogies is a valid mathematical exercise.

In fact, every equality between boolean expressions in v and ^ only , can be translated into the equality between real expression in $\uparrow$ and $^\downarrow$ only. For instance, the law of Absorption

$$ X \vee (X \wedge Y) \equiv X $$

${y}{1}{y}{2}$

and $\left( {{XvY} \land \left( {{YvZ}}\right) \land \left( {{ZvX}}\right) }\right. \equiv$

$$ (X \wedge Y) \vee (Y \wedge Z) \vee (Z \wedge X) $$

$\left( {x \uparrow y}\right) \downarrow \left( {y \uparrow z}\right) \downarrow \left( {z \uparrow x}\right) =$

$$ (x \downarrow y) \uparrow (y \downarrow z) \uparrow (z \downarrow x) $$

or: for any three real numbers the minimum

of the pairwise maxima equals the maximum

of the pairwise minima. The matter will not

be pursued here, we prove another theorem

instead.

Theorem 4 Addition distributes over $\uparrow$ ,i.e. for any $x,y,z$

$\left( {x + y}\right) + z = \left( {x + z}\right) \uparrow \left( {y + z}\right)$

Proof In view of (5), it suffices to observe for any $x,y,z,w$

(End of Proof.)

$$ \begin{array}{l} (x \uparrow y) + z \leq w \ {\mathrm {a r i t h m e t i c} } \ (x \uparrow y) \leq w - z \ = {\left(0\right) w i t h w := w - z } \ x \leq w - z \land y \leq w - z \ = {\mathrm {a r i t h m e t i c}, \mathrm {t w i c e} } \ x + z \leq w \quad \land \quad y + z \leq w \ = {0) w i t h x, y := x + z, y + z } \ (x + z) \uparrow (y + z) \leq w \ \end{array} $$

Finally we show

$$ \mathrm {T h e o r e m 5} \quad x ^ {\uparrow} y \leq x + y \equiv 0 \leq x \land 0 \leq y $$

Proof We observe for any $x,y$

$$ \begin{array}{l} x \uparrow y \leq x + y \ = {0) w i t h w := x + y } \ \end{array} $$

$$ \begin{array}{l} x \leq x + y \land y \leq x + y \ = {\mathrm {a r i t h m e t i c}, \mathrm {t w i c e} } \ \end{array} $$

$$ 0 \leq y \land 0 \leq x $$

Mathematical Methodology

(End of Proof.)

All the above proofs owe their brevity to our freedom to instantiate (0) through (3) with special values for $w$ - be it directly or through (5) or (6)- . Had we taken for the maximum a definition like

$$ i f x \geq y \rightarrow x \quad 0 y \geq x \rightarrow y \quad 0 $$

proofs with case analyses would have been unavoidable.

We conclude this chapter with two proofs of the associativity of functional composition, i.e. for functions $f,g,h$ (of the appropriate types) we have to show

$$ (1 2) \quad f _ {0} (g o h) = (f _ {0} g) o h $$

The first proof is based on a definition of functional composition expressed in terms of the formalism of the $\lambda$ -calculus. For functions $p, q$ , the function $p^q$ is defined by

$$ (1 3) \quad p \circ q = (\lambda z: p. (q. z)) $$

at the right-hand side, the dummy $z$ is a fresh variable (i.e., $z$ does not occur as free

variable in $p$ or in $q$ ; consequently, the only occurrence of the free variable $z$ in $p.(q.z)$ is the one shown as the argument to which $q$ is applied.

From the $\lambda$ -calculus we use

(14) $\left( {\lambda x : E}\right) .y =$ " $E$ with $y$ substituted for ${x}^{\prime \prime }$ .

We observe for any $f,g,h$

$$ \begin{array}{l} f _ {0} (g _ {0} h) \ = {(1 3) \mathrm {w i t h} p, q := f, (g o h) } \ (\lambda z: f. ((g o h). z)) \ = {(1 3) \mathrm {w i t h} p, q, z := g, h, x } \ (\lambda z: f. ((\lambda x: g. (h. x)). z)) \ = {(1 4) \mathrm {w i t h} ^ {\prime} E, y := g (h. x), z } \ (\lambda z: f. (g. (h. z))) \ = {(1 4) \mathrm {w i t h} E, y := f. (g. x), h. z } \ (\lambda z: (\lambda x: f. (g \cdot x)) \cdot (h \cdot z)) \ = {1 3) w i t h p, q, z := f, g, x \ (\lambda z: (f _ {0} g). (h. z)) \ = {(1 3) \mathrm {w i t h} p, q := (f o g), h } \ (f \circ g) \circ h \ \end{array} $$

thus having proved (12). The use of the $\lambda$ -calculus enabled us to carry out this proof in terms of equality of functions. Let us now pursue what happens when we

avoid the $\lambda$ -calculus and carry the argument out in terms of equality of function applications. Expressed in function applications, our demonstrandum (12) becomes

(15) $\left( {f \circ \left( {g \circ h}\right) }\right) .z = \left( {\left( {f \circ g}\right) \circ h}\right) .z\;$ for all $z$ and the definition of functional composition (16) $\left( {p \circ q}\right) .z = p.\left( {q \cdot z}\right)$ for all $z$ .

In order to demonstrate (15), we observe for any $f, g, h, z$

$$ \begin{array}{l} (f \circ (g \circ h)). 2 \ = {(1 6) w i t h p, q := f, (g o h) } \ f. ((g \circ h). z) \ = {(1 6) \mathrm {w i t h} p, q := g, h } \ f. (g. (h. z)) \ = {1 6) w i t h p, q, z := f, g, (h. z) } \ (f o g). (h, z) \ = {f (1 6) \mathrm {w i t h} p, q := (p o g), h } \ ((f \circ g) \circ h). z \ \end{array} $$

As the instantiations of p,q show, this

There are striking quantitative differences. The former proof requires 6 steps, the latter one only 4. In the latter proof the depth of parenthesis nesting is homogeneously 2, in the former proof it begins and ends at 1, but reaches 4 in between (which seems excessive). Symbol counts for the equated expressions in the former yield 7,16,23,16,23,16,7 (sum 108), in the latter 11,11,11,11,11 (sum 55); sum and maximum differ both by a factor of 2. More important than these differences themselves is understanding their origin.

The theorem is about equality of functions, the former proof manipulates function expressions. Equality of functions, however, is defined in terms of there application

$$ (1 7) \quad \varphi = \psi \equiv (\underline {{A}} z: \varphi . z = \psi . z) $$

and instead of transforming $\varphi$ into $\psi$ , as the former proof does, the latter one transforms $\varphi .z$ into $\psi .z$ for arbitrary $z$ . We could change the former proof into one transforming $\varphi .z$ into $\psi .z$ by postfixing each of its equated expressions by " $.z$ " -actually prefixing by " $.z$ and postfixing by " $.z$ " but our latter proof is very different: none of

the three intermediate results has the form of a function applied to 2 . In other words, the extra manipulative freedom provided by the initial and final “.z” is used all through the calculation (and evidently at good advantage).

A second source of brevity is that definition (16) of functional composition really combines what we need from (13) and (14). To deduce (16) from the latter two we observe for any $p, q, z$

$$ \begin{array}{l} (p \circ q). z \ = {1 3 } \ \end{array} $$

$$ (\lambda z: p. (q. z)). 2 $$

$$ \begin{array}{l} = {(\mathrm {1 4}) \mathrm {w i t h} x, E, y := z, p _ {\bullet} (q. z), z } \ p. (q. z) \ \end{array} $$

and, since, thanks to (17), (16) captures all there is to be said about functional composition, we don't need lvmbras at all.

The advantage of (16) over (13) as definition of functional composition is that it contains a variable more that can be instantiated; it is that additional freedom that allows us to eliminate in the latter proof the two middle steps of the former proof.

In comparison to (13), definition (16) of functional composition also limits our manipulative freedom: using it, we can only manipulate a functional composition that is applied to an argument. In the latter proof we are forced to eliminate the outer $0$ first, whereas in the former proof the first two steps could have been interchanged; but the outcome is the same and the freedom is irrelevant. The reader is invited to verify that the proof using (16) can be constructed on the very simple principle: "There is only one thing you can do."

Acknowledgement I owe the examples with the maximum to W.H.J. Feijen. (End of Acknowledgement.)

Austin, 11 February 1991

propd. Edsger W. Dgksra Department of Computer Sciences The University of Texas at Austin Austin, TX 78712-1188 USA