~/jendhub

proofs/math/number/egcd.bend

bend-collections-laws-math@1.0.0.0 · 100 lines · 13 definitions

1import Base
2import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as A
3import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
4import bend-collections-laws-math@1.0.0.0/src/math/number.bend as NB
5import bend-collections-laws-math@1.0.0.0/spec/math/number.bend as SN
6import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as R
7
8# The extended Euclidean algorithm (Knuth 4.5.2, Algorithm X; Lean 4
9# Mathlib Nat.xgcd with Nat.gcd_eq_gcd_ab: a * gcdA a b + b * gcdB a b =
10# gcd a b). The recursion is natural.bend's gcd_go step for step, so its
11# gcd is gcd_go's; the Bezout identity is carried up the recursion with the
12# sign flipping at each level (the magnitudes of Algorithm X).
13
14# ---- the gcd ----
15
16def up_gcd(+q: Nat, r: NB.EGcd) -> {SN.eg_gcd(NB.eg_up(q, r)) == SN.eg_gcd(r) : Nat}:
17  match r:
18    case NB.EG{+g, +x, +y, +neg}:
19      {==}
20
21def gcd_go(+f: Nat, +a: Nat, +b: Nat) -> {SN.eg_gcd(NB.egcd_go(f, a, b)) == M.gcd_go(f, a, b) : Nat}:
22  match f b:
23    case 0n _:
24      {==}
25    case 1n+ +g 0n:
26      {==}
27    case 1n+ +g 1n+ +bp:
28      %Equal.sym(Nat, SN.eg_gcd(NB.eg_up(Nat.div(a, 1n+bp), NB.egcd_go(g, 1n+bp, Nat.mod(a, 1n+bp)))), SN.eg_gcd(NB.egcd_go(g, 1n+bp, Nat.mod(a, 1n+bp))), up_gcd(Nat.div(a, 1n+bp), NB.egcd_go(g, 1n+bp, Nat.mod(a, 1n+bp)))) : {_ == M.gcd_go(1n+g, a, 1n+bp) : Nat}
29      gcd_go(g, 1n+bp, Nat.mod(a, 1n+bp))
30
31def egcd_gcd(+a: Nat, +b: Nat) -> SN.Egcd.gcd(a, b):
32  gcd_go(b, a, b)
33
34# ---- the Bezout identity ----
35
36# (q b) y == b (q y)
37def qby(+q: Nat, +b: Nat, +y: Nat) -> {Nat.mul(Nat.mul(q, b), y) == Nat.mul(b, Nat.mul(q, y)) : Nat}:
38  %Equal.sym(Nat, Nat.mul(q, b), Nat.mul(b, q), A.mul_comm(q, b)) : {Nat.mul(_, y) == Nat.mul(b, Nat.mul(q, y)) : Nat}
39  A.mul_assoc(b, q, y)
40
41# (q b + r) y == b (q y) + r y
42def spread(+q: Nat, +b: Nat, +r: Nat, +y: Nat) -> {Nat.mul(Nat.add(Nat.mul(q, b), r), y) == Nat.add(Nat.mul(b, Nat.mul(q, y)), Nat.mul(r, y)) : Nat}:
43  %Equal.sym(Nat, Nat.mul(Nat.add(Nat.mul(q, b), r), y), Nat.add(Nat.mul(Nat.mul(q, b), y), Nat.mul(r, y)), A.mul_add_right(Nat.mul(q, b), r, y)) : {_ == Nat.add(Nat.mul(b, Nat.mul(q, y)), Nat.mul(r, y)) : Nat}
44  %Equal.sym(Nat, Nat.mul(Nat.mul(q, b), y), Nat.mul(b, Nat.mul(q, y)), qby(q, b, y)) : {Nat.add(_, Nat.mul(r, y)) == Nat.add(Nat.mul(b, Nat.mul(q, y)), Nat.mul(r, y)) : Nat}
45  {==}
46
47# child b x == g + r y  gives  b (x + q y) == g + (q b + r) y
48def alg_pos(+g: Nat, +x: Nat, +y: Nat, +q: Nat, +b: Nat, +r: Nat, +ih: {Nat.mul(b, x) == Nat.add(g, Nat.mul(r, y)) : Nat}) -> {Nat.mul(b, Nat.add(x, Nat.mul(q, y))) == Nat.add(g, Nat.mul(Nat.add(Nat.mul(q, b), r), y)) : Nat}:
49  %Equal.sym(Nat, Nat.mul(b, Nat.add(x, Nat.mul(q, y))), Nat.add(Nat.mul(b, x), Nat.mul(b, Nat.mul(q, y))), A.mul_add_left(b, x, Nat.mul(q, y))) : {_ == Nat.add(g, Nat.mul(Nat.add(Nat.mul(q, b), r), y)) : Nat}
50  %Equal.sym(Nat, Nat.mul(Nat.add(Nat.mul(q, b), r), y), Nat.add(Nat.mul(b, Nat.mul(q, y)), Nat.mul(r, y)), spread(q, b, r, y)) : {Nat.add(Nat.mul(b, x), Nat.mul(b, Nat.mul(q, y))) == Nat.add(g, _) : Nat}
51  %Equal.sym(Nat, Nat.mul(b, x), Nat.add(g, Nat.mul(r, y)), ih) : {Nat.add(_, Nat.mul(b, Nat.mul(q, y))) == Nat.add(g, Nat.add(Nat.mul(b, Nat.mul(q, y)), Nat.mul(r, y))) : Nat}
52  %Equal.sym(Nat, Nat.add(Nat.mul(b, Nat.mul(q, y)), Nat.mul(r, y)), Nat.add(Nat.mul(r, y), Nat.mul(b, Nat.mul(q, y))), A.add_comm(Nat.mul(b, Nat.mul(q, y)), Nat.mul(r, y))) : {Nat.add(Nat.add(g, Nat.mul(r, y)), Nat.mul(b, Nat.mul(q, y))) == Nat.add(g, _) : Nat}
53  A.add_assoc(g, Nat.mul(r, y), Nat.mul(b, Nat.mul(q, y)))
54
55# child r y == g + b x  gives  (q b + r) y == g + b (x + q y)
56def alg_neg(+g: Nat, +x: Nat, +y: Nat, +q: Nat, +b: Nat, +r: Nat, +ih: {Nat.mul(r, y) == Nat.add(g, Nat.mul(b, x)) : Nat}) -> {Nat.mul(Nat.add(Nat.mul(q, b), r), y) == Nat.add(g, Nat.mul(b, Nat.add(x, Nat.mul(q, y)))) : Nat}:
57  %Equal.sym(Nat, Nat.mul(Nat.add(Nat.mul(q, b), r), y), Nat.add(Nat.mul(b, Nat.mul(q, y)), Nat.mul(r, y)), spread(q, b, r, y)) : {_ == Nat.add(g, Nat.mul(b, Nat.add(x, Nat.mul(q, y)))) : Nat}
58  %Equal.sym(Nat, Nat.mul(r, y), Nat.add(g, Nat.mul(b, x)), ih) : {Nat.add(Nat.mul(b, Nat.mul(q, y)), _) == Nat.add(g, Nat.mul(b, Nat.add(x, Nat.mul(q, y)))) : Nat}
59  %Equal.sym(Nat, Nat.mul(b, Nat.add(x, Nat.mul(q, y))), Nat.add(Nat.mul(b, x), Nat.mul(b, Nat.mul(q, y))), A.mul_add_left(b, x, Nat.mul(q, y))) : {Nat.add(Nat.mul(b, Nat.mul(q, y)), Nat.add(g, Nat.mul(b, x))) == Nat.add(g, _) : Nat}
60  %Equal.sym(Nat, Nat.add(Nat.mul(b, Nat.mul(q, y)), Nat.add(g, Nat.mul(b, x))), Nat.add(g, Nat.add(Nat.mul(b, Nat.mul(q, y)), Nat.mul(b, x))), A.add_swap(Nat.mul(b, Nat.mul(q, y)), g, Nat.mul(b, x))) : {_ == Nat.add(g, Nat.add(Nat.mul(b, x), Nat.mul(b, Nat.mul(q, y)))) : Nat}
61  %Equal.sym(Nat, Nat.add(Nat.mul(b, Nat.mul(q, y)), Nat.mul(b, x)), Nat.add(Nat.mul(b, x), Nat.mul(b, Nat.mul(q, y))), A.add_comm(Nat.mul(b, Nat.mul(q, y)), Nat.mul(b, x))) : {Nat.add(g, _) == Nat.add(g, Nat.add(Nat.mul(b, x), Nat.mul(b, Nat.mul(q, y)))) : Nat}
62  {==}
63
64# the base case: a * 1 == a + b * 0
65def base(+a: Nat, +b: Nat) -> {Nat.mul(a, 1n) == Nat.add(a, Nat.mul(b, 0n)) : Nat}:
66  %Equal.sym(Nat, Nat.mul(a, 1n), a, A.mul_one(a)) : {_ == Nat.add(a, Nat.mul(b, 0n)) : Nat}
67  %Equal.sym(Nat, Nat.mul(b, 0n), 0n, A.mul_zero(b)) : {a == Nat.add(a, _) : Nat}
68  Equal.sym(Nat, Nat.add(a, 0n), a, A.add_zero(a))
69
70def up_sign(+a: Nat, +b: Nat, +q: Nat, +r: Nat, +ha: {a == Nat.add(Nat.mul(q, b), r) : Nat}, +g: Nat, +x: Nat, +y: Nat, +neg: Bool, +ih: {SN.eg_pos(b, r, NB.EG{g, x, y, neg}) == SN.eg_neg(b, r, NB.EG{g, x, y, neg}) : Nat}) -> {SN.eg_pos(a, b, NB.eg_up(q, NB.EG{g, x, y, neg})) == SN.eg_neg(a, b, NB.eg_up(q, NB.EG{g, x, y, neg})) : Nat}:
71  match neg:
72    case False{}:
73      %Equal.sym(Nat, a, Nat.add(Nat.mul(q, b), r), ha) : {Nat.mul(b, Nat.add(x, Nat.mul(q, y))) == Nat.add(g, Nat.mul(_, y)) : Nat}
74      alg_pos(g, x, y, q, b, r, ih)
75    case True{}:
76      %Equal.sym(Nat, a, Nat.add(Nat.mul(q, b), r), ha) : {Nat.mul(_, y) == Nat.add(g, Nat.mul(b, Nat.add(x, Nat.mul(q, y)))) : Nat}
77      alg_neg(g, x, y, q, b, r, ih)
78
79# one level up: from the child's identity for (b, r) to the parent's for
80# (a, b), a == q b + r
81def up_bez(+a: Nat, +b: Nat, +q: Nat, +r: Nat, +ha: {a == Nat.add(Nat.mul(q, b), r) : Nat}, c: NB.EGcd, +ih: {SN.eg_pos(b, r, c) == SN.eg_neg(b, r, c) : Nat}) -> {SN.eg_pos(a, b, NB.eg_up(q, c)) == SN.eg_neg(a, b, NB.eg_up(q, c)) : Nat}:
82  match c:
83    case NB.EG{+g, +x, +y, +neg}:
84      up_sign(a, b, q, r, ha, g, x, y, neg, ih)
85
86# a == (a div b) b + a mod b
87def split(+a: Nat, +bp: Nat) -> {a == Nat.add(Nat.mul(Nat.div(a, 1n+bp), 1n+bp), Nat.mod(a, 1n+bp)) : Nat}:
88  R.dm_eq(bp, a)
89
90def bez_go(+f: Nat, +a: Nat, +b: Nat) -> {SN.eg_pos(a, b, NB.egcd_go(f, a, b)) == SN.eg_neg(a, b, NB.egcd_go(f, a, b)) : Nat}:
91  match f b:
92    case 0n _:
93      base(a, b)
94    case 1n+ +g 0n:
95      base(a, 0n)
96    case 1n+ +g 1n+ +bp:
97      up_bez(a, 1n+bp, Nat.div(a, 1n+bp), Nat.mod(a, 1n+bp), split(a, bp), NB.egcd_go(g, 1n+bp, Nat.mod(a, 1n+bp)), bez_go(g, 1n+bp, Nat.mod(a, 1n+bp)))
98
99def egcd_bezout(+a: Nat, +b: Nat) -> SN.Egcd.bezout(a, b):
100  bez_go(b, a, b)