1	import Base
2	import ../../lib/nat.bend as N
3	import ../../lib/lemmas/proofs/nat_algebra.bend as A
4	import ../../lib/lemmas/proofs/word_value.bend as WV
5	import ../../lib/lemmas/proofs/natural_division.bend as ND
6	
7	# Natural-number arithmetic the math proofs share: the division theorem,
8	# cancellation, and the order/division exchange. Statement shapes follow
9	# Lean 4 Mathlib (Nat.div_add_mod, Nat.mod_lt, Nat.le_div_iff_mul_le,
10	# Nat.eq_of_mul_eq_mul_right, Nat.mul_sub_right_distrib); the divisor is
11	# written 1+d so that it is positive.
12	
13	# ---- the division theorem ----
14	
15	def dm_e2(+bp: Nat, +v: Nat, g: WV.go_equation(bp, v, bp, 0n, 0n)) -> {v == Nat.add(Nat.mul(Nat.div(v, 1n+bp), 1n+bp), Nat.mod(v, 1n+bp)) : Nat}:
16	  (e, l) = g
17	  e
18	
19	def dm_l2(+bp: Nat, +v: Nat, g: WV.go_equation(bp, v, bp, 0n, 0n)) -> {Nat.is_lt(Nat.mod(v, 1n+bp), 1n+bp) == True{} : Bool}:
20	  (e, l) = g
21	  N.le_lt_succ(Nat.mod(v, 1n+bp), bp, l)
22	
23	# v == (v / n) n + v mod n   (Mathlib Nat.div_add_mod)
24	def dm_eq(+bp: Nat, +v: Nat) -> {v == Nat.add(Nat.mul(Nat.div(v, 1n+bp), 1n+bp), Nat.mod(v, 1n+bp)) : Nat}:
25	  dm_e2(bp, v, WV.go(bp, v, bp, 0n, 0n, N.add_zero(bp)))
26	
27	# v mod n < n   (Mathlib Nat.mod_lt)
28	def dm_lt(+bp: Nat, +v: Nat) -> {Nat.is_lt(Nat.mod(v, 1n+bp), 1n+bp) == True{} : Bool}:
29	  dm_l2(bp, v, WV.go(bp, v, bp, 0n, 0n, N.add_zero(bp)))
30	
31	# the quotient and remainder are unique
32	def div_of(+q: Nat, +bp: Nat, +r: Nat, +h: {Nat.is_lt(r, 1n+bp) == True{} : Bool}) -> {Nat.div(Nat.add(Nat.mul(q, 1n+bp), r), 1n+bp) == q : Nat}:
33	  ND.quotient(q, bp, r, N.lt_succ_le(r, bp, h))
34	
35	def mod_of(+q: Nat, +bp: Nat, +r: Nat, +h: {Nat.is_lt(r, 1n+bp) == True{} : Bool}) -> {Nat.mod(Nat.add(Nat.mul(q, 1n+bp), r), 1n+bp) == r : Nat}:
36	  ND.remainder(q, bp, r, N.lt_succ_le(r, bp, h))
37	
38	# ---- cancellation ----
39	
40	# c + a == c + b gives a == b   (Mathlib Nat.add_left_cancel)
41	def add_cancel(+c: Nat, +a: Nat, +b: Nat, +e: {Nat.add(c, a) == Nat.add(c, b) : Nat}) -> {a == b : Nat}:
42	  match c:
43	    case 0n:
44	      e
45	    case 1n+ +cp:
46	      add_cancel(cp, a, b, N.succ_inj(Nat.add(cp, a), Nat.add(cp, b), e))
47	
48	# x c == y c with c > 0 gives x == y   (Mathlib Nat.eq_of_mul_eq_mul_right)
49	def mul_cancel(+x: Nat, +y: Nat, +bp: Nat, +e: {Nat.mul(x, 1n+bp) == Nat.mul(y, 1n+bp) : Nat}) -> {x == y : Nat}:
50	  match x y:
51	    case 0n 0n:
52	      {==}
53	    case 0n 1n+yp:
54	      Empty.absurd({0n == 1n+yp : Nat}, N.zero_succ(Nat.add(bp, Nat.mul(yp, 1n+bp)), e))
55	    case 1n+xp 0n:
56	      Empty.absurd({1n+xp == 0n : Nat}, N.succ_zero(Nat.add(bp, Nat.mul(xp, 1n+bp)), e))
57	    case 1n+ +xp 1n+ +yp:
58	      N.succ_cong(xp, yp, mul_cancel(xp, yp, bp, add_cancel(1n+bp, Nat.mul(xp, 1n+bp), Nat.mul(yp, 1n+bp), e)))
59	
60	# ---- order and division ----
61	
62	# d + x <= d + y is x <= y
63	def le_add_cancel(+d: Nat, +x: Nat, +y: Nat) -> {Nat.is_le(Nat.add(d, x), Nat.add(d, y)) == Nat.is_le(x, y) : Bool}:
64	  match d:
65	    case 0n:
66	      {==}
67	    case 1n+ +dp:
68	      le_add_cancel(dp, x, y)
69	
70	def le_div_g(+x: Nat, +q: Nat, +bp: Nat, +r: Nat, +hr: {Nat.is_lt(r, 1n+bp) == True{} : Bool}) -> {Nat.is_le(x, q) == Nat.is_le(Nat.mul(x, 1n+bp), Nat.add(Nat.mul(q, 1n+bp), r)) : Bool}:
71	  match x q:
72	    case 0n q0:
73	      %Equal.sym(Bool, Nat.is_le(0n, q0), True{}, N.zero_le(q0)) : {_ == Nat.is_le(0n, Nat.add(Nat.mul(q0, 1n+bp), r)) : Bool}
74	      Equal.sym(Bool, Nat.is_le(0n, Nat.add(Nat.mul(q0, 1n+bp), r)), True{}, N.zero_le(Nat.add(Nat.mul(q0, 1n+bp), r)))
75	    case 1n+ +xp 0n:
76	      Equal.sym(Bool, Nat.is_le(Nat.add(1n+bp, Nat.mul(xp, 1n+bp)), r), False{}, N.lt_not_le(r, Nat.add(1n+bp, Nat.mul(xp, 1n+bp)), N.lt_le_trans(r, 1n+bp, Nat.add(1n+bp, Nat.mul(xp, 1n+bp)), hr, N.le_add_right(1n+bp, Nat.mul(xp, 1n+bp)))))
77	    case 1n+ +xp 1n+ +qp:
78	      %Equal.sym(Nat, Nat.add(Nat.add(1n+bp, Nat.mul(qp, 1n+bp)), r), Nat.add(1n+bp, Nat.add(Nat.mul(qp, 1n+bp), r)), A.add_assoc(1n+bp, Nat.mul(qp, 1n+bp), r)) : {Nat.is_le(xp, qp) == Nat.is_le(Nat.add(1n+bp, Nat.mul(xp, 1n+bp)), _) : Bool}
79	      %Equal.sym(Bool, Nat.is_le(Nat.add(1n+bp, Nat.mul(xp, 1n+bp)), Nat.add(1n+bp, Nat.add(Nat.mul(qp, 1n+bp), r))), Nat.is_le(Nat.mul(xp, 1n+bp), Nat.add(Nat.mul(qp, 1n+bp), r)), le_add_cancel(1n+bp, Nat.mul(xp, 1n+bp), Nat.add(Nat.mul(qp, 1n+bp), r))) : {Nat.is_le(xp, qp) == _ : Bool}
80	      le_div_g(xp, qp, bp, r, hr)
81	
82	# x <= n / d is x d <= n   (Mathlib Nat.le_div_iff_mul_le)
83	def le_div(+bp: Nat, +x: Nat, +n: Nat) -> {Nat.is_le(x, Nat.div(n, 1n+bp)) == Nat.is_le(Nat.mul(x, 1n+bp), n) : Bool}:
84	  +e = dm_eq(bp, n)
85	  %Equal.sym(Nat, n, Nat.add(Nat.mul(Nat.div(n, 1n+bp), 1n+bp), Nat.mod(n, 1n+bp)), e) : {Nat.is_le(x, Nat.div(n, 1n+bp)) == Nat.is_le(Nat.mul(x, 1n+bp), _) : Bool}
86	  le_div_g(x, Nat.div(n, 1n+bp), bp, Nat.mod(n, 1n+bp), dm_lt(bp, n))
87	
88	# ---- subtraction ----
89	
90	def zsub(+b: Nat) -> {Nat.sub(0n, b) == 0n : Nat}:
91	  match b:
92	    case 0n:
93	      {==}
94	    case 1n+p:
95	      {==}
96	
97	def sub_cancel_l(+c: Nat, +a: Nat, +b: Nat) -> {Nat.sub(Nat.add(c, a), Nat.add(c, b)) == Nat.sub(a, b) : Nat}:
98	  match c:
99	    case 0n:
100	      {==}
101	    case 1n+ +cp:
102	      sub_cancel_l(cp, a, b)
103	
104	# (x - y) c == x c - y c   (Mathlib Nat.mul_sub_right_distrib)
105	def mul_sub(+x: Nat, +y: Nat, +c: Nat) -> {Nat.mul(Nat.sub(x, y), c) == Nat.sub(Nat.mul(x, c), Nat.mul(y, c)) : Nat}:
106	  match x y:
107	    case 0n 0n:
108	      {==}
109	    case 0n 1n+ +yp:
110	      Equal.sym(Nat, Nat.sub(0n, Nat.add(c, Nat.mul(yp, c))), 0n, zsub(Nat.add(c, Nat.mul(yp, c))))
111	    case 1n+ +xp 0n:
112	      Equal.sym(Nat, Nat.sub(Nat.add(c, Nat.mul(xp, c)), 0n), Nat.add(c, Nat.mul(xp, c)), N.sub_zero(Nat.add(c, Nat.mul(xp, c))))
113	    case 1n+ +xp 1n+ +yp:
114	      %Equal.sym(Nat, Nat.sub(Nat.add(c, Nat.mul(xp, c)), Nat.add(c, Nat.mul(yp, c))), Nat.sub(Nat.mul(xp, c), Nat.mul(yp, c)), sub_cancel_l(c, Nat.mul(xp, c), Nat.mul(yp, c))) : {Nat.mul(Nat.sub(xp, yp), c) == _ : Nat}
115	      mul_sub(xp, yp, c)
116	
117	# ---- congruences mod n = 1+bp ----
118	
119	# (q n + r) mod n == r mod n   (Mathlib Nat.mul_add_mod)
120	def absorb(+bp: Nat, +q: Nat, +r: Nat) -> {Nat.mod(Nat.add(Nat.mul(q, 1n+bp), r), 1n+bp) == Nat.mod(r, 1n+bp) : Nat}:
121	  +n = {1n+bp : Nat}
122	  +qr = Nat.div(r, n)
123	  +m = Nat.mod(r, n)
124	  +e = Equal.trans(Nat, Nat.add(Nat.mul(q, n), r), Nat.add(Nat.mul(q, n), Nat.add(Nat.mul(qr, n), m)), Nat.add(Nat.mul(Nat.add(q, qr), n), m),
125	    Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(q, n), z), r, Nat.add(Nat.mul(qr, n), m), dm_eq(bp, r)),
126	    Equal.trans(Nat, Nat.add(Nat.mul(q, n), Nat.add(Nat.mul(qr, n), m)), Nat.add(Nat.add(Nat.mul(q, n), Nat.mul(qr, n)), m), Nat.add(Nat.mul(Nat.add(q, qr), n), m),
127	      Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(q, n), Nat.mul(qr, n)), m), Nat.add(Nat.mul(q, n), Nat.add(Nat.mul(qr, n), m)), A.add_assoc(Nat.mul(q, n), Nat.mul(qr, n), m)),
128	      Equal.cong(Nat, Nat, z => Nat.add(z, m), Nat.add(Nat.mul(q, n), Nat.mul(qr, n)), Nat.mul(Nat.add(q, qr), n), Equal.sym(Nat, Nat.mul(Nat.add(q, qr), n), Nat.add(Nat.mul(q, n), Nat.mul(qr, n)), A.mul_add_right(q, qr, n)))))
129	  Equal.trans(Nat, Nat.mod(Nat.add(Nat.mul(q, n), r), n), Nat.mod(Nat.add(Nat.mul(Nat.add(q, qr), n), m), n), m, Equal.cong(Nat, Nat, z => Nat.mod(z, n), Nat.add(Nat.mul(q, n), r), Nat.add(Nat.mul(Nat.add(q, qr), n), m), e), mod_of(Nat.add(q, qr), bp, m, dm_lt(bp, r)))
130	
131	# (x mod n) mod n == x mod n   (Mathlib Nat.mod_mod)
132	def mod_mod(+bp: Nat, +x: Nat) -> {Nat.mod(Nat.mod(x, 1n+bp), 1n+bp) == Nat.mod(x, 1n+bp) : Nat}:
133	  mod_of(0n, bp, Nat.mod(x, 1n+bp), dm_lt(bp, x))
134	
135	# (x + y mod n) mod n == (x + y) mod n   (Mathlib Nat.add_mod)
136	def mod_add_r(+bp: Nat, +x: Nat, +y: Nat) -> {Nat.mod(Nat.add(x, Nat.mod(y, 1n+bp)), 1n+bp) == Nat.mod(Nat.add(x, y), 1n+bp) : Nat}:
137	  +n = {1n+bp : Nat}
138	  +qy = Nat.div(y, n)
139	  +my = Nat.mod(y, n)
140	  +e = Equal.trans(Nat, Nat.add(x, y), Nat.add(x, Nat.add(Nat.mul(qy, n), my)), Nat.add(Nat.mul(qy, n), Nat.add(x, my)),
141	    Equal.cong(Nat, Nat, z => Nat.add(x, z), y, Nat.add(Nat.mul(qy, n), my), dm_eq(bp, y)),
142	    A.add_swap(x, Nat.mul(qy, n), my))
143	  Equal.sym(Nat, Nat.mod(Nat.add(x, y), n), Nat.mod(Nat.add(x, my), n), Equal.trans(Nat, Nat.mod(Nat.add(x, y), n), Nat.mod(Nat.add(Nat.mul(qy, n), Nat.add(x, my)), n), Nat.mod(Nat.add(x, my), n), Equal.cong(Nat, Nat, z => Nat.mod(z, n), Nat.add(x, y), Nat.add(Nat.mul(qy, n), Nat.add(x, my)), e), absorb(bp, qy, Nat.add(x, my))))
144	
145	def mod_add_l(+bp: Nat, +x: Nat, +y: Nat) -> {Nat.mod(Nat.add(Nat.mod(x, 1n+bp), y), 1n+bp) == Nat.mod(Nat.add(x, y), 1n+bp) : Nat}:
146	  %Equal.sym(Nat, Nat.add(Nat.mod(x, 1n+bp), y), Nat.add(y, Nat.mod(x, 1n+bp)), A.add_comm(Nat.mod(x, 1n+bp), y)) : {Nat.mod(_, 1n+bp) == Nat.mod(Nat.add(x, y), 1n+bp) : Nat}
147	  %Equal.sym(Nat, Nat.add(x, y), Nat.add(y, x), A.add_comm(x, y)) : {Nat.mod(Nat.add(y, Nat.mod(x, 1n+bp)), 1n+bp) == Nat.mod(_, 1n+bp) : Nat}
148	  mod_add_r(bp, y, x)
149	
150	# (x (y mod n)) mod n == (x y) mod n   (Mathlib Nat.mul_mod)
151	def mod_mul_r(+bp: Nat, +x: Nat, +y: Nat) -> {Nat.mod(Nat.mul(x, Nat.mod(y, 1n+bp)), 1n+bp) == Nat.mod(Nat.mul(x, y), 1n+bp) : Nat}:
152	  +n = {1n+bp : Nat}
153	  +qy = Nat.div(y, n)
154	  +my = Nat.mod(y, n)
155	  +e = Equal.trans(Nat, Nat.mul(x, y), Nat.mul(x, Nat.add(Nat.mul(qy, n), my)), Nat.add(Nat.mul(Nat.mul(x, qy), n), Nat.mul(x, my)),
156	    Equal.cong(Nat, Nat, z => Nat.mul(x, z), y, Nat.add(Nat.mul(qy, n), my), dm_eq(bp, y)),
157	    Equal.trans(Nat, Nat.mul(x, Nat.add(Nat.mul(qy, n), my)), Nat.add(Nat.mul(x, Nat.mul(qy, n)), Nat.mul(x, my)), Nat.add(Nat.mul(Nat.mul(x, qy), n), Nat.mul(x, my)),
158	      A.mul_add_left(x, Nat.mul(qy, n), my),
159	      Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(x, my)), Nat.mul(x, Nat.mul(qy, n)), Nat.mul(Nat.mul(x, qy), n), Equal.sym(Nat, Nat.mul(Nat.mul(x, qy), n), Nat.mul(x, Nat.mul(qy, n)), A.mul_assoc(x, qy, n)))))
160	  Equal.sym(Nat, Nat.mod(Nat.mul(x, y), n), Nat.mod(Nat.mul(x, my), n), Equal.trans(Nat, Nat.mod(Nat.mul(x, y), n), Nat.mod(Nat.add(Nat.mul(Nat.mul(x, qy), n), Nat.mul(x, my)), n), Nat.mod(Nat.mul(x, my), n), Equal.cong(Nat, Nat, z => Nat.mod(z, n), Nat.mul(x, y), Nat.add(Nat.mul(Nat.mul(x, qy), n), Nat.mul(x, my)), e), absorb(bp, Nat.mul(x, qy), Nat.mul(x, my))))
161	
162	def mod_mul_l(+bp: Nat, +x: Nat, +y: Nat) -> {Nat.mod(Nat.mul(Nat.mod(x, 1n+bp), y), 1n+bp) == Nat.mod(Nat.mul(x, y), 1n+bp) : Nat}:
163	  %Equal.sym(Nat, Nat.mul(Nat.mod(x, 1n+bp), y), Nat.mul(y, Nat.mod(x, 1n+bp)), A.mul_comm(Nat.mod(x, 1n+bp), y)) : {Nat.mod(_, 1n+bp) == Nat.mod(Nat.mul(x, y), 1n+bp) : Nat}
164	  %Equal.sym(Nat, Nat.mul(x, y), Nat.mul(y, x), A.mul_comm(x, y)) : {Nat.mod(Nat.mul(y, Nat.mod(x, 1n+bp)), 1n+bp) == Nat.mod(_, 1n+bp) : Nat}
165	  mod_mul_r(bp, y, x)
166	
167	# ---- powers ----
168	
169	# a^(x + y) == a^x a^y   (Mathlib pow_add)
170	def pow_add(+a: Nat, +x: Nat, +y: Nat) -> {Nat.pow(a, Nat.add(x, y)) == Nat.mul(Nat.pow(a, x), Nat.pow(a, y)) : Nat}:
171	  match x:
172	    case 0n:
173	      Equal.sym(Nat, Nat.add(Nat.pow(a, y), 0n), Nat.pow(a, y), A.add_zero(Nat.pow(a, y)))
174	    case 1n+ +xp:
175	      %Equal.sym(Nat, Nat.pow(a, Nat.add(xp, y)), Nat.mul(Nat.pow(a, xp), Nat.pow(a, y)), pow_add(a, xp, y)) : {Nat.mul(a, _) == Nat.mul(Nat.mul(a, Nat.pow(a, xp)), Nat.pow(a, y)) : Nat}
176	      Equal.sym(Nat, Nat.mul(Nat.mul(a, Nat.pow(a, xp)), Nat.pow(a, y)), Nat.mul(a, Nat.mul(Nat.pow(a, xp), Nat.pow(a, y))), A.mul_assoc(a, Nat.pow(a, xp), Nat.pow(a, y)))
177	
178	# (a b)(c d) == (a c)(b d)
179	def mul_swap4(+a: Nat, +b: Nat, +c: Nat, +d: Nat) -> {Nat.mul(Nat.mul(a, b), Nat.mul(c, d)) == Nat.mul(Nat.mul(a, c), Nat.mul(b, d)) : Nat}:
180	  %Equal.sym(Nat, Nat.mul(Nat.mul(a, b), Nat.mul(c, d)), Nat.mul(a, Nat.mul(b, Nat.mul(c, d))), A.mul_assoc(a, b, Nat.mul(c, d))) : {_ == Nat.mul(Nat.mul(a, c), Nat.mul(b, d)) : Nat}
181	  %Equal.sym(Nat, Nat.mul(Nat.mul(a, c), Nat.mul(b, d)), Nat.mul(a, Nat.mul(c, Nat.mul(b, d))), A.mul_assoc(a, c, Nat.mul(b, d))) : {Nat.mul(a, Nat.mul(b, Nat.mul(c, d))) == _ : Nat}
182	  %Equal.sym(Nat, Nat.mul(b, Nat.mul(c, d)), Nat.mul(Nat.mul(b, c), d), Equal.sym(Nat, Nat.mul(Nat.mul(b, c), d), Nat.mul(b, Nat.mul(c, d)), A.mul_assoc(b, c, d))) : {Nat.mul(a, _) == Nat.mul(a, Nat.mul(c, Nat.mul(b, d))) : Nat}
183	  %Equal.sym(Nat, Nat.mul(c, Nat.mul(b, d)), Nat.mul(Nat.mul(c, b), d), Equal.sym(Nat, Nat.mul(Nat.mul(c, b), d), Nat.mul(c, Nat.mul(b, d)), A.mul_assoc(c, b, d))) : {Nat.mul(a, Nat.mul(Nat.mul(b, c), d)) == Nat.mul(a, _) : Nat}
184	  %Equal.sym(Nat, Nat.mul(b, c), Nat.mul(c, b), A.mul_comm(b, c)) : {Nat.mul(a, Nat.mul(_, d)) == Nat.mul(a, Nat.mul(Nat.mul(c, b), d)) : Nat}
185	  {==}
186	
187	# (x y)^k == x^k y^k   (Mathlib mul_pow)
188	def mul_pow(+x: Nat, +y: Nat, +k: Nat) -> {Nat.pow(Nat.mul(x, y), k) == Nat.mul(Nat.pow(x, k), Nat.pow(y, k)) : Nat}:
189	  match k:
190	    case 0n:
191	      {==}
192	    case 1n+ +kp:
193	      %Equal.sym(Nat, Nat.pow(Nat.mul(x, y), kp), Nat.mul(Nat.pow(x, kp), Nat.pow(y, kp)), mul_pow(x, y, kp)) : {Nat.mul(Nat.mul(x, y), _) == Nat.mul(Nat.mul(x, Nat.pow(x, kp)), Nat.mul(y, Nat.pow(y, kp))) : Nat}
194	      mul_swap4(x, y, Nat.pow(x, kp), Nat.pow(y, kp))