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 ./gcd.bend as G
7	import ./lcm.bend as LC
8	import ../../../spec/math/natural.bend as S
9	
10	# sum and prod are List.sum and List.prod (Lean 4 Mathlib
11	# Mathlib/Algebra/BigOperators/Group/List: List.sum_cons, List.prod_cons),
12	# and gcd_all / lcm_all are the gcd and lcm of a list: they divide / are
13	# divided by every element, and every common divisor / multiple divides /
14	# is divided by them (Mathlib Mathlib/Algebra/GCDMonoid/Finset:
15	# Finset.gcd_dvd, Finset.dvd_gcd, Finset.dvd_lcm, Finset.lcm_dvd). Python:
16	# math.gcd(*xs), math.lcm(*xs), math.prod, sum; gcd() == 0, lcm() == 1.
17	
18	# ---- sum and prod ----
19	
20	def sum_go(+xs: List<&2, Nat>, +acc: Nat) -> {M.sum_go(xs, acc) == Nat.add(acc, S.lsum(xs)) : Nat}:
21	  match xs:
22	    case Nil{}:
23	      Equal.sym(Nat, Nat.add(acc, 0n), acc, A.add_zero(acc))
24	    case Con{+x, +t}:
25	      Equal.trans(Nat, M.sum_go(t, Nat.add(acc, x)), Nat.add(Nat.add(acc, x), S.lsum(t)), Nat.add(acc, Nat.add(x, S.lsum(t))), sum_go(t, Nat.add(acc, x)), A.add_assoc(acc, x, S.lsum(t)))
26	
27	def sum_ok(+xs: List<&2, Nat>) -> {M.sum(xs) == S.lsum(xs) : Nat}:
28	  sum_go(xs, 0n)
29	
30	def prod_go(+xs: List<&2, Nat>, +acc: Nat) -> {M.prod_go(xs, acc) == Nat.mul(acc, S.lprod(xs)) : Nat}:
31	  match xs:
32	    case Nil{}:
33	      Equal.sym(Nat, Nat.mul(acc, 1n), acc, A.mul_one(acc))
34	    case Con{+x, +t}:
35	      Equal.trans(Nat, M.prod_go(t, Nat.mul(acc, x)), Nat.mul(Nat.mul(acc, x), S.lprod(t)), Nat.mul(acc, Nat.mul(x, S.lprod(t))), prod_go(t, Nat.mul(acc, x)), A.mul_assoc(acc, x, S.lprod(t)))
36	
37	def prod_ok(+xs: List<&2, Nat>) -> {M.prod(xs) == S.lprod(xs) : Nat}:
38	  Equal.trans(Nat, M.prod(xs), Nat.mul(1n, S.lprod(xs)), S.lprod(xs), prod_go(xs, 1n), LC.one_mul(S.lprod(xs)))
39	
40	# ---- gcd_all ----
41	
42	def nth0(+xs: List<&2, Nat>, +i: Nat, +d: Nat) -> Nat:
43	  S.nth0(xs, i, d)
44	
45	# d divides every element: xs[i] == ks[i] d
46	def dvd_with(+d: Nat, +xs: List<&2, Nat>, +ks: List<&2, Nat>) -> Type:
47	  S.dvd_with(d, xs, ks)
48	
49	# m is a multiple of every element: m == ks[i] xs[i]
50	def mul_with(+m: Nat, +xs: List<&2, Nat>, +ks: List<&2, Nat>) -> Type:
51	  S.mul_with(m, xs, ks)
52	
53	# (a == k1 b and b == k2 c) gives a == (k1 k2) c
54	def dvd_trans(+a: Nat, +b: Nat, +c: Nat, +k1: Nat, +k2: Nat, +e1: {a == Nat.mul(k1, b) : Nat}, +e2: {b == Nat.mul(k2, c) : Nat}) -> {a == Nat.mul(Nat.mul(k1, k2), c) : Nat}:
55	  Equal.trans(Nat, a, Nat.mul(k1, b), Nat.mul(Nat.mul(k1, k2), c), e1, Equal.trans(Nat, Nat.mul(k1, b), Nat.mul(k1, Nat.mul(k2, c)), Nat.mul(Nat.mul(k1, k2), c), Equal.cong(Nat, Nat, z => Nat.mul(k1, z), b, Nat.mul(k2, c), e2), Equal.sym(Nat, Nat.mul(Nat.mul(k1, k2), c), Nat.mul(k1, Nat.mul(k2, c)), A.mul_assoc(k1, k2, c))))
56	
57	# the quotient acc / gcd_all_go(xs, acc)
58	def gw_acc(+xs: List<&2, Nat>, +acc: Nat) -> Nat:
59	  match xs:
60	    case Nil{}:
61	      1n
62	    case Con{+x, +t}:
63	      Nat.mul(G.wl(G.ws(x, acc, x)), gw_acc(t, M.gcd(acc, x)))
64	
65	def g_acc(+xs: List<&2, Nat>, +acc: Nat) -> {acc == Nat.mul(gw_acc(xs, acc), M.gcd_all_go(xs, acc)) : Nat}:
66	  match xs:
67	    case Nil{}:
68	      Equal.sym(Nat, Nat.mul(1n, acc), acc, LC.one_mul(acc))
69	    case Con{+x, +t}:
70	      dvd_trans(acc, M.gcd(acc, x), M.gcd_all_go(t, M.gcd(acc, x)), G.wl(G.ws(x, acc, x)), gw_acc(t, M.gcd(acc, x)), G.gcd_dvd_left(acc, x), g_acc(t, M.gcd(acc, x)))
71	
72	# the quotient (xs[i]) / gcd_all_go(xs, acc)
73	def gw_nth(+xs: List<&2, Nat>, +acc: Nat, +i: Nat) -> Nat:
74	  match xs i:
75	    case Nil{} i0:
76	      0n
77	    case Con{+x, +t} 0n:
78	      Nat.mul(G.wr(G.ws(x, acc, x)), gw_acc(t, M.gcd(acc, x)))
79	    case Con{+x, +t} 1n+ +j:
80	      gw_nth(t, M.gcd(acc, x), j)
81	
82	def g_nth(+xs: List<&2, Nat>, +acc: Nat, +i: Nat) -> {nth0(xs, i, 0n) == Nat.mul(gw_nth(xs, acc, i), M.gcd_all_go(xs, acc)) : Nat}:
83	  match xs i:
84	    case Nil{} i0:
85	      {==}
86	    case Con{+x, +t} 0n:
87	      dvd_trans(x, M.gcd(acc, x), M.gcd_all_go(t, M.gcd(acc, x)), G.wr(G.ws(x, acc, x)), gw_acc(t, M.gcd(acc, x)), G.gcd_dvd_right(acc, x), g_acc(t, M.gcd(acc, x)))
88	    case Con{+x, +t} 1n+ +j:
89	      g_nth(t, M.gcd(acc, x), j)
90	
91	# gcd_all(xs) divides every element: xs[i] == k gcd_all(xs) (0 past the end)   (Mathlib Finset.gcd_dvd)
92	def gcd_all_dvd(+xs: List<&2, Nat>, +i: Nat) -> {nth0(xs, i, 0n) == Nat.mul(gw_nth(xs, 0n, i), M.gcd_all(xs)) : Nat}:
93	  g_nth(xs, 0n, i)
94	
95	# the quotient gcd_all_go(xs, acc) / d for a common divisor d
96	def gw_dvd(+xs: List<&2, Nat>, +ks: List<&2, Nat>, +acc: Nat, +ka: Nat) -> Nat:
97	  match xs ks:
98	    case Nil{} Nil{}:
99	      ka
100	    case Nil{} Con{k, kt}:
101	      ka
102	    case Con{x, t} Nil{}:
103	      0n
104	    case Con{+x, +t} Con{+k, +kt}:
105	      gw_dvd(t, kt, M.gcd(acc, x), G.dw(x, acc, x, ka, k))
106	
107	def g_dvd(+d: Nat, +xs: List<&2, Nat>, +ks: List<&2, Nat>, +acc: Nat, +ka: Nat, +ea: {acc == Nat.mul(ka, d) : Nat}, h: dvd_with(d, xs, ks)) -> {M.gcd_all_go(xs, acc) == Nat.mul(gw_dvd(xs, ks, acc, ka), d) : Nat}:
108	  match xs ks:
109	    case Nil{} Nil{}:
110	      ea
111	    case Nil{} Con{k, kt}:
112	      ea
113	    case Con{x, t} Nil{}:
114	      Empty.absurd({M.gcd_all_go(Con{x, t}, acc) == Nat.mul(gw_dvd(Con{x, t}, Nil{}, acc, ka), d) : Nat}, h)
115	    case Con{+x, +t} Con{+k, +kt}:
116	      (ex, ht) = h
117	      g_dvd(d, t, kt, M.gcd(acc, x), G.dw(x, acc, x, ka, k), G.dvd_gcd(acc, x, d, ka, k, ea, ex), ht)
118	
119	# every common divisor of the elements divides gcd_all(xs)   (Mathlib Finset.dvd_gcd)
120	def dvd_gcd_all(+d: Nat, +xs: List<&2, Nat>, +ks: List<&2, Nat>, h: dvd_with(d, xs, ks)) -> {M.gcd_all(xs) == Nat.mul(gw_dvd(xs, ks, 0n, 0n), d) : Nat}:
121	  g_dvd(d, xs, ks, 0n, 0n, {==}, h)
122	
123	# ---- lcm_all ----
124	
125	def lw_acc(+xs: List<&2, Nat>, +acc: Nat) -> Nat:
126	  match xs:
127	    case Nil{}:
128	      1n
129	    case Con{+x, +t}:
130	      Nat.mul(lw_acc(t, M.lcm(acc, x)), LC.lcm_wl(acc, x))
131	
132	def l_acc(+xs: List<&2, Nat>, +acc: Nat) -> {M.lcm_all_go(xs, acc) == Nat.mul(lw_acc(xs, acc), acc) : Nat}:
133	  match xs:
134	    case Nil{}:
135	      Equal.sym(Nat, Nat.mul(1n, acc), acc, LC.one_mul(acc))
136	    case Con{+x, +t}:
137	      dvd_trans(M.lcm_all_go(t, M.lcm(acc, x)), M.lcm(acc, x), acc, lw_acc(t, M.lcm(acc, x)), LC.lcm_wl(acc, x), l_acc(t, M.lcm(acc, x)), LC.dvd_lcm_left(acc, x))
138	
139	def lw_nth(+xs: List<&2, Nat>, +acc: Nat, +i: Nat) -> Nat:
140	  match xs i:
141	    case Nil{} i0:
142	      acc
143	    case Con{+x, +t} 0n:
144	      Nat.mul(lw_acc(t, M.lcm(acc, x)), LC.lcm_wr(acc, x))
145	    case Con{+x, +t} 1n+ +j:
146	      lw_nth(t, M.lcm(acc, x), j)
147	
148	def l_nth(+xs: List<&2, Nat>, +acc: Nat, +i: Nat) -> {M.lcm_all_go(xs, acc) == Nat.mul(lw_nth(xs, acc, i), nth0(xs, i, 1n)) : Nat}:
149	  match xs i:
150	    case Nil{} i0:
151	      Equal.sym(Nat, Nat.mul(acc, 1n), acc, A.mul_one(acc))
152	    case Con{+x, +t} 0n:
153	      dvd_trans(M.lcm_all_go(t, M.lcm(acc, x)), M.lcm(acc, x), x, lw_acc(t, M.lcm(acc, x)), LC.lcm_wr(acc, x), l_acc(t, M.lcm(acc, x)), LC.dvd_lcm_right(acc, x))
154	    case Con{+x, +t} 1n+ +j:
155	      l_nth(t, M.lcm(acc, x), j)
156	
157	# every element divides lcm_all(xs) (1 past the end)   (Mathlib Finset.dvd_lcm)
158	def dvd_lcm_all(+xs: List<&2, Nat>, +i: Nat) -> {M.lcm_all(xs) == Nat.mul(lw_nth(xs, 1n, i), nth0(xs, i, 1n)) : Nat}:
159	  l_nth(xs, 1n, i)
160	
161	def lw_mul(+m: Nat, +xs: List<&2, Nat>, +ks: List<&2, Nat>, +acc: Nat, +ka: Nat) -> Nat:
162	  match xs ks:
163	    case Nil{} Nil{}:
164	      ka
165	    case Nil{} Con{k, kt}:
166	      ka
167	    case Con{x, t} Nil{}:
168	      0n
169	    case Con{+x, +t} Con{+k, +kt}:
170	      lw_mul(m, t, kt, M.lcm(acc, x), LC.lcm_dw(acc, x, m, ka, k))
171	
172	def l_mul(+m: Nat, +xs: List<&2, Nat>, +ks: List<&2, Nat>, +acc: Nat, +ka: Nat, +ea: {m == Nat.mul(ka, acc) : Nat}, h: mul_with(m, xs, ks)) -> {m == Nat.mul(lw_mul(m, xs, ks, acc, ka), M.lcm_all_go(xs, acc)) : Nat}:
173	  match xs ks:
174	    case Nil{} Nil{}:
175	      ea
176	    case Nil{} Con{k, kt}:
177	      ea
178	    case Con{x, t} Nil{}:
179	      Empty.absurd({m == Nat.mul(lw_mul(m, Con{x, t}, Nil{}, acc, ka), M.lcm_all_go(Con{x, t}, acc)) : Nat}, h)
180	    case Con{+x, +t} Con{+k, +kt}:
181	      (ex, ht) = h
182	      l_mul(m, t, kt, M.lcm(acc, x), LC.lcm_dw(acc, x, m, ka, k), LC.lcm_dvd(acc, x, m, ka, k, ea, ex), ht)
183	
184	# lcm_all(xs) divides every common multiple of the elements   (Mathlib Finset.lcm_dvd)
185	def lcm_all_dvd(+m: Nat, +xs: List<&2, Nat>, +ks: List<&2, Nat>, h: mul_with(m, xs, ks)) -> {m == Nat.mul(lw_mul(m, xs, ks, 1n, m), M.lcm_all(xs)) : Nat}:
186	  l_mul(m, xs, ks, 1n, m, Equal.sym(Nat, Nat.mul(m, 1n), m, A.mul_one(m)), h)