# mathlibdocumentation

data.pnat.xgcd

@[instance]

structure pnat.xgcd_type  :
Type

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

@[instance]

Equations
@[instance]

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

Equations
def pnat.xgcd_type.mk'  :
ℕ+ℕ+

Equations

Equations

Equations

Equations

Equations

Equations

Equations

Equations

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

Equations

Equations

is_special holds if the matrix has determinant one.

Equations

Equations

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

Equations

Equations
@[simp]
theorem pnat.xgcd_type.flip_w (u : pnat.xgcd_type) :
u.flip.w = u.z

@[simp]
theorem pnat.xgcd_type.flip_x (u : pnat.xgcd_type) :
u.flip.x = u.y

@[simp]
theorem pnat.xgcd_type.flip_y (u : pnat.xgcd_type) :
u.flip.y = u.x

@[simp]
theorem pnat.xgcd_type.flip_z (u : pnat.xgcd_type) :
u.flip.z = u.w

@[simp]
theorem pnat.xgcd_type.flip_a (u : pnat.xgcd_type) :
u.flip.a = u.b

@[simp]
theorem pnat.xgcd_type.flip_b (u : pnat.xgcd_type) :
u.flip.b = u.a

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.

theorem pnat.xgcd_type.qp_eq (u : pnat.xgcd_type) :
u.r = 0u.q = u.qp + 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.

Equations
theorem pnat.xgcd_type.start_v (a b : ℕ+) :
b).v = (a, b)

Equations
theorem pnat.xgcd_type.finish_v (u : pnat.xgcd_type) :
u.r = 0u.finish.v = u.v

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

Equations
theorem pnat.xgcd_type.step_wf (u : pnat.xgcd_type) :
u.r 0 <

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

theorem pnat.xgcd_type.step_v (u : pnat.xgcd_type) :
u.r 0u.step.v = u.v.swap

The reduction step does not change the product vector.

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
def pnat.xgcd  :

Equations
def pnat.gcd_d  :
ℕ+ℕ+ℕ+

Equations
def pnat.gcd_w  :
ℕ+ℕ+ℕ+

Equations
def pnat.gcd_x  :
ℕ+ℕ+

Equations
def pnat.gcd_y  :
ℕ+ℕ+

Equations
def pnat.gcd_z  :
ℕ+ℕ+ℕ+

Equations
def pnat.gcd_a'  :
ℕ+ℕ+ℕ+

Equations
def pnat.gcd_b'  :
ℕ+ℕ+ℕ+

Equations
theorem pnat.gcd_a'_coe (a b : ℕ+) :
(a.gcd_a' b) = (a.gcd_w b) + a.gcd_x b

theorem pnat.gcd_b'_coe (a b : ℕ+) :
(a.gcd_b' b) = a.gcd_y b + (a.gcd_z b)

theorem pnat.gcd_props (a b : ℕ+) :
let d : ℕ+ := a.gcd_d b, w : ℕ+ := a.gcd_w b, x : := a.gcd_x b, y : := a.gcd_y b, z : ℕ+ := a.gcd_z b, a' : ℕ+ := a.gcd_a' b, b' : ℕ+ := a.gcd_b' b in w * z = (x * y).succ_pnat a = a' * d b = b' * d z * a' = (x * b').succ_pnat w * b' = (y * a').succ_pnat (z) * a = x * b + d (w) * b = y * a + d

theorem pnat.gcd_eq (a b : ℕ+) :
a.gcd_d b = a.gcd b

theorem pnat.gcd_det_eq (a b : ℕ+) :
(a.gcd_w b) * a.gcd_z b = ((a.gcd_x b) * a.gcd_y b).succ_pnat

theorem pnat.gcd_a_eq (a b : ℕ+) :
a = (a.gcd_a' b) * a.gcd b

theorem pnat.gcd_b_eq (a b : ℕ+) :
b = (a.gcd_b' b) * a.gcd b

theorem pnat.gcd_rel_left' (a b : ℕ+) :
(a.gcd_z b) * a.gcd_a' b = ((a.gcd_x b) * (a.gcd_b' b)).succ_pnat

theorem pnat.gcd_rel_right' (a b : ℕ+) :
(a.gcd_w b) * a.gcd_b' b = ((a.gcd_y b) * (a.gcd_a' b)).succ_pnat

theorem pnat.gcd_rel_left (a b : ℕ+) :
((a.gcd_z b)) * a = (a.gcd_x b) * b + (a.gcd b)

theorem pnat.gcd_rel_right (a b : ℕ+) :
((a.gcd_w b)) * b = (a.gcd_y b) * a + (a.gcd b)