1 import Base 2 import ../../../src/math/natural.bend as M 3 import ../../../spec/lib/common.bend as SC 4 import ../../../spec/math/natural.bend as S 5 import ./arith.bend as R 6 import ./gcd.bend as G 7 import ./lcm.bend as LC 8 import ./fact.bend as F 9 import ./bits.bend as B 10 import ./roots.bend as RT 11 import ./sqrtn.bend as SQ 12 import ./logs.bend as LG 13 import ./modpow.bend as MP 14 import ./inverse.bend as IV 15 import ./lists.bend as LS 16 import ./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 26 def 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 34 def 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 39 def 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 42 def 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 45 def 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 48 def mul_left(+c: Nat, +a: Nat, +b: Nat) -> S.Gcd.mul_left(c, a, b): 49 LC.gcd_mul_left(c, a, b) 50 51 def 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 54 def 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 57 def 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 60 def 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 65 def 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 68 def 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 71 def 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 74 def 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 77 def sum_value(+xs: List<&2, Nat>) -> S.Sum.value(xs): 78 LS.sum_ok(xs) 79 80 def prod_value(+xs: List<&2, Nat>) -> S.Prod.value(xs): 81 LS.prod_ok(xs) 82 83 # ---- factorial, perm, comb ---- 84 85 def factorial_value(+n: Nat) -> S.Factorial.value(n): 86 F.factorial_ok(n) 87 88 def perm_value(+n: Nat, +k: Nat) -> S.Perm.value(n, k): 89 F.perm_ok(n, k) 90 91 def 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 94 def comb_value(+n: Nat, +k: Nat) -> S.Comb.value(n, k): 95 F.comb_ok(n, k) 96 97 def 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 102 def 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 106 def 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 111 def isqrt_le(+n: Nat) -> S.Isqrt.le(n): 112 SQ.isqrt_le(n) 113 114 def isqrt_lt_succ(+n: Nat) -> S.Isqrt.lt_succ(n): 115 SQ.lt_succ_isqrt(n) 116 117 def iroot_done(+n: Nat, +kp: Nat) -> S.Iroot.done(n, kp): 118 (M.iroot_k(n, 1n+kp), RT.iroot_done(n, kp)) 119 120 def 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 123 def 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 127 def 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 131 def zero_degree(+n: Nat) -> S.Iroot.zero_degree(n): 132 RT.iroot_zero(n) 133 134 def ilog_done(+np: Nat, +bq: Nat) -> S.Ilog.done(np, bq): 135 (LG.ilog_value(np, bq), LG.ilog_done(np, bq)) 136 137 def 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 140 def 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 144 def 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 148 def ilog_zero(+b: Nat) -> S.Ilog.zero(b): 149 LG.ilog_zero(b) 150 151 def 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 154 def bit_length_lt(+n: Nat) -> S.BitLength.lt(n): 155 B.bit_length_lt(n) 156 157 def bit_length_le(+np: Nat) -> S.BitLength.le(np): 158 B.bit_length_le(np) 159 160 # ---- modular arithmetic ---- 161 162 def pow_mod_value(+b: Nat, +e: Nat, +mp: Nat) -> S.PowMod.value(b, e, mp): 163 MP.pow_mod_ok(b, e, mp) 164 165 def pow_mod_zero_modulus(+b: Nat, +e: Nat) -> S.PowMod.zero_modulus(b, e): 166 MP.pow_mod_zero(b, e) 167 168 def 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 171 def 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 175 def 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 180 def 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 183 def inverse_zero_modulus(+a: Nat) -> S.ModInverse.zero_modulus(a): 184 IV.inverse_zero(a) 185 186 # ---- divmod and clamp ---- 187 188 def divmod_value(+a: Nat, +bp: Nat) -> S.DivMod.value(a, bp): 189 MS.divmod_done(a, bp) 190 191 def euclid(+a: Nat, +bp: Nat) -> S.DivMod.euclid(a, bp): 192 MS.divmod_eq(a, bp) 193 194 def rem_lt(+a: Nat, +bp: Nat) -> S.DivMod.rem_lt(a, bp): 195 MS.divmod_lt(a, bp) 196 197 def zero_divisor(+a: Nat) -> S.DivMod.zero_divisor(a): 198 MS.divmod_zero(a) 199 200 def 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 203 def 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 206 def clamp_le(+x: Nat, +lo: Nat, +hi: Nat) -> S.Clamp.le(x, lo, hi): 207 MS.clamp_le(x, lo, hi) 208 209 def 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 212 def 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)