Euclid’s gcd algorithm

Johan G. F. Belinfante
2009 April 1

SetDirectory["l:"];   << goedel.09mar31b;  <<  
      tools.m

summary

In this notebook Art Quaife’s Theorem (GCD23) is derived, along with some corollaries, including Art Quaife’s Theorems (GCD22) and (GCD24), the latter being the basis for Euclid’s gcd algorithm.

"Art Quaife, Automated Development of Fundamental Mathematical Theories, Appendix 3. Theorems Proved in Peano's Arithmetic, Kluwer Academic Publishers, Dordrecht, 1992. Cf. pp. 202-206";

temporary abbreviations

divides[x_, y_] := member[pair[x, y], DIV]

gcd[x_] := APPLY[GLB[DIV], x]

derivation

To derive the equation in (GCD23) it suffices to show that each side divides the other.

Lemma.

SubstTest[implies, and[divides[t, u], divides[t, v]], 
        divides[t, natadd[u, v]], {t -> gcd[set[nat[x], nat[y]]], 
          u -> nat[x], v -> natmul[nat[w], nat[y]]}] // 
      Reverse

(% /. {w -> w_, x -> x_, y -> y_}) /. 
      Equal -> SetDelayed

Theorem.  Divisibility in one direction.

SubstTest[implies, and[divides[t, u], divides[t, v]], 
        divides[t, gcd[set[u, v]]], {t -> gcd[set[nat[x], nat[y]]], 
          u -> nat[y], 
          v -> natadd[nat[x], natmul[nat[w], nat[y]]]}] // 
      Reverse

(% /. {w -> w_, x -> x_, y -> y_}) /. 
      Equal -> SetDelayed

Four lemmas are needed to derive divisibility in the opposite direction.

Lemma.

SubstTest[divides, gcd[set[nat[y], nat[t]]], nat[y], 
        t -> natadd[nat[x], natmul[nat[w], nat[y]]]] // Reverse

(% /. {w -> w_, x -> x_, y -> y_}) /. 
      Equal -> SetDelayed

Lemma.

SubstTest[divides, gcd[set[nat[y], nat[t]]], nat[t], 
        t -> natadd[nat[x], natmul[nat[w], nat[y]]]] // Reverse

(% /. {w -> w_, x -> x_, y -> y_}) /. 
      Equal -> SetDelayed

Lemma.

SubstTest[implies, and[divides[t, u], divides[u, v]], 
        divides[t, 
          v], {t -> gcd[set[nat[y], natadd[nat[x], natmul[nat[w], nat[y]]]]], 
          u -> nat[y], v -> natmul[nat[w], nat[y]]}] // 
      Reverse

(% /. {w -> w_, x -> x_, y -> y_}) /. 
      Equal -> SetDelayed

Lemma.

SubstTest[implies, and[divides[t, v], divides[t, natadd[u, v]]], 
        divides[t, 
          u], {t -> 
            gcd[set[nat[y], natadd[nat[x], natmul[nat[w], nat[y]]]]], 
          u -> nat[x], v -> natmul[nat[w], nat[y]]}] // 
      Reverse

(% /. {w -> w_, x -> x_, y -> y_}) /. 
      Equal -> SetDelayed

Theorem.  Divisibility in the other direction.

SubstTest[implies, and[divides[t, u], divides[t, v]], 
        divides[t, 
          gcd[set[u, v]]], {t -> 
            gcd[set[nat[y], natadd[nat[x], natmul[nat[w], nat[y]]]]], 
          u -> nat[x], v -> nat[y]}] // Reverse

(% /. {x -> x_, y -> y_}) /. 
      Equal -> SetDelayed

Theorem.  Quaife’s Theorem  (GCD23).

SubstTest[and, divides[u, v], 
      divides[v, u], {u -> gcd[set[nat[x], nat[y]]], 
        v -> gcd[
            set[nat[y], natadd[nat[x], natmul[nat[w], nat[y]]]]]}]

APPLY[GLB[DIV], 
        set[nat[y_], natadd[nat[x_], natmul[nat[w_], nat[y_]]]]] := 
      APPLY[GLB[DIV], set[nat[x], nat[y]]]

Quaife’s theorems (GCD22) and (GCD24)

Various corollaries of Quaife’s Theorem (GCD23) are derived in this section.

Corollary.  The special case w = 1.

SubstTest[APPLY, GLB[DIV], 
        set[nat[y], natadd[nat[x], natmul[nat[w], nat[y]]]], 
        w -> set[0]] // Reverse

APPLY[GLB[DIV], set[nat[y_], natadd[nat[x_], nat[y_]]]] := 
      APPLY[GLB[DIV], set[nat[x], nat[y]]]

Lemma.  The nat wrappers are removed and natsub is introduced here.

(SubstTest[implies, 
            and[equal[x, nat[u]], equal[y, nat[v]], equal[z, natadd[x, y]]], 
            equal[APPLY[GLB[DIV], set[x, y]], 
              APPLY[GLB[DIV], set[x, z]]], {u -> x, v -> y}] // 
          Reverse) /. y -> natsub[z, x]

(% /. {x -> x_, z -> z_}) /. 
      Equal -> SetDelayed

Theorem.  Analog of Quaife’s Theorem (GCD22) with natsub in place of monus.

SubstTest[or, 
        equal[APPLY[GLB[DIV], set[u, v]], 
          APPLY[GLB[DIV], set[u, natsub[v, u]]]], not[member[u, omega]], 
        not[member[v, omega]], 
        not[subclass[u, v]], {u -> nat[x], v -> nat[y]}] // 
      Reverse

or[equal[APPLY[GLB[DIV], set[nat[x_], nat[y_]]], 
          APPLY[GLB[DIV], set[nat[x_], natsub[nat[y_], nat[x_]]]]], 
        member[nat[y_], nat[x_]]] := True

For completeness the original monus version of Quaife’s Theorem (GCD22) is derived as a corollary.

Corollary.  Quaife’s Theorem (GCD22).

SubstTest[implies, equal[t, set[nat[x], natsub[nat[y], nat[x]]]], 
        or[equal[APPLY[GLB[DIV], set[nat[x], nat[y]]], APPLY[GLB[DIV], t]], 
          member[nat[y], nat[x]]], 
        t -> set[nat[x], nat[natsub[nat[y], nat[x]]]]] // 
      Reverse

or[equal[APPLY[GLB[DIV], set[nat[natsub[nat[y_], nat[x_]]], nat[x_]]], 
          APPLY[GLB[DIV], set[nat[x_], nat[y_]]]], member[nat[y_], nat[x_]]] := 
      True

Theorem.  Quaife’s Theorem (GCD24).  The basis for Euclid’s algorithm for computing gcd’s.  To prevent looping, the rewrite rule for this equation must be oriented in a direction opposite to the way it is used in Euclid’s algorithm.

(SubstTest[implies, equal[t, nat[z]], 
            equal[APPLY[GLB[DIV], set[t, nat[y]]], 
              APPLY[GLB[DIV], 
                set[nat[y], natadd[t, natmul[nat[w], nat[y]]]]]], 
            z -> t] /. {t -> natmod[nat[x], nat[y]], 
            w -> natquot[nat[x], nat[y]]}) // Reverse

APPLY[GLB[DIV], set[nat[y_], natmod[nat[x_], nat[y_]]]] := 
      APPLY[GLB[DIV], set[nat[x], nat[y]]]