Proving the equality of infinite sequences

Proving the equality of infinite sequences

In EWD827, I gave a very short proof of the equality of two infinite sequences by showing that the one sequence satisfied the defining equation of the other. I was annoyed by the destruction of the symmetry, the more so since I could not do it the other way round. I also pulled what at the time looked like a rabbit out of the hat, and the formalism used to conduct the proof in went beyond SASL, in which the sequences had been defined. Here is what could be a more systematic approach.

In order to prove $x = y$ for infinite sequences

the base: $P.\left( {x,y}\right)$

the step: $P\left( {a : p,b : q}\right) \Rightarrow a = b \land P\left( {p,q}\right)$

Here we apply this to the example of EWD827.

The function

(0) $\operatorname{from}n = n : \operatorname{from}\left( {n + 1}\right) \;$ for all $n$ .

The sequence nat is given by

(1) $\operatorname{nat} = 0 : \operatorname{inc.nat}$

where inc is given by

(2)inc. (head: tail) = head+1 : inc.tai We are requested to prove (3) $\operatorname{from.}0 = \operatorname{nat}\;$ .

From (3) and the base we see that we have to choose a $P$ such that

(4) $P.\left( {{f}_{\text{from}}0,\text{nat}}\right)$ is satisfied. To find a suitable P we observe

$$ s = f r o m. 0 \quad \land \quad t = n a t $$

$\Rightarrow \;\left{ \left( 1\right) \right}$

$$ s = f r o m. 0 \quad \land \quad t = 0: i n c. t $$

$\Rightarrow$ {instantiation}

$$ (\underline {{E}} n: \quad s = f r o m. n \quad \wedge t = n: i n c. t) $$

from which we see that (4) -the base- is satisfied if we choose

(5) $P\left( {s,t}\right) = \left( {{En} : s = {from}.\right. n\;t = n : {inc}.t)$

In order to prove the step we observe for any $a,b,p,q$

$P\left( {a;p,b;q}\right)$ $\left{ \left( 5\right) \text{ with }s,t \mathrel{\text{:=}} a : p,b : q\right}$

$$ (E n: a: p = f r o m. n \wedge b: q = n: i n c. (b: q)) $$

$= \;\left{ {\left( 0\right) ,\left( 2\right) \text{ with head, tail } = b,q}\right}$

$$ (\mathrm {E n}: a: p = n: f r o m. (n + 1) \land b: q = n: b + 1: i n c. q) $$

$=$ {head} : tail = head! tail' ≡

$$ h e a d = h e a d ^ {\prime} \wedge t a i l = t a i l ^ {\prime}; L e i b n i z $$

$$ \begin{array}{l} (\mathrm {E n}:: a = n \land p = f r o m. (n + 1) \land \ b = n \wedge q = n + 1: i n c. q) \ \Rightarrow \quad {\mathrm {p r e d i c a t e c a l c u l u s} } \ a = b ^ {\prime} \wedge (\mathrm {E n}: p = f r o m. (n + 1) \wedge q = n + 1; i n c. q) \ \Rightarrow {\mathrm {t r a n s f o r m i n g}, \mathrm {t h e d u m m y a n d (5)} } \ a = b \wedge P. (p, q). \ \end{array} $$

The advantage of the above proof format is that it absorbs the fact that from and nat have been defined by rather different recursion patterns.

Finally we would like to point out that the introduction of the dummy n and the existential quantification in the design of $P$ are not such rabbits. Though our demonstrandum

(3) only contains from.0 , we have to use

from (0) that the definition of

for all $n$ . Hence the generalization $s = f r o m.n$ ;

the "invariance requirement" of $P$ makes the intro

duction of n in the other conjunct all but

obligatory.

Austin 12 February 1991

propd. Edsger W. Dgiksha

Department of Computer Sciences

The University of Texas at Austin

Austin, TX 78712- 1188

USA