proofs/math/natural/lists.bend
bend-collections-laws-containers@1.0.0.0 · 186 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/logic.bend as L
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as A
5import bend-collections-laws-containers@1.0.0.0/src/math/natural.bend as M
6import bend-collections-laws-containers@1.0.0.0/proofs/math/natural/gcd.bend as G
7import bend-collections-laws-containers@1.0.0.0/proofs/math/natural/lcm.bend as LC
8import bend-collections-laws-containers@1.0.0.0/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
20def 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
27def sum_ok(+xs: List<&2, Nat>) -> {M.sum(xs) == S.lsum(xs) : Nat}:
28 sum_go(xs, 0n)
29
30def 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
37def 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
42def 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
46def 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]
50def 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
54def 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)
58def 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
65def 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)
73def 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
82def 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)
92def 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
96def 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
107def 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)
120def 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
125def 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
132def 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
139def 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
148def 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)
158def 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
161def 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
172def 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)
185def 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)