Skip to main content
PRL Project

An Algorithm for the Greatest Common Divisor

by Anne Trostle    2013

Here we show how to use the Nuprl proof assistant to develop an existence proof for the greatest common divisor of two natural numbers. We then take the proof a step further and show that the greatest common divisor, or GCD, can be calculated as a linear combination of the two numbers. For each proof, we also show that Nuprl can extract a program from the proof that can be used to perform calculations.

The greatest common divisor is defined in Nuprl as follows:

Definition 1: gcd_p GCD(m;n;g) == (g | m) ∧ (g | n) ∧ (∀z:ℤ. (((z | m) ∧ (z | n)) ⇒ (z | g))) Definition 2: divides b | a == ∃c:ℤ. (a = (b * c))

In words, Definition 1 means that g is the greatest common divisor of m and n when g divides both m and n, and any other common divisor of m and n divides g.


To prove that the GCD exists, we are going to use Euclid's algorithm, which is based on the property that for two integers m and n, the GCD of m and n is equivalent to the GCD of n and the remainder from m ÷ n:

Lemma 1: div_rem_gcd_anne ∀m:ℤ. ∀n:ℤ-0. ∀g:ℤ. (GCD(m;n;g) ⇔ GCD(n;m rem n;g)) View a PDF of the proof of this lemma


Another useful fact about the GCD is that the GCD of an integer z and 0 is z. A proof of this property can be done by showing that each part of Definition 1 is satisfied.

Lemma 2: gcd_p_zero ∀z:ℤ. GCD(z;0;z) View an example proof for this lemma 1

From these properties we can see a method for calculating the greatest common divisor of two numbers: continue finding remainders until you reach 0 and then use the fact that the GCD of an integer z and 0 is z. Since the GCD stays the same as you reduce the terms, z is also the GCD of the original pair of numbers. This is Euclid's algorithm. Here is an example of how it works, using 18 and 12:

GCD(18;12;g) = GCD(12;18 rem 12;g)
             = GCD(12;6;g)
             = GCD(6;12 rem 6;g)
             = GCD(6;0;g)
           → g = 6

Using this idea we can not only prove that the GCD exists but we can also construct a method for actually computing the GCD. A great feature of Nuprl is that when we run a constructive existence proof, we can extract a program from it and use the program to perform calculations. In the next section we show in detail how to develop a constructive existence proof for the GCD using induction. Induction proofs often go hand-in-hand with recursive programs, and sure enough, a very clean recursive program can be extracted from the proof, and this program follows exactly the method that we just came up with:

λn. letrec gcd(n) = λm. if n = 0 then m else (gcd (m rem n) n) in gcd(n)


The program here is an example of currying: a function of n that results in another function which then uses m. This isn't necessarily intuitive, since when we think of the GCD we think of a function of a pair (or more) of numbers, so we might expect the program to start with something like "gcd(m, n) = ... ". But the proof that follows uses natural induction on a single variable and flows very nicely, giving reason to prefer the curried function here. To develop a proof that produces a function of the pair (m, n) would require induction on the pair itself which isn't as intuitive or easy to understand as natural induction on a single variable.


Proof by Induction: ∀n,m:ℕ. (∃g:{ℕ| GCD(m;n;g)})

For the proof, we consider strong induction on n and ask ourselves, can we prove that the theorem holds for n, if we assume that it does for all natural numbers less than n? The answer here is yes: since (m rem n) < n (proven in a separate Nuprl lemma), we can use (m rem n) with the induction hypothesis and then apply Lemma 1 above to relate it to the case for n. Furthermore, the key steps in this proof reveal the recursive algorithm. Here's how we start:

⊢ ∀n,m:ℕ. (∃g:{ℕ| GCD(m;n;g)}) | BY (D 0 THENA Auto) Decompose ∀n to assume an arbitrary n | 1. n: ℕ ⊢ ∀m:ℕ. (∃g:{ℕ| GCD(m;n;g)}) | BY (GeneralNatInd 1 THENA Auto) Natural induction on n | 2. ∀n1:ℕn. ∀m:ℕ. (∃g:{ℕ| GCD(m;n1;g)}) Induction hypothesis ⊢ ∀m:ℕ. (∃g:{ℕ| GCD(m;n;g)}) (n1:ℕn. means 0 ≤ n1 < n) | BY (D 0 THENA Auto) Decompose ∀m to assume an arbitrary m | 3. m: ℕ ⊢ ∃g:{ℕ| GCD(m;n;g)}


Since our method will involve using the remainder from m ÷ n, we must consider the case of n = 0 separately, i.e. our base case for the induction. For n = 0, we use Lemma 2 from above. Notice that this matches the "if" case in the recursive algorithm.

1. n: ℕ 2. ∀n1:ℕn. ∀m:ℕ. (∃g:{ℕ| GCD(m;n1;g)}) 3. m: ℕ ⊢ ∃g:{ℕ| GCD(m;n;g)} | BY (Decide ⌈n = 0⌉ THENA Auto) | 4. n = 0 Assume n = 0 ⊢ ∃g:{ℕ| GCD(m;n;g)} | BY (SqHypSubst 4 0 THENA Auto) Substitute 0 for n in the conclusion | ⊢ ∃g:{ℕ| GCD(m;0;g)} | BY (InstConcl [⌈m⌉] THENA Auto) Instantiate the conclusion with m | ⊢ GCD(m;0;m) | BY (InstLemma `gcd_p_zero` [⌈m⌉] THENA Auto) Apply the Nuprl lemma that | proves that the GCD 5. GCD(m;0;m) of m and 0 is m ⊢ GCD(m;0;m) | BY NthHyp 5


For the case of n ≠ 0, we apply the induction hypothesis to (m rem n) and n. Notice that this matches the "else" case in our recursive algorithm. To meet the condition of the induction hypothesis, we must prove that (m rem n) < n. This property is part of the Nuprl lemma rem_bounds_1 and leads to an important result: since (m rem n) < n and we know how to handle the base case of 0, this means that our recursive algorithm will terminate, rather than go on forever.

1. n: ℕ 2. ∀n1:ℕn. ∀m:ℕ. (∃g:{ℕ| GCD(m;n1;g)}) 3. m: ℕ ⊢ ∃g:{ℕ| GCD(m;n;g)} | BY (Decide ⌈n = 0⌉ THENA Auto) | 4. ¬(n = 0) Assume n ≠ 0 ⊢ ∃g:{ℕ| GCD(m;n;g)} | BY (InstHyp [⌈m rem n⌉;⌈n⌉] 2 THENA Auto) Apply the induction hypothesis, | setting n1 = (m rem n) and m = n ⊢ (m rem n) < n | BY (InstLemma `rem_bounds_1` [⌈m⌉;⌈n⌉] THENA Auto) Apply the Nuprl lemma | that proves that 5. (0 ≤ (m rem n)) ∧ ((m rem n) < n) (m rem n) < n, a condition ⊢ (m rem n) < n of the induction hypothesis | BY Auto


By the induction hypothesis, there exists a natural number g which is the greatest common divisor of n and (m rem n). We know from Lemma 1 that GCD(m;n;g) ⇔ GCD(n;m rem n;g), so therefore the greatest common divisor exists for m and n, and is also g.

1. n: ℕ 2. ∀n1:ℕn. ∀m:ℕ. (∃g:{ℕ| GCD(m;n1;g)}) 3. m: ℕ 4. ¬(n = 0) 5. ∃g:{ℕ| GCD(n;m rem n;g)} Result from applying the induction hypothesis ⊢ ∃g:{ℕ| GCD(m;n;g)} | BY D 5 Decompose hypothesis 5 to extract g, | the GCD of n and (m rem n) 5. g: ℕ [6]. GCD(n;m rem n;g) ⊢ ∃g:{ℕ| GCD(m;n;g)} | BY (InstConcl [⌈g⌉] THENA Auto) Instantiate the conclusion with g | ⊢ GCD(m;n;g) | BY (InstLemma `div_rem_gcd_anne` [⌈m⌉;⌈n⌉;⌈g⌉] THENA Auto) | Apply the Nuprl lemma 7. GCD(m;n;g) ⇔ GCD(n;m rem n;g) that proves that the GCD ⊢ GCD(m;n;g) of m and n is equivalent to | the GCD of n and (m rem n) BY Auto





Taking the proof a step further: Bezout's Identity

The theorem above claims that the greatest common divisor exists. But we can take this a step further and instead prove that not only does the GCD of a pair of numbers exist, but it exists as a linear combination of the two numbers, i.e. there are integers x and y such that the GCD of m and n is (x ∗ m) + (y ∗ n). This property is referred to as Bezout's Identity.

Note that when the GCD is written in this form, we can see that it truly is the greatest of the common divisors and satisfies the definition given for the GCD (Definition 1). Say g = (x ∗ m) + (y ∗ n) is the GCD of m and n. If another number d also divides m and n, then m = d ∗ c1 and n = d ∗ c2 for some integers c1 and c2 based on the definition of divides (Definition 2). Substituting these equations into the linear combination gives us g = (x ∗ d ∗ c1) + (y ∗ d ∗ c2), and thus g = d ∗ (x ∗ c1 + y ∗ c2). This means that d also divides g.

The proof below follows closely to the one already shown, except that now we are dealing with a pair of numbers p = x,y used to calculate the GCD rather than the GCD itself. Therefore the induction step isn't quite as simple as before and will require some extra algebraic steps. But in the end Nuprl still provides a clean recursive algorithm when extracting a program from the proof:

λn. letrec bezout(n) = λm. if n = 0 then 〈1, 0〉 else let p1,p2 = bezout (m rem n) n in 〈p2, p1 - p2 * (m ÷ n)〉 in bezout(n)


Again, the program is written as a curried function starting with n, since that's how we approach the proof using induction on n. The key steps in the proof below will reveal this recursive algorithm.


Proof by Induction:
∀n,m:ℕ. (∃p:{ℤ X ℤ| let x,y = p in GCD(m;n;(x ∗ m) + (y ∗ n))})

We start the proof the same way as before, by performing natural induction on n. Since we are working with a pair of numbers used to calculate the GCD, the resulting induction hypothesis is that such a pair exists for all natural numbers less than n:

⊢ ∀n,m:ℕ. (∃p:{ℤ X ℤ| let x,y = p in GCD(m;n;(x ∗ m) + (y ∗ n))}) | BY (D 0 THENA Auto) Decompose ∀n to assume an arbitrary n | 1. n: ℕ ⊢ ∀m:ℕ. (∃p:{ℤ X ℤ| let x,y = p in GCD(m;n;(x ∗ m) + (y ∗ n))}) | BY (GeneralNatInd 1 THENA Auto) Natural induction on n | 2. ∀n1:ℕn. ∀m:ℕ. (∃p:{ℤ X ℤ| let x,y = p in GCD(m;n1;(x ∗ m) + (y ∗ n1))}) | Induction hypothesis (n1:ℕn. means 0 ≤ n1 < n) | ⊢ ∀m:ℕ. (∃p:{ℤ X ℤ| let x,y = p in GCD(m;n;(x ∗ m) + (y ∗ n))}) | BY (D 0 THENA Auto) Decompose ∀m to assume an arbitrary m | 3. m: ℕ ⊢ ∃p:{ℤ X ℤ| let x,y = p in GCD(m;n;(x ∗ m) + (y ∗ n))}

Once again we consider the case of n = 0 separately. When n = 0, we find that the resulting pair of integers is 〈1,0〉 to get GCD(m;0;m), and then we use Lemma 2. Notice that this matches the "if" case in the recursive algorithm.

1. n: ℕ 2. ∀n1:ℕn. ∀m:ℕ. (∃p:{ℤ X ℤ| let x,y = p in GCD(m;n1;(x ∗ m) + (y ∗ n1))}) 3. m: ℕ ⊢ ∃p:{ℤ X ℤ| let x,y = p in GCD(m;n;(x ∗ m) + (y ∗ n))} | BY (Decide ⌈n = 0⌉ THENA Auto) | 4. n = 0 Assume n = 0 ⊢ ∃p:{ℤ X ℤ| let x,y = p in GCD(m;n;(x ∗ m) + (y ∗ n))} | BY (SqHypSubst 4 0 THENA Auto) Substitute 0 for n in the conclusion | ⊢ ∃p:{ℤ X ℤ| let x,y = p in GCD(m;0;(x ∗ m) + (y ∗ 0))} | BY (InstConcl [⌈〈1, 0〉⌉] THENA Auto) Instantiate the conclusion | with 〈1,0〉 ⊢ let x,y = 〈1, 0〉 in GCD(m;0;(x ∗ m) + (y ∗ 0)) | BY Reduce 0 Simplify the conclusion | ⊢ GCD(m;0;(1 ∗ m) + 0) | BY (InstLemma `gcd_p_zero` [⌈m⌉] THENA Auto) Apply the Nuprl lemma that | proves that the GCD 5. GCD(m;0;m) of m and 0 is m ⊢ GCD(m;0;(1 ∗ m) + 0) | BY Auto

For the case of n ≠ 0, we apply the induction hypothesis to (m rem n) and n. Notice that this lines up with the "else" case in the recursive algorithm. To meet the condition of the induction hypothesis, we must prove that (m rem n) < n. This property is part of the Nuprl lemma rem_bounds_1. Like the original proof, this means that the recursive algorithm will terminate since (m rem n) < n and we know the result for the base case of 0.

1. n: ℕ 2. ∀n1:ℕn. ∀m:ℕ. (∃p:{ℤ X ℤ| let x,y = p in GCD(m;n1;(x ∗ m) + (y ∗ n1))}) 3. m: ℕ ⊢ ∃p:{ℤ X ℤ| let x,y = p in GCD(m;n;(x ∗ m) + (y ∗ n))} | BY (Decide ⌈n = 0⌉ THENA Auto) | 4. ¬(n = 0) Assume n ≠ 0 ⊢ ∃p:{ℤ X ℤ| let x,y = p in GCD(m;n;(x ∗ m) + (y ∗ n))} | BY (InstHyp [⌈m rem n⌉;⌈n⌉] 2 THENA Auto) Apply the induction hypothesis, | setting n1 = (m rem n) and m = n ⊢ (m rem n) < n | BY (InstLemma `rem_bounds_1` [⌈m⌉;⌈n⌉] THENA Auto) Apply the Nuprl lemma | that proves that 5. (0 ≤ (m rem n)) ∧ ((m rem n) < n) (m rem n) < n, a condition ⊢ (m rem n) < n of the induction hypothesis | BY Auto


So far the proof has been pretty much the same as the original one shown above, but now there will be a little bit of extra work. By the induction hypothesis, there exists a pair of integers p = p1,p2 such that (p1 ∗ n) + (p2 ∗ (m rem n)) is the greatest common divisor of n and (m rem n). We know that GCD(m;n;g) ⇔ GCD(n;m rem n;g), and we can use this property to find the pair of integers for m and n if we can rearrange the expression (p1 ∗ n) + (p2 ∗ (m rem n)) to be something times m plus something times n. For this we will use the property that (m rem n) = (m - (m ÷ n) ∗ n), which is proven separately in the Nuprl lemma rem_to_div.

1. n: ℕ 2. ∀n1:ℕn. ∀m:ℕ. (∃p:{ℤ X ℤ| let x,y = p in GCD(m;n1;(x ∗ m) + (y ∗ n1))}) 3. m: ℕ 4. ¬(n = 0) 5. ∃p:{ℤ X ℤ| let x,y = p in GCD(n;m rem n;(x ∗ n) + (y ∗ (m rem n)))} | Result from applying the induction hypothesis | ⊢ ∃p:{ℤ X ℤ| let x,y = p in GCD(m;n;(x ∗ m) + (y ∗ n))} | BY D 5 Decompose hypothesis 5 to extract p, | the pair of integers for the GCD of n and (m rem n) 5. p: ℤ X ℤ [6]. let x,y = p in GCD(n;m rem n;(x ∗ n) + (y ∗ (m rem n))) ⊢ ∃p:{ℤ X ℤ| let x,y = p in GCD(m;n;(x ∗ m) + (y ∗ n))} | BY D 5 Decompose again to separate out | the components of the pair 5. p1: ℤ 6. p2: ℤ [7]. let x,y = 〈p1, p2〉 in GCD(n;m rem n;(x ∗ n) + (y ∗ (m rem n))) ⊢ ∃p:{ℤ X ℤ| let x,y = p in GCD(m;n;(x ∗ m) + (y ∗ n))} | By Reduce 7 Simplify hypothesis 7 | [7]. GCD(n;m rem n;(p1 ∗ n) + (p2 ∗ (m rem n))) ⊢ ∃p:{ℤ X ℤ| let x,y = p in GCD(m;n;(x ∗ m) + (y ∗ n))} | BY (InstLemma `rem_to_div` [⌈m⌉;⌈n⌉] THENA Auto) Apply a Nuprl lemma | to restate (m rem n) 8. (m rem n) = (m - (m ÷ n) ∗ n) ⊢ ∃p:{ℤ X ℤ| let x,y = p in GCD(m;n;(x ∗ m) + (y ∗ n))} | BY Assert ⌈((p1 ∗ n) + (p2 ∗ (m rem n))) = || ((p2 ∗ m) + ((p1 - p2 ∗ (m ÷ n)) ∗ n))⌉ | \ | 7. GCD(n;m rem n;(p1 ∗ n) + (p2 ∗ (m rem n))) | ⊢ ((p1 ∗ n) + (p2 ∗ (m rem n))) = ((p2 ∗ m) + ((p1 - p2 ∗ (m ÷ n)) ∗ n)) | | Prove the assertion (algebra) 1 BY (SqHypSubst 8 0 THENA Auto) | | | ⊢ ((p1 ∗ n) + (p2 ∗ (m - (m ÷ n) ∗ n))) = | | ((p2 ∗ m) + ((p1 - p2 ∗ (m ÷ n)) ∗ n)) | | 1 BY Auto \ 9. ((p1 ∗ n) + (p2 ∗ (m rem n))) = ((p2 ∗ m) + ((p1 - p2 ∗ (m ÷ n)) ∗ n)) ⊢ ∃p:{ℤ X ℤ| let x,y = p in GCD(m;n;(x ∗ m) + (y ∗ n))} | BY (SqHypSubst 9 7 THENA Auto) Use the assertion to restate the | GCD in the induction hypothesis [7]. GCD(n;m rem n;(p2 ∗ m) + ((p1 - p2 ∗ (m ÷ n)) ∗ n)) ⊢ ∃p:{ℤ X ℤ| let x,y = p in GCD(m;n;(x ∗ m) + (y ∗ n))} | BY (InstConcl [⌈〈p2, p1 - p2 ∗ (m ÷ n)〉⌉] THENA Auto) | Instantiate the conclusion | with the pair 〈p2, p1 - p2 ∗ (m ÷ n)〉 7. GCD(n;m rem n;(p2 ∗ m) + ((p1 - p2 ∗ (m ÷ n)) ∗ n)) ⊢ let x,y = 〈p2, p1 - p2 ∗ (m ÷ n)〉 in GCD(m;n;(x ∗ m) + (y ∗ n)) | BY Reduce 0 Simplify the conclusion | ⊢ GCD(m;n;(p2 ∗ m) + ((p1 - p2 ∗ (m ÷ n)) ∗ n)) | BY (InstLemma `div_rem_gcd_anne` | [⌈m⌉;⌈n⌉;⌈(p2 ∗ m) + ((p1 - p2 ∗ (m ÷ n)) ∗ n)⌉] THENA Auto) | Apply the Nuprl lemma 10. GCD(m;n;(p2 ∗ m) + ((p1 - p2 ∗ (m ÷ n)) ∗ n)) ⇔ that proves that the GCD GCD(n;m rem n;(p2 ∗ m) + ((p1 - p2 ∗ (m ÷ n)) ∗ n)) of m and n is equivalent to ⊢ GCD(m;n;(p2 ∗ m) + ((p1 - p2 ∗ (m ÷ n)) ∗ n)) the GCD of n and (m rem n) | BY Auto





References

"Case Study in Verification: Development and Proof of the Euclidean Algorithm for GCD." Cornell University CS3110 Lecture Notes, Spring 2013.

Oystein Ore. Invitation to Number Theory. Random House, 1967.



1 The theorems on this page use the Nuprl lemma gcd_p_zero. The linked PDF for the proof of Lemma 2 is actually from the Nuprl lemma gcd_p_zero_anne, which proves the same property but shows the steps in more detail for educational purposes.