Some annotated proofs

Some annotated proofs

Without the work of W.H.J. Fejér, A.J.M van Gasteren and R.M.Dgkstra, the following would not have been written; I owe them a lot.

The topic of this note is the design of formal proofs. Besides giving a number of proofs I shall give the considerations that are of relevance for their construction.

To begin with, we consider the beautiful theorem -from the collection of etudes composed by WF&Avg , and dubbed "the see-saw lemma

(0) $\left[x \Rightarrow x ; \sim x ; x\right] \quad \text {f o r a l l} x ,$

to be proven from first principles.

Which first principles? Well, the consequent $x; \sim x; x$ suggests two things: firstly, because of the 2 semicolons, that the associativity of the composition will be involved, and, secondly, that we shall need the exchange rules as they provide the link between com-position and transposition.

Because of the involvement of the ex- change rules, we follow the suggestion of EWD1141 to switch to composition's conjugate, the confrontation, in terms of which the exchange rules are a little bit cleaner.

Extract I recall from EWD1141, that the "confrontation" is denoted by $\left. {{}^{\prime }!{}^{\prime }}\right\rbrack$ ,is defined

and ,hence, is associative, has an identity element - 7J -, and is universally conjunctive. In terms of ! , the exchange rules are

$$ [ x, y \vee z ] \equiv [ z, w y \vee x ] \qquad l e f t - e x c h a n g e $$

$$ [ x! y \vee z ] \equiv [ \sim x! z \vee y ] \qquad \mathrm {r i g h t - e x c h a n g e}. $$

(End of Extract)

In terms of the confrontation, the see-saw lemma reads

(1) $\left\lbrack {{x}^{1},{\sim x}^{1},x \Rightarrow x}\right\rbrack$ for all $x$

Remark In this note I do not intend to spend much attention to things such as the equi- valence of (0) and (1). That part of predicate calculus - including ${\left( \log \right) }^{ * } = {f}^{ * }{g}^{ * } -$ I assume here available. (End of Remark).

The three main proof patterns for establishing $\left\lbrack {p \Rightarrow q}\right\rbrack$ are schematically represented by

(i) $\left\lbrack {p \Rightarrow q}\right\rbrack \Leftarrow$ true

(ii) $\left\lbrack {{p}^{v}z}\right\rbrack \Rightarrow \left\lbrack {q}^{v}z}\right\rbrack$ for all $z$

[\left\lbrack {{7p} \vee z}\right\rbrack \Leftrightarrow \left\lbrack {{7q} \vee z}\right\rbrack ]

(Under (i) I capture here all notational variations such as

• transforming $p \land q$ in a sequence of value-preserving transformations into $p$
• transforming $p$ in a sequence of weakening transformations into $q$ (or $q \lor p$ ), etc.

(ii) and (iii) are different for the universal quantification over the new dummy. Note that (ii) and (iii) represent two intrinsically different ways of introducing the dummy 2: in (ii) "p" becomes a disjoint, in (iii) "ip" does so.)

The shape of the exchange rules suggests (ii), i.e. to establish (1) by establishing (2) $\left\lbrack {x, \sim x, \mid x \vee z}\right\rbrack \Rightarrow \left\lbrack {x \vee z}\right\rbrack \;$ for all $x,z$ .

Remembering that the whole purposc of the introduction of 2 was to create the opportunity of applying an exchange rule, we now suggest to apply an exchange rule - for reasons of symmetry it probably does not matter which one-, i.e. to start our weakening chain as follows:

$$ = \begin{array}{r l} & {\left[ x! \sim x! x \vee z \right]} \ & {{\mathrm {r i g h t - e x c h a n g e} }} \ & {\left[ \sim x! z \vee \sim x! x \right]} \end{array} $$

(The alternative application of the right-exchange rule would have yielded $[v(x!, v x)!, z v x]$ , which looks less inspiring, so we pursue the chosen application first.)

Had! been disjunctive, the next step would have been easy: we would have rewritten our last result as $[vx!, (zv x)]$ . But! is not disjunctive, but conjunctive, i.e. at least monotonic, and this we can exploit, remembering that we are building a weaken- ing chain! We can continue

$\left\lbrack {\sim {x}^{!}\left( {z \vee x}\right) }\right\rbrack$

Remark Here are three alternative formulations

(i) $\left\lbrack {p \Rightarrow q}\right\rbrack \Rightarrow \left\lbrack {f.p \Rightarrow f.9}\right\rbrack$ for all $p,q$ (ii) $\left\lbrack {{f}{p}v{f}{q} \Rightarrow f\left( {p \vee q}\right) }\right\rbrack$ for all $p,q$ (iii) $\left\lbrack {{f}{p} \land {f}{q} \Leftarrow f.}\right\rbrack$ for all $p,q$ .

Monotonicity is too important a property to be known by (i) only; (ii) and (iii) can be generalized to existential and universal quantification respectively. (End of Remark.)

In view of the fact that our target expression $\left\lbrack {\mathrm{x} \vee \mathrm{z}}\right\rbrack$ contains no $\sim$ ,our last trans-

formation was a step in the right direction: the number of $\mathfrak{w}$ 's has been reduced from 2 to 1 . The right-exchange is a proper mechanism for that , but is only applicable after we have made the confrontation into a disjunct.

So we proceed

$= \left{ {{pred}\;{cud}\;{t\alpha }}\right}$

$= {$ right-exchange $}$

$$ \begin{array}{l} [ \sim x! (z \vee x) ] \ [ \sim x! (x \vee z) \vee f a l s e ] \ \end{array} $$

Remark An alternative for the first step, that would have turned the confrontation into a disjunct would have been an appeal to the idempotence of v : it would have yielded

$$ [ \sim x ^ {1}, (z \vee x) \vee \sim x ^ {1}, (z \vee x) ] \quad , $$

reinproducing a second $\sim$ (and more com-. plication). (End of Remark)

Now the only thing left is to get rid of the first disjunct. x!false. However,

$$ [ x, f a l s e v x v z ] \Rightarrow [ x v z ] \quad f o r a l l z $$

is equivalent to

$$ [ x! \mathrm {f a l s e} v x \Rightarrow x ] $$

or [x!false ⇒ x]

which holds because $!$ has a neutral element. (Vide the conjugate relation $[x \Rightarrow x; \text{true}]$ .) So our proof can be completed:

$$ \begin{array}{l} [ x, f a l s e \lor x \lor z ] \ = \begin{array}{l} {\left{\left[ x! \mathrm {p a l s e} \Rightarrow x \right] \right}} \ {\left[ x \lor z \right]} \end{array} \ \end{array} $$

Summarizing the proof, we observe for any $x, z$

$$ \begin{array}{l} [ x _ {1} ^ {\prime}, \dots x _ {1} ^ {\prime} x \vee z ] \ = \left{ \begin{array}{l} \text {r i g h t - e x c h a n g e} \ [ \sim x! z \vee \sim x! x ] \end{array} \right. \ \Rightarrow \begin{array}{l} {{\mathrm {1 , m o n o t o n i c i n s e c o n d a r g u m e n t} }} \ {[ \omega x \frac {1}{2} (z \vee x) ]} \end{array} \ = {\mathrm {p r e d i c a t e c a l c u l u s} } [ \sim x! (x \vee z) \vee f a l s e ] \ = \begin{array}{l} {{\mathrm {r i g h t - e x c h a n g e} }} \ {[ x, f a l s e v x v z ]} \end{array} \ = \begin{array}{l} {{\left[ x _ {2} ^ {\prime} f a l s e \Rightarrow x \right] }} \ {\left[ x v z \right]} \end{array} \ \end{array} $$

Remark in retrospect The only role of the associativity of the composition has been to give us the choice between using the left- or the right-exchange. (End of Remark in reho-spect.)

The reader is kindly invited to note that my "annotated" version of a 5-step argument took about 5 pages of manuscript. The moral of the story is that a formal proof can be a very

compact deposit of our considerations. Furthermore I would like to point out that most of our considerations seemed more general than just the relational calculus. The only really specific element was the lemma $[x, f a l s e \Rightarrow x]$ , but the need for that was the result of calculation.

The next theorem -also from WF&Avg- I want to deal with is

For any right-condition q

(3) $[q; \text {true}; \sim q \equiv q; \sim q]$

A moment's consideration shows that a ping-pong argument is indicated since for pong we don't even need to know that q is a right -condition:

$$ \begin{array}{r l} & {[ q; \mathrm {t r u e}; \sim q \Leftarrow q; \sim q ]} \ {\iff} & {{; \mathrm {m o n o t o n i c} }} \ & {[ q; \mathrm {t r u e} \Leftarrow q ]} \ {=} & {{\mathrm {l e m m a} }} \ & {\mathrm {t r u e}} \end{array} $$

(The lemma follows thus:

$$ \begin{array}{r l} & {\quad x; \mathrm {t r u e}} \ & {\Leftrightarrow \quad {\mathrm {[ t r u e} \Leftrightarrow ] \mathrm {] a n d ; m o n o t o n i c} }} \ & {\quad x; y} \ & {= \quad {\mathrm {y n e u t r a l e l e m e n t o f ;} }} \ & {\quad x.} \end{array} $$

with proving

(4) $\left\lbrack {q;\operatorname{true};\sim q \Rightarrow q;\sim q}\right\rbrack$

I had serious problems, which in retrospect could be traced to an unsufficiently convenient characterization of "q is a right-condition". The original characterization was

$$ [ t r u e; q \equiv q ] $$

which is good to know, but since [true; $x \Leftarrow x$ ] holds for any $x$ , the specific quality of being a right-condition is expressed by

$$ [ t r u e; q \Rightarrow q ] \equiv (q i s a r i g h t - c o n d i t i o n) $$

and it was this equivalence with which I started my work on the current theorem. But it is more convenient its mutual implications separately, depending on whether one wants to show or to use that $q$ is a right condition. In the former case we use

(5) $\left\lbrack {\text{true};q \Rightarrow q}\right\rbrack \Rightarrow \left( {q\text{ is a right-condition }}\right)$ ;

in the latter case we also exploit the mono- tonicity of composition, and get that for any $x$

(6) $\left\lbrack {x;q \Rightarrow q}\right\rbrack \Leftarrow \left( {q\text{ is a right-condition}}\right)$

with the immediate consequence that for any $x$

(6') $\left\lbrack {\neg q;x \Rightarrow \neg q}\right\rbrack \Leftrightarrow \left( {q\text{is a right-condition}}\right) .$

The charm of (6), which almost looks like an

absorption rule, is the dummy $x$ that we can instantiate as we see fit. In particular we can conclude (4) from

(7) $\left\lbrack {q;\operatorname{true};\sim q \Rightarrow q;\sim q;x}\right\rbrack$

In particular and here is still some sort of rabbit - : if x starts with "q; we see in the consequent of (7) as subexpression the consequent of the see-saw lemma.

So let us start with that:

true

$$ = {\mathrm {s e e - s a w l e m m a} } $$

$$ [ q \Rightarrow q; \sim q; q ] $$

$\Rightarrow$ {monotonicity of ; in 1st argument}

$$ [ q; \mathrm {t r u e}; \sim q \Rightarrow q; \sim q; q; \mathrm {t r u e}; \sim q ] $$

$\Rightarrow { {\left( {6}^{\prime }\right) }^{2} + 1 : 1;1 - 1,0 : 0}$

$$ [ q; t r u e; \sim q \Rightarrow q; \sim q ] $$

After the introduction of the see-saw lemma, we compose both sides with "true; ~q" to get the target antecedent, in the process constructing the x with which to apply (6') in the last step.

Austin, 9 November 1992

prof. dr. Edsger W. Dgkstra Department of Computer Sciences The University of Texas at Austin Austin, TX 78712-1188 USA