proofs/math/natural/lists.bend

bend-collections-laws-math@1.0.0.0 · 186 lines · 24 definitions

1import Base
2import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
3import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
4import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as A
5import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
6import bend-collections-laws-math@1.0.0.0/proofs/math/natural/gcd.bend as G
7import bend-collections-laws-math@1.0.0.0/proofs/math/natural/lcm.bend as LC
8import bend-collections-laws-math@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)