Euclidean algorithm for ℕ #
This file sets up a version of the Euclidean algorithm that only works with natural numbers.
0 < a, b, it computes the unique
(w, x, y, z, d) such that the following identities hold:
a = (w + x) d
b = (y + z) d
w * z = x * y + 1
dis then the gcd of
a' := a / d = w + xand
b' := b / d = y + zare coprime.
This story is closely related to the structure of SL₂(ℕ) (as a free monoid on two generators) and the theory of continued fractions.
Main declarations #
xgcd_type: Helper type in defining the gcd. Encapsulates
(wp, x, y, zp, ap, bp). where
bpare the variables getting changed through the algorithm.
wp * zp = x * y + 1
ap = a ∧ bp = b
nat.xgcd for a very similar algorithm allowing values in
The has_repr instance converts terms to strings in a way that reflects the matrix/vector interpretation as above.
The map v gives the product of the matrix [[w, x], [y, z]] = [[wp + 1, x], [y, zp + 1]] and the vector [a, b] = [ap + 1, bp + 1]. The map vp gives [sp, tp] such that v = [sp + 1, tp + 1].
The following function provides the starting point for our algorithm. We will apply an iterative reduction process to it, which will produce a system satisfying is_reduced. The gcd can be read off from this final system.
We can now define the full reduction function, which applies step as long as possible, and then applies finish. Note that the "have" statement puts a fact in the local context, and the equation compiler uses this fact to help construct the full definition in terms of well-founded recursion. The same fact needs to be introduced in all the inductive proofs of properties given below.