Euclidean algorithm for ℕ #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file sets up a version of the Euclidean algorithm that only works with natural numbers. Given 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 d is then the gcd of a and b, and a' := a / d = w + x and b' := b / d = y + z are 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 wp zp, ap, bp are the variables getting changed through the algorithm.
is_special: States wp * zp = x * y + 1
is_reduced: States ap = a ∧ bp = b

Notes #

See nat.xgcd for a very similar algorithm allowing values in ℤ.

source

@[protected, instance]

def pnat.xgcd_type.inhabited :

inhabited pnat.xgcd_type

source

structure pnat.xgcd_type :

Type

wp : ℕ
x : ℕ
y : ℕ
zp : ℕ
ap : ℕ
bp : ℕ

A term of xgcd_type 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].

Instances for pnat.xgcd_type

source

@[protected, instance]

def pnat.xgcd_type.has_sizeof :

has_sizeof pnat.xgcd_type

Equations

pnat.xgcd_type.has_sizeof = {sizeof := λ (u : pnat.xgcd_type), u.bp}

source

@[protected, instance]

def pnat.xgcd_type.has_repr :

has_repr pnat.xgcd_type

The has_repr instance converts terms to strings in a way that reflects the matrix/vector interpretation as above.

Equations

pnat.xgcd_type.has_repr = {repr := λ (u : pnat.xgcd_type), "[[[" ++ repr (u.wp + 1) ++ ", " ++ repr u.x ++ "], [" ++ repr u.y ++ ", " ++ repr (u.zp + 1) ++ "]], [" ++ repr (u.ap + 1) ++ ", " ++ repr (u.bp + 1) ++ "]]"}

source

def pnat.xgcd_type.mk' (w : ℕ+) (x y : ℕ) (z a b : ℕ+) :

pnat.xgcd_type

Equations

pnat.xgcd_type.mk' w x y z a b = {wp := w.val.pred, x := x, y := y, zp := z.val.pred, ap := a.val.pred, bp := b.val.pred}

source

def pnat.xgcd_type.w (u : pnat.xgcd_type) :

ℕ+

Equations

u.w = u.wp.succ_pnat

source

def pnat.xgcd_type.z (u : pnat.xgcd_type) :

ℕ+

Equations

u.z = u.zp.succ_pnat

source

def pnat.xgcd_type.a (u : pnat.xgcd_type) :

ℕ+

Equations

u.a = u.ap.succ_pnat

source

def pnat.xgcd_type.b (u : pnat.xgcd_type) :

ℕ+

Equations

u.b = u.bp.succ_pnat

source

def pnat.xgcd_type.r (u : pnat.xgcd_type) :

ℕ

Equations

u.r = (u.ap + 1) % (u.bp + 1)

source

def pnat.xgcd_type.q (u : pnat.xgcd_type) :

ℕ

Equations

u.q = (u.ap + 1) / (u.bp + 1)

source

def pnat.xgcd_type.qp (u : pnat.xgcd_type) :

ℕ

Equations

u.qp = u.q - 1

source

def pnat.xgcd_type.vp (u : pnat.xgcd_type) :

ℕ × ℕ

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].

Equations

u.vp = (u.wp + u.x + u.ap + u.wp * u.ap + u.x * u.bp, u.y + u.zp + u.bp + u.y * u.ap + u.zp * u.bp)

source

def pnat.xgcd_type.v (u : pnat.xgcd_type) :

ℕ × ℕ

Equations

u.v = (↑(u.w) * ↑(u.a) + u.x * ↑(u.b), u.y * ↑(u.a) + ↑(u.z) * ↑(u.b))

source

def pnat.xgcd_type.succ₂ (t : ℕ × ℕ) :

ℕ × ℕ

Equations

pnat.xgcd_type.succ₂ t = (t.fst.succ, t.snd.succ)

source

theorem pnat.xgcd_type.v_eq_succ_vp (u : pnat.xgcd_type) :

u.v = pnat.xgcd_type.succ₂ u.vp

source

def pnat.xgcd_type.is_special (u : pnat.xgcd_type) :

Prop

is_special holds if the matrix has determinant one.

Equations

u.is_special = (u.wp + u.zp + u.wp * u.zp = u.x * u.y)

source

def pnat.xgcd_type.is_special' (u : pnat.xgcd_type) :

Prop

Equations

u.is_special' = (u.w * u.z = (u.x * u.y).succ_pnat)

source

theorem pnat.xgcd_type.is_special_iff (u : pnat.xgcd_type) :

u.is_special ↔ u.is_special'

source

def pnat.xgcd_type.is_reduced (u : pnat.xgcd_type) :

Prop

is_reduced holds if the two entries in the vector are the same. The reduction algorithm will produce a system with this property, whose product vector is the same as for the original system.

Equations

u.is_reduced = (u.ap = u.bp)

source

def pnat.xgcd_type.is_reduced' (u : pnat.xgcd_type) :

Prop

Equations

u.is_reduced' = (u.a = u.b)

source

theorem pnat.xgcd_type.is_reduced_iff (u : pnat.xgcd_type) :

u.is_reduced ↔ u.is_reduced'

source

def pnat.xgcd_type.flip (u : pnat.xgcd_type) :

pnat.xgcd_type

Equations

u.flip = {wp := u.zp, x := u.y, y := u.x, zp := u.wp, ap := u.bp, bp := u.ap}

source

@[simp]

theorem pnat.xgcd_type.flip_w (u : pnat.xgcd_type) :

u.flip.w = u.z

source

@[simp]

theorem pnat.xgcd_type.flip_x (u : pnat.xgcd_type) :

u.flip.x = u.y

source

@[simp]

theorem pnat.xgcd_type.flip_y (u : pnat.xgcd_type) :

u.flip.y = u.x

source

@[simp]

theorem pnat.xgcd_type.flip_z (u : pnat.xgcd_type) :

u.flip.z = u.w

source

@[simp]

theorem pnat.xgcd_type.flip_a (u : pnat.xgcd_type) :

u.flip.a = u.b

source

@[simp]

theorem pnat.xgcd_type.flip_b (u : pnat.xgcd_type) :

u.flip.b = u.a

source

theorem pnat.xgcd_type.flip_is_reduced (u : pnat.xgcd_type) :

u.flip.is_reduced ↔ u.is_reduced

source

theorem pnat.xgcd_type.flip_is_special (u : pnat.xgcd_type) :

u.flip.is_special ↔ u.is_special

source

theorem pnat.xgcd_type.flip_v (u : pnat.xgcd_type) :

u.flip.v = u.v.swap

source

theorem pnat.xgcd_type.rq_eq (u : pnat.xgcd_type) :

u.r + (u.bp + 1) * u.q = u.ap + 1

Properties of division with remainder for a / b.

source

theorem pnat.xgcd_type.qp_eq (u : pnat.xgcd_type) (hr : u.r = 0) :

u.q = u.qp + 1

source

def pnat.xgcd_type.start (a b : ℕ+) :

pnat.xgcd_type

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.

Equations

pnat.xgcd_type.start a b = {wp := 0, x := 0, y := 0, zp := 0, ap := ↑a - 1, bp := ↑b - 1}

source

theorem pnat.xgcd_type.start_is_special (a b : ℕ+) :

(pnat.xgcd_type.start a b).is_special

source

theorem pnat.xgcd_type.start_v (a b : ℕ+) :

(pnat.xgcd_type.start a b).v = (↑a, ↑b)

source

def pnat.xgcd_type.finish (u : pnat.xgcd_type) :

pnat.xgcd_type

Equations

u.finish = {wp := u.wp, x := (u.wp + 1) * u.qp + u.x, y := u.y, zp := u.y * u.qp + u.zp, ap := u.bp, bp := u.bp}

source

theorem pnat.xgcd_type.finish_is_reduced (u : pnat.xgcd_type) :

u.finish.is_reduced

source

theorem pnat.xgcd_type.finish_is_special (u : pnat.xgcd_type) (hs : u.is_special) :

u.finish.is_special

source

theorem pnat.xgcd_type.finish_v (u : pnat.xgcd_type) (hr : u.r = 0) :

u.finish.v = u.v

source

def pnat.xgcd_type.step (u : pnat.xgcd_type) :

pnat.xgcd_type

This is the main reduction step, which is used when u.r ≠ 0, or equivalently b does not divide a.

Equations

u.step = {wp := u.y * u.q + u.zp, x := u.y, y := (u.wp + 1) * u.q + u.x, zp := u.wp, ap := u.bp, bp := u.r - 1}

source

theorem pnat.xgcd_type.step_wf (u : pnat.xgcd_type) (hr : u.r ≠ 0) :

sizeof u.step < sizeof u

We will apply the above step recursively. The following result is used to ensure that the process terminates.

source

theorem pnat.xgcd_type.step_is_special (u : pnat.xgcd_type) (hs : u.is_special) :

u.step.is_special

source

theorem pnat.xgcd_type.step_v (u : pnat.xgcd_type) (hr : u.r ≠ 0) :

u.step.v = u.v.swap

The reduction step does not change the product vector.

source

def pnat.xgcd_type.reduce :

pnat.xgcd_type → pnat.xgcd_type

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.

Equations