proofs/math/natural/fact.bend
bend-collections-laws-containers@1.0.0.0 · 279 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/arith.bend as R
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# factorial, perm and comb against the structural definitions of
11# spec.bend, following Lean 4 Mathlib (Mathlib/Data/Nat/Factorial/Basic,
12# Mathlib/Data/Nat/Choose/Basic): Nat.factorial_pos,
13# Nat.succ_descFactorial_succ, Nat.descFactorial_self,
14# Nat.factorial_mul_descFactorial, Nat.add_one_mul_choose_eq,
15# Nat.choose_succ_right_eq, Nat.descFactorial_eq_factorial_mul_choose,
16# Nat.choose_mul_factorial_mul_factorial, Nat.choose_symm,
17# Nat.choose_eq_zero_of_lt.
18
19# (x a) f == a (x f)
20def mul_left_comm(+x: Nat, +a: Nat, +f: Nat) -> {Nat.mul(Nat.mul(x, a), f) == Nat.mul(a, Nat.mul(x, f)) : Nat}:
21 Equal.trans(Nat, Nat.mul(Nat.mul(x, a), f), Nat.mul(Nat.mul(a, x), f), Nat.mul(a, Nat.mul(x, f)), Equal.cong(Nat, Nat, z => Nat.mul(z, f), Nat.mul(x, a), Nat.mul(a, x), A.mul_comm(x, a)), A.mul_assoc(a, x, f))
22
23# ---- factorial ----
24
25def factorial_go(+n: Nat, +acc: Nat) -> {M.factorial_go(n, acc) == Nat.mul(acc, S.factorial(n)) : Nat}:
26 match n:
27 case 0n:
28 Equal.sym(Nat, Nat.mul(acc, 1n), acc, A.mul_one(acc))
29 case 1n+ +p:
30 Equal.trans(Nat, M.factorial_go(p, Nat.mul(1n+p, acc)), Nat.mul(Nat.mul(1n+p, acc), S.factorial(p)), Nat.mul(acc, Nat.mul(1n+p, S.factorial(p))), factorial_go(p, Nat.mul(1n+p, acc)), mul_left_comm(1n+p, acc, S.factorial(p)))
31
32# factorial(n) == n!
33def factorial_ok(+n: Nat) -> {M.factorial(n) == S.factorial(n) : Nat}:
34 Equal.trans(Nat, M.factorial(n), Nat.mul(1n, S.factorial(n)), S.factorial(n), factorial_go(n, 1n), LC.one_mul(S.factorial(n)))
35
36def pos_mul(+p: Nat, +f: Nat, +h: {Nat.is_lt(0n, f) == True{} : Bool}) -> {Nat.is_lt(0n, Nat.mul(1n+p, f)) == True{} : Bool}:
37 match f:
38 case 0n:
39 Empty.absurd({Nat.is_lt(0n, Nat.mul(1n+p, 0n)) == True{} : Bool}, L.false_true(h))
40 case 1n+fp:
41 {==}
42
43# 0 < n! (Mathlib Nat.factorial_pos)
44def factorial_pos(+n: Nat) -> {Nat.is_lt(0n, S.factorial(n)) == True{} : Bool}:
45 match n:
46 case 0n:
47 {==}
48 case 1n+ +p:
49 pos_mul(p, S.factorial(p), factorial_pos(p))
50
51# ---- descending factorial: perm ----
52
53# (1+m).desc(1+j) == (1+m) * m.desc(j) (Mathlib Nat.succ_descFactorial_succ)
54def desc_succ(+m: Nat, +j: Nat) -> {S.desc(1n+m, 1n+j) == Nat.mul(1n+m, S.desc(m, j)) : Nat}:
55 match j:
56 case 0n:
57 {==}
58 case 1n+ +i:
59 %Equal.sym(Nat, S.desc(1n+m, 1n+i), Nat.mul(1n+m, S.desc(m, i)), desc_succ(m, i)) : {Nat.mul(Nat.sub(m, i), _) == Nat.mul(1n+m, Nat.mul(Nat.sub(m, i), S.desc(m, i))) : Nat}
60 LC.swap_cw(Nat.sub(m, i), 1n+m, S.desc(m, i))
61
62# m * (m - 1).desc(j) == m.desc(1+j), the order perm multiplies in
63def desc_front(+m: Nat, +j: Nat) -> {Nat.mul(m, S.desc(Nat.sub(m, 1n), j)) == S.desc(m, 1n+j) : Nat}:
64 match m:
65 case 0n:
66 Equal.sym(Nat, Nat.mul(Nat.sub(0n, j), S.desc(0n, j)), 0n, Equal.cong(Nat, Nat, z => Nat.mul(z, S.desc(0n, j)), Nat.sub(0n, j), 0n, R.zsub(j)))
67 case 1n+ +mp:
68 %Equal.sym(Nat, Nat.sub(1n+mp, 1n), mp, N.sub_zero(mp)) : {Nat.mul(1n+mp, S.desc(_, j)) == S.desc(1n+mp, 1n+j) : Nat}
69 Equal.sym(Nat, S.desc(1n+mp, 1n+j), Nat.mul(1n+mp, S.desc(mp, j)), desc_succ(mp, j))
70
71def perm_go(+k: Nat, +m: Nat, +acc: Nat) -> {M.perm_go(k, m, acc) == Nat.mul(acc, S.desc(m, k)) : Nat}:
72 match k:
73 case 0n:
74 Equal.sym(Nat, Nat.mul(acc, 1n), acc, A.mul_one(acc))
75 case 1n+ +j:
76 Equal.trans(Nat, M.perm_go(j, Nat.sub(m, 1n), Nat.mul(acc, m)), Nat.mul(Nat.mul(acc, m), S.desc(Nat.sub(m, 1n), j)), Nat.mul(acc, S.desc(m, 1n+j)), perm_go(j, Nat.sub(m, 1n), Nat.mul(acc, m)),
77 Equal.trans(Nat, Nat.mul(Nat.mul(acc, m), S.desc(Nat.sub(m, 1n), j)), Nat.mul(acc, Nat.mul(m, S.desc(Nat.sub(m, 1n), j))), Nat.mul(acc, S.desc(m, 1n+j)), A.mul_assoc(acc, m, S.desc(Nat.sub(m, 1n), j)),
78 Equal.cong(Nat, Nat, z => Nat.mul(acc, z), Nat.mul(m, S.desc(Nat.sub(m, 1n), j)), S.desc(m, 1n+j), desc_front(m, j))))
79
80# perm(n, k) == n.descFactorial(k)
81def perm_ok(+n: Nat, +k: Nat) -> {M.perm(n, k) == S.desc(n, k) : Nat}:
82 Equal.trans(Nat, M.perm(n, k), Nat.mul(1n, S.desc(n, k)), S.desc(n, k), perm_go(k, n, 1n), LC.one_mul(S.desc(n, k)))
83
84# n.desc(n) == n! (Mathlib Nat.descFactorial_self)
85def desc_self(+n: Nat) -> {S.desc(n, n) == S.factorial(n) : Nat}:
86 match n:
87 case 0n:
88 {==}
89 case 1n+ +p:
90 Equal.trans(Nat, S.desc(1n+p, 1n+p), Nat.mul(1n+p, S.desc(p, p)), S.factorial(1n+p), desc_succ(p, p), Equal.cong(Nat, Nat, z => Nat.mul(1n+p, z), S.desc(p, p), S.factorial(p), desc_self(p)))
91
92# j < n gives n - j == 1 + (n - (1 + j))
93def sub_lt_succ(+n: Nat, +j: Nat, +h: {Nat.is_lt(j, n) == True{} : Bool}) -> {Nat.sub(n, j) == 1n+Nat.sub(n, 1n+j) : Nat}:
94 match n j:
95 case 0n j0:
96 Empty.absurd({Nat.sub(0n, j0) == 1n+Nat.sub(0n, 1n+j0) : Nat}, N.lt_zero_absurd(j0, h))
97 case 1n+ +np 0n:
98 Equal.sym(Nat, 1n+Nat.sub(np, 0n), 1n+np, N.succ_cong(Nat.sub(np, 0n), np, N.sub_zero(np)))
99 case 1n+ +np 1n+ +jp:
100 sub_lt_succ(np, jp, h)
101
102# (n - k)! * n.desc(k) == n! (Mathlib Nat.factorial_mul_descFactorial)
103def factorial_mul_desc(+n: Nat, +k: Nat, +h: {Nat.is_le(k, n) == True{} : Bool}) -> {Nat.mul(S.factorial(Nat.sub(n, k)), S.desc(n, k)) == S.factorial(n) : Nat}:
104 match k:
105 case 0n:
106 %Equal.sym(Nat, Nat.sub(n, 0n), n, N.sub_zero(n)) : {Nat.mul(S.factorial(_), 1n) == S.factorial(n) : Nat}
107 A.mul_one(S.factorial(n))
108 case 1n+ +j:
109 +t = Nat.sub(n, 1n+j)
110 +hj = N.succ_le_lt(j, n, h)
111 +ih = factorial_mul_desc(n, j, N.lt_le(j, n, hj))
112 +es = sub_lt_succ(n, j, hj)
113 # t! * ((n - j) * n.desc(j)) == ((n - j) * t!) * n.desc(j) == (n - j)! * n.desc(j)
114 %Equal.sym(Nat, Nat.mul(S.factorial(t), Nat.mul(Nat.sub(n, j), S.desc(n, j))), Nat.mul(Nat.mul(Nat.sub(n, j), S.factorial(t)), S.desc(n, j)), Equal.sym(Nat, Nat.mul(Nat.mul(Nat.sub(n, j), S.factorial(t)), S.desc(n, j)), Nat.mul(S.factorial(t), Nat.mul(Nat.sub(n, j), S.desc(n, j))), mul_left_comm(Nat.sub(n, j), S.factorial(t), S.desc(n, j)))) : {_ == S.factorial(n) : Nat}
115 %Equal.sym(Nat, Nat.sub(n, j), 1n+t, es) : {Nat.mul(Nat.mul(_, S.factorial(t)), S.desc(n, j)) == S.factorial(n) : Nat}
116 %Equal.sym(Nat, Nat.mul(1n+t, S.factorial(t)), S.factorial(Nat.sub(n, j)), Equal.trans(Nat, Nat.mul(1n+t, S.factorial(t)), S.factorial(1n+t), S.factorial(Nat.sub(n, j)), {==}, Equal.cong(Nat, Nat, z => S.factorial(z), 1n+t, Nat.sub(n, j), Equal.sym(Nat, Nat.sub(n, j), 1n+t, es)))) : {Nat.mul(_, S.desc(n, j)) == S.factorial(n) : Nat}
117 ih
118
119# ---- binomial coefficients ----
120
121def choose_zero_right(+n: Nat) -> {S.choose(n, 0n) == 1n : Nat}:
122 match n:
123 case 0n:
124 {==}
125 case 1n+m:
126 {==}
127
128# C(n, 1) == n
129def choose_one_right(+n: Nat) -> {S.choose(n, 1n) == n : Nat}:
130 match n:
131 case 0n:
132 {==}
133 case 1n+ +m:
134 %Equal.sym(Nat, S.choose(m, 0n), 1n, choose_zero_right(m)) : {Nat.add(_, S.choose(m, 1n)) == 1n+m : Nat}
135 N.succ_cong(S.choose(m, 1n), m, choose_one_right(m))
136
137# (n + 1) C(n, k) == C(n + 1, k + 1) (k + 1) (Mathlib Nat.add_one_mul_choose_eq)
138def succ_mul_choose(+n: Nat, +k: Nat) -> {Nat.mul(1n+n, S.choose(n, k)) == Nat.mul(S.choose(1n+n, 1n+k), 1n+k) : Nat}:
139 match n k:
140 case 0n 0n:
141 {==}
142 case 0n 1n+j:
143 {==}
144 case 1n+ +m 0n:
145 %Equal.sym(Nat, S.choose(1n+m, 0n), 1n, choose_zero_right(1n+m)) : {Nat.mul(2n+m, _) == Nat.mul(Nat.add(S.choose(1n+m, 0n), S.choose(1n+m, 1n)), 1n) : Nat}
146 %Equal.sym(Nat, S.choose(1n+m, 0n), 1n, choose_zero_right(1n+m)) : {Nat.mul(2n+m, 1n) == Nat.mul(Nat.add(_, S.choose(1n+m, 1n)), 1n) : Nat}
147 %Equal.sym(Nat, S.choose(1n+m, 1n), 1n+m, choose_one_right(1n+m)) : {Nat.mul(2n+m, 1n) == Nat.mul(Nat.add(1n, _), 1n) : Nat}
148 {==}
149 case 1n+ +m 1n+ +j:
150 +x = S.choose(1n+m, 1n+j)
151 +y = S.choose(1n+m, 2n+j)
152 +c0 = S.choose(m, j)
153 +c1 = S.choose(m, 1n+j)
154 # (x + y)(2 + j) == x + x(1 + j) + y(2 + j) == x + (1+m) c0 + (1+m) c1 == x + (1+m) x
155 %Equal.sym(Nat, Nat.mul(Nat.add(x, y), 2n+j), Nat.add(Nat.mul(x, 2n+j), Nat.mul(y, 2n+j)), A.mul_add_right(x, y, 2n+j)) : {Nat.mul(2n+m, x) == _ : Nat}
156 %Equal.sym(Nat, Nat.mul(x, 2n+j), Nat.add(x, Nat.mul(x, 1n+j)), A.mul_succ(x, 1n+j)) : {Nat.mul(2n+m, x) == Nat.add(_, Nat.mul(y, 2n+j)) : Nat}
157 %Equal.sym(Nat, Nat.mul(x, 1n+j), Nat.mul(1n+m, c0), Equal.sym(Nat, Nat.mul(1n+m, c0), Nat.mul(x, 1n+j), succ_mul_choose(m, j))) : {Nat.mul(2n+m, x) == Nat.add(Nat.add(x, _), Nat.mul(y, 2n+j)) : Nat}
158 %Equal.sym(Nat, Nat.mul(y, 2n+j), Nat.mul(1n+m, c1), Equal.sym(Nat, Nat.mul(1n+m, c1), Nat.mul(y, 2n+j), succ_mul_choose(m, 1n+j))) : {Nat.mul(2n+m, x) == Nat.add(Nat.add(x, Nat.mul(1n+m, c0)), _) : Nat}
159 %Equal.sym(Nat, Nat.add(Nat.add(x, Nat.mul(1n+m, c0)), Nat.mul(1n+m, c1)), Nat.add(x, Nat.add(Nat.mul(1n+m, c0), Nat.mul(1n+m, c1))), A.add_assoc(x, Nat.mul(1n+m, c0), Nat.mul(1n+m, c1))) : {Nat.mul(2n+m, x) == _ : Nat}
160 %Equal.sym(Nat, Nat.add(Nat.mul(1n+m, c0), Nat.mul(1n+m, c1)), Nat.mul(1n+m, Nat.add(c0, c1)), Equal.sym(Nat, Nat.mul(1n+m, Nat.add(c0, c1)), Nat.add(Nat.mul(1n+m, c0), Nat.mul(1n+m, c1)), A.mul_add_left(1n+m, c0, c1))) : {Nat.mul(2n+m, x) == Nat.add(x, _) : Nat}
161 {==}
162
163# a (x - y) == a x - a y
164def mul_sub_left(+a: Nat, +x: Nat, +y: Nat) -> {Nat.mul(a, Nat.sub(x, y)) == Nat.sub(Nat.mul(a, x), Nat.mul(a, y)) : Nat}:
165 %Equal.sym(Nat, Nat.mul(a, Nat.sub(x, y)), Nat.mul(Nat.sub(x, y), a), A.mul_comm(a, Nat.sub(x, y))) : {_ == Nat.sub(Nat.mul(a, x), Nat.mul(a, y)) : Nat}
166 %Equal.sym(Nat, Nat.mul(a, x), Nat.mul(x, a), A.mul_comm(a, x)) : {Nat.mul(Nat.sub(x, y), a) == Nat.sub(_, Nat.mul(a, y)) : Nat}
167 %Equal.sym(Nat, Nat.mul(a, y), Nat.mul(y, a), A.mul_comm(a, y)) : {Nat.mul(Nat.sub(x, y), a) == Nat.sub(Nat.mul(x, a), _) : Nat}
168 R.mul_sub(x, y, a)
169
170# C(n, k + 1) (k + 1) == C(n, k) (n - k) (Mathlib Nat.choose_succ_right_eq)
171def choose_succ_right(+n: Nat, +k: Nat) -> {Nat.mul(S.choose(n, 1n+k), 1n+k) == Nat.mul(S.choose(n, k), Nat.sub(n, k)) : Nat}:
172 +c = S.choose(n, k)
173 +d = S.choose(n, 1n+k)
174 # (1 + n) c == c (1 + k) + d (1 + k)
175 +e = Equal.trans(Nat, Nat.mul(1n+n, c), Nat.mul(Nat.add(c, d), 1n+k), Nat.add(Nat.mul(c, 1n+k), Nat.mul(d, 1n+k)), succ_mul_choose(n, k), A.mul_add_right(c, d, 1n+k))
176 %Equal.sym(Nat, Nat.mul(c, Nat.sub(n, k)), Nat.sub(Nat.mul(c, 1n+n), Nat.mul(c, 1n+k)), mul_sub_left(c, 1n+n, 1n+k)) : {Nat.mul(d, 1n+k) == _ : Nat}
177 %Equal.sym(Nat, Nat.mul(c, 1n+n), Nat.mul(1n+n, c), A.mul_comm(c, 1n+n)) : {Nat.mul(d, 1n+k) == Nat.sub(_, Nat.mul(c, 1n+k)) : Nat}
178 %Equal.sym(Nat, Nat.mul(1n+n, c), Nat.add(Nat.mul(c, 1n+k), Nat.mul(d, 1n+k)), e) : {Nat.mul(d, 1n+k) == Nat.sub(_, Nat.mul(c, 1n+k)) : Nat}
179 Equal.sym(Nat, Nat.sub(Nat.add(Nat.mul(c, 1n+k), Nat.mul(d, 1n+k)), Nat.mul(c, 1n+k)), Nat.mul(d, 1n+k), N.add_sub_cancel(Nat.mul(c, 1n+k), Nat.mul(d, 1n+k)))
180
181# C(n, k) k! == n.desc(k) (Mathlib Nat.descFactorial_eq_factorial_mul_choose)
182def choose_mul_factorial(+n: Nat, +k: Nat) -> {Nat.mul(S.choose(n, k), S.factorial(k)) == S.desc(n, k) : Nat}:
183 match k:
184 case 0n:
185 %Equal.sym(Nat, S.choose(n, 0n), 1n, choose_zero_right(n)) : {Nat.mul(_, 1n) == 1n : Nat}
186 {==}
187 case 1n+ +j:
188 # C(n, 1+j) ((1+j) j!) == (C(n, 1+j) (1+j)) j! == (C(n, j) (n - j)) j! == (n - j) (C(n, j) j!)
189 %Equal.sym(Nat, Nat.mul(S.choose(n, 1n+j), Nat.mul(1n+j, S.factorial(j))), Nat.mul(Nat.mul(S.choose(n, 1n+j), 1n+j), S.factorial(j)), Equal.sym(Nat, Nat.mul(Nat.mul(S.choose(n, 1n+j), 1n+j), S.factorial(j)), Nat.mul(S.choose(n, 1n+j), Nat.mul(1n+j, S.factorial(j))), A.mul_assoc(S.choose(n, 1n+j), 1n+j, S.factorial(j)))) : {_ == S.desc(n, 1n+j) : Nat}
190 %Equal.sym(Nat, Nat.mul(S.choose(n, 1n+j), 1n+j), Nat.mul(S.choose(n, j), Nat.sub(n, j)), choose_succ_right(n, j)) : {Nat.mul(_, S.factorial(j)) == S.desc(n, 1n+j) : Nat}
191 %Equal.sym(Nat, Nat.mul(Nat.mul(S.choose(n, j), Nat.sub(n, j)), S.factorial(j)), Nat.mul(Nat.sub(n, j), Nat.mul(S.choose(n, j), S.factorial(j))), Equal.trans(Nat, Nat.mul(Nat.mul(S.choose(n, j), Nat.sub(n, j)), S.factorial(j)), Nat.mul(Nat.mul(Nat.sub(n, j), S.choose(n, j)), S.factorial(j)), Nat.mul(Nat.sub(n, j), Nat.mul(S.choose(n, j), S.factorial(j))), Equal.cong(Nat, Nat, z => Nat.mul(z, S.factorial(j)), Nat.mul(S.choose(n, j), Nat.sub(n, j)), Nat.mul(Nat.sub(n, j), S.choose(n, j)), A.mul_comm(S.choose(n, j), Nat.sub(n, j))), A.mul_assoc(Nat.sub(n, j), S.choose(n, j), S.factorial(j)))) : {_ == S.desc(n, 1n+j) : Nat}
192 Equal.cong(Nat, Nat, z => Nat.mul(Nat.sub(n, j), z), Nat.mul(S.choose(n, j), S.factorial(j)), S.desc(n, j), choose_mul_factorial(n, j))
193
194# n < k gives C(n, k) == 0 (Mathlib Nat.choose_eq_zero_of_lt)
195def choose_eq_zero(+n: Nat, +k: Nat, +h: {Nat.is_lt(n, k) == True{} : Bool}) -> {S.choose(n, k) == 0n : Nat}:
196 match n k:
197 case n0 0n:
198 Empty.absurd({S.choose(n0, 0n) == 0n : Nat}, N.lt_zero_absurd(n0, h))
199 case 0n 1n+j:
200 {==}
201 case 1n+ +m 1n+ +j:
202 %Equal.sym(Nat, S.choose(m, j), 0n, choose_eq_zero(m, j, h)) : {Nat.add(_, S.choose(m, 1n+j)) == 0n : Nat}
203 choose_eq_zero(m, 1n+j, N.lt_trans(m, j, 1n+j, h, N.lt_succ(j)))
204
205def pos_pos(+a: Nat, +b: Nat, +ha: {Nat.is_lt(0n, a) == True{} : Bool}, +hb: {Nat.is_lt(0n, b) == True{} : Bool}) -> {Nat.is_lt(0n, Nat.mul(a, b)) == True{} : Bool}:
206 match a:
207 case 0n:
208 Empty.absurd({Nat.is_lt(0n, Nat.mul(0n, b)) == True{} : Bool}, L.false_true(ha))
209 case 1n+ +ap:
210 pos_mul(ap, b, hb)
211
212# C(n, k) (k! (n - k)!) == n! (Mathlib Nat.choose_mul_factorial_mul_factorial)
213def choose_mul_facts(+n: Nat, +k: Nat, +h: {Nat.is_le(k, n) == True{} : Bool}) -> {Nat.mul(S.choose(n, k), Nat.mul(S.factorial(k), S.factorial(Nat.sub(n, k)))) == S.factorial(n) : Nat}:
214 %Equal.sym(Nat, Nat.mul(S.choose(n, k), Nat.mul(S.factorial(k), S.factorial(Nat.sub(n, k)))), Nat.mul(Nat.mul(S.choose(n, k), S.factorial(k)), S.factorial(Nat.sub(n, k))), Equal.sym(Nat, Nat.mul(Nat.mul(S.choose(n, k), S.factorial(k)), S.factorial(Nat.sub(n, k))), Nat.mul(S.choose(n, k), Nat.mul(S.factorial(k), S.factorial(Nat.sub(n, k)))), A.mul_assoc(S.choose(n, k), S.factorial(k), S.factorial(Nat.sub(n, k))))) : {_ == S.factorial(n) : Nat}
215 %Equal.sym(Nat, Nat.mul(S.choose(n, k), S.factorial(k)), S.desc(n, k), choose_mul_factorial(n, k)) : {Nat.mul(_, S.factorial(Nat.sub(n, k))) == S.factorial(n) : Nat}
216 %Equal.sym(Nat, Nat.mul(S.desc(n, k), S.factorial(Nat.sub(n, k))), Nat.mul(S.factorial(Nat.sub(n, k)), S.desc(n, k)), A.mul_comm(S.desc(n, k), S.factorial(Nat.sub(n, k)))) : {_ == S.factorial(n) : Nat}
217 factorial_mul_desc(n, k, h)
218
219# n - (n - k) == k for k <= n
220def sub_sub_self(+n: Nat, +k: Nat, +h: {Nat.is_le(k, n) == True{} : Bool}) -> {Nat.sub(n, Nat.sub(n, k)) == k : Nat}:
221 +e = N.sub_add(n, k, h)
222 %Equal.sym(Nat, n, Nat.add(k, Nat.sub(n, k)), Equal.sym(Nat, Nat.add(k, Nat.sub(n, k)), n, e)) : {Nat.sub(_, Nat.sub(n, k)) == k : Nat}
223 %Equal.sym(Nat, Nat.add(k, Nat.sub(n, k)), Nat.add(Nat.sub(n, k), k), A.add_comm(k, Nat.sub(n, k))) : {Nat.sub(_, Nat.sub(n, k)) == k : Nat}
224 N.add_sub_cancel(Nat.sub(n, k), k)
225
226def sub_le_self(+n: Nat, +k: Nat) -> {Nat.is_le(Nat.sub(n, k), n) == True{} : Bool}:
227 match n k:
228 case 0n k0:
229 %Equal.sym(Nat, Nat.sub(0n, k0), 0n, R.zsub(k0)) : {Nat.is_le(_, 0n) == True{} : Bool}
230 {==}
231 case 1n+ +np 0n:
232 N.le_refl(1n+np)
233 case 1n+ +np 1n+ +kp:
234 N.le_trans(Nat.sub(np, kp), np, 1n+np, sub_le_self(np, kp), N.le_succ(np))
235
236# C(n, n - k) == C(n, k) (Mathlib Nat.choose_symm)
237def choose_symm(+n: Nat, +k: Nat, +h: {Nat.is_le(k, n) == True{} : Bool}) -> {S.choose(n, Nat.sub(n, k)) == S.choose(n, k) : Nat}:
238 +kk = Nat.sub(n, k)
239 +fk = S.factorial(k)
240 +fkk = S.factorial(kk)
241 +e1 = choose_mul_facts(n, kk, sub_le_self(n, k))
242 +e1b = Equal.trans(Nat, Nat.mul(S.choose(n, kk), Nat.mul(fkk, fk)), Nat.mul(S.choose(n, kk), Nat.mul(fkk, S.factorial(Nat.sub(n, kk)))), S.factorial(n),
243 Equal.cong(Nat, Nat, z => Nat.mul(S.choose(n, kk), Nat.mul(fkk, S.factorial(z))), k, Nat.sub(n, kk), Equal.sym(Nat, Nat.sub(n, kk), k, sub_sub_self(n, k, h))), e1)
244 +e2 = Equal.trans(Nat, Nat.mul(S.choose(n, k), Nat.mul(fkk, fk)), Nat.mul(S.choose(n, k), Nat.mul(fk, fkk)), S.factorial(n),
245 Equal.cong(Nat, Nat, z => Nat.mul(S.choose(n, k), z), Nat.mul(fkk, fk), Nat.mul(fk, fkk), A.mul_comm(fkk, fk)), choose_mul_facts(n, k, h))
246 LC.cancel_pos(S.choose(n, kk), S.choose(n, k), Nat.mul(fkk, fk), pos_pos(fkk, fk, factorial_pos(kk), factorial_pos(k)), Equal.trans(Nat, Nat.mul(S.choose(n, kk), Nat.mul(fkk, fk)), S.factorial(n), Nat.mul(S.choose(n, k), Nat.mul(fkk, fk)), e1b, Equal.sym(Nat, Nat.mul(S.choose(n, k), Nat.mul(fkk, fk)), S.factorial(n), e2)))
247
248# ---- comb ----
249
250# every r_i is C(n, i), so each division is exact
251def comb_go(+j: Nat, +n: Nat, +i: Nat) -> {M.comb_go(j, n, i, S.choose(n, i)) == S.choose(n, Nat.add(i, j)) : Nat}:
252 match j:
253 case 0n:
254 Equal.cong(Nat, Nat, z => S.choose(n, z), i, Nat.add(i, 0n), Equal.sym(Nat, Nat.add(i, 0n), i, A.add_zero(i)))
255 case 1n+ +jp:
256 %Equal.sym(Nat, Nat.mul(S.choose(n, i), Nat.sub(n, i)), Nat.add(Nat.mul(S.choose(n, 1n+i), 1n+i), 0n), Equal.trans(Nat, Nat.mul(S.choose(n, i), Nat.sub(n, i)), Nat.mul(S.choose(n, 1n+i), 1n+i), Nat.add(Nat.mul(S.choose(n, 1n+i), 1n+i), 0n), Equal.sym(Nat, Nat.mul(S.choose(n, 1n+i), 1n+i), Nat.mul(S.choose(n, i), Nat.sub(n, i)), choose_succ_right(n, i)), Equal.sym(Nat, Nat.add(Nat.mul(S.choose(n, 1n+i), 1n+i), 0n), Nat.mul(S.choose(n, 1n+i), 1n+i), A.add_zero(Nat.mul(S.choose(n, 1n+i), 1n+i))))) : {M.comb_go(jp, n, 1n+i, Nat.div(_, 1n+i)) == S.choose(n, Nat.add(i, 1n+jp)) : Nat}
257 %Equal.sym(Nat, Nat.div(Nat.add(Nat.mul(S.choose(n, 1n+i), 1n+i), 0n), 1n+i), S.choose(n, 1n+i), R.div_of(S.choose(n, 1n+i), i, 0n, {==})) : {M.comb_go(jp, n, 1n+i, _) == S.choose(n, Nat.add(i, 1n+jp)) : Nat}
258 %Equal.sym(Nat, Nat.add(i, 1n+jp), 1n+Nat.add(i, jp), A.add_succ(i, jp)) : {M.comb_go(jp, n, 1n+i, S.choose(n, 1n+i)) == S.choose(n, _) : Nat}
259 comb_go(jp, n, 1n+i)
260
261def comb_min(+n: Nat, +k: Nat, +hk: {Nat.is_le(k, n) == True{} : Bool}, +b: Bool, +hb: {Nat.is_lt(k, Nat.sub(n, k)) == b : Bool}) -> {S.choose(n, Nat.min(k, Nat.sub(n, k))) == S.choose(n, k) : Nat}:
262 match b:
263 case True{}:
264 Equal.cong(Nat, Nat, z => S.choose(n, z), Nat.min(k, Nat.sub(n, k)), k, N.min_left(k, Nat.sub(n, k), hb))
265 case False{}:
266 Equal.trans(Nat, S.choose(n, Nat.min(k, Nat.sub(n, k))), S.choose(n, Nat.sub(n, k)), S.choose(n, k), Equal.cong(Nat, Nat, z => S.choose(n, z), Nat.min(k, Nat.sub(n, k)), Nat.sub(n, k), N.min_right(k, Nat.sub(n, k), hb)), choose_symm(n, k, hk))
267
268def comb_small(+n: Nat, +k: Nat, +b: Bool, +hb: {Nat.is_lt(n, k) == b : Bool}) -> {M.comb_small(n, k, b) == S.choose(n, k) : Nat}:
269 match b:
270 case True{}:
271 Equal.sym(Nat, S.choose(n, k), 0n, choose_eq_zero(n, k, hb))
272 case False{}:
273 +m = Nat.min(k, Nat.sub(n, k))
274 %Equal.sym(Nat, 1n, S.choose(n, 0n), Equal.sym(Nat, S.choose(n, 0n), 1n, choose_zero_right(n))) : {M.comb_go(m, n, 0n, _) == S.choose(n, k) : Nat}
275 Equal.trans(Nat, M.comb_go(m, n, 0n, S.choose(n, 0n)), S.choose(n, m), S.choose(n, k), comb_go(m, n, 0n), comb_min(n, k, N.not_lt_le(n, k, hb), Nat.is_lt(k, Nat.sub(n, k)), {==}))
276
277# comb(n, k) == C(n, k)
278def comb_ok(+n: Nat, +k: Nat) -> {M.comb(n, k) == S.choose(n, k) : Nat}:
279 comb_small(n, k, Nat.is_lt(n, k), {==})