proofs/math/typed/combnat.bend

bend-collections-laws-math@1.0.0.0 · 189 lines · 26 definitions

1import Base
2import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-math@1.0.0.0/spec/math/natural.bend as S
4import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
5import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
6import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
7import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
8import bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend as AR2
9import bend-collections-laws-math@1.0.0.0/proofs/math/natural/bits.bend as BT
10import bend-collections-laws-math@1.0.0.0/proofs/math/natural/fact.bend as FA
11import bend-collections-laws-math@1.0.0.0/proofs/math/natural/gcd.bend as GC
12import bend-collections-laws-math@1.0.0.0/proofs/math/natural/lcm.bend as LC
13import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natfuel.bend as NF
14
15# Binomial facts behind the generic comb loop (Lean 4 Mathlib
16# Mathlib/Data/Nat/Choose/Basic and Central: Nat.choose_le_succ_of_lt_half_left,
17# Nat.choose_le_choose, Nat.four_pow_le_two_mul_self_mul_centralBinom in its
18# weaker 2^n <= C(2n, n) form; Mathlib/Data/Nat/GCD/Basic:
19# Nat.Coprime.dvd_of_dvd_mul_left, Euclid's lemma, via Nat.gcd_mul_left).
20
21def true_ne_false(+h: {True{} == False{} : Bool}) -> Empty:
22  NF.true_ne_false(h)
23
24# ---- a c <= b c with c > 0 gives a <= b ----
25
26def le_cancel_c(+a: Nat, +b: Nat, +cp: Nat, +h: {Nat.is_le(Nat.mul(a, 1n+cp), Nat.mul(b, 1n+cp)) == True{} : Bool}, +d: Bool, +hd: {Nat.is_lt(b, a) == d : Bool}) -> {Nat.is_le(a, b) == True{} : Bool}:
27  match d:
28    case True{}:
29      +x = Nat.mul(b, 1n+cp)
30      +h1 = N.le_trans(Nat.add(1n+cp, x), Nat.mul(a, 1n+cp), x, AR2.mul_le(1n+b, a, 1n+cp, N.lt_succ_le_succ(b, a, hd)), h)
31      +h2 = L.subst(Nat, z => {Nat.is_le(z, x) == True{} : Bool}, Nat.add(1n+cp, x), Nat.add(x, 1n+cp), N.add_comm(1n+cp, x), h1)
32      Empty.absurd({Nat.is_le(a, b) == True{} : Bool}, true_ne_false(Equal.trans(Bool, True{}, Nat.is_le(Nat.add(x, 1n+cp), x), False{}, Equal.sym(Bool, Nat.is_le(Nat.add(x, 1n+cp), x), True{}, h2), BT.add_succ_nle(x, cp))))
33    case False{}:
34      N.not_lt_le(b, a, hd)
35
36def le_cancel(+a: Nat, +b: Nat, +cp: Nat, +h: {Nat.is_le(Nat.mul(a, 1n+cp), Nat.mul(b, 1n+cp)) == True{} : Bool}) -> {Nat.is_le(a, b) == True{} : Bool}:
37  le_cancel_c(a, b, cp, h, Nat.is_lt(b, a), {==})
38
39# ---- C(n, i) grows up to n / 2 ----
40
41# 1 + 2 i == i + (1 + i), so (1 + 2 i) - i == 1 + i
42def sub_half(+i: Nat) -> {Nat.sub(1n+Nat.double(i), i) == 1n+i : Nat}:
43  +e = Equal.trans(Nat, 1n+Nat.double(i), 1n+Nat.add(i, i), Nat.add(i, 1n+i), Equal.cong(Nat, Nat, t => 1n+t, Nat.double(i), Nat.add(i, i), NA.double_self(i)), Equal.sym(Nat, Nat.add(i, 1n+i), 1n+Nat.add(i, i), NA.add_succ(i, i)))
44  Equal.trans(Nat, Nat.sub(1n+Nat.double(i), i), Nat.sub(Nat.add(i, 1n+i), i), 1n+i, Equal.cong(Nat, Nat, t => Nat.sub(t, i), 1n+Nat.double(i), Nat.add(i, 1n+i), e), N.add_sub_cancel(i, 1n+i))
45
46# 1 + 2 i <= n gives C(n, i) <= C(n, 1 + i)
47def cstep(+n: Nat, +i: Nat, +h: {Nat.is_le(1n+Nat.double(i), n) == True{} : Bool}) -> {Nat.is_le(S.choose(n, i), S.choose(n, 1n+i)) == True{} : Bool}:
48  +c = S.choose(n, i)
49  +c1 = S.choose(n, 1n+i)
50  +hs = L.subst(Nat, z => {Nat.is_le(z, Nat.sub(n, i)) == True{} : Bool}, Nat.sub(1n+Nat.double(i), i), 1n+i, sub_half(i), NF.sub_mono_l(1n+Nat.double(i), n, i, h))
51  +h1 = NF.mul_le_r(c, 1n+i, Nat.sub(n, i), hs)
52  +h2 = L.subst(Nat, z => {Nat.is_le(Nat.mul(c, 1n+i), z) == True{} : Bool}, Nat.mul(c, Nat.sub(n, i)), Nat.mul(c1, 1n+i), Equal.sym(Nat, Nat.mul(c1, 1n+i), Nat.mul(c, Nat.sub(n, i)), FA.choose_succ_right(n, i)), h1)
53  le_cancel(c, c1, i, h2)
54
55# 2 (i + d) <= n gives C(n, i) <= C(n, i + d)
56def cmono_d(+n: Nat, +i: Nat, +d: Nat, +h: {Nat.is_le(Nat.double(Nat.add(i, d)), n) == True{} : Bool}) -> {Nat.is_le(S.choose(n, i), S.choose(n, Nat.add(i, d))) == True{} : Bool}:
57  match d:
58    case 0n:
59      L.subst(Nat, z => {Nat.is_le(S.choose(n, i), S.choose(n, z)) == True{} : Bool}, i, Nat.add(i, 0n), Equal.sym(Nat, Nat.add(i, 0n), i, N.add_zero(i)), N.le_refl(S.choose(n, i)))
60    case 1n+ +dp:
61      +s = Nat.add(i, dp)
62      +es = NA.add_succ(i, dp)
63      +h1 = L.subst(Nat, z => {Nat.is_le(Nat.double(z), n) == True{} : Bool}, Nat.add(i, 1n+dp), 1n+s, es, h)
64      +h2 = N.le_trans(1n+Nat.double(s), Nat.double(1n+s), n, N.le_trans(1n+Nat.double(s), 2n+Nat.double(s), Nat.double(1n+s), N.le_succ(1n+Nat.double(s)), L.subst(Nat, z => {Nat.is_le(2n+Nat.double(s), z) == True{} : Bool}, Nat.add(2n, Nat.double(s)), Nat.double(1n+s), Equal.sym(Nat, Nat.double(1n+s), Nat.add(2n, Nat.double(s)), N.double_succ(s)), N.le_refl(2n+Nat.double(s)))), h1)
65      +h3 = N.le_trans(Nat.double(s), 1n+Nat.double(s), n, N.le_succ(Nat.double(s)), h2)
66      +c = N.le_trans(S.choose(n, i), S.choose(n, s), S.choose(n, 1n+s), cmono_d(n, i, dp, h3), cstep(n, s, h2))
67      L.subst(Nat, z => {Nat.is_le(S.choose(n, i), S.choose(n, z)) == True{} : Bool}, 1n+s, Nat.add(i, 1n+dp), Equal.sym(Nat, Nat.add(i, 1n+dp), 1n+s, es), c)
68
69# i <= k, 2 k <= n give C(n, i) <= C(n, k)
70def cmono(+n: Nat, +i: Nat, +k: Nat, +hi: {Nat.is_le(i, k) == True{} : Bool}, +hk: {Nat.is_le(Nat.double(k), n) == True{} : Bool}) -> {Nat.is_le(S.choose(n, i), S.choose(n, k)) == True{} : Bool}:
71  +ek = N.sub_add(k, i, hi)
72  +h1 = L.subst(Nat, z => {Nat.is_le(Nat.double(z), n) == True{} : Bool}, k, Nat.add(i, Nat.sub(k, i)), Equal.sym(Nat, Nat.add(i, Nat.sub(k, i)), k, ek), hk)
73  L.subst(Nat, z => {Nat.is_le(S.choose(n, i), S.choose(n, z)) == True{} : Bool}, Nat.add(i, Nat.sub(k, i)), k, ek, cmono_d(n, i, Nat.sub(k, i), h1))
74
75# ---- C(m, j) grows with m, and 2^i <= C(2 i, i) ----
76
77def cn_mono(+m: Nat, +j: Nat) -> {Nat.is_le(S.choose(m, j), S.choose(1n+m, j)) == True{} : Bool}:
78  match m j:
79    case 0n 0n:
80      {==}
81    case 0n 1n+jp:
82      N.zero_le(S.choose(1n, 1n+jp))
83    case 1n+mp 0n:
84      {==}
85    case 1n+ +mp 1n+ +jp:
86      +a = S.choose(1n+mp, jp)
87      +b = S.choose(1n+mp, 1n+jp)
88      L.subst(Nat, z => {Nat.is_le(b, z) == True{} : Bool}, Nat.add(b, a), Nat.add(a, b), N.add_comm(b, a), N.le_add_right(b, a))
89
90def cn_mono_d(+m: Nat, +d: Nat, +j: Nat) -> {Nat.is_le(S.choose(m, j), S.choose(Nat.add(d, m), j)) == True{} : Bool}:
91  match d:
92    case 0n:
93      N.le_refl(S.choose(m, j))
94    case 1n+ +dp:
95      N.le_trans(S.choose(m, j), S.choose(Nat.add(dp, m), j), S.choose(1n+Nat.add(dp, m), j), cn_mono_d(m, dp, j), cn_mono(Nat.add(dp, m), j))
96
97def central(+i: Nat) -> {Nat.is_le(C.pow2(i), S.choose(Nat.double(i), i)) == True{} : Bool}:
98  match i:
99    case 0n:
100      {==}
101    case 1n+ +ip:
102      +m = {1n+Nat.double(ip) : Nat}
103      +y = S.choose(m, ip)
104      +hs = L.subst(Nat, z => {S.choose(m, z) == y : Nat}, Nat.sub(m, ip), 1n+ip, sub_half(ip), FA.choose_symm(m, ip, N.le_trans(ip, Nat.double(ip), m, N.double_self_le(ip), N.le_succ(Nat.double(ip)))))
105      +e2 = Equal.trans(Nat, Nat.add(y, S.choose(m, 1n+ip)), Nat.add(y, y), Nat.double(y), Equal.cong(Nat, Nat, t => Nat.add(y, t), S.choose(m, 1n+ip), y, hs), Equal.sym(Nat, Nat.double(y), Nat.add(y, y), NA.double_self(y)))
106      +h1 = N.double_le(C.pow2(ip), y, N.le_trans(C.pow2(ip), S.choose(Nat.double(ip), ip), y, central(ip), cn_mono(Nat.double(ip), ip)))
107      +h2 = L.subst(Nat, z => {Nat.is_le(Nat.double(C.pow2(ip)), z) == True{} : Bool}, Nat.double(y), Nat.add(y, S.choose(m, 1n+ip)), Equal.sym(Nat, Nat.add(y, S.choose(m, 1n+ip)), Nat.double(y), e2), h1)
108      L.subst(Nat, z => {Nat.is_le(Nat.double(C.pow2(ip)), S.choose(z, 1n+ip)) == True{} : Bool}, Nat.add(2n, Nat.double(ip)), Nat.double(1n+ip), Equal.sym(Nat, Nat.double(1n+ip), Nat.add(2n, Nat.double(ip)), N.double_succ(ip)), h2)
109
110# K <= i, 2 i <= n give 2^K <= C(n, i)
111def cbig(+K: Nat, +n: Nat, +i: Nat, +hK: {Nat.is_le(K, i) == True{} : Bool}, +h2: {Nat.is_le(Nat.double(i), n) == True{} : Bool}) -> {Nat.is_le(C.pow2(K), S.choose(n, i)) == True{} : Bool}:
112  +d = Nat.sub(n, Nat.double(i))
113  +en = Equal.trans(Nat, Nat.add(d, Nat.double(i)), Nat.add(Nat.double(i), d), n, N.add_comm(d, Nat.double(i)), N.sub_add(n, Nat.double(i), h2))
114  +h3 = L.subst(Nat, z => {Nat.is_le(S.choose(Nat.double(i), i), S.choose(z, i)) == True{} : Bool}, Nat.add(d, Nat.double(i)), n, en, cn_mono_d(Nat.double(i), d, i))
115  N.le_trans(C.pow2(K), C.pow2(i), S.choose(n, i), N.pow2_mono(K, i, hK), N.le_trans(C.pow2(i), S.choose(Nat.double(i), i), S.choose(n, i), central(i), h3))
116
117# ---- the gcd-reduced step is exact (Euclid's lemma) ----
118
119# g = gcd(c, j), c == wl g, j == wr g for j = 1 + jp
120def gg(+c: Nat, +jp: Nat) -> Nat:
121  M.gcd(c, 1n+jp)
122
123def wl(+c: Nat, +jp: Nat) -> Nat:
124  GC.wl(GC.ws(1n+jp, c, 1n+jp))
125
126def wr(+c: Nat, +jp: Nat) -> Nat:
127  GC.wr(GC.ws(1n+jp, c, 1n+jp))
128
129def e_c(+c: Nat, +jp: Nat) -> {c == Nat.mul(wl(c, jp), gg(c, jp)) : Nat}:
130  GC.gcd_dvd_left(c, 1n+jp)
131
132def e_j(+c: Nat, +jp: Nat) -> {1n+jp == Nat.mul(wr(c, jp), gg(c, jp)) : Nat}:
133  GC.gcd_dvd_right(c, 1n+jp)
134
135def g_pos(+c: Nat, +jp: Nat) -> {Nat.is_lt(0n, gg(c, jp)) == True{} : Bool}:
136  LC.gcd_pos(jp, wr(c, jp), gg(c, jp), e_j(c, jp))
137
138def wr_pos(+c: Nat, +jp: Nat) -> {Nat.is_lt(0n, wr(c, jp)) == True{} : Bool}:
139  LC.gcd_pos(jp, gg(c, jp), wr(c, jp), Equal.trans(Nat, 1n+jp, Nat.mul(wr(c, jp), gg(c, jp)), Nat.mul(gg(c, jp), wr(c, jp)), e_j(c, jp), NA.mul_comm(wr(c, jp), gg(c, jp))))
140
141def div_c(+c: Nat, +jp: Nat) -> {Nat.div(c, gg(c, jp)) == wl(c, jp) : Nat}:
142  LC.div_exact(c, wl(c, jp), gg(c, jp), g_pos(c, jp), e_c(c, jp))
143
144def div_j(+c: Nat, +jp: Nat) -> {Nat.div(1n+jp, gg(c, jp)) == wr(c, jp) : Nat}:
145  LC.div_exact(1n+jp, wr(c, jp), gg(c, jp), g_pos(c, jp), e_j(c, jp))
146
147# gcd(wl, wr) == 1
148def coprime(+c: Nat, +jp: Nat) -> {M.gcd(wl(c, jp), wr(c, jp)) == 1n : Nat}:
149  +g = gg(c, jp)
150  +a = wl(c, jp)
151  +b = wr(c, jp)
152  +ea = Equal.trans(Nat, Nat.mul(g, a), Nat.mul(a, g), c, NA.mul_comm(g, a), Equal.sym(Nat, c, Nat.mul(a, g), e_c(c, jp)))
153  +eb = Equal.trans(Nat, Nat.mul(g, b), Nat.mul(b, g), 1n+jp, NA.mul_comm(g, b), Equal.sym(Nat, 1n+jp, Nat.mul(b, g), e_j(c, jp)))
154  +e1 = Equal.trans(Nat, Nat.mul(g, M.gcd(a, b)), M.gcd(Nat.mul(g, a), Nat.mul(g, b)), g, Equal.sym(Nat, M.gcd(Nat.mul(g, a), Nat.mul(g, b)), Nat.mul(g, M.gcd(a, b)), LC.gcd_mul_left(g, a, b)), Equal.trans(Nat, M.gcd(Nat.mul(g, a), Nat.mul(g, b)), M.gcd(c, Nat.mul(g, b)), g, Equal.cong(Nat, Nat, t => M.gcd(t, Nat.mul(g, b)), Nat.mul(g, a), c, ea), Equal.cong(Nat, Nat, t => M.gcd(c, t), Nat.mul(g, b), 1n+jp, eb)))
155  +e2 = Equal.trans(Nat, Nat.mul(M.gcd(a, b), g), Nat.mul(g, M.gcd(a, b)), Nat.mul(1n, g), NA.mul_comm(M.gcd(a, b), g), Equal.trans(Nat, Nat.mul(g, M.gcd(a, b)), g, Nat.mul(1n, g), e1, Equal.sym(Nat, Nat.mul(1n, g), g, LC.one_mul(g))))
156  LC.cancel_pos(M.gcd(a, b), 1n, g, g_pos(c, jp), e2)
157
158# with c' (1 + jp) == c t: wl t == c' wr
159def cross(+c: Nat, +jp: Nat, +t: Nat, +c1: Nat, +e: {Nat.mul(c1, 1n+jp) == Nat.mul(c, t) : Nat}) -> {Nat.mul(wl(c, jp), t) == Nat.mul(c1, wr(c, jp)) : Nat}:
160  +g = gg(c, jp)
161  +a = wl(c, jp)
162  +b = wr(c, jp)
163  +l = Equal.trans(Nat, Nat.mul(Nat.mul(a, t), g), Nat.mul(a, Nat.mul(t, g)), Nat.mul(c, t), NA.mul_assoc(a, t, g), Equal.trans(Nat, Nat.mul(a, Nat.mul(t, g)), Nat.mul(a, Nat.mul(g, t)), Nat.mul(c, t), Equal.cong(Nat, Nat, z => Nat.mul(a, z), Nat.mul(t, g), Nat.mul(g, t), NA.mul_comm(t, g)), Equal.trans(Nat, Nat.mul(a, Nat.mul(g, t)), Nat.mul(Nat.mul(a, g), t), Nat.mul(c, t), Equal.sym(Nat, Nat.mul(Nat.mul(a, g), t), Nat.mul(a, Nat.mul(g, t)), NA.mul_assoc(a, g, t)), Equal.cong(Nat, Nat, z => Nat.mul(z, t), Nat.mul(a, g), c, Equal.sym(Nat, c, Nat.mul(a, g), e_c(c, jp))))))
164  +r = Equal.trans(Nat, Nat.mul(Nat.mul(c1, b), g), Nat.mul(c1, Nat.mul(b, g)), Nat.mul(c1, 1n+jp), NA.mul_assoc(c1, b, g), Equal.cong(Nat, Nat, z => Nat.mul(c1, z), Nat.mul(b, g), 1n+jp, Equal.sym(Nat, 1n+jp, Nat.mul(b, g), e_j(c, jp))))
165  LC.cancel_pos(Nat.mul(a, t), Nat.mul(c1, b), g, g_pos(c, jp), Equal.trans(Nat, Nat.mul(Nat.mul(a, t), g), Nat.mul(c, t), Nat.mul(Nat.mul(c1, b), g), l, Equal.sym(Nat, Nat.mul(Nat.mul(c1, b), g), Nat.mul(c, t), Equal.trans(Nat, Nat.mul(Nat.mul(c1, b), g), Nat.mul(c1, 1n+jp), Nat.mul(c, t), r, e))))
166
167# the quotient t / wr
168def sq(+c: Nat, +jp: Nat, +t: Nat, +c1: Nat) -> Nat:
169  GC.dw(Nat.mul(t, wr(c, jp)), Nat.mul(t, wl(c, jp)), Nat.mul(t, wr(c, jp)), c1, t)
170
171# Euclid: wr | wl t and gcd(wl, wr) == 1 give wr | t
172def t_eq(+c: Nat, +jp: Nat, +t: Nat, +c1: Nat, +e: {Nat.mul(c1, 1n+jp) == Nat.mul(c, t) : Nat}) -> {t == Nat.mul(sq(c, jp, t, c1), wr(c, jp)) : Nat}:
173  +a = wl(c, jp)
174  +b = wr(c, jp)
175  +ea = Equal.trans(Nat, Nat.mul(t, a), Nat.mul(a, t), Nat.mul(c1, b), NA.mul_comm(t, a), cross(c, jp, t, c1, e))
176  +d = GC.dvd_gcd(Nat.mul(t, a), Nat.mul(t, b), b, c1, t, ea, {==})
177  +g1 = Equal.trans(Nat, M.gcd(Nat.mul(t, a), Nat.mul(t, b)), Nat.mul(t, M.gcd(a, b)), t, LC.gcd_mul_left(t, a, b), Equal.trans(Nat, Nat.mul(t, M.gcd(a, b)), Nat.mul(t, 1n), t, Equal.cong(Nat, Nat, z => Nat.mul(t, z), M.gcd(a, b), 1n, coprime(c, jp)), NA.mul_one(t)))
178  Equal.trans(Nat, t, M.gcd(Nat.mul(t, a), Nat.mul(t, b)), Nat.mul(sq(c, jp, t, c1), b), Equal.sym(Nat, M.gcd(Nat.mul(t, a), Nat.mul(t, b)), t, g1), d)
179
180def div_t(+c: Nat, +jp: Nat, +t: Nat, +c1: Nat, +e: {Nat.mul(c1, 1n+jp) == Nat.mul(c, t) : Nat}) -> {Nat.div(t, wr(c, jp)) == sq(c, jp, t, c1) : Nat}:
181  LC.div_exact(t, sq(c, jp, t, c1), wr(c, jp), wr_pos(c, jp), t_eq(c, jp, t, c1, e))
182
183# (c / g) (t / (j / g)) == c'
184def prod_eq(+c: Nat, +jp: Nat, +t: Nat, +c1: Nat, +e: {Nat.mul(c1, 1n+jp) == Nat.mul(c, t) : Nat}) -> {Nat.mul(wl(c, jp), sq(c, jp, t, c1)) == c1 : Nat}:
185  +a = wl(c, jp)
186  +b = wr(c, jp)
187  +s = sq(c, jp, t, c1)
188  +h1 = Equal.trans(Nat, Nat.mul(Nat.mul(a, s), b), Nat.mul(a, Nat.mul(s, b)), Nat.mul(c1, b), NA.mul_assoc(a, s, b), Equal.trans(Nat, Nat.mul(a, Nat.mul(s, b)), Nat.mul(a, t), Nat.mul(c1, b), Equal.cong(Nat, Nat, z => Nat.mul(a, z), Nat.mul(s, b), t, Equal.sym(Nat, t, Nat.mul(s, b), t_eq(c, jp, t, c1, e))), cross(c, jp, t, c1, e)))
189  LC.cancel_pos(Nat.mul(a, s), c1, b, wr_pos(c, jp), h1)