proofs/math/natural/arith.bend
bend-collections-laws-containers@1.0.0.0 · 194 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as A
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/word_value.bend as WV
5import bend-collections-laws-containers@1.0.0.0/proofs/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
15def 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
19def 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)
24def 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)
28def 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
32def 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
35def 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)
41def 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)
49def 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
63def 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
70def 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)
83def 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
90def zsub(+b: Nat) -> {Nat.sub(0n, b) == 0n : Nat}:
91 match b:
92 case 0n:
93 {==}
94 case 1n+p:
95 {==}
96
97def 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)
105def 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)
120def 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)
132def 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)
136def 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
145def 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)
151def 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
162def 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)
170def 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)
179def 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)
188def 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))