   Go backward to B.5 Deriving New KnowledgeGo up to B Proving Propositions ## B.6 Example

We conclude this chapter by demonstrating in detail the proof of a proposition that is used in the verification of Euclid's algorithm. First we repeat the definitions
 x | y : <=> exists z in N: x*z = y; gcd(x, y) := such z in N: z | x /\  z | y /\  (forall g: (g | x /\  g | y) => g <= z).

Our goal is to prove

forall m in N, n <= m: gcd(m, n) = gcd(m-n, n),

i.e., the greatest common divisor of m and n is also the greatest common divisor of m-n and n.

An argument as it can be found in a typical text book is the following.

Proof  Let g be the gcd of m-n and n. Since g divides m-n and g divides n, g also divides (m-n)+n=m.

Take h such that h divides m and h divides n. Then h also divides m-n. Since g is the gcd of m and m-n, h is less than or equal g.

This "proof skeleton" captures on a very high-level the key idea that represents the basis of a "real" proof. However, this idea is only understandable with the knowledge of the rules introduced in the previous sections. Then it becomes also clear that the skeleton actually reflects the structure of a more detailed proof such as the one given below (with additional explanations that are not part of the proof added in italics).

Proof  Take arbitrary m in N and n <= m.

We have to prove a universally quantified implication. We introduce arbitrary constants m and n and add the implication hypothesis (m in N /\  n <= m) to our knowledge. We now have to show the goal gcd(m, n) = gcd(m-n).

If m=0 /\  n=0, we are done.

We proceed by case distinction. In the first case m=0 /\  n=0, we know gcd(m, n) = gcd(0, 0) = gcd(0-0, 0) = gcd(m-n). By transitivity of =, we have the goal.

Otherwise, m != 0 \/ n != 0. We can show that in this case there exists a unique z in N with

z | m /\  z | n /\  (forall g: (g | m /\  g | n) => g <= z).

The rest of the proof deals with the second case m != 0 \/ n != 0. We claim that in this case above formula holds (which requires a separate proof) and use this as knowledge from now on.

For every z' in N, in order to prove

z' = gcd(m, n),
it therefore suffices to prove
z' | m /\  z' | n /\  (forall g: (g | m /\  g | n) => g <= z').

We justify a reasoning step that will be used below: we have to prove that a particular object equals gcd(m, n). By the rule of substitution, we may insert the definition of gcd and thus have to prove that the object equals the value of a "such term". We thus remind the reader of the proof rule for this kind of terms and instantiate the rule with the concrete formula. The application of this rule requires that only one object satisfies the formula in the "such term", which is exactly what we have added as knowledge above.

Let g := gcd(m-n, n). By n <= m, we know

(1) g | (m-n) /\  g | n /\  (forall h: (h | (m-n) /\  h | n) => h <= g).

We define an abbreviation g for gcd(m-n, n). Since n <= m, we have m-n in N. Since m != 0 \/ n != 0, also m-n != 0 \/ n != 0 (which has to be shown in a small subproof). By the knowledge added above, we thus have an object that satisfies the formula in the definition of gcd(m-n, n). Therefore we may apply the corresponding rule for "such terms" and assume that g satisfies this formula as well.

We have to show g = gcd(m, n), i.e., by the explanation above

(2) g|m /\  g|n /\  (forall h: (h | m /\  h | n) => h <= g).

We apply the reasoning step explained above. Now we have to prove the conjunction by showing each conjunct in turn.

1. We show (3) g | m. Because of (1), we have some a and b with ga = m-n and gb = n. Then we know
g(a+b) = ga + gb = (m-n) + n = m;
which implies (3).

We insert the definition of | into knowledge (1), which gives us an existential formula (exists a: ga = m) and (exists b: gb = n). The application of these existential formulas gives us new constants a and b with the corresponding properties. Then we apply equational reasoning which gives us our goal by the transitivity of =.

2. We know (4) g|n from (1).

The goal is part of our knowledge.

3. We show (5) forall h: (h | m /\  h | n) => h <= g. Take arbitrary h and assume
(6) h | m /\  h | n.

We show (7) h <= g.

We have to show a universally quantified implication. We introduce an arbitrary constant h and assume the implication hypothesis. We now have to show the new goal (7).

By (6) we have some a' and b' with ha' = m and hb' = n.

We insert the definition of | into knowledge (6) which gives two existential formulas that we can apply to introduce the constants a' and b' with the knowledge denoted above.

Then we know

h(a'-b') = ha' - hb' = m-n
and thus (8) h | (m-n).

We apply equational reasoning to yield a formula in our knowledge that is equivalent to the definition of | for arguments h and m-n.

With (6) and (8), (1) implies (7).

We apply the rule of "universal quantification in knowledge" to instantiate the universally quantified implication in (1) by term h. Then we apply the rule of "modus ponens" to this implication and to the conjunction of (6) and (8), which gives us the goal.

While above proof is very detailed, it still relies on the claim that the greatest common divisor is uniquely defined (which has to be shown in an extra proof). The verbosity of the proof stems from the fact that it considers details like "Is m-n actually defined?" or "Is the gcd unique?" that were neglected in the high-level proof skeleton.

Whether one is willing to bother with details is a matter of whether one is actually interested in the truth of a formula as it stands or whether one just wants to know whether the "intention is correct" (whatever this means). For a computer scientist, exactness is important (a "roughly" correct program may be the cause of an airplane crash); she should not be anxious but eager to find an error in a proposition and thus also check all the details that are often neglected in typical mathematical texts.

Author: Wolfgang Schreiner
Last Modification: October 4, 1999   