HOME

Indirect equality enriched (and a proof by Netty)

Show original manuscript

Proofs known as "proofs by indirect equality" traditionally exploit

(0)      x = y     ≡   〈∀u : true : u≡ uy

for some reflexive, antisymmetric ⊑ : they establish equality by establishing the right-hand side of (0). The following lemma shows that we may be able to get away with a proof obligation that is formally weaker.

Lemma For reflexive, antisymmetric &#x2291 and predicate P such that P.xP.y , we have

(1)      x = y     ≡   〈∀u : P.u : u ≡  uy

Proof

LHS ⇒ RHS   This follows from Leibniz's Principle.

RHS ⇐ LHS   We observe for any x,y, P such that P.xP.y

〈∀u : P.u : u≡ uy

⇒       { instantiate u:= x and u:= y }

(P.x ⇒ (xxxy )) ∧ (P.y ⇒ (yxyy ))

≡       { P.xP.y }

(xxxy ) ∧ (yxyy )

≡       { ⊑ is reflexive }

xyyx

⇒       { ⊑ is antisymmetric }

x = y                                           (End of Proof)

*           *
*

An application

Let the above &#x2291 be the partial order of a lattice for which the infimum ↓ is defined by the usual

(2)     u ⊑ xy    ≡    ux  ∧  uy

Fairly directly follow the general lattice properties

(3)     ↓ is idempotent, symmetric, associative

(4)     xyx and xyy

(5)     xy   ≡   x = xy

We now specialize by making the variables x, y, u etc. of type natural and identifying &#x2291 with "divides" —or "is a divisor of"—, which is a partial order on the naturals for which the infimum exists: xy is in fact the Greatest Common Divisor of x and y .

The formal link between our lattice and arithmetic on the naturals &#x2014multiplication in particular— is given by providing 〈∃q :: q*x = y 〉 as a third expression for "x divides ", i.e. we add to our laws

(6)     〈∃q :: q*x = y 〉   ≡   xy

from which the mutually equivalent

(7)     mm*x       and       m  =  m ↓ m*x

immediately follow. (Please note that we have given * a stronger binding power than &#x2193.)

We are now ready to prove that the GCD of two m-tiples is an m-tiple, in formula

(8)     m  ⊑  m*xm*y

Proof    We observe

m   ⊑   m*xm*y

≡        { (5) and associativity of ↓ (3) }

m   =   m*xm*y

≡        { (7) }

m  =  m ↓ m*y

≡        { (7) with x:= y }

true

(End of Proof)


An "m-tiple" is a multiple of m.

And now we are ready for an application of the Lemma with which this note started: we shall show that multiplication distributes over the GCD, in formula

(9)     m * (xy )   =   m*x ↓ m*y

Proof

On account of (7), the LHS of (9) is an m-tiple, on account of (8), the RHS is an m-tiple. Lemma (1) can thus be applied with mu for P.u . Accordingly we observe for 1 ≤ m —the case of m = 0 is obvious—

(9)

≡        { (1) }

〈∀u : mu :  um*(xy )  ≡  um*xm*y

≡        { transforming the dummy: u = m*w }

〈∀w :: m* ⊑  m*(xy )   ≡   m* ⊑  m*xm*y

≡        { (2) }

〈∀w :: m*wm*(xy )   ≡   m*wm* ∧  m*wm*y

≡        { rs   ≡   m*r  ⊑  m*s for 1≤m }

〈∀w :: wxy   ≡   wxwy

≡        { (2) }

true

(End of Proof)

Addendum

For those who are not comfortable with the dummy transformation, here is its pattern in a bit more detail

〈∀u : mu : Q.u

≡        { for non-empty range &#x3008∀w :: C 〉≡ C }

〈∀u : mu : 〈∀w : u = m*w : Q.u 〉〉

≡        { interchange of quantifications }

〈∀w :: 〈∀u : u = m*w  ∧  mu : Q.u 〉〉

≡        { u = m* ⇒  mu }

〈∀w :: 〈∀u : u = m*w : Q.u 〉〉

≡        { one-point rule }

〈∀w :: Q.(m*w ) 〉

(End of Addendum)   

*           *
*

All of the above was triggered by Netty van Gasteren's use of (9) in her ingenious proof of

(10)     xy = 1  ⇒  xy*z = xz    :

xz

=        { antecedent of (10) }

x ↓ (xy )*z

=        { (9) and associativity of ↓ }

xx*zy*z

=        { (7) with m,x := x,z }

xy*z

Nuenen, 14 December 2001             

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