proofs/math/natural/proof.bend
bend-collections-laws-containers@1.0.0.0 · 213 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/src/math/natural.bend as M
3import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
4import bend-collections-laws-containers@1.0.0.0/spec/math/natural.bend as S
5import bend-collections-laws-containers@1.0.0.0/proofs/math/natural/arith.bend as R
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/proofs/math/natural/fact.bend as F
9import bend-collections-laws-containers@1.0.0.0/proofs/math/natural/bits.bend as B
10import bend-collections-laws-containers@1.0.0.0/proofs/math/natural/roots.bend as RT
11import bend-collections-laws-containers@1.0.0.0/proofs/math/natural/sqrtn.bend as SQ
12import bend-collections-laws-containers@1.0.0.0/proofs/math/natural/logs.bend as LG
13import bend-collections-laws-containers@1.0.0.0/proofs/math/natural/modpow.bend as MP
14import bend-collections-laws-containers@1.0.0.0/proofs/math/natural/inverse.bend as IV
15import bend-collections-laws-containers@1.0.0.0/proofs/math/natural/lists.bend as LS
16import bend-collections-laws-containers@1.0.0.0/proofs/math/natural/misc.bend as MS
17
18
19# src/math/natural.bend against its specification spec/math/natural.bend:
20# one definition per contract clause, under the clause's name, typed by the
21# clause. Divisibility is dvd(d, a): the quotient and the equation. The
22# reference proofs each module mirrors are cited in its file (Lean 4
23# Mathlib, the Why3 gallery, HACL*); none assumes a hole or an axiom.
24
25# the value of a successful result, 0 on an error
26def res_val(r: Result<&2, &2, M.MathError, Nat>) -> Nat:
27 match r:
28 case Done{x}:
29 x
30 case Fail{e}:
31 0n
32
33# a result that is Done twice holds one value
34def done_eq(+t: Result<&2, &2, M.MathError, Nat>, +a: Nat, +b: Nat, +ha: {t == Done{a} : Result<&2, &2, M.MathError, Nat>}, +hb: {t == Done{b} : Result<&2, &2, M.MathError, Nat>}) -> {a == b : Nat}:
35 Equal.cong(Result<&2, &2, M.MathError, Nat>, Nat, res_val, Done{a}, Done{b}, Equal.trans(Result<&2, &2, M.MathError, Nat>, Done{a}, t, Done{b}, Equal.sym(Result<&2, &2, M.MathError, Nat>, t, Done{a}, ha), hb))
36
37# ---- gcd, lcm ----
38
39def divides_left(+a: Nat, +b: Nat) -> S.Gcd.divides_left(a, b):
40 (G.wl(G.ws(b, a, b)), G.gcd_dvd_left(a, b))
41
42def divides_right(+a: Nat, +b: Nat) -> S.Gcd.divides_right(a, b):
43 (G.wr(G.ws(b, a, b)), G.gcd_dvd_right(a, b))
44
45def greatest(+a: Nat, +b: Nat, +d: Nat, +ka: Nat, +kb: Nat, +ea: {a == Nat.mul(ka, d) : Nat}, +eb: {b == Nat.mul(kb, d) : Nat}) -> S.Gcd.greatest(a, b, d, ka, kb, ea, eb):
46 (G.dw(b, a, b, ka, kb), G.dvd_gcd(a, b, d, ka, kb, ea, eb))
47
48def mul_left(+c: Nat, +a: Nat, +b: Nat) -> S.Gcd.mul_left(c, a, b):
49 LC.gcd_mul_left(c, a, b)
50
51def lcm_divides_left(+a: Nat, +b: Nat) -> S.Lcm.divides_left(a, b):
52 (LC.lcm_wl(a, b), LC.dvd_lcm_left(a, b))
53
54def lcm_divides_right(+a: Nat, +b: Nat) -> S.Lcm.divides_right(a, b):
55 (LC.lcm_wr(a, b), LC.dvd_lcm_right(a, b))
56
57def least(+a: Nat, +b: Nat, +m: Nat, +x: Nat, +y: Nat, +ex: {m == Nat.mul(x, a) : Nat}, +ey: {m == Nat.mul(y, b) : Nat}) -> S.Lcm.least(a, b, m, x, y, ex, ey):
58 (LC.lcm_dw(a, b, m, x, y), LC.lcm_dvd(a, b, m, x, y, ex, ey))
59
60def gcd_mul_lcm(+a: Nat, +b: Nat) -> S.Lcm.gcd_mul_lcm(a, b):
61 LC.gcd_mul_lcm(a, b)
62
63# ---- lists ----
64
65def gcd_all_divides(+xs: List<&2, Nat>, +i: Nat) -> S.GcdAll.divides(xs, i):
66 (LS.gw_nth(xs, 0n, i), LS.gcd_all_dvd(xs, i))
67
68def gcd_all_greatest(+d: Nat, +xs: List<&2, Nat>, +ks: List<&2, Nat>, h: S.dvd_with(d, xs, ks)) -> S.GcdAll.greatest(d, xs, ks, h):
69 (LS.gw_dvd(xs, ks, 0n, 0n), LS.dvd_gcd_all(d, xs, ks, h))
70
71def lcm_all_divides(+xs: List<&2, Nat>, +i: Nat) -> S.LcmAll.divides(xs, i):
72 (LS.lw_nth(xs, 1n, i), LS.dvd_lcm_all(xs, i))
73
74def lcm_all_least(+m: Nat, +xs: List<&2, Nat>, +ks: List<&2, Nat>, h: S.mul_with(m, xs, ks)) -> S.LcmAll.least(m, xs, ks, h):
75 (LS.lw_mul(m, xs, ks, 1n, m), LS.lcm_all_dvd(m, xs, ks, h))
76
77def sum_value(+xs: List<&2, Nat>) -> S.Sum.value(xs):
78 LS.sum_ok(xs)
79
80def prod_value(+xs: List<&2, Nat>) -> S.Prod.value(xs):
81 LS.prod_ok(xs)
82
83# ---- factorial, perm, comb ----
84
85def factorial_value(+n: Nat) -> S.Factorial.value(n):
86 F.factorial_ok(n)
87
88def perm_value(+n: Nat, +k: Nat) -> S.Perm.value(n, k):
89 F.perm_ok(n, k)
90
91def perm_self(+n: Nat) -> S.Perm.self(n):
92 Equal.trans(Nat, M.perm(n, n), S.desc(n, n), S.factorial(n), F.perm_ok(n, n), F.desc_self(n))
93
94def comb_value(+n: Nat, +k: Nat) -> S.Comb.value(n, k):
95 F.comb_ok(n, k)
96
97def pascal(+m: Nat, +j: Nat) -> S.Comb.pascal(m, j):
98 %Equal.sym(Nat, M.comb(m, j), S.choose(m, j), F.comb_ok(m, j)) : {M.comb(1n+m, 1n+j) == Nat.add(_, M.comb(m, 1n+j)) : Nat}
99 %Equal.sym(Nat, M.comb(m, 1n+j), S.choose(m, 1n+j), F.comb_ok(m, 1n+j)) : {M.comb(1n+m, 1n+j) == Nat.add(S.choose(m, j), _) : Nat}
100 F.comb_ok(1n+m, 1n+j)
101
102def factorials(+n: Nat, +k: Nat, +h: {Nat.is_le(k, n) == True{} : Bool}) -> S.Comb.factorials(n, k, h):
103 %Equal.sym(Nat, M.comb(n, k), S.choose(n, k), F.comb_ok(n, k)) : {Nat.mul(_, Nat.mul(S.factorial(k), S.factorial(Nat.sub(n, k)))) == S.factorial(n) : Nat}
104 F.choose_mul_facts(n, k, h)
105
106def comb_zero(+n: Nat, +k: Nat, +h: {Nat.is_lt(n, k) == True{} : Bool}) -> S.Comb.zero(n, k, h):
107 Equal.trans(Nat, M.comb(n, k), S.choose(n, k), 0n, F.comb_ok(n, k), F.choose_eq_zero(n, k, h))
108
109# ---- roots, logarithms, bits ----
110
111def isqrt_le(+n: Nat) -> S.Isqrt.le(n):
112 SQ.isqrt_le(n)
113
114def isqrt_lt_succ(+n: Nat) -> S.Isqrt.lt_succ(n):
115 SQ.lt_succ_isqrt(n)
116
117def iroot_done(+n: Nat, +kp: Nat) -> S.Iroot.done(n, kp):
118 (M.iroot_k(n, 1n+kp), RT.iroot_done(n, kp))
119
120def iroot_value(+n: Nat, +kp: Nat, +r: Nat, +h: {M.iroot(n, 1n+kp) == Done{r} : Result<&2, &2, M.MathError, Nat>}) -> {M.iroot_k(n, 1n+kp) == r : Nat}:
121 done_eq(M.iroot(n, 1n+kp), M.iroot_k(n, 1n+kp), r, RT.iroot_done(n, kp), h)
122
123def iroot_le(+n: Nat, +kp: Nat, +r: Nat, +h: {M.iroot(n, 1n+kp) == Done{r} : Result<&2, &2, M.MathError, Nat>}) -> S.Iroot.le(n, kp, r, h):
124 %iroot_value(n, kp, r, h) : {Nat.is_le(Nat.pow(_, 1n+kp), n) == True{} : Bool}
125 RT.iroot_le(n, kp)
126
127def iroot_lt_succ(+n: Nat, +kp: Nat, +r: Nat, +h: {M.iroot(n, 1n+kp) == Done{r} : Result<&2, &2, M.MathError, Nat>}) -> S.Iroot.lt_succ(n, kp, r, h):
128 %iroot_value(n, kp, r, h) : {Nat.is_lt(n, Nat.pow(1n+_, 1n+kp)) == True{} : Bool}
129 RT.lt_succ_iroot(n, kp)
130
131def zero_degree(+n: Nat) -> S.Iroot.zero_degree(n):
132 RT.iroot_zero(n)
133
134def ilog_done(+np: Nat, +bq: Nat) -> S.Ilog.done(np, bq):
135 (LG.ilog_value(np, bq), LG.ilog_done(np, bq))
136
137def ilog_value(+np: Nat, +bq: Nat, +r: Nat, +h: {M.ilog(1n+np, 2n+bq) == Done{r} : Result<&2, &2, M.MathError, Nat>}) -> {LG.ilog_value(np, bq) == r : Nat}:
138 done_eq(M.ilog(1n+np, 2n+bq), LG.ilog_value(np, bq), r, LG.ilog_done(np, bq), h)
139
140def pow_le(+np: Nat, +bq: Nat, +r: Nat, +h: {M.ilog(1n+np, 2n+bq) == Done{r} : Result<&2, &2, M.MathError, Nat>}) -> S.Ilog.pow_le(np, bq, r, h):
141 %ilog_value(np, bq, r, h) : {Nat.is_le(Nat.pow(2n+bq, _), 1n+np) == True{} : Bool}
142 LG.pow_ilog_le(np, bq)
143
144def lt_pow_succ(+np: Nat, +bq: Nat, +r: Nat, +h: {M.ilog(1n+np, 2n+bq) == Done{r} : Result<&2, &2, M.MathError, Nat>}) -> S.Ilog.lt_pow_succ(np, bq, r, h):
145 %ilog_value(np, bq, r, h) : {Nat.is_lt(1n+np, Nat.pow(2n+bq, 1n+_)) == True{} : Bool}
146 LG.lt_pow_succ_ilog(np, bq)
147
148def ilog_zero(+b: Nat) -> S.Ilog.zero(b):
149 LG.ilog_zero(b)
150
151def small_base(+n: Nat, +b: Nat, +hb: {Nat.is_lt(b, 2n) == True{} : Bool}) -> S.Ilog.small_base(n, b, hb):
152 LG.ilog_small_base(n, b, hb)
153
154def bit_length_lt(+n: Nat) -> S.BitLength.lt(n):
155 B.bit_length_lt(n)
156
157def bit_length_le(+np: Nat) -> S.BitLength.le(np):
158 B.bit_length_le(np)
159
160# ---- modular arithmetic ----
161
162def pow_mod_value(+b: Nat, +e: Nat, +mp: Nat) -> S.PowMod.value(b, e, mp):
163 MP.pow_mod_ok(b, e, mp)
164
165def pow_mod_zero_modulus(+b: Nat, +e: Nat) -> S.PowMod.zero_modulus(b, e):
166 MP.pow_mod_zero(b, e)
167
168def inverse(+a: Nat, +mp: Nat, +x: Nat, +h: {M.mod_inverse(a, 1n+mp) == Done{x} : Result<&2, &2, M.MathError, Nat>}) -> S.ModInverse.inverse(a, mp, x, h):
169 Pair.fst({Nat.mod(Nat.mul(a, x), 1n+mp) == Nat.mod(1n, 1n+mp) : Nat}, {Nat.is_lt(x, 1n+mp) == True{} : Bool}, IV.inverse_done(a, mp, x, h))
170
171def reduced(+a: Nat, +mp: Nat, +x: Nat, +h: {M.mod_inverse(a, 1n+mp) == Done{x} : Result<&2, &2, M.MathError, Nat>}) -> S.ModInverse.reduced(a, mp, x, h):
172 Pair.snd({Nat.mod(Nat.mul(a, x), 1n+mp) == Nat.mod(1n, 1n+mp) : Nat}, {Nat.is_lt(x, 1n+mp) == True{} : Bool}, IV.inverse_done(a, mp, x, h))
173
174# the shared factor g >= 2 and its two quotients, as dvd pairs
175def factor_parts(+a: Nat, +mp: Nat, +g: Nat, +ka: Nat, +km: Nat, p: {Nat.is_le(2n, g) == True{} : Bool} & ({a == Nat.mul(ka, g) : Nat} & {1n+mp == Nat.mul(km, g) : Nat})) -> {Nat.is_le(2n, g) == True{} : Bool} & (S.dvd(g, a) & S.dvd(g, 1n+mp)):
176 (hg, rest) = p
177 (ea, em) = rest
178 (hg, ((ka, ea), (km, em)))
179
180def not_coprime(+a: Nat, +mp: Nat, +h: {M.mod_inverse(a, 1n+mp) == Fail{M.NotInvertible{}} : Result<&2, &2, M.MathError, Nat>}) -> S.ModInverse.not_coprime(a, mp, h):
181 (IV.bg(IV.inv_bz(a, mp)), factor_parts(a, mp, IV.bg(IV.inv_bz(a, mp)), IV.inv_ka(a, mp), IV.inv_km(a, mp), IV.inverse_fail(a, mp, h)))
182
183def inverse_zero_modulus(+a: Nat) -> S.ModInverse.zero_modulus(a):
184 IV.inverse_zero(a)
185
186# ---- divmod and clamp ----
187
188def divmod_value(+a: Nat, +bp: Nat) -> S.DivMod.value(a, bp):
189 MS.divmod_done(a, bp)
190
191def euclid(+a: Nat, +bp: Nat) -> S.DivMod.euclid(a, bp):
192 MS.divmod_eq(a, bp)
193
194def rem_lt(+a: Nat, +bp: Nat) -> S.DivMod.rem_lt(a, bp):
195 MS.divmod_lt(a, bp)
196
197def zero_divisor(+a: Nat) -> S.DivMod.zero_divisor(a):
198 MS.divmod_zero(a)
199
200def clamp_value(+x: Nat, +lo: Nat, +hi: Nat, +h: {Nat.is_le(lo, hi) == True{} : Bool}) -> S.Clamp.value(x, lo, hi, h):
201 MS.clamp_done(x, lo, hi, h)
202
203def clamp_ge(+x: Nat, +lo: Nat, +hi: Nat, +h: {Nat.is_le(lo, hi) == True{} : Bool}) -> S.Clamp.ge(x, lo, hi, h):
204 MS.clamp_ge(x, lo, hi, h)
205
206def clamp_le(+x: Nat, +lo: Nat, +hi: Nat) -> S.Clamp.le(x, lo, hi):
207 MS.clamp_le(x, lo, hi)
208
209def clamp_id(+x: Nat, +lo: Nat, +hi: Nat, +h1: {Nat.is_le(lo, x) == True{} : Bool}, +h2: {Nat.is_le(x, hi) == True{} : Bool}) -> S.Clamp.id(x, lo, hi, h1, h2):
210 MS.clamp_id(x, lo, hi, h1, h2)
211
212def domain(+x: Nat, +lo: Nat, +hi: Nat, +h: {Nat.is_lt(hi, lo) == True{} : Bool}) -> S.Clamp.domain(x, lo, hi, h):
213 MS.clamp_domain(x, lo, hi, h)