1	import Base
2	import ../../lib/nat.bend as N
3	import ../../lib/logic.bend as L
4	import ../../lib/lemmas/proofs/nat_algebra.bend as A
5	import ../../../src/math/natural.bend as M
6	import ./arith.bend as R
7	import ./gcd.bend as G
8	
9	# lcm is the least common multiple (Lean 4 Mathlib, Mathlib/Data/Nat/GCD:
10	# Nat.dvd_lcm_left, Nat.dvd_lcm_right, Nat.gcd_mul_lcm, Nat.lcm_dvd; the
11	# leastness goes through Nat.gcd_mul_left and dvd antisymmetry,
12	# Nat.dvd_antisymm). Divisibility again carries its witness.
13	
14	# ---- divisibility is antisymmetric ----
15	
16	def add_succ_zero(+b: Nat, +x: Nat, +e: {Nat.add(b, 1n+x) == 0n : Nat}) -> Empty:
17	  N.succ_zero(Nat.add(b, x), Equal.trans(Nat, 1n+Nat.add(b, x), Nat.add(b, 1n+x), 0n, Equal.sym(Nat, Nat.add(b, 1n+x), 1n+Nat.add(b, x), A.add_succ(b, x)), e))
18	
19	def one_s(+ap: Nat, +bq: Nat, +e: {Nat.add(bq, Nat.mul(ap, 1n+bq)) == 0n : Nat}) -> {1n+ap == 1n : Nat}:
20	  match ap:
21	    case 0n:
22	      {==}
23	    case 1n+ +app:
24	      Empty.absurd({2n+app == 1n : Nat}, add_succ_zero(bq, Nat.add(bq, Nat.mul(app, 1n+bq)), e))
25	
26	# a b == 1 gives a == 1   (Mathlib Nat.eq_one_of_mul_eq_one_right)
27	def mul_eq_one(+a: Nat, +b: Nat, +e: {Nat.mul(a, b) == 1n : Nat}) -> {a == 1n : Nat}:
28	  match a b:
29	    case 0n b0:
30	      Empty.absurd({0n == 1n : Nat}, N.zero_succ(0n, e))
31	    case 1n+ +ap 0n:
32	      Empty.absurd({1n+ap == 1n : Nat}, N.zero_succ(0n, Equal.trans(Nat, 0n, Nat.mul(1n+ap, 0n), 1n, Equal.sym(Nat, Nat.mul(1n+ap, 0n), 0n, A.mul_zero(1n+ap)), e)))
33	    case 1n+ +ap 1n+ +bq:
34	      one_s(ap, bq, N.succ_inj(Nat.add(bq, Nat.mul(ap, 1n+bq)), 0n, e))
35	
36	def one_mul(+d: Nat) -> {Nat.mul(1n, d) == d : Nat}:
37	  A.add_zero(d)
38	
39	# x == kx y and y == ky x give x == y   (Mathlib Nat.dvd_antisymm)
40	def dvd_antisymm(+x: Nat, +y: Nat, +kx: Nat, +ky: Nat, +ex: {x == Nat.mul(kx, y) : Nat}, +ey: {y == Nat.mul(ky, x) : Nat}) -> {x == y : Nat}:
41	  match x:
42	    case 0n:
43	      Equal.sym(Nat, y, 0n, Equal.trans(Nat, y, Nat.mul(ky, 0n), 0n, ey, A.mul_zero(ky)))
44	    case 1n+ +xp:
45	      +e1 = Equal.trans(Nat, Nat.mul(Nat.mul(kx, ky), 1n+xp), Nat.mul(kx, Nat.mul(ky, 1n+xp)), Nat.mul(1n, 1n+xp),
46	        A.mul_assoc(kx, ky, 1n+xp),
47	        Equal.trans(Nat, Nat.mul(kx, Nat.mul(ky, 1n+xp)), Nat.mul(kx, y), Nat.mul(1n, 1n+xp),
48	          Equal.cong(Nat, Nat, z => Nat.mul(kx, z), Nat.mul(ky, 1n+xp), y, Equal.sym(Nat, y, Nat.mul(ky, 1n+xp), ey)),
49	          Equal.trans(Nat, Nat.mul(kx, y), 1n+xp, Nat.mul(1n, 1n+xp), Equal.sym(Nat, 1n+xp, Nat.mul(kx, y), ex), Equal.sym(Nat, Nat.mul(1n, 1n+xp), 1n+xp, one_mul(1n+xp)))))
50	      +k1 = mul_eq_one(kx, ky, R.mul_cancel(Nat.mul(kx, ky), 1n, xp, e1))
51	      Equal.trans(Nat, 1n+xp, Nat.mul(kx, y), y, ex, Equal.trans(Nat, Nat.mul(kx, y), Nat.mul(1n, y), y, Equal.cong(Nat, Nat, z => Nat.mul(z, y), kx, 1n, k1), one_mul(y)))
52	
53	# c (w g) == w (c g)
54	def swap_cw(+c: Nat, +w: Nat, +g: Nat) -> {Nat.mul(c, Nat.mul(w, g)) == Nat.mul(w, Nat.mul(c, g)) : Nat}:
55	  Equal.trans(Nat, Nat.mul(c, Nat.mul(w, g)), Nat.mul(Nat.mul(c, w), g), Nat.mul(w, Nat.mul(c, g)),
56	    Equal.sym(Nat, Nat.mul(Nat.mul(c, w), g), Nat.mul(c, Nat.mul(w, g)), A.mul_assoc(c, w, g)),
57	    Equal.trans(Nat, Nat.mul(Nat.mul(c, w), g), Nat.mul(Nat.mul(w, c), g), Nat.mul(w, Nat.mul(c, g)),
58	      Equal.cong(Nat, Nat, z => Nat.mul(z, g), Nat.mul(c, w), Nat.mul(w, c), A.mul_comm(c, w)),
59	      A.mul_assoc(w, c, g)))
60	
61	# x == w g gives c x == w (c g)
62	def scale_dvd(+c: Nat, +x: Nat, +w: Nat, +g: Nat, +e: {x == Nat.mul(w, g) : Nat}) -> {Nat.mul(c, x) == Nat.mul(w, Nat.mul(c, g)) : Nat}:
63	  Equal.trans(Nat, Nat.mul(c, x), Nat.mul(c, Nat.mul(w, g)), Nat.mul(w, Nat.mul(c, g)), Equal.cong(Nat, Nat, z => Nat.mul(c, z), x, Nat.mul(w, g), e), swap_cw(c, w, g))
64	
65	# c x == w (h c) gives x == w h (c > 0)
66	def unscale(+cp: Nat, +x: Nat, +w: Nat, +h: Nat, +e: {Nat.mul(1n+cp, x) == Nat.mul(w, Nat.mul(h, 1n+cp)) : Nat}) -> {x == Nat.mul(w, h) : Nat}:
67	  R.mul_cancel(x, Nat.mul(w, h), cp, Equal.trans(Nat, Nat.mul(x, 1n+cp), Nat.mul(1n+cp, x), Nat.mul(Nat.mul(w, h), 1n+cp), A.mul_comm(x, 1n+cp), Equal.trans(Nat, Nat.mul(1n+cp, x), Nat.mul(w, Nat.mul(h, 1n+cp)), Nat.mul(Nat.mul(w, h), 1n+cp), e, Equal.sym(Nat, Nat.mul(Nat.mul(w, h), 1n+cp), Nat.mul(w, Nat.mul(h, 1n+cp)), A.mul_assoc(w, h, 1n+cp)))))
68	
69	def gcd_mul_pos(+cp: Nat, +a: Nat, +b: Nat) -> {M.gcd(Nat.mul(1n+cp, a), Nat.mul(1n+cp, b)) == Nat.mul(1n+cp, M.gcd(a, b)) : Nat}:
70	  +c = {1n+cp : Nat}
71	  +ca = Nat.mul(c, a)
72	  +cb = Nat.mul(c, b)
73	  +g = M.gcd(a, b)
74	  +gc = M.gcd(ca, cb)
75	  +la = G.wl(G.ws(b, a, b))
76	  +lb = G.wr(G.ws(b, a, b))
77	  # c g divides gc
78	  +eu = G.dvd_gcd(ca, cb, Nat.mul(c, g), la, lb, scale_dvd(c, a, la, g, G.gcd_dvd_left(a, b)), scale_dvd(c, b, lb, g, G.gcd_dvd_right(a, b)))
79	  # c divides gc: gc == h c
80	  +eh = G.dvd_gcd(ca, cb, c, a, b, A.mul_comm(c, a), A.mul_comm(c, b))
81	  +h = G.dw(cb, ca, cb, a, b)
82	  # gc == h c divides c a and c b, so h divides a and b
83	  +ma = G.wl(G.ws(cb, ca, cb))
84	  +mb = G.wr(G.ws(cb, ca, cb))
85	  +ea2 = unscale(cp, a, ma, h, Equal.trans(Nat, ca, Nat.mul(ma, gc), Nat.mul(ma, Nat.mul(h, c)), G.gcd_dvd_left(ca, cb), Equal.cong(Nat, Nat, z => Nat.mul(ma, z), gc, Nat.mul(h, c), eh)))
86	  +eb2 = unscale(cp, b, mb, h, Equal.trans(Nat, cb, Nat.mul(mb, gc), Nat.mul(mb, Nat.mul(h, c)), G.gcd_dvd_right(ca, cb), Equal.cong(Nat, Nat, z => Nat.mul(mb, z), gc, Nat.mul(h, c), eh)))
87	  # so h divides g: g == v h, and c g == v (h c) == v gc
88	  +ev = G.dvd_gcd(a, b, h, ma, mb, ea2, eb2)
89	  +v = G.dw(b, a, b, ma, mb)
90	  +ecg = Equal.trans(Nat, Nat.mul(c, g), Nat.mul(v, Nat.mul(c, h)), Nat.mul(v, gc), scale_dvd(c, g, v, h, ev),
91	    Equal.cong(Nat, Nat, z => Nat.mul(v, z), Nat.mul(c, h), gc, Equal.trans(Nat, Nat.mul(c, h), Nat.mul(h, c), gc, A.mul_comm(c, h), Equal.sym(Nat, gc, Nat.mul(h, c), eh))))
92	  dvd_antisymm(gc, Nat.mul(c, g), G.dw(cb, ca, cb, la, lb), v, eu, ecg)
93	
94	# gcd(c a, c b) == c gcd(a, b)   (Mathlib Nat.gcd_mul_left)
95	def gcd_mul_left(+c: Nat, +a: Nat, +b: Nat) -> {M.gcd(Nat.mul(c, a), Nat.mul(c, b)) == Nat.mul(c, M.gcd(a, b)) : Nat}:
96	  match c:
97	    case 0n:
98	      {==}
99	    case 1n+ +cp:
100	      gcd_mul_pos(cp, a, b)
101	
102	# ---- lcm of positive a, b is (a / g) b ----
103	
104	# a == la g with a > 0 makes g positive
105	def gcd_pos(+ap: Nat, +l: Nat, +g: Nat, +e: {1n+ap == Nat.mul(l, g) : Nat}) -> {Nat.is_lt(0n, g) == True{} : Bool}:
106	  match g:
107	    case 0n:
108	      Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, N.succ_zero(ap, Equal.trans(Nat, 1n+ap, Nat.mul(l, 0n), 0n, e, A.mul_zero(l))))
109	    case 1n+gp:
110	      {==}
111	
112	def div_exact(+x: Nat, +l: Nat, +g: Nat, +hg: {Nat.is_lt(0n, g) == True{} : Bool}, +e: {x == Nat.mul(l, g) : Nat}) -> {Nat.div(x, g) == l : Nat}:
113	  match g:
114	    case 0n:
115	      Empty.absurd({Nat.div(x, 0n) == l : Nat}, L.false_true(hg))
116	    case 1n+ +gp:
117	      %Equal.sym(Nat, x, Nat.add(Nat.mul(l, 1n+gp), 0n), Equal.trans(Nat, x, Nat.mul(l, 1n+gp), Nat.add(Nat.mul(l, 1n+gp), 0n), e, Equal.sym(Nat, Nat.add(Nat.mul(l, 1n+gp), 0n), Nat.mul(l, 1n+gp), A.add_zero(Nat.mul(l, 1n+gp))))) : {Nat.div(_, 1n+gp) == l : Nat}
118	      R.div_of(l, gp, 0n, {==})
119	
120	def lcm_pos(+ap: Nat, +bp: Nat) -> {M.lcm(1n+ap, 1n+bp) == Nat.mul(G.wl(G.ws(1n+bp, 1n+ap, 1n+bp)), 1n+bp) : Nat}:
121	  +g = M.gcd(1n+ap, 1n+bp)
122	  +la = G.wl(G.ws(1n+bp, 1n+ap, 1n+bp))
123	  +ea = G.gcd_dvd_left(1n+ap, 1n+bp)
124	  Equal.cong(Nat, Nat, z => Nat.mul(z, 1n+bp), Nat.div(1n+ap, g), la, div_exact(1n+ap, la, g, gcd_pos(ap, la, g, ea), ea))
125	
126	# lcm(a, b) == kl a and lcm(a, b) == kr b   (Mathlib Nat.dvd_lcm_left/right)
127	def lcm_wl(+a: Nat, +b: Nat) -> Nat:
128	  match a b:
129	    case 0n _:
130	      0n
131	    case 1n+ap 0n:
132	      0n
133	    case 1n+ +ap 1n+ +bp:
134	      G.wr(G.ws(1n+bp, 1n+ap, 1n+bp))
135	
136	def lcm_wr(+a: Nat, +b: Nat) -> Nat:
137	  match a b:
138	    case 0n _:
139	      0n
140	    case 1n+ap 0n:
141	      0n
142	    case 1n+ +ap 1n+ +bp:
143	      G.wl(G.ws(1n+bp, 1n+ap, 1n+bp))
144	
145	def dvd_lcm_left(+a: Nat, +b: Nat) -> {M.lcm(a, b) == Nat.mul(lcm_wl(a, b), a) : Nat}:
146	  match a b:
147	    case 0n b0:
148	      {==}
149	    case 1n+ ap 0n:
150	      {==}
151	    case 1n+ +ap 1n+ +bp:
152	      +g = M.gcd(1n+ap, 1n+bp)
153	      +la = G.wl(G.ws(1n+bp, 1n+ap, 1n+bp))
154	      +lb = G.wr(G.ws(1n+bp, 1n+ap, 1n+bp))
155	      %Equal.sym(Nat, M.lcm(1n+ap, 1n+bp), Nat.mul(la, 1n+bp), lcm_pos(ap, bp)) : {_ == Nat.mul(lb, 1n+ap) : Nat}
156	      %Equal.sym(Nat, 1n+bp, Nat.mul(lb, g), G.gcd_dvd_right(1n+ap, 1n+bp)) : {Nat.mul(la, _) == Nat.mul(lb, 1n+ap) : Nat}
157	      %Equal.sym(Nat, 1n+ap, Nat.mul(la, g), G.gcd_dvd_left(1n+ap, 1n+bp)) : {Nat.mul(la, Nat.mul(lb, g)) == Nat.mul(lb, _) : Nat}
158	      swap_cw(la, lb, g)
159	
160	def dvd_lcm_right(+a: Nat, +b: Nat) -> {M.lcm(a, b) == Nat.mul(lcm_wr(a, b), b) : Nat}:
161	  match a b:
162	    case 0n b0:
163	      Equal.sym(Nat, Nat.mul(0n, b0), 0n, {==})
164	    case 1n+ ap 0n:
165	      Equal.sym(Nat, Nat.mul(0n, 0n), 0n, {==})
166	    case 1n+ +ap 1n+ +bp:
167	      lcm_pos(ap, bp)
168	
169	# gcd(a, b) lcm(a, b) == a b   (Mathlib Nat.gcd_mul_lcm)
170	def gcd_mul_lcm(+a: Nat, +b: Nat) -> {Nat.mul(M.gcd(a, b), M.lcm(a, b)) == Nat.mul(a, b) : Nat}:
171	  match a b:
172	    case 0n b0:
173	      A.mul_zero(M.gcd(0n, b0))
174	    case 1n+ +ap 0n:
175	      Equal.trans(Nat, Nat.mul(M.gcd(1n+ap, 0n), 0n), 0n, Nat.mul(1n+ap, 0n), A.mul_zero(M.gcd(1n+ap, 0n)), Equal.sym(Nat, Nat.mul(1n+ap, 0n), 0n, A.mul_zero(1n+ap)))
176	    case 1n+ +ap 1n+ +bp:
177	      +g = M.gcd(1n+ap, 1n+bp)
178	      +la = G.wl(G.ws(1n+bp, 1n+ap, 1n+bp))
179	      %Equal.sym(Nat, M.lcm(1n+ap, 1n+bp), Nat.mul(la, 1n+bp), lcm_pos(ap, bp)) : {Nat.mul(g, _) == Nat.mul(1n+ap, 1n+bp) : Nat}
180	      %Equal.sym(Nat, Nat.mul(g, Nat.mul(la, 1n+bp)), Nat.mul(Nat.mul(g, la), 1n+bp), Equal.sym(Nat, Nat.mul(Nat.mul(g, la), 1n+bp), Nat.mul(g, Nat.mul(la, 1n+bp)), A.mul_assoc(g, la, 1n+bp))) : {_ == Nat.mul(1n+ap, 1n+bp) : Nat}
181	      %Equal.sym(Nat, Nat.mul(g, la), Nat.mul(la, g), A.mul_comm(g, la)) : {Nat.mul(_, 1n+bp) == Nat.mul(1n+ap, 1n+bp) : Nat}
182	      Equal.cong(Nat, Nat, z => Nat.mul(z, 1n+bp), Nat.mul(la, g), 1n+ap, Equal.sym(Nat, 1n+ap, Nat.mul(la, g), G.gcd_dvd_left(1n+ap, 1n+bp)))
183	
184	def cancel_pos(+x: Nat, +y: Nat, +g: Nat, +hg: {Nat.is_lt(0n, g) == True{} : Bool}, +e: {Nat.mul(x, g) == Nat.mul(y, g) : Nat}) -> {x == y : Nat}:
185	  match g:
186	    case 0n:
187	      Empty.absurd({x == y : Nat}, L.false_true(hg))
188	    case 1n+ +gp:
189	      R.mul_cancel(x, y, gp, e)
190	
191	# the quotient m / lcm(a, b) for a common multiple m == x a == y b
192	def lcm_dw(+a: Nat, +b: Nat, +m: Nat, +x: Nat, +y: Nat) -> Nat:
193	  match a b:
194	    case 0n _:
195	      0n
196	    case 1n+ap 0n:
197	      0n
198	    case 1n+ +ap 1n+ +bp:
199	      G.dw(Nat.mul(m, 1n+bp), Nat.mul(m, 1n+ap), Nat.mul(m, 1n+bp), y, x)
200	
201	def lcm_dvd_pos(+ap: Nat, +bp: Nat, +m: Nat, +x: Nat, +y: Nat, +ex: {m == Nat.mul(x, 1n+ap) : Nat}, +ey: {m == Nat.mul(y, 1n+bp) : Nat}) -> {m == Nat.mul(lcm_dw(1n+ap, 1n+bp, m, x, y), M.lcm(1n+ap, 1n+bp)) : Nat}:
202	  +a = {1n+ap : Nat}
203	  +b = {1n+bp : Nat}
204	  +g = M.gcd(a, b)
205	  +l = M.lcm(a, b)
206	  +ab = Nat.mul(a, b)
207	  +t = lcm_dw(a, b, m, x, y)
208	  +la = G.wl(G.ws(b, a, b))
209	  +ea = Equal.trans(Nat, Nat.mul(m, a), Nat.mul(Nat.mul(y, b), a), Nat.mul(y, ab), Equal.cong(Nat, Nat, z => Nat.mul(z, a), m, Nat.mul(y, b), ey),
210	    Equal.trans(Nat, Nat.mul(Nat.mul(y, b), a), Nat.mul(y, Nat.mul(b, a)), Nat.mul(y, ab), A.mul_assoc(y, b, a), Equal.cong(Nat, Nat, z => Nat.mul(y, z), Nat.mul(b, a), ab, A.mul_comm(b, a))))
211	  +eb = Equal.trans(Nat, Nat.mul(m, b), Nat.mul(Nat.mul(x, a), b), Nat.mul(x, ab), Equal.cong(Nat, Nat, z => Nat.mul(z, b), m, Nat.mul(x, a), ex), A.mul_assoc(x, a, b))
212	  +e2 = G.dvd_gcd(Nat.mul(m, a), Nat.mul(m, b), ab, y, x, ea, eb)
213	  +e1 = gcd_mul_left(m, a, b)
214	  +e3 = Equal.sym(Nat, Nat.mul(g, l), ab, gcd_mul_lcm(a, b))
215	  +emg = Equal.trans(Nat, Nat.mul(m, g), M.gcd(Nat.mul(m, a), Nat.mul(m, b)), Nat.mul(t, Nat.mul(g, l)), Equal.sym(Nat, M.gcd(Nat.mul(m, a), Nat.mul(m, b)), Nat.mul(m, g), e1),
216	    Equal.trans(Nat, M.gcd(Nat.mul(m, a), Nat.mul(m, b)), Nat.mul(t, ab), Nat.mul(t, Nat.mul(g, l)), e2, Equal.cong(Nat, Nat, z => Nat.mul(t, z), ab, Nat.mul(g, l), e3)))
217	  +emg2 = Equal.trans(Nat, Nat.mul(m, g), Nat.mul(t, Nat.mul(g, l)), Nat.mul(Nat.mul(t, l), g), emg,
218	    Equal.trans(Nat, Nat.mul(t, Nat.mul(g, l)), Nat.mul(t, Nat.mul(l, g)), Nat.mul(Nat.mul(t, l), g), Equal.cong(Nat, Nat, z => Nat.mul(t, z), Nat.mul(g, l), Nat.mul(l, g), A.mul_comm(g, l)), Equal.sym(Nat, Nat.mul(Nat.mul(t, l), g), Nat.mul(t, Nat.mul(l, g)), A.mul_assoc(t, l, g))))
219	  cancel_pos(m, Nat.mul(t, l), g, gcd_pos(ap, la, g, G.gcd_dvd_left(a, b)), emg2)
220	
221	# every common multiple of a and b is a multiple of lcm(a, b)   (Mathlib Nat.lcm_dvd)
222	def lcm_dvd(+a: Nat, +b: Nat, +m: Nat, +x: Nat, +y: Nat, +ex: {m == Nat.mul(x, a) : Nat}, +ey: {m == Nat.mul(y, b) : Nat}) -> {m == Nat.mul(lcm_dw(a, b, m, x, y), M.lcm(a, b)) : Nat}:
223	  match a b:
224	    case 0n b0:
225	      Equal.trans(Nat, m, Nat.mul(x, 0n), 0n, ex, A.mul_zero(x))
226	    case 1n+ ap 0n:
227	      Equal.trans(Nat, m, Nat.mul(y, 0n), 0n, ey, A.mul_zero(y))
228	    case 1n+ +ap 1n+ +bp:
229	      lcm_dvd_pos(ap, bp, m, x, y, ex, ey)