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 #
XgcdType: 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
- wp : ℕ
wpis a variable which changes through the algorithm.
- x : ℕ
- y : ℕ
- zp : ℕ
zpis a variable which changes through the algorithm.
- ap : ℕ
apis a variable which changes through the algorithm.
- bp : ℕ
bpis a variable which changes through the algorithm.
A term of
XgcdType is a system of six naturals. They should
be thought of as representing the matrix
[[w, x], [y, z]] = [[wp + 1, x], [y, zp + 1]]
together with the vector [a, b] = [ap + 1, bp + 1].
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.