On an exercise of Tony Hoare’s

On an exercise of Tony Hoare's

Let $\leq$ be a reflexive,transitive relation; Let $f$ and $g$ be such that

$f\left( x\right) \leq y \equiv x \leq g,y\;f\left( x\right) \Rightarrow {x}{1} < y \leq {x}{2}$

Prove that $f$ and $g$ are monotonic with respect to $\leq$ ("preserve $\leq$ ").

Proof We observe for any $u, v$

$$ \begin{array}{l} f. u < f. v \ = {\leq i s r e f l e x i v e a n d p r e d i c a t e c a l c u l u s } \ f \cdot v < f \cdot v \Rightarrow f \cdot u < f \cdot v \ = {(0) \mathrm {w i t h} x, y := v, f. v \mathrm {a n d} x, y := u, f. v } \ v \leq g. (f, v) \Rightarrow u \leq g. (f, v) \ \Leftrightarrow {\leq i s t r a n s i t i v e } \ u \leq v \ \end{array} $$

Because $\geq$ , defined by $x \geq y \equiv y \leq x$ , is also reflexive and transitive, the monotonicity of $g$ follows by this symmetry from the above.

(End of Proof.)

It is a nice example of a shortest proof in the sense that each of the three steps uses one of our data. A further reason for recording it is that the first step is not a rabbit. Our proof obligation is to remove without weakening the f-applications from $\text{f.u} \leq \text{f.v}$ , and only (o)

tells us how to do so, but only for an $f$ -application

Since we have to use that the $f$ in $f.v$ is the function $f$ that satisfies (0), we have to introduce an expression of the form

$$ f \cdot v \leq s o m e t h i n g $$

Since we have to use properties of $\leq$ as well, the simplest choice for "something" is f.v itself: because

$$ f. v \leq f. v $$

equivales true . How do we introduce this representation of true without weakening? Without changing the value of a boolean expression, we can prefix it by "true $\equiv$ ", "true $\land$ ", or "true $\Rightarrow$ "; since of "a $\equiv$ b", "a $\land$ b" and "a $\Rightarrow$ b", the last one is the weakest one, we prefix our demonstrandum

${by}$ ${f}{1}v \leq {f}{1}v \Rightarrow$

Hence our proof.

Austin, 20 September 1989

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