1 import Base 2 import ../../../spec/lib/common.bend as C 3 import ../../../spec/math/generic.bend as SG 4 import ../../../spec/math/natural.bend as NS 5 import ../../../src/math/generic.bend as G 6 import ../../../src/math/num.bend as NM 7 import ../../../src/math/natural.bend as M 8 import ../../../src/math/instances.bend as I 9 import ../../lib/nat.bend as N 10 import ../../lib/logic.bend as L 11 import ../../lib/lemmas/proofs/nat_algebra.bend as NA 12 import ../natural/arith.bend as NR 13 import ./width.bend as WW 14 import ./u32.bend as U32P 15 import ./u32laws.bend as LW 16 import ./u32mont.bend as MO 17 import ../../../src/math/w64.bend as X 18 import ./natfuel.bend as NF 19 import ./combnat.bend as CN 20 import ../../lib/arith.bend as AR2 21 import ../natural/fact.bend as FA 22 import ../natural/roots.bend as RT 23 import ../../../src/math/pow2.bend as P2 24 import ../pow2/pow2.bend as PP 25 import ../../../spec/math/natural.bend as S 26 import ../natural/inverse.bend as IV 27 import ../natural/proof.bend as NP 28 29 # The integer clauses of spec/math/generic.bend at the U32 instance, proved 30 # from the instance laws of spec/math/instances.bend (proofs/math/typed/ 31 # u32laws.bend): each generic function is simulated on the values and 32 # compared with the proved Nat function of natural.bend, as Mathlib proves a 33 # function on a type through its value (Mathlib's Fin / UInt32 lemmas via 34 # toNat). The same text, read with the U64 laws, proves them at U64. 35 36 def v(+x: U32) -> Nat: 37 SG.u32_val(x) 38 39 def of(+n: Nat) -> U32: 40 SG.u32_of(n) 41 42 # x is the U32 of its value 43 def as_of(+x: U32, +n: Nat, +h: {v(x) == n : Nat}) -> {x == of(n) : U32}: 44 Equal.trans(U32, x, of(v(x)), of(n), Equal.sym(U32, of(v(x)), x, LW.rt(x)), Equal.cong(Nat, U32, t => of(t), v(x), n, h)) 45 46 def true_ne_false(+h: {True{} == False{} : Bool}) -> Empty: 47 U32P.true_ne_false(h) 48 49 # ---- isqrt, abs ---- 50 51 def isqrt_agrees(+n: U32) -> SG.Isqrt.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, n): 52 as_of(I.u32_op(NM.Sqrt{n}), M.isqrt(v(n)), LW.ops_sqrt(n)) 53 54 def abs_identity(+x: U32) -> SG.Abs.identity(~U32, ~I.u32_op, ~I.u32_is, x): 55 LW.ops_abs(x) 56 57 # ---- divmod ---- 58 59 def dm(+a: U32, +b: U32, +c: Bool, +hc: {I.u32_is(NM.IsZero{b}) == c : Bool}, +nb: Nat, +hnb: {v(b) == nb : Nat}) -> {G.divmod_ok(~U32, ~I.u32_op, a, b, c) == SG.lift_qr(~U32, ~SG.u32_of, M.divmod(v(a), nb)) : Result<&2, &2, NM.NumError, G.QuotRem>}: 60 match c nb: 61 case True{} 0n: 62 {==} 63 case False{} 0n: 64 +hz = Equal.trans(Bool, False{}, I.u32_is(NM.IsZero{b}), Nat.is_eq(0n, 0n), Equal.sym(Bool, I.u32_is(NM.IsZero{b}), False{}, hc), Equal.trans(Bool, I.u32_is(NM.IsZero{b}), Nat.is_eq(v(b), 0n), Nat.is_eq(0n, 0n), LW.tests_is_zero(b), Equal.cong(Nat, Bool, t => Nat.is_eq(t, 0n), v(b), 0n, hnb))) 65 Empty.absurd({G.divmod_ok(~U32, ~I.u32_op, a, b, False{}) == SG.lift_qr(~U32, ~SG.u32_of, M.divmod(v(a), 0n)) : Result<&2, &2, NM.NumError, G.QuotRem>}, true_ne_false(Equal.sym(Bool, False{}, True{}, hz))) 66 case True{} 1n+ +bp: 67 +hz = Equal.trans(Bool, True{}, I.u32_is(NM.IsZero{b}), Nat.is_eq(1n+bp, 0n), Equal.sym(Bool, I.u32_is(NM.IsZero{b}), True{}, hc), Equal.trans(Bool, I.u32_is(NM.IsZero{b}), Nat.is_eq(v(b), 0n), Nat.is_eq(1n+bp, 0n), LW.tests_is_zero(b), Equal.cong(Nat, Bool, t => Nat.is_eq(t, 0n), v(b), 1n+bp, hnb))) 68 Empty.absurd({G.divmod_ok(~U32, ~I.u32_op, a, b, True{}) == SG.lift_qr(~U32, ~SG.u32_of, M.divmod(v(a), 1n+bp)) : Result<&2, &2, NM.NumError, G.QuotRem>}, true_ne_false(hz)) 69 case False{} 1n+ +bp: 70 +hq = Equal.trans(Bool, Nat.is_eq(v(b), 0n), Nat.is_eq(1n+bp, 0n), False{}, Equal.cong(Nat, Bool, t => Nat.is_eq(t, 0n), v(b), 1n+bp, hnb), {==}) 71 +eq = as_of(I.u32_op(NM.Quot{a, b}), Nat.div(v(a), 1n+bp), Equal.trans(Nat, v(I.u32_op(NM.Quot{a, b})), Nat.div(v(a), v(b)), Nat.div(v(a), 1n+bp), LW.ops_quot(a, b, hq), Equal.cong(Nat, Nat, t => Nat.div(v(a), t), v(b), 1n+bp, hnb))) 72 +er = as_of(I.u32_op(NM.Rem{a, b}), Nat.mod(v(a), 1n+bp), Equal.trans(Nat, v(I.u32_op(NM.Rem{a, b})), Nat.mod(v(a), v(b)), Nat.mod(v(a), 1n+bp), LW.ops_rem(a, b, hq), Equal.cong(Nat, Nat, t => Nat.mod(v(a), t), v(b), 1n+bp, hnb))) 73 %Equal.sym(U32, I.u32_op(NM.Quot{a, b}), of(Nat.div(v(a), 1n+bp)), eq) : {Done{G.TQR{_, I.u32_op(NM.Rem{a, b})}} == Done{G.TQR{of(Nat.div(v(a), 1n+bp)), of(Nat.mod(v(a), 1n+bp))}} : Result<&2, &2, NM.NumError, G.QuotRem>} 74 %Equal.sym(U32, I.u32_op(NM.Rem{a, b}), of(Nat.mod(v(a), 1n+bp)), er) : {Done{G.TQR{of(Nat.div(v(a), 1n+bp)), _}} == Done{G.TQR{of(Nat.div(v(a), 1n+bp)), of(Nat.mod(v(a), 1n+bp))}} : Result<&2, &2, NM.NumError, G.QuotRem>} 75 {==} 76 77 def divmod_agrees(+a: U32, +b: U32) -> SG.DivMod.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, a, b): 78 dm(a, b, I.u32_is(NM.IsZero{b}), {==}, v(b), {==}) 79 80 # ---- selections ---- 81 82 def lt_of(+a: U32, +b: U32, +c: Bool, +hc: {I.u32_is(NM.Lt{a, b}) == c : Bool}) -> {Nat.is_lt(v(a), v(b)) == c : Bool}: 83 Equal.trans(Bool, Nat.is_lt(v(a), v(b)), I.u32_is(NM.Lt{a, b}), c, Equal.sym(Bool, I.u32_is(NM.Lt{a, b}), Nat.is_lt(v(a), v(b)), LW.tests_lt(a, b)), hc) 84 85 def min_c(+a: U32, +b: U32, +c: Bool, +hc: {I.u32_is(NM.Lt{b, a}) == c : Bool}) -> {G.pick(U32, c, b, a) == of(Nat.min(v(a), v(b))) : U32}: 86 match c: 87 case True{}: 88 as_of(b, Nat.min(v(a), v(b)), Equal.sym(Nat, Nat.min(v(a), v(b)), v(b), U32P.min_of_lt(v(a), v(b), lt_of(b, a, True{}, hc)))) 89 case False{}: 90 as_of(a, Nat.min(v(a), v(b)), Equal.sym(Nat, Nat.min(v(a), v(b)), v(a), U32P.min_of_ge(v(a), v(b), lt_of(b, a, False{}, hc)))) 91 92 def min_agrees(+a: U32, +b: U32) -> SG.Min.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, a, b): 93 min_c(a, b, I.u32_is(NM.Lt{b, a}), {==}) 94 95 def max_c(+a: U32, +b: U32, +c: Bool, +hc: {I.u32_is(NM.Lt{a, b}) == c : Bool}) -> {G.pick(U32, c, b, a) == of(Nat.max(v(a), v(b))) : U32}: 96 match c: 97 case True{}: 98 as_of(b, Nat.max(v(a), v(b)), Equal.sym(Nat, Nat.max(v(a), v(b)), v(b), U32P.max_of_lt(v(a), v(b), lt_of(a, b, True{}, hc)))) 99 case False{}: 100 as_of(a, Nat.max(v(a), v(b)), Equal.sym(Nat, Nat.max(v(a), v(b)), v(a), U32P.max_of_ge(v(a), v(b), lt_of(a, b, False{}, hc)))) 101 102 def max_agrees(+a: U32, +b: U32) -> SG.Max.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, a, b): 103 max_c(a, b, I.u32_is(NM.Lt{a, b}), {==}) 104 105 def max_val_c(+x: U32, +lo: U32, +c: Bool, +hc: {I.u32_is(NM.Lt{x, lo}) == c : Bool}) -> {v(G.pick(U32, c, lo, x)) == Nat.max(v(x), v(lo)) : Nat}: 106 match c: 107 case True{}: 108 Equal.sym(Nat, Nat.max(v(x), v(lo)), v(lo), U32P.max_of_lt(v(x), v(lo), lt_of(x, lo, True{}, hc))) 109 case False{}: 110 Equal.sym(Nat, Nat.max(v(x), v(lo)), v(x), U32P.max_of_ge(v(x), v(lo), lt_of(x, lo, False{}, hc))) 111 112 def zero_v() -> {v(I.u32_op(NM.ZeroOp{})) == 0n : Nat}: 113 LW.ops_zero() 114 115 def one_v() -> {v(I.u32_op(NM.One{})) == 1n : Nat}: 116 LW.ops_one() 117 118 def sign_b(+x: U32, +c: Bool, +hc: {I.u32_is(NM.Lt{x, I.u32_op(NM.ZeroOp{})}) == c : Bool}, +hz: {Nat.is_lt(0n, v(x)) == False{} : Bool}) -> {G.sign_below(~U32, ~I.u32_op, ~I.u32_is, x, c) == of(Nat.min(v(x), 1n)) : U32}: 119 match c: 120 case True{}: 121 +hl = L.subst(Nat, z => {Nat.is_lt(v(x), z) == True{} : Bool}, v(I.u32_op(NM.ZeroOp{})), 0n, zero_v(), lt_of(x, I.u32_op(NM.ZeroOp{}), True{}, hc)) 122 Empty.absurd({G.sign_below(~U32, ~I.u32_op, ~I.u32_is, x, True{}) == of(Nat.min(v(x), 1n)) : U32}, N.lt_zero_absurd(v(x), hl)) 123 case False{}: 124 as_of(x, Nat.min(v(x), 1n), Equal.sym(Nat, Nat.min(v(x), 1n), v(x), N.min_left(v(x), 1n, U32P.zero_lt_one(v(x), hz)))) 125 126 def sign_a(+x: U32, +c: Bool, +hc: {I.u32_is(NM.Lt{I.u32_op(NM.ZeroOp{}), x}) == c : Bool}) -> {G.sign_above(~U32, ~I.u32_op, ~I.u32_is, x, c) == of(Nat.min(v(x), 1n)) : U32}: 127 match c: 128 case True{}: 129 +hl = L.subst(Nat, z => {Nat.is_lt(z, v(x)) == True{} : Bool}, v(I.u32_op(NM.ZeroOp{})), 0n, zero_v(), lt_of(I.u32_op(NM.ZeroOp{}), x, True{}, hc)) 130 +em = N.min_right(v(x), 1n, U32P.pos_ge_one(v(x), hl)) 131 Equal.trans(U32, I.u32_op(NM.One{}), of(1n), of(Nat.min(v(x), 1n)), as_of(I.u32_op(NM.One{}), 1n, one_v()), Equal.cong(Nat, U32, t => of(t), 1n, Nat.min(v(x), 1n), Equal.sym(Nat, Nat.min(v(x), 1n), 1n, em))) 132 case False{}: 133 +hl = L.subst(Nat, z => {Nat.is_lt(z, v(x)) == False{} : Bool}, v(I.u32_op(NM.ZeroOp{})), 0n, zero_v(), lt_of(I.u32_op(NM.ZeroOp{}), x, False{}, hc)) 134 sign_b(x, I.u32_is(NM.Lt{x, I.u32_op(NM.ZeroOp{})}), {==}, hl) 135 136 def sign_agrees(+x: U32) -> SG.Sign.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, x): 137 sign_a(x, I.u32_is(NM.Lt{I.u32_op(NM.ZeroOp{}), x}), {==}) 138 139 def clamp_d(+x: U32, +lo: U32, +hi: U32, +c: Bool) -> {G.clamp_ok(~U32, ~I.u32_op, ~I.u32_is, x, lo, hi, c) == SG.lift(~U32, ~SG.u32_of, M.clamp_ok(v(x), v(lo), v(hi), c)) : Result<&2, &2, NM.NumError, U32>}: 140 match c: 141 case True{}: 142 {==} 143 case False{}: 144 +m = G.max(~U32, ~I.u32_op, ~I.u32_is, x, lo) 145 +em = max_val_c(x, lo, I.u32_is(NM.Lt{x, lo}), {==}) 146 %Equal.sym(U32, G.pick(U32, I.u32_is(NM.Lt{hi, m}), hi, m), of(Nat.min(v(m), v(hi))), min_c(m, hi, I.u32_is(NM.Lt{hi, m}), {==})) : {Done{_} == Done{of(Nat.min(Nat.max(v(x), v(lo)), v(hi)))} : Result<&2, &2, NM.NumError, U32>} 147 %Equal.sym(Nat, v(m), Nat.max(v(x), v(lo)), em) : {Done{of(Nat.min(_, v(hi)))} == Done{of(Nat.min(Nat.max(v(x), v(lo)), v(hi)))} : Result<&2, &2, NM.NumError, U32>} 148 {==} 149 150 def clamp_c(+x: U32, +lo: U32, +hi: U32, +c: Bool, +hc: {I.u32_is(NM.Lt{hi, lo}) == c : Bool}) -> {G.clamp_ok(~U32, ~I.u32_op, ~I.u32_is, x, lo, hi, c) == SG.lift(~U32, ~SG.u32_of, M.clamp(v(x), v(lo), v(hi))) : Result<&2, &2, NM.NumError, U32>}: 151 %Equal.sym(Bool, Nat.is_lt(v(hi), v(lo)), c, lt_of(hi, lo, c, hc)) : {G.clamp_ok(~U32, ~I.u32_op, ~I.u32_is, x, lo, hi, c) == SG.lift(~U32, ~SG.u32_of, M.clamp_ok(v(x), v(lo), v(hi), _)) : Result<&2, &2, NM.NumError, U32>} 152 clamp_d(x, lo, hi, c) 153 154 def clamp_agrees(+x: U32, +lo: U32, +hi: U32) -> SG.Clamp.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, x, lo, hi): 155 clamp_c(x, lo, hi, I.u32_is(NM.Lt{hi, lo}), {==}) 156 157 # ---- gcd: Euclid on the values, then enough fuel ---- 158 159 def gcd_sim(+f: Nat, +a: U32, +b: U32, +cz: Bool, +nb: Nat, +hcz: {I.u32_is(NM.IsZero{b}) == cz : Bool}, +hnb: {v(b) == nb : Nat}) -> {v(G.gcd_go(~U32, ~I.u32_op, ~I.u32_is, f, a, (b, cz))) == M.gcd_go(f, v(a), nb) : Nat}: 160 match f cz nb: 161 case 0n _ _: 162 {==} 163 case 1n+g True{} 0n: 164 {==} 165 case 1n+g True{} 1n+bp: 166 +hz = Equal.trans(Bool, True{}, I.u32_is(NM.IsZero{b}), Nat.is_eq(1n+bp, 0n), Equal.sym(Bool, I.u32_is(NM.IsZero{b}), True{}, hcz), Equal.trans(Bool, I.u32_is(NM.IsZero{b}), Nat.is_eq(v(b), 0n), Nat.is_eq(1n+bp, 0n), LW.tests_is_zero(b), Equal.cong(Nat, Bool, t => Nat.is_eq(t, 0n), v(b), 1n+bp, hnb))) 167 Empty.absurd({v(G.gcd_go(~U32, ~I.u32_op, ~I.u32_is, 1n+g, a, (b, True{}))) == M.gcd_go(1n+g, v(a), 1n+bp) : Nat}, true_ne_false(hz)) 168 case 1n+g False{} 0n: 169 +hz = Equal.trans(Bool, False{}, I.u32_is(NM.IsZero{b}), Nat.is_eq(0n, 0n), Equal.sym(Bool, I.u32_is(NM.IsZero{b}), False{}, hcz), Equal.trans(Bool, I.u32_is(NM.IsZero{b}), Nat.is_eq(v(b), 0n), Nat.is_eq(0n, 0n), LW.tests_is_zero(b), Equal.cong(Nat, Bool, t => Nat.is_eq(t, 0n), v(b), 0n, hnb))) 170 Empty.absurd({v(G.gcd_go(~U32, ~I.u32_op, ~I.u32_is, 1n+g, a, (b, False{}))) == M.gcd_go(1n+g, v(a), 0n) : Nat}, true_ne_false(Equal.sym(Bool, False{}, True{}, hz))) 171 case 1n+ +g False{} 1n+ +bp: 172 +rm = I.u32_op(NM.Rem{a, b}) 173 +hq = Equal.trans(Bool, Nat.is_eq(v(b), 0n), Nat.is_eq(1n+bp, 0n), False{}, Equal.cong(Nat, Bool, t => Nat.is_eq(t, 0n), v(b), 1n+bp, hnb), {==}) 174 +erm = Equal.trans(Nat, v(rm), Nat.mod(v(a), v(b)), Nat.mod(v(a), 1n+bp), LW.ops_rem(a, b, hq), Equal.cong(Nat, Nat, t => Nat.mod(v(a), t), v(b), 1n+bp, hnb)) 175 +ih = gcd_sim(g, b, rm, I.u32_is(NM.IsZero{rm}), v(rm), {==}, {==}) 176 Equal.trans(Nat, v(G.gcd_go(~U32, ~I.u32_op, ~I.u32_is, g, b, (rm, I.u32_is(NM.IsZero{rm})))), M.gcd_go(g, v(b), v(rm)), M.gcd_go(g, 1n+bp, Nat.mod(v(a), 1n+bp)), ih, Equal.trans(Nat, M.gcd_go(g, v(b), v(rm)), M.gcd_go(g, 1n+bp, v(rm)), M.gcd_go(g, 1n+bp, Nat.mod(v(a), 1n+bp)), Equal.cong(Nat, Nat, t => M.gcd_go(g, t, v(rm)), v(b), 1n+bp, hnb), Equal.cong(Nat, Nat, t => M.gcd_go(g, 1n+bp, t), v(rm), Nat.mod(v(a), 1n+bp), erm))) 177 178 def gcd_val_k(+k: Nat, +hk: {k == 32n : Nat}, +a: U32, +b: U32) -> {v(G.gcd(~U32, ~I.u32_op, ~I.u32_is, a, b)) == M.gcd(v(a), v(b)) : Nat}: 179 +hk2 = L.subst(Nat, z => {Nat.is_le(1n+Nat.double(z), 140n) == True{} : Bool}, 32n, k, Equal.sym(Nat, k, 32n, hk), {==}) 180 Equal.trans(Nat, v(G.gcd(~U32, ~I.u32_op, ~I.u32_is, a, b)), M.gcd_go(140n, v(a), v(b)), M.gcd(v(a), v(b)), gcd_sim(140n, a, b, I.u32_is(NM.IsZero{b}), v(b), {==}, {==}), NF.gcd_140(k, v(a), v(b), hk2, U32P.val_lt(1n, {==}, k, hk, b))) 181 182 def gcd_val(+a: U32, +b: U32) -> {v(G.gcd(~U32, ~I.u32_op, ~I.u32_is, a, b)) == M.gcd(v(a), v(b)) : Nat}: 183 gcd_val_k(32n, {==}, a, b) 184 185 def gcd_agrees(+a: U32, +b: U32) -> SG.Gcd.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, a, b): 186 as_of(G.gcd(~U32, ~I.u32_op, ~I.u32_is, a, b), M.gcd(v(a), v(b)), gcd_val(a, b)) 187 188 # ---- gcd_all: the fold on values ---- 189 190 def vals(xs: List<&2, U32>) -> List<&2, Nat>: 191 SG.vals(~U32, ~SG.u32_val, xs) 192 193 def gall(+xs: List<&2, U32>, +acc: U32) -> {v(G.gcd_all_go(~U32, ~I.u32_op, ~I.u32_is, xs, acc)) == M.gcd_all_go(vals(xs), v(acc)) : Nat}: 194 match xs: 195 case Nil{}: 196 {==} 197 case Con{+x, +t}: 198 +g = G.gcd(~U32, ~I.u32_op, ~I.u32_is, acc, x) 199 Equal.trans(Nat, v(G.gcd_all_go(~U32, ~I.u32_op, ~I.u32_is, t, g)), M.gcd_all_go(vals(t), v(g)), M.gcd_all_go(vals(t), M.gcd(v(acc), v(x))), gall(t, g), Equal.cong(Nat, Nat, z => M.gcd_all_go(vals(t), z), v(g), M.gcd(v(acc), v(x)), gcd_val(acc, x))) 200 201 def gcd_all_agrees(+xs: List<&2, U32>) -> SG.GcdAll.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, xs): 202 +z = I.u32_op(NM.ZeroOp{}) 203 as_of(G.gcd_all(~U32, ~I.u32_op, ~I.u32_is, xs), M.gcd_all(vals(xs)), Equal.trans(Nat, v(G.gcd_all_go(~U32, ~I.u32_op, ~I.u32_is, xs, z)), M.gcd_all_go(vals(xs), v(z)), M.gcd_all_go(vals(xs), 0n), gall(xs, z), Equal.cong(Nat, Nat, t => M.gcd_all_go(vals(xs), t), v(z), 0n, zero_v()))) 204 205 # ---- a checked product ---- 206 207 def mo_of(+q: U32, +b: U32, +n: Nat, +hn: {Nat.mul(v(q), v(b)) == n : Nat}, +c: Bool, +hc: {C.fits(32n, n) == c : Bool}) -> {I.u32_is(NM.MulOver{q, b}) == Bool.not(c) : Bool}: 208 +e1 = Equal.trans(Bool, I.u32_is(NM.MulOver{q, b}), Bool.not(C.fits(32n, Nat.mul(v(q), v(b)))), Bool.not(C.fits(32n, n)), LW.tests_mul_over(q, b), Equal.cong(Nat, Bool, t => Bool.not(C.fits(32n, t)), Nat.mul(v(q), v(b)), n, hn)) 209 Equal.trans(Bool, I.u32_is(NM.MulOver{q, b}), Bool.not(C.fits(32n, n)), Bool.not(c), e1, Equal.cong(Bool, Bool, t => Bool.not(t), C.fits(32n, n), c, hc)) 210 211 def cm(+q: U32, +b: U32, +n: Nat, +hn: {Nat.mul(v(q), v(b)) == n : Nat}, +c: Bool, +hc: {C.fits(32n, n) == c : Bool}) -> {G.ok(U32, G.cmul(~U32, ~I.u32_op, ~I.u32_is, q, b)) == SG.checked(~U32, ~SG.u32_of, 32n, n) : Result<&2, &2, NM.NumError, U32>}: 212 match c: 213 case True{}: 214 +hmo2 = mo_of(q, b, n, hn, True{}, hc) 215 %Equal.sym(Bool, I.u32_is(NM.MulOver{q, b}), False{}, hmo2) : {G.ok(U32, G.fits(U32, _, I.u32_op(NM.Mul{q, b}))) == SG.checked(~U32, ~SG.u32_of, 32n, n) : Result<&2, &2, NM.NumError, U32>} 216 %Equal.sym(Bool, C.fits(32n, n), True{}, hc) : {Done{I.u32_op(NM.Mul{q, b})} == SG.checked_pick(~U32, ~SG.u32_of, n, _) : Result<&2, &2, NM.NumError, U32>} 217 %Equal.sym(U32, I.u32_op(NM.Mul{q, b}), of(n), as_of(I.u32_op(NM.Mul{q, b}), n, Equal.trans(Nat, v(I.u32_op(NM.Mul{q, b})), Nat.mul(v(q), v(b)), n, LW.ops_mul(q, b, hmo2), hn))) : {Done{_} == Done{of(n)} : Result<&2, &2, NM.NumError, U32>} 218 {==} 219 case False{}: 220 +hmo = mo_of(q, b, n, hn, False{}, hc) 221 %Equal.sym(Bool, I.u32_is(NM.MulOver{q, b}), True{}, hmo) : {G.ok(U32, G.fits(U32, _, I.u32_op(NM.Mul{q, b}))) == SG.checked(~U32, ~SG.u32_of, 32n, n) : Result<&2, &2, NM.NumError, U32>} 222 %Equal.sym(Bool, C.fits(32n, n), False{}, hc) : {Fail{NM.Overflow{}} == SG.checked_pick(~U32, ~SG.u32_of, n, _) : Result<&2, &2, NM.NumError, U32>} 223 {==} 224 225 # ---- lcm ---- 226 227 def gpos_d(+ap: Nat, +b: Nat, d: NS.dvd(M.gcd(1n+ap, b), 1n+ap), +g: Nat, +hg: {M.gcd(1n+ap, b) == g : Nat}) -> {Nat.is_eq(M.gcd(1n+ap, b), 0n) == False{} : Bool}: 228 (k, e) = d 229 match g: 230 case 0n: 231 +e0 = Equal.trans(Nat, 1n+ap, Nat.mul(k, M.gcd(1n+ap, b)), 0n, e, Equal.trans(Nat, Nat.mul(k, M.gcd(1n+ap, b)), Nat.mul(k, 0n), 0n, Equal.cong(Nat, Nat, t => Nat.mul(k, t), M.gcd(1n+ap, b), 0n, hg), NA.mul_zero(k))) 232 Empty.absurd({Nat.is_eq(M.gcd(1n+ap, b), 0n) == False{} : Bool}, N.succ_zero(ap, e0)) 233 case 1n+gp: 234 %Equal.sym(Nat, M.gcd(1n+ap, b), 1n+gp, hg) : {Nat.is_eq(_, 0n) == False{} : Bool} 235 {==} 236 237 # gcd of a positive number is positive 238 def gpos(+ap: Nat, +b: Nat) -> {Nat.is_eq(M.gcd(1n+ap, b), 0n) == False{} : Bool}: 239 gpos_d(ap, b, NP.divides_left(1n+ap, b), M.gcd(1n+ap, b), {==}) 240 241 def iz(+a: U32, +n: Nat, +h: {v(a) == n : Nat}) -> {I.u32_is(NM.IsZero{a}) == Nat.is_eq(n, 0n) : Bool}: 242 Equal.trans(Bool, I.u32_is(NM.IsZero{a}), Nat.is_eq(v(a), 0n), Nat.is_eq(n, 0n), LW.tests_is_zero(a), Equal.cong(Nat, Bool, t => Nat.is_eq(t, 0n), v(a), n, h)) 243 244 def lcmc(+a: U32, +b: U32, +c: Bool, +na: Nat, +nb: Nat, +hc: {Bool.or(I.u32_is(NM.IsZero{a}), I.u32_is(NM.IsZero{b})) == c : Bool}, +hna: {v(a) == na : Nat}, +hnb: {v(b) == nb : Nat}) -> {G.lcm_ok(~U32, ~I.u32_op, ~I.u32_is, a, b, c) == SG.checked(~U32, ~SG.u32_of, 32n, M.lcm(na, nb)) : Result<&2, &2, NM.NumError, U32>}: 245 match c na nb: 246 case True{} 0n _: 247 Equal.cong(U32, Result<&2, &2, NM.NumError, U32>, t => Done{t}, I.u32_op(NM.ZeroOp{}), of(0n), as_of(I.u32_op(NM.ZeroOp{}), 0n, zero_v())) 248 case True{} 1n+ap 0n: 249 Equal.cong(U32, Result<&2, &2, NM.NumError, U32>, t => Done{t}, I.u32_op(NM.ZeroOp{}), of(0n), as_of(I.u32_op(NM.ZeroOp{}), 0n, zero_v())) 250 case True{} 1n+ +ap 1n+ +bp: 251 Empty.absurd({G.lcm_ok(~U32, ~I.u32_op, ~I.u32_is, a, b, True{}) == SG.checked(~U32, ~SG.u32_of, 32n, M.lcm(1n+ap, 1n+bp)) : Result<&2, &2, NM.NumError, U32>}, true_ne_false(Equal.trans(Bool, True{}, Bool.or(False{}, I.u32_is(NM.IsZero{b})), False{}, Equal.sym(Bool, Bool.or(False{}, I.u32_is(NM.IsZero{b})), True{}, L.subst(Bool, t => {Bool.or(t, I.u32_is(NM.IsZero{b})) == True{} : Bool}, I.u32_is(NM.IsZero{a}), False{}, iz(a, 1n+ap, hna), hc)), iz(b, 1n+bp, hnb)))) 252 case False{} 0n _: 253 Empty.absurd({G.lcm_ok(~U32, ~I.u32_op, ~I.u32_is, a, b, False{}) == SG.checked(~U32, ~SG.u32_of, 32n, M.lcm(0n, nb)) : Result<&2, &2, NM.NumError, U32>}, true_ne_false(Equal.trans(Bool, True{}, Bool.or(True{}, I.u32_is(NM.IsZero{b})), False{}, {==}, L.subst(Bool, t => {Bool.or(t, I.u32_is(NM.IsZero{b})) == False{} : Bool}, I.u32_is(NM.IsZero{a}), True{}, iz(a, 0n, hna), hc)))) 254 case False{} 1n+ +ap 0n: 255 +h2 = L.subst(Bool, t => {Bool.or(t, I.u32_is(NM.IsZero{b})) == False{} : Bool}, I.u32_is(NM.IsZero{a}), False{}, iz(a, 1n+ap, hna), hc) 256 Empty.absurd({G.lcm_ok(~U32, ~I.u32_op, ~I.u32_is, a, b, False{}) == SG.checked(~U32, ~SG.u32_of, 32n, M.lcm(1n+ap, 0n)) : Result<&2, &2, NM.NumError, U32>}, true_ne_false(Equal.trans(Bool, True{}, I.u32_is(NM.IsZero{b}), False{}, Equal.sym(Bool, I.u32_is(NM.IsZero{b}), True{}, iz(b, 0n, hnb)), h2))) 257 case False{} 1n+ +ap 1n+ +bp: 258 +g = G.gcd(~U32, ~I.u32_op, ~I.u32_is, a, b) 259 +gg = M.gcd(1n+ap, 1n+bp) 260 +eg = Equal.trans(Nat, v(g), M.gcd(v(a), v(b)), gg, gcd_val(a, b), Equal.trans(Nat, M.gcd(v(a), v(b)), M.gcd(1n+ap, v(b)), gg, Equal.cong(Nat, Nat, t => M.gcd(t, v(b)), v(a), 1n+ap, hna), Equal.cong(Nat, Nat, t => M.gcd(1n+ap, t), v(b), 1n+bp, hnb))) 261 +hgz = L.subst(Nat, t => {Nat.is_eq(t, 0n) == False{} : Bool}, gg, v(g), Equal.sym(Nat, v(g), gg, eg), gpos(ap, 1n+bp)) 262 +q = I.u32_op(NM.Quot{a, g}) 263 +eq = Equal.trans(Nat, v(q), Nat.div(v(a), v(g)), Nat.div(1n+ap, gg), LW.ops_quot(a, g, hgz), Equal.trans(Nat, Nat.div(v(a), v(g)), Nat.div(1n+ap, v(g)), Nat.div(1n+ap, gg), Equal.cong(Nat, Nat, t => Nat.div(t, v(g)), v(a), 1n+ap, hna), Equal.cong(Nat, Nat, t => Nat.div(1n+ap, t), v(g), gg, eg))) 264 +n = Nat.mul(Nat.div(1n+ap, gg), 1n+bp) 265 +hn = Equal.trans(Nat, Nat.mul(v(q), v(b)), Nat.mul(Nat.div(1n+ap, gg), v(b)), n, Equal.cong(Nat, Nat, t => Nat.mul(t, v(b)), v(q), Nat.div(1n+ap, gg), eq), Equal.cong(Nat, Nat, t => Nat.mul(Nat.div(1n+ap, gg), t), v(b), 1n+bp, hnb)) 266 cm(q, b, n, hn, C.fits(32n, n), {==}) 267 268 def lcm_checked(+a: U32, +b: U32) -> SG.Lcm.checked(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 32n, a, b): 269 lcmc(a, b, Bool.or(I.u32_is(NM.IsZero{a}), I.u32_is(NM.IsZero{b})), v(a), v(b), {==}, {==}, {==}) 270 271 # ---- lcm_all: the fold stops at the first overflow ---- 272 273 def lall_fail(xs: List<&2, U32>, +e: NM.NumError) -> {G.lcm_all_go(~U32, ~I.u32_op, ~I.u32_is, xs, Fail{e}) == Fail{e} : Result<&2, &2, NM.NumError, U32>}: 274 match xs: 275 case Nil{}: 276 {==} 277 case Con{x, t}: 278 {==} 279 280 def lgo_false(xs: List<&2, Nat>, +acc: Nat) -> {SG.lcm_go(32n, xs, acc, False{}) == (acc, False{}) : Nat & Bool}: 281 match xs: 282 case Nil{}: 283 {==} 284 case Con{x, t}: 285 {==} 286 287 # the fold on an accumulator r == checked(n) (c == fits(32, n)) 288 def lall(+xs: List<&2, U32>, +r: Result<&2, &2, NM.NumError, U32>, +n: Nat, +c: Bool, +hr: {r == SG.checked_pick(~U32, ~SG.u32_of, n, c) : Result<&2, &2, NM.NumError, U32>}, +hc: {C.fits(32n, n) == c : Bool}) -> {G.lcm_all_go(~U32, ~I.u32_op, ~I.u32_is, xs, r) == SG.prefix_fin(~U32, ~SG.u32_of, SG.lcm_go(32n, vals(xs), n, c)) : Result<&2, &2, NM.NumError, U32>}: 289 match xs c: 290 case Nil{} _: 291 hr 292 case Con{x, t} False{}: 293 %Equal.sym(Result<&2, &2, NM.NumError, U32>, r, Fail{NM.Overflow{}}, hr) : {G.lcm_all_go(~U32, ~I.u32_op, ~I.u32_is, Con{x, t}, _) == Fail{NM.Overflow{}} : Result<&2, &2, NM.NumError, U32>} 294 {==} 295 case Con{+x, +t} True{}: 296 %Equal.sym(Result<&2, &2, NM.NumError, U32>, r, Done{of(n)}, hr) : {G.lcm_all_go(~U32, ~I.u32_op, ~I.u32_is, Con{x, t}, _) == SG.prefix_fin(~U32, ~SG.u32_of, SG.lcm_go(32n, vals(t), M.lcm(n, v(x)), C.fits(32n, M.lcm(n, v(x))))) : Result<&2, &2, NM.NumError, U32>} 297 +en = LW.vo(n, hc) 298 +el = Equal.trans(Result<&2, &2, NM.NumError, U32>, G.lcm(~U32, ~I.u32_op, ~I.u32_is, of(n), x), SG.checked(~U32, ~SG.u32_of, 32n, M.lcm(v(of(n)), v(x))), SG.checked(~U32, ~SG.u32_of, 32n, M.lcm(n, v(x))), lcm_checked(of(n), x), Equal.cong(Nat, Result<&2, &2, NM.NumError, U32>, z => SG.checked(~U32, ~SG.u32_of, 32n, M.lcm(z, v(x))), v(of(n)), n, en)) 299 lall(t, G.lcm(~U32, ~I.u32_op, ~I.u32_is, of(n), x), M.lcm(n, v(x)), C.fits(32n, M.lcm(n, v(x))), el, {==}) 300 301 def lcm_all_checked(+xs: List<&2, U32>) -> SG.LcmAll.checked(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 32n, xs): 302 lall(xs, Done{I.u32_op(NM.One{})}, 1n, True{}, Equal.cong(U32, Result<&2, &2, NM.NumError, U32>, t => Done{t}, I.u32_op(NM.One{}), of(1n), as_of(I.u32_op(NM.One{}), 1n, one_v())), {==}) 303 304 # ---- prod: the fold stops at the first overflow ---- 305 306 def cmul_rel(+q: U32, +x: U32, +n: Nat, +hn: {Nat.mul(v(q), v(x)) == n : Nat}, +c: Bool, +hc: {C.fits(32n, n) == c : Bool}) -> {G.cmul(~U32, ~I.u32_op, ~I.u32_is, q, x) == G.fits(U32, Bool.not(c), of(n)) : Maybe<&2, U32>}: 307 match c: 308 case True{}: 309 +hmo = mo_of(q, x, n, hn, True{}, hc) 310 %Equal.sym(Bool, I.u32_is(NM.MulOver{q, x}), False{}, hmo) : {G.fits(U32, _, I.u32_op(NM.Mul{q, x})) == Some{of(n)} : Maybe<&2, U32>} 311 Equal.cong(U32, Maybe<&2, U32>, t => Some{t}, I.u32_op(NM.Mul{q, x}), of(n), as_of(I.u32_op(NM.Mul{q, x}), n, Equal.trans(Nat, v(I.u32_op(NM.Mul{q, x})), Nat.mul(v(q), v(x)), n, LW.ops_mul(q, x, hmo), hn))) 312 case False{}: 313 %Equal.sym(Bool, I.u32_is(NM.MulOver{q, x}), True{}, mo_of(q, x, n, hn, False{}, hc)) : {G.fits(U32, _, I.u32_op(NM.Mul{q, x})) == None{} : Maybe<&2, U32>} 314 {==} 315 316 def pal(+xs: List<&2, U32>, +r: Maybe<&2, U32>, +n: Nat, +c: Bool, +hr: {r == G.fits(U32, Bool.not(c), of(n)) : Maybe<&2, U32>}, +hc: {C.fits(32n, n) == c : Bool}) -> {G.ok(U32, G.prod_go(~U32, ~I.u32_op, ~I.u32_is, xs, r)) == SG.prefix_fin(~U32, ~SG.u32_of, SG.prod_go(32n, vals(xs), n, c)) : Result<&2, &2, NM.NumError, U32>}: 317 match xs c: 318 case Nil{} True{}: 319 %Equal.sym(Maybe<&2, U32>, r, Some{of(n)}, hr) : {G.ok(U32, _) == Done{of(n)} : Result<&2, &2, NM.NumError, U32>} 320 {==} 321 case Nil{} False{}: 322 %Equal.sym(Maybe<&2, U32>, r, None{}, hr) : {G.ok(U32, _) == Fail{NM.Overflow{}} : Result<&2, &2, NM.NumError, U32>} 323 {==} 324 case Con{x, t} False{}: 325 %Equal.sym(Maybe<&2, U32>, r, None{}, hr) : {G.ok(U32, G.prod_go(~U32, ~I.u32_op, ~I.u32_is, Con{x, t}, _)) == Fail{NM.Overflow{}} : Result<&2, &2, NM.NumError, U32>} 326 {==} 327 case Con{+x, +t} True{}: 328 %Equal.sym(Maybe<&2, U32>, r, Some{of(n)}, hr) : {G.ok(U32, G.prod_go(~U32, ~I.u32_op, ~I.u32_is, Con{x, t}, _)) == SG.prefix_fin(~U32, ~SG.u32_of, SG.prod_go(32n, vals(t), Nat.mul(n, v(x)), C.fits(32n, Nat.mul(n, v(x))))) : Result<&2, &2, NM.NumError, U32>} 329 +hn = Equal.cong(Nat, Nat, z => Nat.mul(z, v(x)), v(of(n)), n, LW.vo(n, hc)) 330 pal(t, G.cmul(~U32, ~I.u32_op, ~I.u32_is, of(n), x), Nat.mul(n, v(x)), C.fits(32n, Nat.mul(n, v(x))), cmul_rel(of(n), x, Nat.mul(n, v(x)), hn, C.fits(32n, Nat.mul(n, v(x))), {==}), {==}) 331 332 def prod_checked(+xs: List<&2, U32>) -> SG.Prod.checked(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 32n, xs): 333 pal(xs, Some{I.u32_op(NM.One{})}, 1n, True{}, Equal.cong(U32, Maybe<&2, U32>, t => Some{t}, I.u32_op(NM.One{}), of(1n), as_of(I.u32_op(NM.One{}), 1n, one_v())), {==}) 334 335 # ---- sum: the partial sums only grow ---- 336 337 def ao_of(+q: U32, +b: U32, +n: Nat, +hn: {Nat.add(v(q), v(b)) == n : Nat}, +c: Bool, +hc: {C.fits(32n, n) == c : Bool}) -> {I.u32_is(NM.AddOver{q, b}) == Bool.not(c) : Bool}: 338 +e1 = Equal.trans(Bool, I.u32_is(NM.AddOver{q, b}), Bool.not(C.fits(32n, Nat.add(v(q), v(b)))), Bool.not(C.fits(32n, n)), LW.tests_add_over(q, b), Equal.cong(Nat, Bool, t => Bool.not(C.fits(32n, t)), Nat.add(v(q), v(b)), n, hn)) 339 Equal.trans(Bool, I.u32_is(NM.AddOver{q, b}), Bool.not(C.fits(32n, n)), Bool.not(c), e1, Equal.cong(Bool, Bool, t => Bool.not(t), C.fits(32n, n), c, hc)) 340 341 def cadd_rel(+q: U32, +x: U32, +n: Nat, +hn: {Nat.add(v(q), v(x)) == n : Nat}, +c: Bool, +hc: {C.fits(32n, n) == c : Bool}) -> {G.cadd(~U32, ~I.u32_op, ~I.u32_is, q, x) == G.fits(U32, Bool.not(c), of(n)) : Maybe<&2, U32>}: 342 match c: 343 case True{}: 344 +hao = ao_of(q, x, n, hn, True{}, hc) 345 %Equal.sym(Bool, I.u32_is(NM.AddOver{q, x}), False{}, hao) : {G.fits(U32, _, I.u32_op(NM.Add{q, x})) == Some{of(n)} : Maybe<&2, U32>} 346 Equal.cong(U32, Maybe<&2, U32>, t => Some{t}, I.u32_op(NM.Add{q, x}), of(n), as_of(I.u32_op(NM.Add{q, x}), n, Equal.trans(Nat, v(I.u32_op(NM.Add{q, x})), Nat.add(v(q), v(x)), n, LW.ops_add(q, x, hao), hn))) 347 case False{}: 348 %Equal.sym(Bool, I.u32_is(NM.AddOver{q, x}), True{}, ao_of(q, x, n, hn, False{}, hc)) : {G.fits(U32, _, I.u32_op(NM.Add{q, x})) == None{} : Maybe<&2, U32>} 349 {==} 350 351 # a value that does not fit stays unfit when it grows 352 def unfit_mono(+k: Nat, +a: Nat, +b: Nat, +h: {Nat.is_le(a, b) == True{} : Bool}, +hf: {C.fits(k, a) == False{} : Bool}) -> {C.fits(k, b) == False{} : Bool}: 353 +na = Equal.trans(Bool, Nat.is_lt(a, C.pow2(k)), C.fits(k, a), False{}, Equal.sym(Bool, C.fits(k, a), Nat.is_lt(a, C.pow2(k)), WW.fits_lt(k, a)), hf) 354 Equal.trans(Bool, C.fits(k, b), Nat.is_lt(b, C.pow2(k)), False{}, WW.fits_lt(k, b), N.le_not_lt(b, C.pow2(k), N.le_trans(C.pow2(k), a, b, N.not_lt_le(a, C.pow2(k), na), h))) 355 356 def sal(+xs: List<&2, U32>, +r: Maybe<&2, U32>, +n: Nat, +c: Bool, +hr: {r == G.fits(U32, Bool.not(c), of(n)) : Maybe<&2, U32>}, +hc: {C.fits(32n, n) == c : Bool}) -> {G.ok(U32, G.sum_go(~U32, ~I.u32_op, ~I.u32_is, xs, r)) == SG.checked(~U32, ~SG.u32_of, 32n, Nat.add(n, NS.lsum(vals(xs)))) : Result<&2, &2, NM.NumError, U32>}: 357 match xs c: 358 case Nil{} True{}: 359 %Equal.sym(Maybe<&2, U32>, r, Some{of(n)}, hr) : {G.ok(U32, _) == SG.checked(~U32, ~SG.u32_of, 32n, Nat.add(n, 0n)) : Result<&2, &2, NM.NumError, U32>} 360 %Equal.sym(Nat, Nat.add(n, 0n), n, N.add_zero(n)) : {Done{of(n)} == SG.checked(~U32, ~SG.u32_of, 32n, _) : Result<&2, &2, NM.NumError, U32>} 361 %Equal.sym(Bool, C.fits(32n, n), True{}, hc) : {Done{of(n)} == SG.checked_pick(~U32, ~SG.u32_of, n, _) : Result<&2, &2, NM.NumError, U32>} 362 {==} 363 case Nil{} False{}: 364 %Equal.sym(Maybe<&2, U32>, r, None{}, hr) : {G.ok(U32, _) == SG.checked(~U32, ~SG.u32_of, 32n, Nat.add(n, 0n)) : Result<&2, &2, NM.NumError, U32>} 365 %Equal.sym(Nat, Nat.add(n, 0n), n, N.add_zero(n)) : {Fail{NM.Overflow{}} == SG.checked(~U32, ~SG.u32_of, 32n, _) : Result<&2, &2, NM.NumError, U32>} 366 %Equal.sym(Bool, C.fits(32n, n), False{}, hc) : {Fail{NM.Overflow{}} == SG.checked_pick(~U32, ~SG.u32_of, n, _) : Result<&2, &2, NM.NumError, U32>} 367 {==} 368 case Con{x, t} False{}: 369 %Equal.sym(Maybe<&2, U32>, r, None{}, hr) : {G.ok(U32, G.sum_go(~U32, ~I.u32_op, ~I.u32_is, Con{x, t}, _)) == SG.checked(~U32, ~SG.u32_of, 32n, Nat.add(n, NS.lsum(vals(Con{x, t})))) : Result<&2, &2, NM.NumError, U32>} 370 +s = Nat.add(n, NS.lsum(vals(Con{x, t}))) 371 %Equal.sym(Bool, C.fits(32n, s), False{}, unfit_mono(32n, n, s, N.le_add_right(n, NS.lsum(vals(Con{x, t}))), hc)) : {Fail{NM.Overflow{}} == SG.checked_pick(~U32, ~SG.u32_of, s, _) : Result<&2, &2, NM.NumError, U32>} 372 {==} 373 case Con{+x, +t} True{}: 374 +n2 = Nat.add(n, v(x)) 375 +hn = Equal.cong(Nat, Nat, z => Nat.add(z, v(x)), v(of(n)), n, LW.vo(n, hc)) 376 %Equal.sym(Maybe<&2, U32>, r, Some{of(n)}, hr) : {G.ok(U32, G.sum_go(~U32, ~I.u32_op, ~I.u32_is, Con{x, t}, _)) == SG.checked(~U32, ~SG.u32_of, 32n, Nat.add(n, Nat.add(v(x), NS.lsum(vals(t))))) : Result<&2, &2, NM.NumError, U32>} 377 %NA.add_assoc(n, v(x), NS.lsum(vals(t))) : {G.ok(U32, G.sum_go(~U32, ~I.u32_op, ~I.u32_is, t, G.cadd(~U32, ~I.u32_op, ~I.u32_is, of(n), x))) == SG.checked(~U32, ~SG.u32_of, 32n, _) : Result<&2, &2, NM.NumError, U32>} 378 sal(t, G.cadd(~U32, ~I.u32_op, ~I.u32_is, of(n), x), n2, C.fits(32n, n2), cadd_rel(of(n), x, n2, hn, C.fits(32n, n2), {==}), {==}) 379 380 def sum_checked(+xs: List<&2, U32>) -> SG.Sum.checked(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 32n, xs): 381 sal(xs, Some{I.u32_op(NM.ZeroOp{})}, 0n, True{}, Equal.cong(U32, Maybe<&2, U32>, t => Some{t}, I.u32_op(NM.ZeroOp{}), of(0n), as_of(I.u32_op(NM.ZeroOp{}), 0n, zero_v())), {==}) 382 383 # ---- bit_length: halvings on the values ---- 384 385 def blsim(+f: Nat, +k: Nat, +n: U32, +cz: Bool, +nn: Nat, +hcz: {I.u32_is(NM.IsZero{n}) == cz : Bool}, +hnn: {v(n) == nn : Nat}) -> {G.bit_length_go(~U32, ~I.u32_op, ~I.u32_is, f, k, (n, cz)) == M.bit_length_go(f, nn, k) : Nat}: 386 match f cz nn: 387 case 0n _ _: 388 {==} 389 case 1n+g True{} 0n: 390 {==} 391 case 1n+g True{} 1n+np: 392 Empty.absurd({G.bit_length_go(~U32, ~I.u32_op, ~I.u32_is, 1n+g, k, (n, True{})) == M.bit_length_go(1n+g, 1n+np, k) : Nat}, true_ne_false(Equal.trans(Bool, True{}, I.u32_is(NM.IsZero{n}), False{}, Equal.sym(Bool, I.u32_is(NM.IsZero{n}), True{}, hcz), iz(n, 1n+np, hnn)))) 393 case 1n+g False{} 0n: 394 Empty.absurd({G.bit_length_go(~U32, ~I.u32_op, ~I.u32_is, 1n+g, k, (n, False{})) == M.bit_length_go(1n+g, 0n, k) : Nat}, true_ne_false(Equal.trans(Bool, True{}, I.u32_is(NM.IsZero{n}), False{}, Equal.sym(Bool, I.u32_is(NM.IsZero{n}), True{}, iz(n, 0n, hnn)), hcz))) 395 case 1n+ +g False{} 1n+ +np: 396 +h = I.u32_op(NM.Half{n}) 397 +eh = Equal.trans(Nat, v(h), Nat.div(v(n), 2n), Nat.div(1n+np, 2n), LW.ops_half(n), Equal.cong(Nat, Nat, t => Nat.div(t, 2n), v(n), 1n+np, hnn)) 398 blsim(g, 1n+k, h, I.u32_is(NM.IsZero{h}), Nat.div(1n+np, 2n), {==}, eh) 399 400 def bit_length_k(+k: Nat, +hk: {k == 32n : Nat}, +n: U32) -> {G.bit_length(~U32, ~I.u32_op, ~I.u32_is, n) == M.bit_length(v(n)) : Nat}: 401 +hj = L.subst(Nat, z => {Nat.is_le(z, 140n) == True{} : Bool}, 32n, k, Equal.sym(Nat, k, 32n, hk), {==}) 402 Equal.trans(Nat, G.bit_length(~U32, ~I.u32_op, ~I.u32_is, n), M.bit_length_go(140n, v(n), 0n), M.bit_length(v(n)), blsim(140n, 0n, n, I.u32_is(NM.IsZero{n}), v(n), {==}, {==}), NF.bl_140(k, v(n), hj, U32P.val_lt(1n, {==}, k, hk, n))) 403 404 def bit_length_agrees(+n: U32) -> SG.BitLength.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, n): 405 bit_length_k(32n, {==}, n) 406 407 # ---- pow_mod: binary exponentiation on the values, below m ---- 408 409 def pmo_lt(+mp: Nat, +d: Nat, +base: Nat, +acc: Nat, +ha: {Nat.is_lt(acc, 1n+mp) == True{} : Bool}) -> {Nat.is_lt(M.pow_mod_odd(1n+mp, d, base, acc), 1n+mp) == True{} : Bool}: 410 match d: 411 case 0n: 412 ha 413 case 1n+z: 414 NR.dm_lt(mp, Nat.mul(acc, base)) 415 416 def lt_m(+x: U32, +m: U32, +mp: Nat, +hm: {v(m) == 1n+mp : Nat}, +h: {Nat.is_lt(v(x), 1n+mp) == True{} : Bool}) -> {Nat.is_lt(v(x), v(m)) == True{} : Bool}: 417 L.subst(Nat, z => {Nat.is_lt(v(x), z) == True{} : Bool}, 1n+mp, v(m), Equal.sym(Nat, v(m), 1n+mp, hm), h) 418 419 def mmb_v(+m: U32, +b: U32, +acc: U32, +mp: Nat, +hm: {v(m) == 1n+mp : Nat}, +hb: {Nat.is_lt(v(b), 1n+mp) == True{} : Bool}, +ha: {Nat.is_lt(v(acc), 1n+mp) == True{} : Bool}, +d: Nat, +o: Bool, +hd: {Nat.is_lt(d, 2n) == True{} : Bool}, +ho: {o == Nat.is_eq(d, 1n) : Bool}) -> {v(G.mm_bit(~U32, ~I.u32_op, o, m, b, acc)) == M.pow_mod_odd(1n+mp, d, v(b), v(acc)) : Nat}: 420 match d o: 421 case 0n False{}: 422 {==} 423 case 0n True{}: 424 Empty.absurd({v(G.mm_bit(~U32, ~I.u32_op, True{}, m, b, acc)) == M.pow_mod_odd(1n+mp, 0n, v(b), v(acc)) : Nat}, true_ne_false(ho)) 425 case 1n True{}: 426 Equal.trans(Nat, v(I.u32_op(NM.MulMod{acc, b, m})), Nat.mod(Nat.mul(v(acc), v(b)), v(m)), Nat.mod(Nat.mul(v(acc), v(b)), 1n+mp), LW.ops_mulmod(acc, b, m, lt_m(acc, m, mp, hm, ha), lt_m(b, m, mp, hm, hb)), Equal.cong(Nat, Nat, t => Nat.mod(Nat.mul(v(acc), v(b)), t), v(m), 1n+mp, hm)) 427 case 1n False{}: 428 Empty.absurd({v(G.mm_bit(~U32, ~I.u32_op, False{}, m, b, acc)) == M.pow_mod_odd(1n+mp, 1n, v(b), v(acc)) : Nat}, true_ne_false(Equal.sym(Bool, False{}, True{}, ho))) 429 case 2n+q _: 430 Empty.absurd({v(G.mm_bit(~U32, ~I.u32_op, o, m, b, acc)) == M.pow_mod_odd(1n+mp, 2n+q, v(b), v(acc)) : Nat}, N.lt_zero_absurd(q, hd)) 431 432 def pmsim(+f: Nat, +m: U32, +b: U32, +acc: U32, +e: U32, +mp: Nat, +hm: {v(m) == 1n+mp : Nat}, +hb: {Nat.is_lt(v(b), 1n+mp) == True{} : Bool}, +ha: {Nat.is_lt(v(acc), 1n+mp) == True{} : Bool}, +ez: Bool, +ne: Nat, +hez: {I.u32_is(NM.IsZero{e}) == ez : Bool}, +hne: {v(e) == ne : Nat}) -> {v(G.pow_mod_go(~U32, ~I.u32_op, ~I.u32_is, f, m, b, acc, (e, ez))) == M.pow_mod_go(f, 1n+mp, ne, v(b), v(acc)) : Nat}: 433 match f ez ne: 434 case 0n _ _: 435 {==} 436 case 1n+g True{} 0n: 437 {==} 438 case 1n+g True{} 1n+ep: 439 Empty.absurd({v(G.pow_mod_go(~U32, ~I.u32_op, ~I.u32_is, 1n+g, m, b, acc, (e, True{}))) == M.pow_mod_go(1n+g, 1n+mp, 1n+ep, v(b), v(acc)) : Nat}, true_ne_false(Equal.trans(Bool, True{}, I.u32_is(NM.IsZero{e}), False{}, Equal.sym(Bool, I.u32_is(NM.IsZero{e}), True{}, hez), iz(e, 1n+ep, hne)))) 440 case 1n+g False{} 0n: 441 Empty.absurd({v(G.pow_mod_go(~U32, ~I.u32_op, ~I.u32_is, 1n+g, m, b, acc, (e, False{}))) == M.pow_mod_go(1n+g, 1n+mp, 0n, v(b), v(acc)) : Nat}, true_ne_false(Equal.trans(Bool, True{}, I.u32_is(NM.IsZero{e}), False{}, Equal.sym(Bool, I.u32_is(NM.IsZero{e}), True{}, iz(e, 0n, hne)), hez))) 442 case 1n+ +g False{} 1n+ +ep: 443 +b2 = I.u32_op(NM.MulMod{b, b, m}) 444 +eb2 = Equal.trans(Nat, v(b2), Nat.mod(Nat.mul(v(b), v(b)), v(m)), Nat.mod(Nat.mul(v(b), v(b)), 1n+mp), LW.ops_mulmod(b, b, m, lt_m(b, m, mp, hm, hb), lt_m(b, m, mp, hm, hb)), Equal.cong(Nat, Nat, t => Nat.mod(Nat.mul(v(b), v(b)), t), v(m), 1n+mp, hm)) 445 +hb2 = L.subst(Nat, z => {Nat.is_lt(z, 1n+mp) == True{} : Bool}, Nat.mod(Nat.mul(v(b), v(b)), 1n+mp), v(b2), Equal.sym(Nat, v(b2), Nat.mod(Nat.mul(v(b), v(b)), 1n+mp), eb2), NR.dm_lt(mp, Nat.mul(v(b), v(b)))) 446 +o = I.u32_is(NM.Odd{e}) 447 +d = Nat.mod(1n+ep, 2n) 448 +ho = Equal.trans(Bool, o, Nat.is_eq(Nat.mod(v(e), 2n), 1n), Nat.is_eq(d, 1n), LW.tests_odd(e), Equal.cong(Nat, Bool, t => Nat.is_eq(Nat.mod(t, 2n), 1n), v(e), 1n+ep, hne)) 449 +acc2 = G.mm_bit(~U32, ~I.u32_op, o, m, b, acc) 450 +ea2 = mmb_v(m, b, acc, mp, hm, hb, ha, d, o, NR.dm_lt(1n, 1n+ep), ho) 451 +ha2 = L.subst(Nat, z => {Nat.is_lt(z, 1n+mp) == True{} : Bool}, M.pow_mod_odd(1n+mp, d, v(b), v(acc)), v(acc2), Equal.sym(Nat, v(acc2), M.pow_mod_odd(1n+mp, d, v(b), v(acc)), ea2), pmo_lt(mp, d, v(b), v(acc), ha)) 452 +e2 = I.u32_op(NM.Half{e}) 453 +ee2 = Equal.trans(Nat, v(e2), Nat.div(v(e), 2n), Nat.div(1n+ep, 2n), LW.ops_half(e), Equal.cong(Nat, Nat, t => Nat.div(t, 2n), v(e), 1n+ep, hne)) 454 +ih = pmsim(g, m, b2, acc2, e2, mp, hm, hb2, ha2, I.u32_is(NM.IsZero{e2}), Nat.div(1n+ep, 2n), {==}, ee2) 455 Equal.trans(Nat, v(G.pow_mod_go(~U32, ~I.u32_op, ~I.u32_is, g, m, b2, acc2, (e2, I.u32_is(NM.IsZero{e2})))), M.pow_mod_go(g, 1n+mp, Nat.div(1n+ep, 2n), v(b2), v(acc2)), M.pow_mod_go(g, 1n+mp, Nat.div(1n+ep, 2n), Nat.mod(Nat.mul(v(b), v(b)), 1n+mp), M.pow_mod_odd(1n+mp, d, v(b), v(acc))), ih, Equal.trans(Nat, M.pow_mod_go(g, 1n+mp, Nat.div(1n+ep, 2n), v(b2), v(acc2)), M.pow_mod_go(g, 1n+mp, Nat.div(1n+ep, 2n), Nat.mod(Nat.mul(v(b), v(b)), 1n+mp), v(acc2)), M.pow_mod_go(g, 1n+mp, Nat.div(1n+ep, 2n), Nat.mod(Nat.mul(v(b), v(b)), 1n+mp), M.pow_mod_odd(1n+mp, d, v(b), v(acc))), Equal.cong(Nat, Nat, t => M.pow_mod_go(g, 1n+mp, Nat.div(1n+ep, 2n), t, v(acc2)), v(b2), Nat.mod(Nat.mul(v(b), v(b)), 1n+mp), eb2), Equal.cong(Nat, Nat, t => M.pow_mod_go(g, 1n+mp, Nat.div(1n+ep, 2n), Nat.mod(Nat.mul(v(b), v(b)), 1n+mp), t), v(acc2), M.pow_mod_odd(1n+mp, d, v(b), v(acc)), ea2))) 456 457 def pm_rem(+x: U32, +m: U32, +mp: Nat, +hm: {v(m) == 1n+mp : Nat}) -> {v(I.u32_op(NM.Rem{x, m})) == Nat.mod(v(x), 1n+mp) : Nat}: 458 +hq = Equal.trans(Bool, Nat.is_eq(v(m), 0n), Nat.is_eq(1n+mp, 0n), False{}, Equal.cong(Nat, Bool, t => Nat.is_eq(t, 0n), v(m), 1n+mp, hm), {==}) 459 Equal.trans(Nat, v(I.u32_op(NM.Rem{x, m})), Nat.mod(v(x), v(m)), Nat.mod(v(x), 1n+mp), LW.ops_rem(x, m, hq), Equal.cong(Nat, Nat, t => Nat.mod(v(x), t), v(m), 1n+mp, hm)) 460 461 462 # the generic MulMod loop (mont32_ok(m) False) 463 def pm_gen(+k: Nat, +hk: {k == 32n : Nat}, +b: U32, +e: U32, +m: U32, +mp: Nat, +hnm: {v(m) == 1n+mp : Nat}) -> {v(G.pow_mod_go(~U32, ~I.u32_op, ~I.u32_is, 140n, m, I.u32_op(NM.Rem{b, m}), I.u32_op(NM.Rem{I.u32_op(NM.One{}), m}), (e, I.u32_is(NM.IsZero{e})))) == M.pow_mod_go(v(e), 1n+mp, v(e), Nat.mod(v(b), 1n+mp), Nat.mod(1n, 1n+mp)) : Nat}: 464 +rb = I.u32_op(NM.Rem{b, m}) 465 +ra = I.u32_op(NM.Rem{I.u32_op(NM.One{}), m}) 466 +eb = pm_rem(b, m, mp, hnm) 467 +ea = Equal.trans(Nat, v(ra), Nat.mod(v(I.u32_op(NM.One{})), 1n+mp), Nat.mod(1n, 1n+mp), pm_rem(I.u32_op(NM.One{}), m, mp, hnm), Equal.cong(Nat, Nat, t => Nat.mod(t, 1n+mp), v(I.u32_op(NM.One{})), 1n, one_v())) 468 +hb = L.subst(Nat, z => {Nat.is_lt(z, 1n+mp) == True{} : Bool}, Nat.mod(v(b), 1n+mp), v(rb), Equal.sym(Nat, v(rb), Nat.mod(v(b), 1n+mp), eb), NR.dm_lt(mp, v(b))) 469 +ha = L.subst(Nat, z => {Nat.is_lt(z, 1n+mp) == True{} : Bool}, Nat.mod(1n, 1n+mp), v(ra), Equal.sym(Nat, v(ra), Nat.mod(1n, 1n+mp), ea), NR.dm_lt(mp, 1n)) 470 +hj = L.subst(Nat, z => {Nat.is_le(z, 140n) == True{} : Bool}, 32n, k, Equal.sym(Nat, k, 32n, hk), {==}) 471 +s = pmsim(140n, m, rb, ra, e, mp, hnm, hb, ha, I.u32_is(NM.IsZero{e}), v(e), {==}, {==}) 472 +c1 = Equal.trans(Nat, M.pow_mod_go(140n, 1n+mp, v(e), v(rb), v(ra)), M.pow_mod_go(140n, 1n+mp, v(e), Nat.mod(v(b), 1n+mp), v(ra)), M.pow_mod_go(140n, 1n+mp, v(e), Nat.mod(v(b), 1n+mp), Nat.mod(1n, 1n+mp)), Equal.cong(Nat, Nat, t => M.pow_mod_go(140n, 1n+mp, v(e), t, v(ra)), v(rb), Nat.mod(v(b), 1n+mp), eb), Equal.cong(Nat, Nat, t => M.pow_mod_go(140n, 1n+mp, v(e), Nat.mod(v(b), 1n+mp), t), v(ra), Nat.mod(1n, 1n+mp), ea)) 473 +c2 = NF.pm_140(k, 1n+mp, v(e), Nat.mod(v(b), 1n+mp), Nat.mod(1n, 1n+mp), hj, U32P.val_lt(1n, {==}, k, hk, e)) 474 Equal.trans(Nat, v(G.pow_mod_go(~U32, ~I.u32_op, ~I.u32_is, 140n, m, I.u32_op(NM.Rem{b, m}), I.u32_op(NM.Rem{I.u32_op(NM.One{}), m}), (e, I.u32_is(NM.IsZero{e})))), M.pow_mod_go(140n, 1n+mp, v(e), v(rb), v(ra)), M.pow_mod_go(v(e), 1n+mp, v(e), Nat.mod(v(b), 1n+mp), Nat.mod(1n, 1n+mp)), s, Equal.trans(Nat, M.pow_mod_go(140n, 1n+mp, v(e), v(rb), v(ra)), M.pow_mod_go(140n, 1n+mp, v(e), Nat.mod(v(b), 1n+mp), Nat.mod(1n, 1n+mp)), M.pow_mod_go(v(e), 1n+mp, v(e), Nat.mod(v(b), 1n+mp), Nat.mod(1n, 1n+mp)), c1, c2)) 475 476 # 32-bit Montgomery multiplication (mont32_ok(m) True) 477 def pm_mont(+k: Nat, +hk: {k == 32n : Nat}, +b: U32, +e: U32, +m: U32, +mp: Nat, +hnm: {v(m) == 1n+mp : Nat}, +hok: {X.mont32_ok(m) == True{} : Bool}) -> {v(I.u32_op(NM.PowMod{I.u32_op(NM.Rem{b, m}), e, m})) == M.pow_mod_go(v(e), 1n+mp, v(e), Nat.mod(v(b), 1n+mp), Nat.mod(1n, 1n+mp)) : Nat}: 478 +hj = L.subst(Nat, z => {Nat.is_le(z, 140n) == True{} : Bool}, 32n, k, Equal.sym(Nat, k, 32n, hk), {==}) 479 Equal.trans(Nat, v(X.mpow32(U32.mod(b, m), e, m)), M.pow_mod_go(140n, 1n+mp, v(e), Nat.mod(v(b), 1n+mp), Nat.mod(1n, 1n+mp)), M.pow_mod_go(v(e), 1n+mp, v(e), Nat.mod(v(b), 1n+mp), Nat.mod(1n, 1n+mp)), MO.mpow_top(1n, {==}, mp, m, hnm, hok, b, e), NF.pm_140(k, 1n+mp, v(e), Nat.mod(v(b), 1n+mp), Nat.mod(1n, 1n+mp), hj, U32P.val_lt(1n, {==}, k, hk, e))) 480 481 def pm_pick(+k: Nat, +hk: {k == 32n : Nat}, +b: U32, +e: U32, +m: U32, +mp: Nat, +hnm: {v(m) == 1n+mp : Nat}, +c: Bool, +hc: {X.mont32_ok(m) == c : Bool}) -> {v(G.pow_mod_pick(~U32, ~I.u32_op, ~I.u32_is, b, e, m, c)) == M.pow_mod_go(v(e), 1n+mp, v(e), Nat.mod(v(b), 1n+mp), Nat.mod(1n, 1n+mp)) : Nat}: 482 match c: 483 case True{}: 484 pm_mont(k, hk, b, e, m, mp, hnm, hc) 485 case False{}: 486 pm_gen(k, hk, b, e, m, mp, hnm) 487 488 def pm_top(+k: Nat, +hk: {k == 32n : Nat}, +b: U32, +e: U32, +m: U32, +c: Bool, +hc: {I.u32_is(NM.IsZero{m}) == c : Bool}, +nm: Nat, +hnm: {v(m) == nm : Nat}) -> {G.pow_mod_ok(~U32, ~I.u32_op, ~I.u32_is, b, e, m, c) == SG.lift(~U32, ~SG.u32_of, M.pow_mod(v(b), v(e), nm)) : Result<&2, &2, NM.NumError, U32>}: 489 match c nm: 490 case True{} 0n: 491 {==} 492 case False{} 0n: 493 Empty.absurd({G.pow_mod_ok(~U32, ~I.u32_op, ~I.u32_is, b, e, m, False{}) == SG.lift(~U32, ~SG.u32_of, M.pow_mod(v(b), v(e), 0n)) : Result<&2, &2, NM.NumError, U32>}, true_ne_false(Equal.trans(Bool, True{}, I.u32_is(NM.IsZero{m}), False{}, Equal.sym(Bool, I.u32_is(NM.IsZero{m}), True{}, iz(m, 0n, hnm)), hc))) 494 case True{} 1n+ +mp: 495 Empty.absurd({G.pow_mod_ok(~U32, ~I.u32_op, ~I.u32_is, b, e, m, True{}) == SG.lift(~U32, ~SG.u32_of, M.pow_mod(v(b), v(e), 1n+mp)) : Result<&2, &2, NM.NumError, U32>}, true_ne_false(Equal.trans(Bool, True{}, I.u32_is(NM.IsZero{m}), False{}, Equal.sym(Bool, I.u32_is(NM.IsZero{m}), True{}, hc), iz(m, 1n+mp, hnm)))) 496 case False{} 1n+ +mp: 497 +g = G.pow_mod_pick(~U32, ~I.u32_op, ~I.u32_is, b, e, m, I.u32_is(NM.Mont{m})) 498 +r = M.pow_mod_go(v(e), 1n+mp, v(e), Nat.mod(v(b), 1n+mp), Nat.mod(1n, 1n+mp)) 499 Equal.cong(U32, Result<&2, &2, NM.NumError, U32>, t => Done{t}, g, of(r), as_of(g, r, pm_pick(k, hk, b, e, m, mp, hnm, X.mont32_ok(m), {==}))) 500 501 def powmod_agrees(+b: U32, +e: U32, +m: U32) -> SG.PowMod.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, b, e, m): 502 pm_top(32n, {==}, b, e, m, I.u32_is(NM.IsZero{m}), {==}, v(m), {==}) 503 504 # ---- mod_inverse: extended Euclid on the values, coefficients below m ---- 505 506 def nlt(+a: Nat, +b: Nat, +na: Nat, +nb: Nat, +ha: {a == na : Nat}, +hb: {b == nb : Nat}) -> {Nat.is_lt(a, b) == Nat.is_lt(na, nb) : Bool}: 507 Equal.trans(Bool, Nat.is_lt(a, b), Nat.is_lt(na, b), Nat.is_lt(na, nb), Equal.cong(Nat, Bool, t => Nat.is_lt(t, b), a, na, ha), Equal.cong(Nat, Bool, t => Nat.is_lt(na, t), b, nb, hb)) 508 509 def ltv(+a: U32, +b: U32, +na: Nat, +nb: Nat, +ha: {v(a) == na : Nat}, +hb: {v(b) == nb : Nat}) -> {I.u32_is(NM.Lt{a, b}) == Nat.is_lt(na, nb) : Bool}: 510 Equal.trans(Bool, I.u32_is(NM.Lt{a, b}), Nat.is_lt(v(a), v(b)), Nat.is_lt(na, nb), LW.tests_lt(a, b), nlt(v(a), v(b), na, nb, ha, hb)) 511 512 def nsub(+a: Nat, +b: Nat, +na: Nat, +nb: Nat, +ha: {a == na : Nat}, +hb: {b == nb : Nat}) -> {Nat.sub(a, b) == Nat.sub(na, nb) : Nat}: 513 Equal.trans(Nat, Nat.sub(a, b), Nat.sub(na, b), Nat.sub(na, nb), Equal.cong(Nat, Nat, t => Nat.sub(t, b), a, na, ha), Equal.cong(Nat, Nat, t => Nat.sub(na, t), b, nb, hb)) 514 515 def nadd(+a: Nat, +b: Nat, +na: Nat, +nb: Nat, +ha: {a == na : Nat}, +hb: {b == nb : Nat}) -> {Nat.add(a, b) == Nat.add(na, nb) : Nat}: 516 Equal.trans(Nat, Nat.add(a, b), Nat.add(na, b), Nat.add(na, nb), Equal.cong(Nat, Nat, t => Nat.add(t, b), a, na, ha), Equal.cong(Nat, Nat, t => Nat.add(na, t), b, nb, hb)) 517 518 def mv(+k: Nat, +hk: {k == 32n : Nat}, +m: U32, +mp: Nat, +hm: {v(m) == 1n+mp : Nat}) -> {Nat.is_lt(1n+mp, C.pow2(k)) == True{} : Bool}: 519 L.subst(Nat, z => {Nat.is_lt(z, C.pow2(k)) == True{} : Bool}, v(m), 1n+mp, hm, U32P.val_lt(1n, {==}, k, hk, m)) 520 521 def fits32(+k: Nat, +hk: {k == 32n : Nat}, +n: Nat, +h: {Nat.is_lt(n, C.pow2(k)) == True{} : Bool}) -> {C.fits(32n, n) == True{} : Bool}: 522 L.subst(Nat, z => {C.fits(z, n) == True{} : Bool}, k, 32n, hk, Equal.trans(Bool, C.fits(k, n), Nat.is_lt(n, C.pow2(k)), True{}, WW.fits_lt(k, n), h)) 523 524 def lt_mn(+x: U32, +m: U32, +mp: Nat, +hm: {v(m) == 1n+mp : Nat}, +nx: Nat, +hx: {v(x) == nx : Nat}, +h: {Nat.is_lt(nx, 1n+mp) == True{} : Bool}) -> {Nat.is_lt(v(x), v(m)) == True{} : Bool}: 525 lt_m(x, m, mp, hm, L.subst(Nat, z => {Nat.is_lt(z, 1n+mp) == True{} : Bool}, nx, v(x), Equal.sym(Nat, v(x), nx, hx), h)) 526 527 def subv(+k: Nat, +hk: {k == 32n : Nat}, +m: U32, +mp: Nat, +hm: {v(m) == 1n+mp : Nat}, +s0: U32, +x: U32, +ns0: Nat, +nx: Nat, +hs0: {v(s0) == ns0 : Nat}, +hx: {v(x) == nx : Nat}, +hb0: {Nat.is_lt(ns0, 1n+mp) == True{} : Bool}, +hbx: {Nat.is_lt(nx, 1n+mp) == True{} : Bool}, +c: Bool, +hc: {I.u32_is(NM.Lt{s0, x}) == c : Bool}) -> {v(G.submod(~U32, ~I.u32_op, m, s0, x, c)) == Nat.mod(Nat.add(ns0, Nat.sub(1n+mp, nx)), 1n+mp) : Nat}: 528 match c: 529 case True{}: 530 +hl = Equal.trans(Bool, Nat.is_lt(ns0, nx), I.u32_is(NM.Lt{s0, x}), True{}, Equal.sym(Bool, I.u32_is(NM.Lt{s0, x}), Nat.is_lt(ns0, nx), ltv(s0, x, ns0, nx, hs0, hx)), hc) 531 +y = I.u32_op(NM.Sub{m, x}) 532 +ey = Equal.trans(Nat, v(y), Nat.sub(v(m), v(x)), Nat.sub(1n+mp, nx), LW.ops_sub(m, x, N.lt_le(v(x), v(m), lt_mn(x, m, mp, hm, nx, hx, hbx))), nsub(v(m), v(x), 1n+mp, nx, hm, hx)) 533 +sum = Nat.add(ns0, Nat.sub(1n+mp, nx)) 534 +hsum = NF.sm_lt(1n+mp, ns0, nx, hl, N.lt_le(nx, 1n+mp, hbx)) 535 +esum = nadd(v(s0), v(y), ns0, Nat.sub(1n+mp, nx), hs0, ey) 536 +hfit = fits32(k, hk, Nat.add(v(s0), v(y)), L.subst(Nat, z => {Nat.is_lt(z, C.pow2(k)) == True{} : Bool}, sum, Nat.add(v(s0), v(y)), Equal.sym(Nat, Nat.add(v(s0), v(y)), sum, esum), N.lt_trans(sum, 1n+mp, C.pow2(k), hsum, mv(k, hk, m, mp, hm)))) 537 +hao = Equal.trans(Bool, I.u32_is(NM.AddOver{s0, y}), Bool.not(C.fits(32n, Nat.add(v(s0), v(y)))), False{}, LW.tests_add_over(s0, y), Equal.cong(Bool, Bool, t => Bool.not(t), C.fits(32n, Nat.add(v(s0), v(y))), True{}, hfit)) 538 Equal.trans(Nat, v(I.u32_op(NM.Add{s0, y})), Nat.add(v(s0), v(y)), Nat.mod(sum, 1n+mp), LW.ops_add(s0, y, hao), Equal.trans(Nat, Nat.add(v(s0), v(y)), sum, Nat.mod(sum, 1n+mp), esum, Equal.sym(Nat, Nat.mod(sum, 1n+mp), sum, NF.mod_small(mp, sum, hsum)))) 539 case False{}: 540 +hl = Equal.trans(Bool, Nat.is_lt(ns0, nx), I.u32_is(NM.Lt{s0, x}), False{}, Equal.sym(Bool, I.u32_is(NM.Lt{s0, x}), Nat.is_lt(ns0, nx), ltv(s0, x, ns0, nx, hs0, hx)), hc) 541 +hlv = Equal.trans(Bool, Nat.is_lt(v(s0), v(x)), I.u32_is(NM.Lt{s0, x}), False{}, Equal.sym(Bool, I.u32_is(NM.Lt{s0, x}), Nat.is_lt(v(s0), v(x)), LW.tests_lt(s0, x)), hc) 542 Equal.trans(Nat, v(I.u32_op(NM.Sub{s0, x})), Nat.sub(v(s0), v(x)), Nat.mod(Nat.add(ns0, Nat.sub(1n+mp, nx)), 1n+mp), LW.ops_sub(s0, x, N.not_lt_le(v(s0), v(x), hlv)), Equal.trans(Nat, Nat.sub(v(s0), v(x)), Nat.sub(ns0, nx), Nat.mod(Nat.add(ns0, Nat.sub(1n+mp, nx)), 1n+mp), nsub(v(s0), v(x), ns0, nx, hs0, hx), Equal.sym(Nat, Nat.mod(Nat.add(ns0, Nat.sub(1n+mp, nx)), 1n+mp), Nat.sub(ns0, nx), NF.sm_ge(mp, ns0, nx, N.not_lt_le(ns0, nx, hl), hb0)))) 543 544 def stepv(+k: Nat, +hk: {k == 32n : Nat}, +m: U32, +mp: Nat, +hm: {v(m) == 1n+mp : Nat}, +q: U32, +s0: U32, +s1: U32, +nq: Nat, +ns0: Nat, +ns1: Nat, +hq: {v(q) == nq : Nat}, +hs0: {v(s0) == ns0 : Nat}, +hs1: {v(s1) == ns1 : Nat}, +hb0: {Nat.is_lt(ns0, 1n+mp) == True{} : Bool}, +hb1: {Nat.is_lt(ns1, 1n+mp) == True{} : Bool}) -> {v(G.inv_step(~U32, ~I.u32_op, ~I.u32_is, m, q, s0, s1)) == M.inv_step(1n+mp, nq, ns0, ns1) : Nat}: 545 +rq = I.u32_op(NM.Rem{q, m}) 546 +erq = Equal.trans(Nat, v(rq), Nat.mod(v(q), 1n+mp), Nat.mod(nq, 1n+mp), pm_rem(q, m, mp, hm), Equal.cong(Nat, Nat, t => Nat.mod(t, 1n+mp), v(q), nq, hq)) 547 +x = I.u32_op(NM.MulMod{rq, s1, m}) 548 e1 = LW.ops_mulmod(rq, s1, m, lt_mn(rq, m, mp, hm, Nat.mod(nq, 1n+mp), erq, NR.dm_lt(mp, nq)), lt_mn(s1, m, mp, hm, ns1, hs1, hb1)) 549 +e2 = Equal.trans(Nat, Nat.mod(Nat.mul(v(rq), v(s1)), v(m)), Nat.mod(Nat.mul(v(rq), v(s1)), 1n+mp), Nat.mod(Nat.mul(Nat.mod(nq, 1n+mp), ns1), 1n+mp), Equal.cong(Nat, Nat, t => Nat.mod(Nat.mul(v(rq), v(s1)), t), v(m), 1n+mp, hm), Equal.trans(Nat, Nat.mod(Nat.mul(v(rq), v(s1)), 1n+mp), Nat.mod(Nat.mul(Nat.mod(nq, 1n+mp), v(s1)), 1n+mp), Nat.mod(Nat.mul(Nat.mod(nq, 1n+mp), ns1), 1n+mp), Equal.cong(Nat, Nat, t => Nat.mod(Nat.mul(t, v(s1)), 1n+mp), v(rq), Nat.mod(nq, 1n+mp), erq), Equal.cong(Nat, Nat, t => Nat.mod(Nat.mul(Nat.mod(nq, 1n+mp), t), 1n+mp), v(s1), ns1, hs1))) 550 +ex = Equal.trans(Nat, v(x), Nat.mod(Nat.mul(v(rq), v(s1)), v(m)), Nat.mod(Nat.mul(nq, ns1), 1n+mp), e1, Equal.trans(Nat, Nat.mod(Nat.mul(v(rq), v(s1)), v(m)), Nat.mod(Nat.mul(Nat.mod(nq, 1n+mp), ns1), 1n+mp), Nat.mod(Nat.mul(nq, ns1), 1n+mp), e2, NR.mod_mul_l(mp, nq, ns1))) 551 subv(k, hk, m, mp, hm, s0, x, ns0, Nat.mod(Nat.mul(nq, ns1), 1n+mp), hs0, ex, hb0, NR.dm_lt(mp, Nat.mul(nq, ns1)), I.u32_is(NM.Lt{s0, x}), {==}) 552 553 def pv(p: U32 & U32) -> M.Bezout: 554 (+g, +s) = p 555 M.BZ{v(g), v(s)} 556 557 def bzeq(+a: Nat, +b: Nat, +na: Nat, +nb: Nat, +ha: {a == na : Nat}, +hb: {b == nb : Nat}) -> {M.BZ{a, b} == M.BZ{na, nb} : M.Bezout}: 558 Equal.trans(M.Bezout, M.BZ{a, b}, M.BZ{na, b}, M.BZ{na, nb}, Equal.cong(Nat, M.Bezout, t => M.BZ{t, b}, a, na, ha), Equal.cong(Nat, M.Bezout, t => M.BZ{na, t}, b, nb, hb)) 559 560 def or_true(+x: Bool) -> {Bool.or(x, True{}) == True{} : Bool}: 561 match x: 562 case True{}: 563 {==} 564 case False{}: 565 {==} 566 567 def invsim(+f: Nat, +k: Nat, +hk: {k == 32n : Nat}, +m: U32, +mp: Nat, +hm: {v(m) == 1n+mp : Nat}, +r0: U32, +s0: U32, +s1: U32, +r1: U32, +nr0: Nat, +ns0: Nat, +ns1: Nat, +hr0: {v(r0) == nr0 : Nat}, +hs0: {v(s0) == ns0 : Nat}, +hs1: {v(s1) == ns1 : Nat}, +hb0: {Nat.is_lt(ns0, 1n+mp) == True{} : Bool}, +cz: Bool, +nr1: Nat, +hcz: {I.u32_is(NM.IsZero{r1}) == cz : Bool}, +hr1: {v(r1) == nr1 : Nat}, +hb1: {Bool.or(Nat.is_eq(nr1, 0n), Nat.is_lt(ns1, 1n+mp)) == True{} : Bool}) -> {pv(G.inv_go(~U32, ~I.u32_op, ~I.u32_is, f, m, r0, s0, s1, (r1, cz))) == M.inv_go(f, 1n+mp, nr0, ns0, nr1, ns1) : M.Bezout}: 568 match f cz nr1: 569 case 0n _ _: 570 bzeq(v(r0), v(s0), nr0, ns0, hr0, hs0) 571 case 1n+g True{} 0n: 572 bzeq(v(r0), v(s0), nr0, ns0, hr0, hs0) 573 case 1n+g True{} 1n+rp: 574 Empty.absurd({pv(G.inv_go(~U32, ~I.u32_op, ~I.u32_is, 1n+g, m, r0, s0, s1, (r1, True{}))) == M.inv_go(1n+g, 1n+mp, nr0, ns0, 1n+rp, ns1) : M.Bezout}, true_ne_false(Equal.trans(Bool, True{}, I.u32_is(NM.IsZero{r1}), False{}, Equal.sym(Bool, I.u32_is(NM.IsZero{r1}), True{}, hcz), iz(r1, 1n+rp, hr1)))) 575 case 1n+g False{} 0n: 576 Empty.absurd({pv(G.inv_go(~U32, ~I.u32_op, ~I.u32_is, 1n+g, m, r0, s0, s1, (r1, False{}))) == M.inv_go(1n+g, 1n+mp, nr0, ns0, 0n, ns1) : M.Bezout}, true_ne_false(Equal.trans(Bool, True{}, I.u32_is(NM.IsZero{r1}), False{}, Equal.sym(Bool, I.u32_is(NM.IsZero{r1}), True{}, iz(r1, 0n, hr1)), hcz))) 577 case 1n+ +g False{} 1n+ +rp: 578 +hnz = Equal.trans(Bool, Nat.is_eq(v(r1), 0n), Nat.is_eq(1n+rp, 0n), False{}, Equal.cong(Nat, Bool, t => Nat.is_eq(t, 0n), v(r1), 1n+rp, hr1), {==}) 579 +q = I.u32_op(NM.Quot{r0, r1}) 580 +eq = Equal.trans(Nat, v(q), Nat.div(v(r0), v(r1)), Nat.div(nr0, 1n+rp), LW.ops_quot(r0, r1, hnz), Equal.trans(Nat, Nat.div(v(r0), v(r1)), Nat.div(nr0, v(r1)), Nat.div(nr0, 1n+rp), Equal.cong(Nat, Nat, t => Nat.div(t, v(r1)), v(r0), nr0, hr0), Equal.cong(Nat, Nat, t => Nat.div(nr0, t), v(r1), 1n+rp, hr1))) 581 +r2 = I.u32_op(NM.Rem{r0, r1}) 582 +er2 = Equal.trans(Nat, v(r2), Nat.mod(v(r0), v(r1)), Nat.mod(nr0, 1n+rp), LW.ops_rem(r0, r1, hnz), Equal.trans(Nat, Nat.mod(v(r0), v(r1)), Nat.mod(nr0, v(r1)), Nat.mod(nr0, 1n+rp), Equal.cong(Nat, Nat, t => Nat.mod(t, v(r1)), v(r0), nr0, hr0), Equal.cong(Nat, Nat, t => Nat.mod(nr0, t), v(r1), 1n+rp, hr1))) 583 +ns2 = M.inv_step(1n+mp, Nat.div(nr0, 1n+rp), ns0, ns1) 584 +es2 = stepv(k, hk, m, mp, hm, q, s0, s1, Nat.div(nr0, 1n+rp), ns0, ns1, eq, hs0, hs1, hb0, hb1) 585 +hb2 = L.subst(Bool, t => {Bool.or(Nat.is_eq(Nat.mod(nr0, 1n+rp), 0n), t) == True{} : Bool}, True{}, Nat.is_lt(ns2, 1n+mp), Equal.sym(Bool, Nat.is_lt(ns2, 1n+mp), True{}, NR.dm_lt(mp, Nat.add(ns0, Nat.sub(1n+mp, Nat.mod(Nat.mul(Nat.div(nr0, 1n+rp), ns1), 1n+mp))))), or_true(Nat.is_eq(Nat.mod(nr0, 1n+rp), 0n))) 586 invsim(g, k, hk, m, mp, hm, r1, s1, G.inv_step(~U32, ~I.u32_op, ~I.u32_is, m, q, s0, s1), r2, 1n+rp, ns1, ns2, hr1, hs1, es2, hb1, I.u32_is(NM.IsZero{r2}), Nat.mod(nr0, 1n+rp), {==}, er2, hb2) 587 588 def fin2(+m: U32, +mp: Nat, +hm: {v(m) == 1n+mp : Nat}, +s: U32, +sn: Nat, +hs: {v(s) == sn : Nat}, +cb: Bool, +gn: Nat, +hcb: {Bool.and(Bool.not(Nat.is_lt(gn, 1n)), Bool.not(Nat.is_lt(1n, gn))) == cb : Bool}) -> {G.inv_one(~U32, ~I.u32_op, m, s, cb) == SG.lift(~U32, ~SG.u32_of, M.inv_fin(1n+mp, M.BZ{gn, sn})) : Result<&2, &2, NM.NumError, U32>}: 589 match cb gn: 590 case True{} 1n: 591 Equal.cong(U32, Result<&2, &2, NM.NumError, U32>, t => Done{t}, I.u32_op(NM.Rem{s, m}), of(Nat.mod(sn, 1n+mp)), as_of(I.u32_op(NM.Rem{s, m}), Nat.mod(sn, 1n+mp), Equal.trans(Nat, v(I.u32_op(NM.Rem{s, m})), Nat.mod(v(s), 1n+mp), Nat.mod(sn, 1n+mp), pm_rem(s, m, mp, hm), Equal.cong(Nat, Nat, t => Nat.mod(t, 1n+mp), v(s), sn, hs)))) 592 case False{} 1n: 593 Empty.absurd({G.inv_one(~U32, ~I.u32_op, m, s, False{}) == SG.lift(~U32, ~SG.u32_of, M.inv_fin(1n+mp, M.BZ{1n, sn})) : Result<&2, &2, NM.NumError, U32>}, true_ne_false(hcb)) 594 case True{} 0n: 595 Empty.absurd({G.inv_one(~U32, ~I.u32_op, m, s, True{}) == SG.lift(~U32, ~SG.u32_of, M.inv_fin(1n+mp, M.BZ{0n, sn})) : Result<&2, &2, NM.NumError, U32>}, true_ne_false(Equal.sym(Bool, False{}, True{}, hcb))) 596 case False{} 0n: 597 {==} 598 case True{} 2n+h: 599 Empty.absurd({G.inv_one(~U32, ~I.u32_op, m, s, True{}) == SG.lift(~U32, ~SG.u32_of, M.inv_fin(1n+mp, M.BZ{2n+h, sn})) : Result<&2, &2, NM.NumError, U32>}, true_ne_false(Equal.sym(Bool, False{}, True{}, hcb))) 600 case False{} 2n+h: 601 {==} 602 603 def finsim(+m: U32, +mp: Nat, +hm: {v(m) == 1n+mp : Nat}, p: U32 & U32, +bz: M.Bezout, +h: {pv(p) == bz : M.Bezout}) -> {G.inv_fin(~U32, ~I.u32_op, ~I.u32_is, m, p) == SG.lift(~U32, ~SG.u32_of, M.inv_fin(1n+mp, bz)) : Result<&2, &2, NM.NumError, U32>}: 604 match p bz: 605 case Tuple{+g, +s} M.BZ{+gn, +sn}: 606 +hg = Equal.cong(M.Bezout, Nat, z => IV.bg(z), M.BZ{v(g), v(s)}, M.BZ{gn, sn}, h) 607 +hs = Equal.cong(M.Bezout, Nat, z => IV.bc(z), M.BZ{v(g), v(s)}, M.BZ{gn, sn}, h) 608 +one = I.u32_op(NM.One{}) 609 +e = Equal.trans(Bool, Bool.and(Bool.not(I.u32_is(NM.Lt{g, one})), Bool.not(I.u32_is(NM.Lt{one, g}))), Bool.and(Bool.not(Nat.is_lt(gn, 1n)), Bool.not(I.u32_is(NM.Lt{one, g}))), Bool.and(Bool.not(Nat.is_lt(gn, 1n)), Bool.not(Nat.is_lt(1n, gn))), Equal.cong(Bool, Bool, t => Bool.and(Bool.not(t), Bool.not(I.u32_is(NM.Lt{one, g}))), I.u32_is(NM.Lt{g, one}), Nat.is_lt(gn, 1n), ltv(g, one, gn, 1n, hg, one_v())), Equal.cong(Bool, Bool, t => Bool.and(Bool.not(Nat.is_lt(gn, 1n)), Bool.not(t)), I.u32_is(NM.Lt{one, g}), Nat.is_lt(1n, gn), ltv(one, g, 1n, gn, one_v(), hg))) 610 fin2(m, mp, hm, s, sn, hs, Bool.and(Bool.not(I.u32_is(NM.Lt{g, one})), Bool.not(I.u32_is(NM.Lt{one, g}))), gn, Equal.sym(Bool, Bool.and(Bool.not(I.u32_is(NM.Lt{g, one})), Bool.not(I.u32_is(NM.Lt{one, g}))), Bool.and(Bool.not(Nat.is_lt(gn, 1n)), Bool.not(Nat.is_lt(1n, gn))), e)) 611 612 def lt1_eq(+x: Nat, +h: {Nat.is_lt(x, 1n) == True{} : Bool}) -> {Nat.is_eq(x, 0n) == True{} : Bool}: 613 match x: 614 case 0n: 615 {==} 616 case 1n+y: 617 Empty.absurd({Nat.is_eq(1n+y, 0n) == True{} : Bool}, N.lt_zero_absurd(y, h)) 618 619 def hb_init(+mp: Nat, +a: Nat) -> {Bool.or(Nat.is_eq(Nat.mod(a, 1n+mp), 0n), Nat.is_lt(1n, 1n+mp)) == True{} : Bool}: 620 match mp: 621 case 0n: 622 L.subst(Bool, t => {Bool.or(t, Nat.is_lt(1n, 1n)) == True{} : Bool}, True{}, Nat.is_eq(Nat.mod(a, 1n), 0n), Equal.sym(Bool, Nat.is_eq(Nat.mod(a, 1n), 0n), True{}, lt1_eq(Nat.mod(a, 1n), NR.dm_lt(0n, a))), {==}) 623 case 1n+q: 624 or_true(Nat.is_eq(Nat.mod(a, 2n+q), 0n)) 625 626 def inv_top(+k: Nat, +hk: {k == 32n : Nat}, +a: U32, +m: U32, +c: Bool, +hc: {I.u32_is(NM.IsZero{m}) == c : Bool}, +nm: Nat, +hnm: {v(m) == nm : Nat}) -> {G.inv_ok(~U32, ~I.u32_op, ~I.u32_is, a, m, c) == SG.lift(~U32, ~SG.u32_of, M.mod_inverse(v(a), nm)) : Result<&2, &2, NM.NumError, U32>}: 627 match c nm: 628 case True{} 0n: 629 {==} 630 case False{} 0n: 631 Empty.absurd({G.inv_ok(~U32, ~I.u32_op, ~I.u32_is, a, m, False{}) == SG.lift(~U32, ~SG.u32_of, M.mod_inverse(v(a), 0n)) : Result<&2, &2, NM.NumError, U32>}, true_ne_false(Equal.trans(Bool, True{}, I.u32_is(NM.IsZero{m}), False{}, Equal.sym(Bool, I.u32_is(NM.IsZero{m}), True{}, iz(m, 0n, hnm)), hc))) 632 case True{} 1n+ +mp: 633 Empty.absurd({G.inv_ok(~U32, ~I.u32_op, ~I.u32_is, a, m, True{}) == SG.lift(~U32, ~SG.u32_of, M.mod_inverse(v(a), 1n+mp)) : Result<&2, &2, NM.NumError, U32>}, true_ne_false(Equal.trans(Bool, True{}, I.u32_is(NM.IsZero{m}), False{}, Equal.sym(Bool, I.u32_is(NM.IsZero{m}), True{}, hc), iz(m, 1n+mp, hnm)))) 634 case False{} 1n+ +mp: 635 +r1 = I.u32_op(NM.Rem{a, m}) 636 +ra = Nat.mod(v(a), 1n+mp) 637 +hk2 = L.subst(Nat, z => {Nat.is_le(1n+Nat.double(z), 140n) == True{} : Bool}, 32n, k, Equal.sym(Nat, k, 32n, hk), {==}) 638 +s = invsim(140n, k, hk, m, mp, hnm, m, I.u32_op(NM.ZeroOp{}), I.u32_op(NM.One{}), r1, 1n+mp, 0n, 1n, hnm, zero_v(), one_v(), {==}, I.u32_is(NM.IsZero{r1}), ra, {==}, pm_rem(a, m, mp, hnm), hb_init(mp, v(a))) 639 +bz = M.inv_go(1n+mp, 1n+mp, 1n+mp, 0n, ra, 1n) 640 g = G.inv_go(~U32, ~I.u32_op, ~I.u32_is, 140n, m, m, I.u32_op(NM.ZeroOp{}), I.u32_op(NM.One{}), (r1, I.u32_is(NM.IsZero{r1}))) 641 finsim(m, mp, hnm, g, bz, Equal.trans(M.Bezout, pv(g), M.inv_go(140n, 1n+mp, 1n+mp, 0n, ra, 1n), bz, s, NF.inv_140(k, mp, v(a), hk2, mv(k, hk, m, mp, hnm)))) 642 643 def modinv_agrees(+a: U32, +m: U32) -> SG.ModInverse.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, a, m): 644 inv_top(32n, {==}, a, m, I.u32_is(NM.IsZero{m}), {==}, v(m), {==}) 645 646 # ---- ilog: the multiply-up loop on the values ---- 647 648 def nle(+a: Nat, +b: Nat, +c: Bool, +hc: {Nat.is_lt(a, b) == c : Bool}) -> {Bool.not(c) == Nat.is_le(b, a) : Bool}: 649 match c: 650 case True{}: 651 Equal.sym(Bool, Nat.is_le(b, a), False{}, N.lt_not_le(a, b, hc)) 652 case False{}: 653 Equal.sym(Bool, Nat.is_le(b, a), True{}, N.not_lt_le(a, b, hc)) 654 655 def nmul(+a: Nat, +b: Nat, +na: Nat, +nb: Nat, +ha: {a == na : Nat}, +hb: {b == nb : Nat}) -> {Nat.mul(a, b) == Nat.mul(na, nb) : Nat}: 656 Equal.trans(Nat, Nat.mul(a, b), Nat.mul(na, b), Nat.mul(na, nb), Equal.cong(Nat, Nat, t => Nat.mul(t, b), a, na, ha), Equal.cong(Nat, Nat, t => Nat.mul(na, t), b, nb, hb)) 657 658 # le(x, y) on U32 is is_le on the values 659 def lev(+x: U32, +y: U32, +nx: Nat, +ny: Nat, +hx: {v(x) == nx : Nat}, +hy: {v(y) == ny : Nat}) -> {G.le(~U32, ~I.u32_is, x, y) == Nat.is_le(nx, ny) : Bool}: 660 Equal.trans(Bool, Bool.not(I.u32_is(NM.Lt{y, x})), Bool.not(Nat.is_lt(ny, nx)), Nat.is_le(nx, ny), Equal.cong(Bool, Bool, t => Bool.not(t), I.u32_is(NM.Lt{y, x}), Nat.is_lt(ny, nx), ltv(y, x, ny, nx, hy, hx)), nle(ny, nx, Nat.is_lt(ny, nx), {==})) 661 662 def ilsim(+f: Nat, +q: U32, +b: U32, +k: Nat, +p: U32, +nn: Nat, +bq: Nat, +np: Nat, +hq: {v(q) == Nat.div(nn, 2n+bq) : Nat}, +hb: {v(b) == 2n+bq : Nat}, +hp: {v(p) == np : Nat}, +K: Nat, +hK: {K == 32n : Nat}, +hn: {Nat.is_lt(nn, C.pow2(K)) == True{} : Bool}, +up: Bool, +hup: {up == Nat.is_le(np, Nat.div(nn, 2n+bq)) : Bool}) -> {G.ilog_go(~U32, ~I.u32_op, ~I.u32_is, f, q, b, k, p, up) == M.ilog_go(f, nn, 2n+bq, k, np, up) : Nat}: 663 match f up: 664 case 0n _: 665 {==} 666 case 1n+g False{}: 667 {==} 668 case 1n+ +g True{}: 669 +hle = Equal.sym(Bool, True{}, Nat.is_le(np, Nat.div(nn, 2n+bq)), hup) 670 +hmn = Equal.trans(Bool, Nat.is_le(Nat.mul(np, 2n+bq), nn), Nat.is_le(np, Nat.div(nn, 2n+bq)), True{}, Equal.sym(Bool, Nat.is_le(np, Nat.div(nn, 2n+bq)), Nat.is_le(Nat.mul(np, 2n+bq), nn), NR.le_div(1n+bq, np, nn)), hle) 671 +emul = nmul(v(p), v(b), np, 2n+bq, hp, hb) 672 +hfit = fits32(K, hK, Nat.mul(v(p), v(b)), L.subst(Nat, z => {Nat.is_lt(z, C.pow2(K)) == True{} : Bool}, Nat.mul(np, 2n+bq), Nat.mul(v(p), v(b)), Equal.sym(Nat, Nat.mul(v(p), v(b)), Nat.mul(np, 2n+bq), emul), N.le_lt_trans(Nat.mul(np, 2n+bq), nn, C.pow2(K), hmn, hn))) 673 +hmo = Equal.trans(Bool, I.u32_is(NM.MulOver{p, b}), Bool.not(C.fits(32n, Nat.mul(v(p), v(b)))), False{}, LW.tests_mul_over(p, b), Equal.cong(Bool, Bool, t => Bool.not(t), C.fits(32n, Nat.mul(v(p), v(b))), True{}, hfit)) 674 +pb = I.u32_op(NM.Mul{p, b}) 675 +epb = Equal.trans(Nat, v(pb), Nat.mul(v(p), v(b)), Nat.mul(np, 2n+bq), LW.ops_mul(p, b, hmo), emul) 676 +u2 = G.le(~U32, ~I.u32_is, pb, q) 677 +hu2 = lev(pb, q, Nat.mul(np, 2n+bq), Nat.div(nn, 2n+bq), epb, hq) 678 Equal.trans(Nat, G.ilog_go(~U32, ~I.u32_op, ~I.u32_is, g, q, b, 1n+k, pb, u2), M.ilog_go(g, nn, 2n+bq, 1n+k, Nat.mul(np, 2n+bq), u2), M.ilog_go(g, nn, 2n+bq, 1n+k, Nat.mul(np, 2n+bq), Nat.is_le(Nat.mul(np, 2n+bq), Nat.div(nn, 2n+bq))), ilsim(g, q, b, 1n+k, pb, nn, bq, Nat.mul(np, 2n+bq), hq, hb, epb, K, hK, hn, u2, hu2), Equal.cong(Bool, Nat, t => M.ilog_go(g, nn, 2n+bq, 1n+k, Nat.mul(np, 2n+bq), t), u2, Nat.is_le(Nat.mul(np, 2n+bq), Nat.div(nn, 2n+bq)), hu2)) 679 680 def or_false_r(+x: Bool, +y: Bool, +h: {Bool.or(x, y) == False{} : Bool}) -> {y == False{} : Bool}: 681 match x: 682 case True{}: 683 Empty.absurd({y == False{} : Bool}, true_ne_false(h)) 684 case False{}: 685 h 686 687 def ilog_fin(+K: Nat, +hK: {K == 32n : Nat}, +n: U32, +b: U32, +nb: Nat, +hb: {v(b) == nb : Nat}, +hl: {Nat.is_lt(nb, 2n) == False{} : Bool}) -> {G.ilog_ok(~U32, ~I.u32_op, ~I.u32_is, n, b, False{}) == SG.lift_nat(M.ilog_ok(v(n), nb, False{})) : Result<&2, &2, NM.NumError, Nat>}: 688 match nb: 689 case 0n: 690 Empty.absurd({G.ilog_ok(~U32, ~I.u32_op, ~I.u32_is, n, b, False{}) == SG.lift_nat(M.ilog_ok(v(n), 0n, False{})) : Result<&2, &2, NM.NumError, Nat>}, true_ne_false(hl)) 691 case 1n: 692 Empty.absurd({G.ilog_ok(~U32, ~I.u32_op, ~I.u32_is, n, b, False{}) == SG.lift_nat(M.ilog_ok(v(n), 1n, False{})) : Result<&2, &2, NM.NumError, Nat>}, true_ne_false(hl)) 693 case 2n+ +bq: 694 +hnz = Equal.trans(Bool, Nat.is_eq(v(b), 0n), Nat.is_eq(2n+bq, 0n), False{}, Equal.cong(Nat, Bool, t => Nat.is_eq(t, 0n), v(b), 2n+bq, hb), {==}) 695 +q = I.u32_op(NM.Quot{n, b}) 696 +dq = Nat.div(v(n), 2n+bq) 697 +eq = Equal.trans(Nat, v(q), Nat.div(v(n), v(b)), dq, LW.ops_quot(n, b, hnz), Equal.cong(Nat, Nat, t => Nat.div(v(n), t), v(b), 2n+bq, hb)) 698 +one = I.u32_op(NM.One{}) 699 +up = G.le(~U32, ~I.u32_is, one, q) 700 +hup = lev(one, q, 1n, dq, one_v(), eq) 701 +hn = U32P.val_lt(1n, {==}, K, hK, n) 702 +hK2 = L.subst(Nat, z => {Nat.is_le(z, 140n) == True{} : Bool}, 32n, K, Equal.sym(Nat, K, 32n, hK), {==}) 703 +s = ilsim(140n, q, b, 0n, one, v(n), bq, 1n, eq, hb, one_v(), K, hK, hn, up, hup) 704 +c1 = Equal.cong(Bool, Nat, t => M.ilog_go(140n, v(n), 2n+bq, 0n, 1n, t), up, Nat.is_le(1n, dq), hup) 705 +c2 = NF.il_140(K, v(n), bq, hK2, N.le_lt_trans(dq, v(n), C.pow2(K), AR2.div_le(v(n), 2n+bq), hn)) 706 +r = M.ilog_go(v(n), v(n), 2n+bq, 0n, 1n, Nat.is_le(1n, dq)) 707 Equal.cong(Nat, Result<&2, &2, NM.NumError, Nat>, t => Done{t}, G.ilog_go(~U32, ~I.u32_op, ~I.u32_is, 140n, q, b, 0n, one, up), r, Equal.trans(Nat, G.ilog_go(~U32, ~I.u32_op, ~I.u32_is, 140n, q, b, 0n, one, up), M.ilog_go(140n, v(n), 2n+bq, 0n, 1n, up), r, s, Equal.trans(Nat, M.ilog_go(140n, v(n), 2n+bq, 0n, 1n, up), M.ilog_go(140n, v(n), 2n+bq, 0n, 1n, Nat.is_le(1n, dq)), r, c1, c2))) 708 709 def ilog_top(+K: Nat, +hK: {K == 32n : Nat}, +n: U32, +b: U32, +bad: Bool, +hN: {Bool.or(Nat.is_eq(v(n), 0n), Nat.is_lt(v(b), 2n)) == bad : Bool}) -> {G.ilog_ok(~U32, ~I.u32_op, ~I.u32_is, n, b, bad) == SG.lift_nat(M.ilog_ok(v(n), v(b), bad)) : Result<&2, &2, NM.NumError, Nat>}: 710 match bad: 711 case True{}: 712 {==} 713 case False{}: 714 ilog_fin(K, hK, n, b, v(b), {==}, or_false_r(Nat.is_eq(v(n), 0n), Nat.is_lt(v(b), 2n), hN)) 715 716 def two_v() -> {v(I.u32_op(NM.Add{I.u32_op(NM.One{}), I.u32_op(NM.One{})})) == 2n : Nat}: 717 +one = I.u32_op(NM.One{}) 718 +e11 = nadd(v(one), v(one), 1n, 1n, one_v(), one_v()) 719 +hao = Equal.trans(Bool, I.u32_is(NM.AddOver{one, one}), Bool.not(C.fits(32n, Nat.add(v(one), v(one)))), False{}, LW.tests_add_over(one, one), Equal.cong(Nat, Bool, t => Bool.not(C.fits(32n, t)), Nat.add(v(one), v(one)), 2n, e11)) 720 Equal.trans(Nat, v(I.u32_op(NM.Add{one, one})), Nat.add(v(one), v(one)), 2n, LW.ops_add(one, one, hao), e11) 721 722 def ilog_agrees(+n: U32, +b: U32) -> SG.Ilog.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, n, b): 723 +two = I.u32_op(NM.Add{I.u32_op(NM.One{}), I.u32_op(NM.One{})}) 724 +bu = Bool.or(I.u32_is(NM.IsZero{n}), I.u32_is(NM.Lt{b, two})) 725 +bn = Bool.or(Nat.is_eq(v(n), 0n), Nat.is_lt(v(b), 2n)) 726 +eb = Equal.trans(Bool, bu, Bool.or(Nat.is_eq(v(n), 0n), I.u32_is(NM.Lt{b, two})), bn, Equal.cong(Bool, Bool, t => Bool.or(t, I.u32_is(NM.Lt{b, two})), I.u32_is(NM.IsZero{n}), Nat.is_eq(v(n), 0n), LW.tests_is_zero(n)), Equal.cong(Bool, Bool, t => Bool.or(Nat.is_eq(v(n), 0n), t), I.u32_is(NM.Lt{b, two}), Nat.is_lt(v(b), 2n), ltv(b, two, v(b), 2n, {==}, two_v()))) 727 Equal.trans(Result<&2, &2, NM.NumError, Nat>, G.ilog_ok(~U32, ~I.u32_op, ~I.u32_is, n, b, bu), SG.lift_nat(M.ilog_ok(v(n), v(b), bu)), SG.lift_nat(M.ilog_ok(v(n), v(b), bn)), ilog_top(32n, {==}, n, b, bu, Equal.sym(Bool, bu, bn, eb)), Equal.cong(Bool, Result<&2, &2, NM.NumError, Nat>, t => SG.lift_nat(M.ilog_ok(v(n), v(b), t)), bu, bn, eb)) 728 729 # ---- factorial: 2 * 3 * ... bottom-up, stopping at the first overflow ---- 730 731 # the value when the flag says it fits 732 def FR(ok: Bool, a: U32, x: Nat) -> Type: 733 match ok: 734 case True{}: 735 {v(a) == x : Nat} 736 case False{}: 737 {x == x : Nat} 738 739 def not_not(+c: Bool) -> {Bool.not(Bool.not(c)) == c : Bool}: 740 match c: 741 case True{}: 742 {==} 743 case False{}: 744 {==} 745 746 def fr_mul(+a: U32, +x: U32, +n: Nat, +hn: {Nat.mul(v(a), v(x)) == n : Nat}, +c: Bool, +hc: {C.fits(32n, n) == c : Bool}) -> FR(Bool.not(I.u32_is(NM.MulOver{a, x})), I.u32_op(NM.Mul{a, x}), n): 747 match c: 748 case True{}: 749 +hmo = mo_of(a, x, n, hn, True{}, hc) 750 %Equal.sym(Bool, I.u32_is(NM.MulOver{a, x}), False{}, hmo) : FR(Bool.not(_), I.u32_op(NM.Mul{a, x}), n) 751 Equal.trans(Nat, v(I.u32_op(NM.Mul{a, x})), Nat.mul(v(a), v(x)), n, LW.ops_mul(a, x, hmo), hn) 752 case False{}: 753 %Equal.sym(Bool, I.u32_is(NM.MulOver{a, x}), True{}, mo_of(a, x, n, hn, False{}, hc)) : FR(Bool.not(_), I.u32_op(NM.Mul{a, x}), n) 754 {==} 755 756 # the flag after a checked multiply is fits(product) 757 def ok_mul(+a: U32, +x: U32, +n: Nat, +hn: {Nat.mul(v(a), v(x)) == n : Nat}) -> {C.fits(32n, n) == Bool.not(I.u32_is(NM.MulOver{a, x})) : Bool}: 758 Equal.sym(Bool, Bool.not(I.u32_is(NM.MulOver{a, x})), C.fits(32n, n), Equal.trans(Bool, Bool.not(I.u32_is(NM.MulOver{a, x})), Bool.not(Bool.not(C.fits(32n, n))), C.fits(32n, n), Equal.cong(Bool, Bool, t => Bool.not(t), I.u32_is(NM.MulOver{a, x}), Bool.not(C.fits(32n, n)), mo_of(a, x, n, hn, C.fits(32n, n), {==})), not_not(C.fits(32n, n)))) 759 760 def fk(+K: Nat, +hK: {K == 32n : Nat}, +x: Nat, +h: {C.fits(32n, x) == True{} : Bool}) -> {Nat.is_lt(x, C.pow2(K)) == True{} : Bool}: 761 +h2 = L.subst(Nat, z => {C.fits(z, x) == True{} : Bool}, 32n, K, Equal.sym(Nat, K, 32n, hK), h) 762 Equal.trans(Bool, Nat.is_lt(x, C.pow2(K)), C.fits(K, x), True{}, Equal.sym(Bool, C.fits(K, x), Nat.is_lt(x, C.pow2(K)), WW.fits_lt(K, x)), h2) 763 764 def succ_le(+a: Nat, +b: Nat, +h: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.is_le(1n+a, b) == True{} : Bool}: 765 match a b: 766 case _ 0n: 767 Empty.absurd({Nat.is_le(1n+a, 0n) == True{} : Bool}, N.lt_zero_absurd(a, h)) 768 case 0n 1n+y: 769 N.zero_le(y) 770 case 1n+ +x 1n+ +y: 771 succ_le(x, y, h) 772 773 def plus1(+x: Nat) -> {Nat.add(x, 1n) == 1n+x : Nat}: 774 Equal.trans(Nat, Nat.add(x, 1n), 1n+Nat.add(x, 0n), 1n+x, NA.add_succ(x, 0n), Equal.cong(Nat, Nat, t => 1n+t, Nat.add(x, 0n), x, N.add_zero(x))) 775 776 # inc(i) for i < n is i + 1 777 def inc_v(+K: Nat, +hK: {K == 32n : Nat}, +i: U32, +n: U32, +ni: Nat, +nn: Nat, +hi: {v(i) == ni : Nat}, +hn: {v(n) == nn : Nat}, +hlt: {Nat.is_lt(ni, nn) == True{} : Bool}) -> {v(G.inc(~U32, ~I.u32_op, i)) == 1n+ni : Nat}: 778 +one = I.u32_op(NM.One{}) 779 +hnK = L.subst(Nat, z => {Nat.is_lt(z, C.pow2(K)) == True{} : Bool}, v(n), nn, hn, U32P.val_lt(1n, {==}, K, hK, n)) 780 +hfit = fits32(K, hK, 1n+ni, N.le_lt_trans(1n+ni, nn, C.pow2(K), succ_le(ni, nn, hlt), hnK)) 781 +hn1 = Equal.trans(Nat, Nat.add(v(i), v(one)), Nat.add(ni, 1n), 1n+ni, nadd(v(i), v(one), ni, 1n, hi, one_v()), plus1(ni)) 782 Equal.trans(Nat, v(I.u32_op(NM.Add{i, one})), Nat.add(v(i), v(one)), 1n+ni, LW.ops_add(i, one, ao_of(i, one, 1n+ni, hn1, True{}, hfit)), hn1) 783 784 def factsim(+f: Nat, +i: U32, +n: U32, +a: U32, +ni: Nat, +nn: Nat, +K: Nat, +ok: Bool, +more: Bool, +cn: Bool, +hK: {K == 32n : Nat}, +hi: {v(i) == ni : Nat}, +hn: {v(n) == nn : Nat}, +hmono: {Nat.is_le(S.factorial(ni), S.factorial(nn)) == True{} : Bool}, +hf: {Nat.is_le(1n+K, Nat.add(f, ni)) == True{} : Bool}, +hok: {C.fits(32n, S.factorial(ni)) == ok : Bool}, ha: FR(ok, a, S.factorial(ni)), +hmore: {more == Nat.is_lt(ni, nn) : Bool}, +hcn: {C.fits(32n, S.factorial(nn)) == cn : Bool}) -> {G.fact_go(~U32, ~I.u32_op, ~I.u32_is, f, i, n, (a, ok), more) == G.fits(U32, Bool.not(cn), of(S.factorial(nn))) : Maybe<&2, U32>}: 785 match f ok more cn: 786 case 0n True{} _ _: 787 +big = NF.fbig(K, ni, hf) 788 Empty.absurd({G.fact_go(~U32, ~I.u32_op, ~I.u32_is, 0n, i, n, (a, True{}), more) == G.fits(U32, Bool.not(cn), of(S.factorial(nn))) : Maybe<&2, U32>}, true_ne_false(Equal.trans(Bool, True{}, Nat.is_lt(S.factorial(ni), C.pow2(K)), False{}, Equal.sym(Bool, Nat.is_lt(S.factorial(ni), C.pow2(K)), True{}, fk(K, hK, S.factorial(ni), hok)), N.le_not_lt(S.factorial(ni), C.pow2(K), big)))) 789 case 0n False{} _ True{}: 790 Empty.absurd({G.fact_go(~U32, ~I.u32_op, ~I.u32_is, 0n, i, n, (a, False{}), more) == G.fits(U32, Bool.not(True{}), of(S.factorial(nn))) : Maybe<&2, U32>}, true_ne_false(Equal.trans(Bool, True{}, C.fits(32n, S.factorial(nn)), False{}, Equal.sym(Bool, C.fits(32n, S.factorial(nn)), True{}, hcn), unfit_mono(32n, S.factorial(ni), S.factorial(nn), hmono, hok)))) 791 case 0n False{} _ False{}: 792 {==} 793 case 1n+g False{} _ True{}: 794 Empty.absurd({G.fact_go(~U32, ~I.u32_op, ~I.u32_is, 1n+g, i, n, (a, False{}), more) == G.fits(U32, Bool.not(True{}), of(S.factorial(nn))) : Maybe<&2, U32>}, true_ne_false(Equal.trans(Bool, True{}, C.fits(32n, S.factorial(nn)), False{}, Equal.sym(Bool, C.fits(32n, S.factorial(nn)), True{}, hcn), unfit_mono(32n, S.factorial(ni), S.factorial(nn), hmono, hok)))) 795 case 1n+g False{} _ False{}: 796 {==} 797 case 1n+g True{} False{} True{}: 798 +eqF = N.le_antisym(S.factorial(ni), S.factorial(nn), hmono, NF.fmono(nn, ni, N.not_lt_le(ni, nn, Equal.sym(Bool, False{}, Nat.is_lt(ni, nn), hmore)))) 799 Equal.cong(U32, Maybe<&2, U32>, t => Some{t}, a, of(S.factorial(nn)), as_of(a, S.factorial(nn), Equal.trans(Nat, v(a), S.factorial(ni), S.factorial(nn), ha, eqF))) 800 case 1n+g True{} False{} False{}: 801 +eqF = N.le_antisym(S.factorial(ni), S.factorial(nn), hmono, NF.fmono(nn, ni, N.not_lt_le(ni, nn, Equal.sym(Bool, False{}, Nat.is_lt(ni, nn), hmore)))) 802 Empty.absurd({G.fact_go(~U32, ~I.u32_op, ~I.u32_is, 1n+g, i, n, (a, True{}), False{}) == G.fits(U32, Bool.not(False{}), of(S.factorial(nn))) : Maybe<&2, U32>}, true_ne_false(Equal.trans(Bool, True{}, C.fits(32n, S.factorial(ni)), False{}, Equal.sym(Bool, C.fits(32n, S.factorial(ni)), True{}, hok), Equal.trans(Bool, C.fits(32n, S.factorial(ni)), C.fits(32n, S.factorial(nn)), False{}, Equal.cong(Nat, Bool, t => C.fits(32n, t), S.factorial(ni), S.factorial(nn), eqF), hcn)))) 803 case 1n+ +g True{} True{} _: 804 +hlt = Equal.sym(Bool, True{}, Nat.is_lt(ni, nn), hmore) 805 +x = G.inc(~U32, ~I.u32_op, i) 806 +ex = inc_v(K, hK, i, n, ni, nn, hi, hn, hlt) 807 +pn = S.factorial(1n+ni) 808 +hpn = Equal.trans(Nat, Nat.mul(v(a), v(x)), Nat.mul(S.factorial(ni), 1n+ni), pn, nmul(v(a), v(x), S.factorial(ni), 1n+ni, ha, ex), NA.mul_comm(S.factorial(ni), 1n+ni)) 809 +hf2 = L.subst(Nat, z => {Nat.is_le(1n+K, z) == True{} : Bool}, 1n+Nat.add(g, ni), Nat.add(g, 1n+ni), Equal.sym(Nat, Nat.add(g, 1n+ni), 1n+Nat.add(g, ni), NA.add_succ(g, ni)), hf) 810 factsim(g, x, n, I.u32_op(NM.Mul{a, x}), 1n+ni, nn, K, Bool.not(I.u32_is(NM.MulOver{a, x})), I.u32_is(NM.Lt{x, n}), cn, hK, ex, hn, NF.fmono(1n+ni, nn, succ_le(ni, nn, hlt)), hf2, ok_mul(a, x, pn, hpn), fr_mul(a, x, pn, hpn, C.fits(32n, pn), {==}), ltv(x, n, 1n+ni, nn, ex, hn), hcn) 811 812 def okfits(+x: Nat, +c: Bool) -> {G.ok(U32, G.fits(U32, Bool.not(c), of(x))) == SG.checked_pick(~U32, ~SG.u32_of, x, c) : Result<&2, &2, NM.NumError, U32>}: 813 match c: 814 case True{}: 815 {==} 816 case False{}: 817 {==} 818 819 def fact_top(+K: Nat, +hK: {K == 32n : Nat}, +n: U32) -> SG.Factorial.checked(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 32n, n): 820 +one = I.u32_op(NM.One{}) 821 +F = S.factorial(v(n)) 822 +hf0 = L.subst(Nat, z => {Nat.is_le(1n+z, 141n) == True{} : Bool}, 32n, K, Equal.sym(Nat, K, 32n, hK), {==}) 823 +s = factsim(140n, one, n, one, 1n, v(n), K, True{}, I.u32_is(NM.Lt{one, n}), C.fits(32n, F), hK, one_v(), {==}, NF.fmono(0n, v(n), N.zero_le(v(n))), hf0, {==}, one_v(), ltv(one, n, 1n, v(n), one_v(), {==}), {==}) 824 +g = G.fact_go(~U32, ~I.u32_op, ~I.u32_is, 140n, one, n, (one, True{}), I.u32_is(NM.Lt{one, n})) 825 Equal.trans(Result<&2, &2, NM.NumError, U32>, G.ok(U32, g), SG.checked_pick(~U32, ~SG.u32_of, F, C.fits(32n, F)), SG.checked(~U32, ~SG.u32_of, 32n, M.factorial(v(n))), Equal.trans(Result<&2, &2, NM.NumError, U32>, G.ok(U32, g), G.ok(U32, G.fits(U32, Bool.not(C.fits(32n, F)), of(F))), SG.checked_pick(~U32, ~SG.u32_of, F, C.fits(32n, F)), Equal.cong(Maybe<&2, U32>, Result<&2, &2, NM.NumError, U32>, t => G.ok(U32, t), g, G.fits(U32, Bool.not(C.fits(32n, F)), of(F)), s), okfits(F, C.fits(32n, F))), Equal.cong(Nat, Result<&2, &2, NM.NumError, U32>, t => SG.checked(~U32, ~SG.u32_of, 32n, t), F, M.factorial(v(n)), Equal.sym(Nat, M.factorial(v(n)), F, FA.factorial_ok(v(n))))) 826 827 def factorial_checked(+n: U32) -> SG.Factorial.checked(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 32n, n): 828 fact_top(32n, {==}, n) 829 830 # ---- perm: n (n - 1) ... multiplied top-down, j factors taken, r left ---- 831 832 def pmon(+nn: Nat, +j: Nat, +r: Nat, +k0: Nat, +hj: {Nat.add(j, r) == k0 : Nat}, +hle: {Nat.is_le(k0, nn) == True{} : Bool}) -> {Nat.is_le(S.desc(nn, j), S.desc(nn, k0)) == True{} : Bool}: 833 +h1 = NF.dmono(nn, j, r, L.subst(Nat, z => {Nat.is_le(z, nn) == True{} : Bool}, k0, Nat.add(j, r), Equal.sym(Nat, Nat.add(j, r), k0, hj), hle)) 834 L.subst(Nat, z => {Nat.is_le(S.desc(nn, j), S.desc(nn, z)) == True{} : Bool}, Nat.add(j, r), k0, hj, h1) 835 836 def le_v(+a: U32, +b: U32, +na: Nat, +nb: Nat, +ha: {v(a) == na : Nat}, +hb: {v(b) == nb : Nat}, +h: {Nat.is_le(na, nb) == True{} : Bool}) -> {Nat.is_le(v(a), v(b)) == True{} : Bool}: 837 +h1 = L.subst(Nat, z => {Nat.is_le(z, nb) == True{} : Bool}, na, v(a), Equal.sym(Nat, v(a), na, ha), h) 838 L.subst(Nat, z => {Nat.is_le(v(a), z) == True{} : Bool}, nb, v(b), Equal.sym(Nat, v(b), nb, hb), h1) 839 840 def permsim(+f: Nat, +k: U32, +m: U32, +a: U32, +nn: Nat, +j: Nat, +r: Nat, +k0: Nat, +K: Nat, +ok: Bool, +more: Bool, +cn: Bool, +hK: {K == 32n : Nat}, +hkr: {v(k) == r : Nat}, +hm: {v(m) == Nat.sub(nn, j) : Nat}, +hj: {Nat.add(j, r) == k0 : Nat}, +hle: {Nat.is_le(k0, nn) == True{} : Bool}, +hf: {Nat.is_le(1n+K, Nat.add(f, j)) == True{} : Bool}, +hok: {C.fits(32n, S.desc(nn, j)) == ok : Bool}, ha: FR(ok, a, S.desc(nn, j)), +hmore: {more == Bool.not(Nat.is_eq(r, 0n)) : Bool}, +hcn: {C.fits(32n, S.desc(nn, k0)) == cn : Bool}) -> {G.perm_go(~U32, ~I.u32_op, ~I.u32_is, f, k, m, (a, ok), more) == G.fits(U32, Bool.not(cn), of(S.desc(nn, k0))) : Maybe<&2, U32>}: 841 match f r ok more cn: 842 case 0n _ True{} _ _: 843 +hjk = L.subst(Nat, z => {Nat.is_le(j, z) == True{} : Bool}, Nat.add(j, r), k0, hj, N.le_add_right(j, r)) 844 +big = NF.dbig(K, nn, j, hf, N.le_trans(j, k0, nn, hjk, hle)) 845 Empty.absurd({G.perm_go(~U32, ~I.u32_op, ~I.u32_is, 0n, k, m, (a, True{}), more) == G.fits(U32, Bool.not(cn), of(S.desc(nn, k0))) : Maybe<&2, U32>}, true_ne_false(Equal.trans(Bool, True{}, Nat.is_lt(S.desc(nn, j), C.pow2(K)), False{}, Equal.sym(Bool, Nat.is_lt(S.desc(nn, j), C.pow2(K)), True{}, fk(K, hK, S.desc(nn, j), hok)), N.le_not_lt(S.desc(nn, j), C.pow2(K), big)))) 846 case 0n _ False{} _ True{}: 847 Empty.absurd({G.perm_go(~U32, ~I.u32_op, ~I.u32_is, 0n, k, m, (a, False{}), more) == G.fits(U32, Bool.not(True{}), of(S.desc(nn, k0))) : Maybe<&2, U32>}, true_ne_false(Equal.trans(Bool, True{}, C.fits(32n, S.desc(nn, k0)), False{}, Equal.sym(Bool, C.fits(32n, S.desc(nn, k0)), True{}, hcn), unfit_mono(32n, S.desc(nn, j), S.desc(nn, k0), pmon(nn, j, r, k0, hj, hle), hok)))) 848 case 0n _ False{} _ False{}: 849 {==} 850 case 1n+g _ False{} _ True{}: 851 Empty.absurd({G.perm_go(~U32, ~I.u32_op, ~I.u32_is, 1n+g, k, m, (a, False{}), more) == G.fits(U32, Bool.not(True{}), of(S.desc(nn, k0))) : Maybe<&2, U32>}, true_ne_false(Equal.trans(Bool, True{}, C.fits(32n, S.desc(nn, k0)), False{}, Equal.sym(Bool, C.fits(32n, S.desc(nn, k0)), True{}, hcn), unfit_mono(32n, S.desc(nn, j), S.desc(nn, k0), pmon(nn, j, r, k0, hj, hle), hok)))) 852 case 1n+g _ False{} _ False{}: 853 {==} 854 case 1n+g 0n True{} False{} True{}: 855 +ejk = Equal.trans(Nat, j, Nat.add(j, 0n), k0, Equal.sym(Nat, Nat.add(j, 0n), j, N.add_zero(j)), hj) 856 Equal.cong(U32, Maybe<&2, U32>, t => Some{t}, a, of(S.desc(nn, k0)), as_of(a, S.desc(nn, k0), Equal.trans(Nat, v(a), S.desc(nn, j), S.desc(nn, k0), ha, Equal.cong(Nat, Nat, t => S.desc(nn, t), j, k0, ejk)))) 857 case 1n+g 0n True{} False{} False{}: 858 +ejk = Equal.trans(Nat, j, Nat.add(j, 0n), k0, Equal.sym(Nat, Nat.add(j, 0n), j, N.add_zero(j)), hj) 859 Empty.absurd({G.perm_go(~U32, ~I.u32_op, ~I.u32_is, 1n+g, k, m, (a, True{}), False{}) == G.fits(U32, Bool.not(False{}), of(S.desc(nn, k0))) : Maybe<&2, U32>}, true_ne_false(Equal.trans(Bool, True{}, C.fits(32n, S.desc(nn, j)), False{}, Equal.sym(Bool, C.fits(32n, S.desc(nn, j)), True{}, hok), Equal.trans(Bool, C.fits(32n, S.desc(nn, j)), C.fits(32n, S.desc(nn, k0)), False{}, Equal.cong(Nat, Bool, t => C.fits(32n, S.desc(nn, t)), j, k0, ejk), hcn)))) 860 case 1n+g 1n+rp True{} False{} _: 861 Empty.absurd({G.perm_go(~U32, ~I.u32_op, ~I.u32_is, 1n+g, k, m, (a, True{}), False{}) == G.fits(U32, Bool.not(cn), of(S.desc(nn, k0))) : Maybe<&2, U32>}, true_ne_false(Equal.sym(Bool, False{}, True{}, hmore))) 862 case 1n+g 0n True{} True{} _: 863 Empty.absurd({G.perm_go(~U32, ~I.u32_op, ~I.u32_is, 1n+g, k, m, (a, True{}), True{}) == G.fits(U32, Bool.not(cn), of(S.desc(nn, k0))) : Maybe<&2, U32>}, true_ne_false(hmore)) 864 case 1n+ +g 1n+ +rp True{} True{} _: 865 +one = I.u32_op(NM.One{}) 866 +es = NA.add_succ(j, rp) 867 +hj1 = N.le_lt_trans(j, Nat.add(j, rp), 1n+Nat.add(j, rp), N.le_add_right(j, rp), N.lt_succ(Nat.add(j, rp))) 868 +hj2 = L.subst(Nat, z => {Nat.is_lt(j, z) == True{} : Bool}, 1n+Nat.add(j, rp), k0, Equal.trans(Nat, 1n+Nat.add(j, rp), Nat.add(j, 1n+rp), k0, Equal.sym(Nat, Nat.add(j, 1n+rp), 1n+Nat.add(j, rp), es), hj), hj1) 869 +hjn = N.lt_le_trans(j, k0, nn, hj2, hle) 870 +X = Nat.sub(nn, 1n+j) 871 +esx = FA.sub_lt_succ(nn, j, hjn) 872 +hpn = Equal.trans(Nat, Nat.mul(v(a), v(m)), Nat.mul(S.desc(nn, j), Nat.sub(nn, j)), S.desc(nn, 1n+j), nmul(v(a), v(m), S.desc(nn, j), Nat.sub(nn, j), ha, hm), NA.mul_comm(S.desc(nn, j), Nat.sub(nn, j))) 873 +dk = G.dec(~U32, ~I.u32_op, k) 874 +edk = Equal.trans(Nat, v(dk), Nat.sub(v(k), v(one)), rp, LW.ops_sub(k, one, le_v(one, k, 1n, 1n+rp, one_v(), hkr, N.zero_le(rp))), Equal.trans(Nat, Nat.sub(v(k), v(one)), Nat.sub(1n+rp, 1n), rp, nsub(v(k), v(one), 1n+rp, 1n, hkr, one_v()), N.sub_zero(rp))) 875 +emx = Equal.trans(Nat, v(m), Nat.sub(nn, j), 1n+X, hm, esx) 876 +dm2 = G.dec(~U32, ~I.u32_op, m) 877 +edm = Equal.trans(Nat, v(dm2), Nat.sub(v(m), v(one)), X, LW.ops_sub(m, one, le_v(one, m, 1n, 1n+X, one_v(), emx, N.zero_le(X))), Equal.trans(Nat, Nat.sub(v(m), v(one)), Nat.sub(1n+X, 1n), X, nsub(v(m), v(one), 1n+X, 1n, emx, one_v()), N.sub_zero(X))) 878 +hmore2 = Equal.cong(Bool, Bool, t => Bool.not(t), I.u32_is(NM.IsZero{dk}), Nat.is_eq(rp, 0n), iz(dk, rp, edk)) 879 +hjj = Equal.trans(Nat, 1n+Nat.add(j, rp), Nat.add(j, 1n+rp), k0, Equal.sym(Nat, Nat.add(j, 1n+rp), 1n+Nat.add(j, rp), es), hj) 880 +hf2 = L.subst(Nat, z => {Nat.is_le(1n+K, z) == True{} : Bool}, 1n+Nat.add(g, j), Nat.add(g, 1n+j), Equal.sym(Nat, Nat.add(g, 1n+j), 1n+Nat.add(g, j), NA.add_succ(g, j)), hf) 881 +pn = S.desc(nn, 1n+j) 882 permsim(g, dk, dm2, I.u32_op(NM.Mul{a, m}), nn, 1n+j, rp, k0, K, Bool.not(I.u32_is(NM.MulOver{a, m})), Bool.not(I.u32_is(NM.IsZero{dk})), cn, hK, edk, edm, hjj, hle, hf2, ok_mul(a, m, pn, hpn), fr_mul(a, m, pn, hpn, C.fits(32n, pn), {==}), hmore2, hcn) 883 884 def perm_top(+K: Nat, +hK: {K == 32n : Nat}, +n: U32, +k: U32, +big: Bool, +hbig: {I.u32_is(NM.Lt{n, k}) == big : Bool}) -> {G.perm_big(~U32, ~I.u32_op, ~I.u32_is, n, k, big) == SG.checked(~U32, ~SG.u32_of, 32n, S.desc(v(n), v(k))) : Result<&2, &2, NM.NumError, U32>}: 885 match big: 886 case True{}: 887 +dz = NF.desc_zero(v(n), v(k), lt_of(n, k, True{}, hbig)) 888 Equal.trans(Result<&2, &2, NM.NumError, U32>, Done{I.u32_op(NM.ZeroOp{})}, SG.checked(~U32, ~SG.u32_of, 32n, 0n), SG.checked(~U32, ~SG.u32_of, 32n, S.desc(v(n), v(k))), Equal.cong(U32, Result<&2, &2, NM.NumError, U32>, t => Done{t}, I.u32_op(NM.ZeroOp{}), of(0n), as_of(I.u32_op(NM.ZeroOp{}), 0n, zero_v())), Equal.cong(Nat, Result<&2, &2, NM.NumError, U32>, t => SG.checked(~U32, ~SG.u32_of, 32n, t), 0n, S.desc(v(n), v(k)), Equal.sym(Nat, S.desc(v(n), v(k)), 0n, dz))) 889 case False{}: 890 +one = I.u32_op(NM.One{}) 891 +D = S.desc(v(n), v(k)) 892 +hge = N.not_lt_le(v(n), v(k), lt_of(n, k, False{}, hbig)) 893 +hf0 = L.subst(Nat, z => {Nat.is_le(1n+z, 140n) == True{} : Bool}, 32n, K, Equal.sym(Nat, K, 32n, hK), {==}) 894 +hm0 = Equal.sym(Nat, Nat.sub(v(n), 0n), v(n), N.sub_zero(v(n))) 895 +more = Bool.not(I.u32_is(NM.IsZero{k})) 896 +hmore = Equal.cong(Bool, Bool, t => Bool.not(t), I.u32_is(NM.IsZero{k}), Nat.is_eq(v(k), 0n), iz(k, v(k), {==})) 897 +s = permsim(140n, k, n, one, v(n), 0n, v(k), v(k), K, True{}, more, C.fits(32n, D), hK, {==}, hm0, {==}, hge, hf0, {==}, one_v(), hmore, {==}) 898 +g = G.perm_go(~U32, ~I.u32_op, ~I.u32_is, 140n, k, n, (one, True{}), more) 899 Equal.trans(Result<&2, &2, NM.NumError, U32>, G.ok(U32, g), G.ok(U32, G.fits(U32, Bool.not(C.fits(32n, D)), of(D))), SG.checked(~U32, ~SG.u32_of, 32n, D), Equal.cong(Maybe<&2, U32>, Result<&2, &2, NM.NumError, U32>, t => G.ok(U32, t), g, G.fits(U32, Bool.not(C.fits(32n, D)), of(D)), s), okfits(D, C.fits(32n, D))) 900 901 def perm_checked(+n: U32, +k: U32) -> SG.Perm.checked(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 32n, n, k): 902 Equal.trans(Result<&2, &2, NM.NumError, U32>, G.perm_big(~U32, ~I.u32_op, ~I.u32_is, n, k, I.u32_is(NM.Lt{n, k})), SG.checked(~U32, ~SG.u32_of, 32n, S.desc(v(n), v(k))), SG.checked(~U32, ~SG.u32_of, 32n, M.perm(v(n), v(k))), perm_top(32n, {==}, n, k, I.u32_is(NM.Lt{n, k}), {==}), Equal.cong(Nat, Result<&2, &2, NM.NumError, U32>, t => SG.checked(~U32, ~SG.u32_of, 32n, t), S.desc(v(n), v(k)), M.perm(v(n), v(k)), Equal.sym(Nat, M.perm(v(n), v(k)), S.desc(v(n), v(k)), FA.perm_ok(v(n), v(k))))) 903 904 # ---- pow: square-and-multiply with fit flags ---- 905 906 # y when ok, else x: {fv(ok, v(a), x) == x} says v(a) == x when ok 907 def fv(ok: Bool, +y: Nat, +x: Nat) -> Nat: 908 match ok: 909 case True{}: 910 y 911 case False{}: 912 x 913 914 # md: every value >= 1, or every value <= 1 (the base 0 case) 915 def mode(md: Bool, +x: Nat) -> Bool: 916 match md: 917 case True{}: 918 Nat.is_le(1n, x) 919 case False{}: 920 Nat.is_le(x, 1n) 921 922 def small_fits(+x: Nat, +h: {Nat.is_le(x, 1n) == True{} : Bool}) -> {C.fits(32n, x) == True{} : Bool}: 923 match x: 924 case 0n: 925 {==} 926 case 1n: 927 {==} 928 case 2n+y: 929 Empty.absurd({C.fits(32n, 2n+y) == True{} : Bool}, true_ne_false(Equal.sym(Bool, False{}, True{}, h))) 930 931 def small_mul(+x: Nat, +y: Nat, +hx: {Nat.is_le(x, 1n) == True{} : Bool}, +hy: {Nat.is_le(y, 1n) == True{} : Bool}) -> {Nat.is_le(Nat.mul(x, y), 1n) == True{} : Bool}: 932 match x: 933 case 0n: 934 {==} 935 case 1n: 936 L.subst(Nat, z => {Nat.is_le(z, 1n) == True{} : Bool}, y, Nat.add(y, 0n), Equal.sym(Nat, Nat.add(y, 0n), y, N.add_zero(y)), hy) 937 case 2n+z: 938 Empty.absurd({Nat.is_le(Nat.mul(2n+z, y), 1n) == True{} : Bool}, true_ne_false(Equal.sym(Bool, False{}, True{}, hx))) 939 940 def pos_of(+x: Nat, +h: {Nat.is_le(1n, x) == True{} : Bool}) -> {Nat.is_lt(0n, x) == True{} : Bool}: 941 match x: 942 case 0n: 943 Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, true_ne_false(Equal.sym(Bool, False{}, True{}, h))) 944 case 1n+y: 945 {==} 946 947 # x unfit, 1 <= y: x y unfit 948 def unfit_mul(+x: Nat, +y: Nat, +hx: {C.fits(32n, x) == False{} : Bool}, +hy: {Nat.is_le(1n, y) == True{} : Bool}) -> {C.fits(32n, Nat.mul(x, y)) == False{} : Bool}: 949 unfit_mono(32n, x, Nat.mul(x, y), RT.le_mul_pos(x, y, pos_of(y, hy)), hx) 950 951 def unfit_mul_r(+x: Nat, +y: Nat, +hy: {C.fits(32n, y) == False{} : Bool}, +hx: {Nat.is_le(1n, x) == True{} : Bool}) -> {C.fits(32n, Nat.mul(x, y)) == False{} : Bool}: 952 L.subst(Nat, z => {C.fits(32n, z) == False{} : Bool}, Nat.mul(y, x), Nat.mul(x, y), NA.mul_comm(y, x), unfit_mul(y, x, hy, hx)) 953 954 # an unfit value is >= 1, so the mode is the >= 1 one 955 def unfit_big(+x: Nat, +md: Bool, +hm: {mode(md, x) == True{} : Bool}, +hx: {C.fits(32n, x) == False{} : Bool}) -> {md == True{} : Bool}: 956 match md: 957 case True{}: 958 {==} 959 case False{}: 960 Empty.absurd({False{} == True{} : Bool}, true_ne_false(Equal.trans(Bool, True{}, C.fits(32n, x), False{}, Equal.sym(Bool, C.fits(32n, x), True{}, small_fits(x, hm)), hx))) 961 962 def fv_mul(+a: U32, +x: U32, +n: Nat, +hn: {Nat.mul(v(a), v(x)) == n : Nat}, +c: Bool, +hc: {C.fits(32n, n) == c : Bool}) -> {fv(Bool.not(I.u32_is(NM.MulOver{a, x})), v(I.u32_op(NM.Mul{a, x})), n) == n : Nat}: 963 match c: 964 case True{}: 965 +hmo = mo_of(a, x, n, hn, True{}, hc) 966 %Equal.sym(Bool, I.u32_is(NM.MulOver{a, x}), False{}, hmo) : {fv(Bool.not(_), v(I.u32_op(NM.Mul{a, x})), n) == n : Nat} 967 Equal.trans(Nat, v(I.u32_op(NM.Mul{a, x})), Nat.mul(v(a), v(x)), n, LW.ops_mul(a, x, hmo), hn) 968 case False{}: 969 %Equal.sym(Bool, I.u32_is(NM.MulOver{a, x}), True{}, mo_of(a, x, n, hn, False{}, hc)) : {fv(Bool.not(_), v(I.u32_op(NM.Mul{a, x})), n) == n : Nat} 970 {==} 971 972 # -- the squared base -- 973 974 def sq_fits(+more: Bool, +b: U32, +bok: Bool, +nb: Nat, +md: Bool, +hB: {C.fits(32n, nb) == bok : Bool}, +hb: {fv(bok, v(b), nb) == nb : Nat}, +hm: {mode(md, nb) == True{} : Bool}) -> {C.fits(32n, NF.sqn(more, nb)) == G.sq_ok(~U32, ~I.u32_is, more, b, bok) : Bool}: 975 match more bok: 976 case False{} _: 977 hB 978 case True{} True{}: 979 ok_mul(b, b, Nat.mul(nb, nb), nmul(v(b), v(b), nb, nb, hb, hb)) 980 case True{} False{}: 981 +md1 = unfit_big(nb, md, hm, hB) 982 +h1 = L.subst(Bool, t => {mode(t, nb) == True{} : Bool}, md, True{}, md1, hm) 983 unfit_mul(nb, nb, hB, h1) 984 985 def sq_fv(+more: Bool, +b: U32, +bok: Bool, +nb: Nat, +hb: {fv(bok, v(b), nb) == nb : Nat}) -> {fv(G.sq_ok(~U32, ~I.u32_is, more, b, bok), v(G.sq_val(~U32, ~I.u32_op, more, b)), NF.sqn(more, nb)) == NF.sqn(more, nb) : Nat}: 986 match more bok: 987 case False{} _: 988 hb 989 case True{} True{}: 990 fv_mul(b, b, Nat.mul(nb, nb), nmul(v(b), v(b), nb, nb, hb, hb), C.fits(32n, Nat.mul(nb, nb)), {==}) 991 case True{} False{}: 992 {==} 993 994 def sq_mode(+more: Bool, +nb: Nat, +md: Bool, +hm: {mode(md, nb) == True{} : Bool}) -> {mode(md, NF.sqn(more, nb)) == True{} : Bool}: 995 match more md: 996 case False{} _: 997 hm 998 case True{} True{}: 999 N.le_trans(1n, nb, Nat.mul(nb, nb), hm, RT.le_mul_pos(nb, nb, pos_of(nb, hm))) 1000 case True{} False{}: 1001 small_mul(nb, nb, hm, hm) 1002 1003 # -- the accumulator -- 1004 1005 def ms_a(bit: Bool, +a: U32, +b: U32) -> U32: 1006 match bit: 1007 case True{}: 1008 I.u32_op(NM.Mul{a, b}) 1009 case False{}: 1010 a 1011 1012 def ms_ok(bit: Bool, +a: U32, +aok: Bool, +b: U32, +bok: Bool) -> Bool: 1013 match bit: 1014 case True{}: 1015 Bool.and(Bool.and(aok, bok), Bool.not(I.u32_is(NM.MulOver{a, b}))) 1016 case False{}: 1017 aok 1018 1019 def ms_eq(+bit: Bool, +b: U32, +bok: Bool, +a: U32, +aok: Bool) -> {G.mul_st(~U32, ~I.u32_op, ~I.u32_is, bit, b, bok, (a, aok)) == (ms_a(bit, a, b), ms_ok(bit, a, aok, b, bok)) : U32 & Bool}: 1020 match bit: 1021 case True{}: 1022 {==} 1023 case False{}: 1024 {==} 1025 1026 def ms_fits(+bit: Bool, +a: U32, +aok: Bool, +b: U32, +bok: Bool, +na: Nat, +nb: Nat, +md: Bool, +hA: {C.fits(32n, na) == aok : Bool}, +ha: {fv(aok, v(a), na) == na : Nat}, +hma: {mode(md, na) == True{} : Bool}, +hB: {C.fits(32n, nb) == bok : Bool}, +hb: {fv(bok, v(b), nb) == nb : Nat}, +hmb: {mode(md, nb) == True{} : Bool}) -> {C.fits(32n, NF.msn(bit, na, nb)) == ms_ok(bit, a, aok, b, bok) : Bool}: 1027 match bit aok bok: 1028 case False{} _ _: 1029 hA 1030 case True{} True{} True{}: 1031 ok_mul(a, b, Nat.mul(na, nb), nmul(v(a), v(b), na, nb, ha, hb)) 1032 case True{} False{} _: 1033 +md1 = unfit_big(na, md, hma, hA) 1034 unfit_mul(na, nb, hA, L.subst(Bool, t => {mode(t, nb) == True{} : Bool}, md, True{}, md1, hmb)) 1035 case True{} True{} False{}: 1036 +md1 = unfit_big(nb, md, hmb, hB) 1037 unfit_mul_r(na, nb, hB, L.subst(Bool, t => {mode(t, na) == True{} : Bool}, md, True{}, md1, hma)) 1038 1039 def ms_fv(+bit: Bool, +a: U32, +aok: Bool, +b: U32, +bok: Bool, +na: Nat, +nb: Nat, +ha: {fv(aok, v(a), na) == na : Nat}, +hb: {fv(bok, v(b), nb) == nb : Nat}) -> {fv(ms_ok(bit, a, aok, b, bok), v(ms_a(bit, a, b)), NF.msn(bit, na, nb)) == NF.msn(bit, na, nb) : Nat}: 1040 match bit aok bok: 1041 case False{} _ _: 1042 ha 1043 case True{} True{} True{}: 1044 fv_mul(a, b, Nat.mul(na, nb), nmul(v(a), v(b), na, nb, ha, hb), C.fits(32n, Nat.mul(na, nb)), {==}) 1045 case True{} False{} _: 1046 {==} 1047 case True{} True{} False{}: 1048 {==} 1049 1050 def ms_mode(+bit: Bool, +na: Nat, +nb: Nat, +md: Bool, +hma: {mode(md, na) == True{} : Bool}, +hmb: {mode(md, nb) == True{} : Bool}) -> {mode(md, NF.msn(bit, na, nb)) == True{} : Bool}: 1051 match bit md: 1052 case False{} _: 1053 hma 1054 case True{} True{}: 1055 N.le_trans(1n, na, Nat.mul(na, nb), hma, RT.le_mul_pos(na, nb, pos_of(nb, hmb))) 1056 case True{} False{}: 1057 small_mul(na, nb, hma, hmb) 1058 1059 def pw_fin(+a: U32, +aok: Bool, +na: Nat, +t0: Nat, +ct: Bool, +hA: {C.fits(32n, na) == aok : Bool}, +ha: {fv(aok, v(a), na) == na : Nat}, +et: {na == t0 : Nat}, +hct: {C.fits(32n, t0) == ct : Bool}) -> {G.fits(U32, Bool.not(aok), a) == G.fits(U32, Bool.not(ct), of(t0)) : Maybe<&2, U32>}: 1060 match aok ct: 1061 case True{} True{}: 1062 Equal.cong(U32, Maybe<&2, U32>, t => Some{t}, a, of(t0), as_of(a, t0, Equal.trans(Nat, v(a), na, t0, ha, et))) 1063 case False{} False{}: 1064 {==} 1065 case True{} False{}: 1066 Empty.absurd({G.fits(U32, Bool.not(True{}), a) == G.fits(U32, Bool.not(False{}), of(t0)) : Maybe<&2, U32>}, true_ne_false(Equal.trans(Bool, True{}, C.fits(32n, na), False{}, Equal.sym(Bool, C.fits(32n, na), True{}, hA), Equal.trans(Bool, C.fits(32n, na), C.fits(32n, t0), False{}, Equal.cong(Nat, Bool, t => C.fits(32n, t), na, t0, et), hct)))) 1067 case False{} True{}: 1068 Empty.absurd({G.fits(U32, Bool.not(False{}), a) == G.fits(U32, Bool.not(True{}), of(t0)) : Maybe<&2, U32>}, true_ne_false(Equal.trans(Bool, True{}, C.fits(32n, t0), False{}, Equal.sym(Bool, C.fits(32n, t0), True{}, hct), Equal.trans(Bool, C.fits(32n, t0), C.fits(32n, na), False{}, Equal.cong(Nat, Bool, t => C.fits(32n, t), t0, na, Equal.sym(Nat, na, t0, et)), hA)))) 1069 1070 def powsim(+f: Nat, +e: Nat, +b: U32, +bok: Bool, +a: U32, +aok: Bool, +nb: Nat, +na: Nat, +t0: Nat, +md: Bool, +ct: Bool, +he: {Nat.is_le(e, f) == True{} : Bool}, +hB: {C.fits(32n, nb) == bok : Bool}, +hb: {fv(bok, v(b), nb) == nb : Nat}, +hmb: {mode(md, nb) == True{} : Bool}, +hA: {C.fits(32n, na) == aok : Bool}, +ha: {fv(aok, v(a), na) == na : Nat}, +hma: {mode(md, na) == True{} : Bool}, +ht: {Nat.mul(na, Nat.pow(nb, e)) == t0 : Nat}, +hct: {C.fits(32n, t0) == ct : Bool}) -> {G.pow_go(~U32, ~I.u32_op, ~I.u32_is, f, e, b, bok, (a, aok)) == G.fits(U32, Bool.not(ct), of(t0)) : Maybe<&2, U32>}: 1071 match f e: 1072 case 0n 0n: 1073 pw_fin(a, aok, na, t0, ct, hA, ha, Equal.trans(Nat, na, Nat.mul(na, 1n), t0, Equal.sym(Nat, Nat.mul(na, 1n), na, NA.mul_one(na)), ht), hct) 1074 case 0n 1n+j: 1075 Empty.absurd({G.pow_go(~U32, ~I.u32_op, ~I.u32_is, 0n, 1n+j, b, bok, (a, aok)) == G.fits(U32, Bool.not(ct), of(t0)) : Maybe<&2, U32>}, true_ne_false(Equal.sym(Bool, False{}, True{}, he))) 1076 case 1n+g 0n: 1077 pw_fin(a, aok, na, t0, ct, hA, ha, Equal.trans(Nat, na, Nat.mul(na, 1n), t0, Equal.sym(Nat, Nat.mul(na, 1n), na, NA.mul_one(na)), ht), hct) 1078 case 1n+ +g 1n+ +j: 1079 +more = Nat.is_lt(1n, 1n+j) 1080 +bit = Nat.is_eq(Nat.mod(1n+j, 2n), 1n) 1081 +e2 = Nat.div(1n+j, 2n) 1082 +ht2 = Equal.trans(Nat, Nat.mul(NF.msn(bit, na, nb), Nat.pow(NF.sqn(more, nb), e2)), Nat.mul(na, Nat.pow(nb, 1n+j)), t0, NF.powstep(j, na, nb), ht) 1083 +he2 = N.le_trans(e2, j, g, NF.half_le(j), he) 1084 +ih = powsim(g, e2, G.sq_val(~U32, ~I.u32_op, more, b), G.sq_ok(~U32, ~I.u32_is, more, b, bok), ms_a(bit, a, b), ms_ok(bit, a, aok, b, bok), NF.sqn(more, nb), NF.msn(bit, na, nb), t0, md, ct, he2, sq_fits(more, b, bok, nb, md, hB, hb, hmb), sq_fv(more, b, bok, nb, hb), sq_mode(more, nb, md, hmb), ms_fits(bit, a, aok, b, bok, na, nb, md, hA, ha, hma, hB, hb, hmb), ms_fv(bit, a, aok, b, bok, na, nb, ha, hb), ms_mode(bit, na, nb, md, hma, hmb), ht2, hct) 1085 L.subst(U32 & Bool, z => {G.pow_go(~U32, ~I.u32_op, ~I.u32_is, g, e2, G.sq_val(~U32, ~I.u32_op, more, b), G.sq_ok(~U32, ~I.u32_is, more, b, bok), z) == G.fits(U32, Bool.not(ct), of(t0)) : Maybe<&2, U32>}, (ms_a(bit, a, b), ms_ok(bit, a, aok, b, bok)), G.mul_st(~U32, ~I.u32_op, ~I.u32_is, bit, b, bok, (a, aok)), Equal.sym(U32 & Bool, G.mul_st(~U32, ~I.u32_op, ~I.u32_is, bit, b, bok, (a, aok)), (ms_a(bit, a, b), ms_ok(bit, a, aok, b, bok)), ms_eq(bit, b, bok, a, aok)), ih) 1086 1087 def md_init(+x: Nat) -> {mode(Nat.is_le(1n, x), x) == True{} : Bool} & {mode(Nat.is_le(1n, x), 1n) == True{} : Bool}: 1088 match x: 1089 case 0n: 1090 ({==}, {==}) 1091 case 1n+y: 1092 +ez = Equal.sym(Bool, Nat.is_le(0n, y), True{}, N.zero_le(y)) 1093 (L.subst(Bool, t => {mode(t, 1n+y) == True{} : Bool}, True{}, Nat.is_le(0n, y), ez, N.zero_le(y)), L.subst(Bool, t => {mode(t, 1n) == True{} : Bool}, True{}, Nat.is_le(0n, y), ez, {==})) 1094 1095 def pow_fin(+x: U32, +k: Nat, p: {mode(Nat.is_le(1n, v(x)), v(x)) == True{} : Bool} & {mode(Nat.is_le(1n, v(x)), 1n) == True{} : Bool}) -> SG.Pow.checked(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 32n, x, k): 1096 (+hmb, +hma) = p 1097 +one = I.u32_op(NM.One{}) 1098 +t0 = Nat.pow(v(x), k) 1099 +ht = Equal.trans(Nat, Nat.mul(1n, t0), Nat.add(t0, 0n), t0, {==}, N.add_zero(t0)) 1100 +s = powsim(1n+k, k, x, True{}, one, True{}, v(x), 1n, t0, Nat.is_le(1n, v(x)), C.fits(32n, t0), N.le_succ(k), LW.vb(x), {==}, hmb, {==}, one_v(), hma, ht, {==}) 1101 +g = G.pow_go(~U32, ~I.u32_op, ~I.u32_is, 1n+k, k, x, True{}, (one, True{})) 1102 Equal.trans(Result<&2, &2, NM.NumError, U32>, G.ok(U32, g), G.ok(U32, G.fits(U32, Bool.not(C.fits(32n, t0)), of(t0))), SG.checked(~U32, ~SG.u32_of, 32n, t0), Equal.cong(Maybe<&2, U32>, Result<&2, &2, NM.NumError, U32>, t => G.ok(U32, t), g, G.fits(U32, Bool.not(C.fits(32n, t0)), of(t0)), s), okfits(t0, C.fits(32n, t0))) 1103 1104 def pow_checked(+x: U32, +k: Nat) -> SG.Pow.checked(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 32n, x, k): 1105 pow_fin(x, k, md_init(v(x))) 1106 1107 # ---- iroot: bisection with lo <= R < lo + w, the width halving ---- 1108 1109 def pw_val(+x: U32, +k: Nat, p: {mode(Nat.is_le(1n, v(x)), v(x)) == True{} : Bool} & {mode(Nat.is_le(1n, v(x)), 1n) == True{} : Bool}) -> {G.pow_go(~U32, ~I.u32_op, ~I.u32_is, 1n+k, k, x, True{}, (I.u32_op(NM.One{}), True{})) == G.fits(U32, Bool.not(C.fits(32n, Nat.pow(v(x), k))), of(Nat.pow(v(x), k))) : Maybe<&2, U32>}: 1110 (+hmb, +hma) = p 1111 +t0 = Nat.pow(v(x), k) 1112 +ht = Equal.trans(Nat, Nat.mul(1n, t0), Nat.add(t0, 0n), t0, {==}, N.add_zero(t0)) 1113 powsim(1n+k, k, x, True{}, I.u32_op(NM.One{}), True{}, v(x), 1n, t0, Nat.is_le(1n, v(x)), C.fits(32n, t0), N.le_succ(k), LW.vb(x), {==}, hmb, {==}, one_v(), hma, ht, {==}) 1114 1115 def rlf(+K: Nat, +hK: {K == 32n : Nat}, +n: U32, +P: Nat, +c: Bool, +hc: {C.fits(32n, P) == c : Bool}) -> {G.root_le_fin(~U32, ~I.u32_op, ~I.u32_is, n, G.fits(U32, Bool.not(c), of(P))) == Nat.is_le(P, v(n)) : Bool}: 1116 match c: 1117 case True{}: 1118 lev(of(P), n, P, v(n), LW.vo(P, hc), {==}) 1119 case False{}: 1120 +h1 = L.subst(Nat, z => {C.fits(z, P) == False{} : Bool}, 32n, K, Equal.sym(Nat, K, 32n, hK), hc) 1121 +h2 = Equal.trans(Bool, Nat.is_lt(P, C.pow2(K)), C.fits(K, P), False{}, Equal.sym(Bool, C.fits(K, P), Nat.is_lt(P, C.pow2(K)), WW.fits_lt(K, P)), h1) 1122 +hn = N.lt_le_trans(v(n), C.pow2(K), P, U32P.val_lt(1n, {==}, K, hK, n), N.not_lt_le(P, C.pow2(K), h2)) 1123 Equal.sym(Bool, Nat.is_le(P, v(n)), False{}, N.lt_not_le(v(n), P, hn)) 1124 1125 def rl_v(+K: Nat, +hK: {K == 32n : Nat}, +n: U32, +k: Nat, +r: U32) -> {G.root_le(~U32, ~I.u32_op, ~I.u32_is, n, k, r) == Nat.is_le(Nat.pow(v(r), k), v(n)) : Bool}: 1126 +P = Nat.pow(v(r), k) 1127 Equal.trans(Bool, G.root_le_fin(~U32, ~I.u32_op, ~I.u32_is, n, G.pow_go(~U32, ~I.u32_op, ~I.u32_is, 1n+k, k, r, True{}, (I.u32_op(NM.One{}), True{}))), G.root_le_fin(~U32, ~I.u32_op, ~I.u32_is, n, G.fits(U32, Bool.not(C.fits(32n, P)), of(P))), Nat.is_le(P, v(n)), Equal.cong(Maybe<&2, U32>, Bool, t => G.root_le_fin(~U32, ~I.u32_op, ~I.u32_is, n, t), G.pow_go(~U32, ~I.u32_op, ~I.u32_is, 1n+k, k, r, True{}, (I.u32_op(NM.One{}), True{})), G.fits(U32, Bool.not(C.fits(32n, P)), of(P)), pw_val(r, k, md_init(v(r)))), rlf(K, hK, n, P, C.fits(32n, P), {==})) 1128 1129 def imid_v(+K: Nat, +hK: {K == 32n : Nat}, +lo: U32, +hi: U32, +a: Nat, +w: Nat, +ha: {v(lo) == a : Nat}, +hh: {v(hi) == Nat.add(a, w) : Nat}) -> {v(G.imid(~U32, ~I.u32_op, lo, hi)) == Nat.add(a, Nat.div(w, 2n)) : Nat}: 1130 +s = I.u32_op(NM.Sub{hi, lo}) 1131 +es = Equal.trans(Nat, v(s), Nat.sub(v(hi), v(lo)), w, LW.ops_sub(hi, lo, le_v(lo, hi, a, Nat.add(a, w), ha, hh, N.le_add_right(a, w))), Equal.trans(Nat, Nat.sub(v(hi), v(lo)), Nat.sub(Nat.add(a, w), a), w, nsub(v(hi), v(lo), Nat.add(a, w), a, hh, ha), N.add_sub_cancel(a, w))) 1132 +h = I.u32_op(NM.Half{s}) 1133 +eh = Equal.trans(Nat, v(h), Nat.div(v(s), 2n), Nat.div(w, 2n), LW.ops_half(s), Equal.cong(Nat, Nat, t => Nat.div(t, 2n), v(s), w, es)) 1134 +sum = Nat.add(a, Nat.div(w, 2n)) 1135 +esum = nadd(v(lo), v(h), a, Nat.div(w, 2n), ha, eh) 1136 +hle = N.le_add_left(Nat.div(w, 2n), w, a, AR2.div_le(w, 2n)) 1137 +hhk = L.subst(Nat, z => {Nat.is_lt(z, C.pow2(K)) == True{} : Bool}, v(hi), Nat.add(a, w), hh, U32P.val_lt(1n, {==}, K, hK, hi)) 1138 +hfit = fits32(K, hK, sum, N.le_lt_trans(sum, Nat.add(a, w), C.pow2(K), hle, hhk)) 1139 Equal.trans(Nat, v(I.u32_op(NM.Add{lo, h})), Nat.add(v(lo), v(h)), sum, LW.ops_add(lo, h, ao_of(lo, h, sum, esum, True{}, hfit)), esum) 1140 1141 def lt_add_r(+a: Nat, +q: Nat, +h: {Nat.is_lt(0n, q) == True{} : Bool}) -> {Nat.is_lt(a, Nat.add(a, q)) == True{} : Bool}: 1142 +h1 = Equal.trans(Bool, Nat.is_lt(Nat.add(a, 0n), Nat.add(a, q)), Nat.is_lt(0n, q), True{}, NF.lt_add_cancel(a, 0n, q), h) 1143 L.subst(Nat, z => {Nat.is_lt(z, Nat.add(a, q)) == True{} : Bool}, Nat.add(a, 0n), a, N.add_zero(a), h1) 1144 1145 # inc(lo) < lo + w as 1 < w 1146 def more_v(+K: Nat, +hK: {K == 32n : Nat}, +lo: U32, +hi: U32, +a: Nat, +w: Nat, +ha: {v(lo) == a : Nat}, +hh: {v(hi) == Nat.add(a, w) : Nat}, +hw: {Nat.is_lt(0n, w) == True{} : Bool}) -> {I.u32_is(NM.Lt{G.inc(~U32, ~I.u32_op, lo), hi}) == Nat.is_lt(1n, w) : Bool}: 1147 +ei = inc_v(K, hK, lo, hi, a, Nat.add(a, w), ha, hh, lt_add_r(a, w, hw)) 1148 Equal.trans(Bool, I.u32_is(NM.Lt{G.inc(~U32, ~I.u32_op, lo), hi}), Nat.is_lt(1n+a, Nat.add(a, w)), Nat.is_lt(1n, w), ltv(G.inc(~U32, ~I.u32_op, lo), hi, 1n+a, Nat.add(a, w), ei, hh), L.subst(Nat, z => {Nat.is_lt(z, Nat.add(a, w)) == Nat.is_lt(1n, w) : Bool}, Nat.add(a, 1n), 1n+a, plus1(a), NF.lt_add_cancel(a, 1n, w))) 1149 1150 def srch(+f: Nat, +n: U32, +k: Nat, +lo: U32, +hi: U32, +m: U32, +more: Bool, +hit: Bool, +j: Nat, +nlo: Nat, +w: Nat, +R: Nat, +K: Nat, +hK: {K == 32n : Nat}, +hlo: {v(lo) == nlo : Nat}, +hhi: {v(hi) == Nat.add(nlo, w) : Nat}, +hm: {v(m) == Nat.add(nlo, Nat.div(w, 2n)) : Nat}, +hR1: {Nat.is_le(Nat.pow(R, k), v(n)) == True{} : Bool}, +hR2: {Nat.is_lt(v(n), Nat.pow(1n+R, k)) == True{} : Bool}, +hl: {Nat.is_le(nlo, R) == True{} : Bool}, +hr: {Nat.is_lt(R, Nat.add(nlo, w)) == True{} : Bool}, +hmore: {more == Nat.is_lt(1n, w) : Bool}, +hhit: {hit == Nat.is_le(Nat.pow(Nat.add(nlo, Nat.div(w, 2n)), k), v(n)) : Bool}, +hw: {Nat.is_le(w, C.pow2(j)) == True{} : Bool}, +hf: {Nat.is_le(1n+j, f) == True{} : Bool}) -> {v(G.search_go(~U32, ~I.u32_op, ~I.u32_is, f, n, k, lo, hi, m, more, hit)) == R : Nat}: 1151 match f more hit j: 1152 case 0n _ _ _: 1153 Empty.absurd({v(G.search_go(~U32, ~I.u32_op, ~I.u32_is, 0n, n, k, lo, hi, m, more, hit)) == R : Nat}, true_ne_false(Equal.sym(Bool, False{}, True{}, hf))) 1154 case 1n+g False{} _ _: 1155 +hw1 = N.not_lt_le(1n, w, Equal.sym(Bool, False{}, Nat.is_lt(1n, w), hmore)) 1156 +h1 = L.subst(Nat, z => {Nat.is_le(Nat.add(nlo, w), z) == True{} : Bool}, Nat.add(nlo, 1n), 1n+nlo, plus1(nlo), N.le_add_left(w, 1n, nlo, hw1)) 1157 +hrl = N.lt_succ_le(R, nlo, N.lt_le_trans(R, Nat.add(nlo, w), 1n+nlo, hr, h1)) 1158 Equal.trans(Nat, v(lo), nlo, R, hlo, N.le_antisym(nlo, R, hl, hrl)) 1159 case 1n+g True{} _ 0n: 1160 Empty.absurd({v(G.search_go(~U32, ~I.u32_op, ~I.u32_is, 1n+g, n, k, lo, hi, m, True{}, hit)) == R : Nat}, true_ne_false(Equal.trans(Bool, True{}, Nat.is_lt(1n, w), False{}, hmore, N.le_not_lt(1n, w, hw)))) 1161 case 1n+ +g True{} True{} 1n+ +jp: 1162 +q = Nat.div(w, 2n) 1163 +X = Nat.add(nlo, q) 1164 +w2 = Nat.sub(w, q) 1165 +hqw = Equal.trans(Nat, Nat.add(q, w2), w, w, N.sub_add(w, q, AR2.div_le(w, 2n)), {==}) 1166 +ehi = Equal.trans(Nat, Nat.add(X, w2), Nat.add(nlo, Nat.add(q, w2)), Nat.add(nlo, w), N.add_assoc(nlo, q, w2), Equal.cong(Nat, Nat, t => Nat.add(nlo, t), Nat.add(q, w2), w, hqw)) 1167 +hhi2 = Equal.trans(Nat, v(hi), Nat.add(nlo, w), Nat.add(X, w2), hhi, Equal.sym(Nat, Nat.add(X, w2), Nat.add(nlo, w), ehi)) 1168 +hw0 = N.lt_trans(0n, 1n, w, {==}, Equal.sym(Bool, True{}, Nat.is_lt(1n, w), hmore)) 1169 +hdw = L.subst(Nat, z => {Nat.is_lt(w, z) == True{} : Bool}, Nat.add(w, w), Nat.double(w), Equal.sym(Nat, Nat.double(w), Nat.add(w, w), NA.double_self(w)), lt_add_r(w, w, hw0)) 1170 +hpos = RT.sub_pos(q, w, NF.half_below(w, w, hdw)) 1171 +m2 = G.imid(~U32, ~I.u32_op, m, hi) 1172 +hm2 = imid_v(K, hK, m, hi, X, w2, hm, hhi2) 1173 +hmore2 = more_v(K, hK, m, hi, X, w2, hm, hhi2, hpos) 1174 +hhit2 = Equal.trans(Bool, G.root_le(~U32, ~I.u32_op, ~I.u32_is, n, k, m2), Nat.is_le(Nat.pow(v(m2), k), v(n)), Nat.is_le(Nat.pow(Nat.add(X, Nat.div(w2, 2n)), k), v(n)), rl_v(K, hK, n, k, m2), Equal.cong(Nat, Bool, t => Nat.is_le(Nat.pow(t, k), v(n)), v(m2), Nat.add(X, Nat.div(w2, 2n)), hm2)) 1175 +hl2 = NF.root_below(R, X, k, v(n), Equal.sym(Bool, True{}, Nat.is_le(Nat.pow(X, k), v(n)), hhit), hR2) 1176 +hr2 = L.subst(Nat, z => {Nat.is_lt(R, z) == True{} : Bool}, Nat.add(nlo, w), Nat.add(X, w2), Equal.sym(Nat, Nat.add(X, w2), Nat.add(nlo, w), ehi), hr) 1177 +hw3 = NF.w_hi(w, C.pow2(jp), hw) 1178 srch(g, n, k, m, hi, m2, I.u32_is(NM.Lt{G.inc(~U32, ~I.u32_op, m), hi}), G.root_le(~U32, ~I.u32_op, ~I.u32_is, n, k, m2), jp, X, w2, R, K, hK, hm, hhi2, hm2, hR1, hR2, hl2, hr2, Equal.sym(Bool, Nat.is_lt(1n, w2), I.u32_is(NM.Lt{G.inc(~U32, ~I.u32_op, m), hi}), Equal.sym(Bool, I.u32_is(NM.Lt{G.inc(~U32, ~I.u32_op, m), hi}), Nat.is_lt(1n, w2), hmore2)), hhit2, hw3, hf) 1179 case 1n+ +g True{} False{} 1n+ +jp: 1180 +q = Nat.div(w, 2n) 1181 +X = Nat.add(nlo, q) 1182 +h2w = N.lt_succ_le_succ(1n, w, Equal.sym(Bool, True{}, Nat.is_lt(1n, w), hmore)) 1183 +hq1 = Equal.trans(Bool, Nat.is_le(1n, q), Nat.is_le(Nat.mul(1n, 2n), w), True{}, NR.le_div(1n, 1n, w), h2w) 1184 +hpos = pos_of(q, hq1) 1185 +m2 = G.imid(~U32, ~I.u32_op, lo, m) 1186 +hm2 = imid_v(K, hK, lo, m, nlo, q, hlo, hm) 1187 +hmore2 = more_v(K, hK, lo, m, nlo, q, hlo, hm, hpos) 1188 +hhit2 = Equal.trans(Bool, G.root_le(~U32, ~I.u32_op, ~I.u32_is, n, k, m2), Nat.is_le(Nat.pow(v(m2), k), v(n)), Nat.is_le(Nat.pow(Nat.add(nlo, Nat.div(q, 2n)), k), v(n)), rl_v(K, hK, n, k, m2), Equal.cong(Nat, Bool, t => Nat.is_le(Nat.pow(t, k), v(n)), v(m2), Nat.add(nlo, Nat.div(q, 2n)), hm2)) 1189 +hr2 = NF.root_above(R, X, k, v(n), Equal.sym(Bool, False{}, Nat.is_le(Nat.pow(X, k), v(n)), hhit), hR1) 1190 +hw3 = NF.w_lo(w, C.pow2(jp), hw) 1191 srch(g, n, k, lo, m, m2, I.u32_is(NM.Lt{G.inc(~U32, ~I.u32_op, lo), m}), G.root_le(~U32, ~I.u32_op, ~I.u32_is, n, k, m2), jp, nlo, q, R, K, hK, hlo, hm, hm2, hR1, hR2, hl, hr2, Equal.sym(Bool, Nat.is_lt(1n, q), I.u32_is(NM.Lt{G.inc(~U32, ~I.u32_op, lo), m}), Equal.sym(Bool, I.u32_is(NM.Lt{G.inc(~U32, ~I.u32_op, lo), m}), Nat.is_lt(1n, q), hmore2)), hhit2, hw3, hf) 1192 1193 def iroot_big(+K: Nat, +hK: {K == 32n : Nat}, +n: U32, +kp: Nat) -> {v(G.iroot_k(~U32, ~I.u32_op, ~I.u32_is, n, 2n+kp)) == M.iroot_k(v(n), 2n+kp) : Nat}: 1194 +bg = G.bit_length(~U32, ~I.u32_op, ~I.u32_is, n) 1195 +bl = M.bit_length(v(n)) 1196 +ebl = bit_length_k(K, hK, n) 1197 +hn = U32P.val_lt(1n, {==}, K, hK, n) 1198 +hbl = L.subst(Nat, z => {Nat.is_le(bl, z) == True{} : Bool}, K, 32n, hK, NF.bl_le_n(K, v(n), hn)) 1199 +E2 = {1n+Nat.div(bl, 2n+kp) : Nat} 1200 +E = {1n+Nat.div(bg, 2n+kp) : Nat} 1201 +eE = Equal.cong(Nat, Nat, t => 1n+Nat.div(t, 2n+kp), bg, bl, ebl) 1202 +hE2 = NF.e_lt(kp, bl, hbl) 1203 +hE = L.subst(Nat, z => {Nat.is_lt(z, 32n) == True{} : Bool}, E2, E, Equal.sym(Nat, E, E2, eE), hE2) 1204 +hi = I.u32_op(NM.Pow2{E}) 1205 +W = C.pow2(E2) 1206 ehi0 = LW.ops_pow2(E, hE) 1207 +ehi = Equal.trans(Nat, v(hi), C.pow2(E), W, ehi0, Equal.cong(Nat, Nat, t => C.pow2(t), E, E2, eE)) 1208 +zero = I.u32_op(NM.ZeroOp{}) 1209 +m = G.imid(~U32, ~I.u32_op, zero, hi) 1210 +hm = imid_v(K, hK, zero, hi, 0n, W, zero_v(), ehi) 1211 +hmore = ltv(I.u32_op(NM.One{}), hi, 1n, W, one_v(), ehi) 1212 +hhit = Equal.trans(Bool, G.root_le(~U32, ~I.u32_op, ~I.u32_is, n, 2n+kp, m), Nat.is_le(Nat.pow(v(m), 2n+kp), v(n)), Nat.is_le(Nat.pow(Nat.div(W, 2n), 2n+kp), v(n)), rl_v(K, hK, n, 2n+kp, m), Equal.cong(Nat, Bool, t => Nat.is_le(Nat.pow(t, 2n+kp), v(n)), v(m), Nat.div(W, 2n), hm)) 1213 +R = M.iroot_k(v(n), 2n+kp) 1214 +hb = Equal.trans(Bool, Nat.is_le(Nat.pow(P2.pow2t(E2), 2n+kp), v(n)), M.root_le(v(n), 2n+kp, P2.pow2t(E2)), False{}, Equal.sym(Bool, M.root_le(v(n), 2n+kp, P2.pow2t(E2)), Nat.is_le(Nat.pow(P2.pow2t(E2), 2n+kp), v(n)), RT.root_le_ok(v(n), 2n+kp, P2.pow2t(E2))), RT.hi_bound(v(n), 1n+kp)) 1215 +hb2 = L.subst(Nat, z => {Nat.is_le(Nat.pow(z, 2n+kp), v(n)) == False{} : Bool}, P2.pow2t(E2), W, PP.same(E2), hb) 1216 +hR1 = RT.iroot_le(v(n), 1n+kp) 1217 +hr = NF.root_above(R, W, 2n+kp, v(n), hb2, hR1) 1218 +hf = N.le_trans(1n+E2, 32n, 140n, N.lt_succ_le_succ(E2, 32n, hE2), {==}) 1219 srch(140n, n, 2n+kp, zero, hi, m, I.u32_is(NM.Lt{I.u32_op(NM.One{}), hi}), G.root_le(~U32, ~I.u32_op, ~I.u32_is, n, 2n+kp, m), E2, 0n, W, R, K, hK, zero_v(), ehi, hm, hR1, RT.lt_succ_iroot(v(n), 1n+kp), N.zero_le(R), hr, hmore, hhit, N.le_refl(W), hf) 1220 1221 def iroot_agrees(+n: U32, +k: Nat) -> SG.Iroot.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, n, k): 1222 match k: 1223 case 0n: 1224 {==} 1225 case 1n: 1226 Equal.cong(U32, Result<&2, &2, NM.NumError, U32>, t => Done{t}, n, of(v(n)), as_of(n, v(n), {==})) 1227 case 2n+ +kp: 1228 Equal.cong(U32, Result<&2, &2, NM.NumError, U32>, t => Done{t}, G.iroot_k(~U32, ~I.u32_op, ~I.u32_is, n, 2n+kp), of(M.iroot_k(v(n), 2n+kp)), as_of(G.iroot_k(~U32, ~I.u32_op, ~I.u32_is, n, 2n+kp), M.iroot_k(v(n), 2n+kp), iroot_big(32n, {==}, n, kp))) 1229 1230 # ---- comb: C(n, i + 1) = (r / g) ((n - i) / ((i + 1) / g)), g = gcd(r, i + 1) ---- 1231 1232 def nz_of(+x: U32, +n: Nat, +hx: {v(x) == n : Nat}, +h: {Nat.is_lt(0n, n) == True{} : Bool}) -> {Nat.is_eq(v(x), 0n) == False{} : Bool}: 1233 Equal.trans(Bool, Nat.is_eq(v(x), 0n), Nat.is_eq(n, 0n), False{}, Equal.cong(Nat, Bool, t => Nat.is_eq(t, 0n), v(x), n, hx), N.is_eq_sym_false(0n, n, N.is_eq_lt(0n, n, h))) 1234 1235 def ndiv(+a: Nat, +b: Nat, +na: Nat, +nb: Nat, +ha: {a == na : Nat}, +hb: {b == nb : Nat}) -> {Nat.div(a, b) == Nat.div(na, nb) : Nat}: 1236 Equal.trans(Nat, Nat.div(a, b), Nat.div(na, b), Nat.div(na, nb), Equal.cong(Nat, Nat, t => Nat.div(t, b), a, na, ha), Equal.cong(Nat, Nat, t => Nat.div(na, t), b, nb, hb)) 1237 1238 def quot_v(+a: U32, +b: U32, +na: Nat, +nb: Nat, +ha: {v(a) == na : Nat}, +hb: {v(b) == nb : Nat}, +hpos: {Nat.is_lt(0n, nb) == True{} : Bool}) -> {v(I.u32_op(NM.Quot{a, b})) == Nat.div(na, nb) : Nat}: 1239 Equal.trans(Nat, v(I.u32_op(NM.Quot{a, b})), Nat.div(v(a), v(b)), Nat.div(na, nb), LW.ops_quot(a, b, nz_of(b, nb, hb, hpos)), ndiv(v(a), v(b), na, nb, ha, hb)) 1240 1241 def combsim(+f: Nat, +n: U32, +i: U32, +k: U32, +r: U32, +nn: Nat, +ni: Nat, +k0: Nat, +K: Nat, +ok: Bool, +more: Bool, +cn: Bool, +hK: {K == 32n : Nat}, +hn: {v(n) == nn : Nat}, +hi: {v(i) == ni : Nat}, +hk: {v(k) == k0 : Nat}, +h2: {Nat.is_le(Nat.double(k0), nn) == True{} : Bool}, +hle: {Nat.is_le(ni, k0) == True{} : Bool}, +hf: {Nat.is_le(1n+K, Nat.add(f, ni)) == True{} : Bool}, +hok: {C.fits(32n, S.choose(nn, ni)) == ok : Bool}, +ha: {fv(ok, v(r), S.choose(nn, ni)) == S.choose(nn, ni) : Nat}, +hmore: {more == Nat.is_lt(ni, k0) : Bool}, +hcn: {C.fits(32n, S.choose(nn, k0)) == cn : Bool}) -> {G.comb_go(~U32, ~I.u32_op, ~I.u32_is, f, n, i, k, (r, ok), more) == G.fits(U32, Bool.not(cn), of(S.choose(nn, k0))) : Maybe<&2, U32>}: 1242 match f ok more cn: 1243 case 0n True{} _ _: 1244 +h2i = N.le_trans(Nat.double(ni), Nat.double(k0), nn, N.double_le(ni, k0, hle), h2) 1245 +big = CN.cbig(K, nn, ni, N.le_trans(K, 1n+K, ni, N.le_succ(K), hf), h2i) 1246 Empty.absurd({G.comb_go(~U32, ~I.u32_op, ~I.u32_is, 0n, n, i, k, (r, True{}), more) == G.fits(U32, Bool.not(cn), of(S.choose(nn, k0))) : Maybe<&2, U32>}, true_ne_false(Equal.trans(Bool, True{}, Nat.is_lt(S.choose(nn, ni), C.pow2(K)), False{}, Equal.sym(Bool, Nat.is_lt(S.choose(nn, ni), C.pow2(K)), True{}, fk(K, hK, S.choose(nn, ni), hok)), N.le_not_lt(S.choose(nn, ni), C.pow2(K), big)))) 1247 case 0n False{} _ True{}: 1248 Empty.absurd({G.comb_go(~U32, ~I.u32_op, ~I.u32_is, 0n, n, i, k, (r, False{}), more) == G.fits(U32, Bool.not(True{}), of(S.choose(nn, k0))) : Maybe<&2, U32>}, true_ne_false(Equal.trans(Bool, True{}, C.fits(32n, S.choose(nn, k0)), False{}, Equal.sym(Bool, C.fits(32n, S.choose(nn, k0)), True{}, hcn), unfit_mono(32n, S.choose(nn, ni), S.choose(nn, k0), CN.cmono(nn, ni, k0, hle, h2), hok)))) 1249 case 0n False{} _ False{}: 1250 {==} 1251 case 1n+g False{} _ True{}: 1252 Empty.absurd({G.comb_go(~U32, ~I.u32_op, ~I.u32_is, 1n+g, n, i, k, (r, False{}), more) == G.fits(U32, Bool.not(True{}), of(S.choose(nn, k0))) : Maybe<&2, U32>}, true_ne_false(Equal.trans(Bool, True{}, C.fits(32n, S.choose(nn, k0)), False{}, Equal.sym(Bool, C.fits(32n, S.choose(nn, k0)), True{}, hcn), unfit_mono(32n, S.choose(nn, ni), S.choose(nn, k0), CN.cmono(nn, ni, k0, hle, h2), hok)))) 1253 case 1n+g False{} _ False{}: 1254 {==} 1255 case 1n+g True{} False{} True{}: 1256 +eik = N.le_antisym(ni, k0, hle, N.not_lt_le(ni, k0, Equal.sym(Bool, False{}, Nat.is_lt(ni, k0), hmore))) 1257 Equal.cong(U32, Maybe<&2, U32>, t => Some{t}, r, of(S.choose(nn, k0)), as_of(r, S.choose(nn, k0), Equal.trans(Nat, v(r), S.choose(nn, ni), S.choose(nn, k0), ha, Equal.cong(Nat, Nat, t => S.choose(nn, t), ni, k0, eik)))) 1258 case 1n+g True{} False{} False{}: 1259 +eik = N.le_antisym(ni, k0, hle, N.not_lt_le(ni, k0, Equal.sym(Bool, False{}, Nat.is_lt(ni, k0), hmore))) 1260 Empty.absurd({G.comb_go(~U32, ~I.u32_op, ~I.u32_is, 1n+g, n, i, k, (r, True{}), False{}) == G.fits(U32, Bool.not(False{}), of(S.choose(nn, k0))) : Maybe<&2, U32>}, true_ne_false(Equal.trans(Bool, True{}, C.fits(32n, S.choose(nn, ni)), False{}, Equal.sym(Bool, C.fits(32n, S.choose(nn, ni)), True{}, hok), Equal.trans(Bool, C.fits(32n, S.choose(nn, ni)), C.fits(32n, S.choose(nn, k0)), False{}, Equal.cong(Nat, Bool, t => C.fits(32n, S.choose(nn, t)), ni, k0, eik), hcn)))) 1261 case 1n+ +g True{} True{} _: 1262 +hlt = Equal.sym(Bool, True{}, Nat.is_lt(ni, k0), hmore) 1263 +hin = N.le_trans(ni, k0, nn, N.lt_le(ni, k0, hlt), N.le_trans(k0, Nat.double(k0), nn, N.double_self_le(k0), h2)) 1264 +x = G.inc(~U32, ~I.u32_op, i) 1265 +ex = inc_v(K, hK, i, k, ni, k0, hi, hk, hlt) 1266 +t = I.u32_op(NM.Sub{n, i}) 1267 +tn = Nat.sub(nn, ni) 1268 +et = Equal.trans(Nat, v(t), Nat.sub(v(n), v(i)), tn, LW.ops_sub(n, i, le_v(i, n, ni, nn, hi, hn, hin)), nsub(v(n), v(i), nn, ni, hn, hi)) 1269 +c = S.choose(nn, ni) 1270 +c1 = S.choose(nn, 1n+ni) 1271 +ce = FA.choose_succ_right(nn, ni) 1272 +gu = G.gcd(~U32, ~I.u32_op, ~I.u32_is, r, x) 1273 +eg = Equal.trans(Nat, v(gu), M.gcd(v(r), v(x)), CN.gg(c, ni), gcd_val(r, x), Equal.trans(Nat, M.gcd(v(r), v(x)), M.gcd(c, v(x)), M.gcd(c, 1n+ni), Equal.cong(Nat, Nat, z => M.gcd(z, v(x)), v(r), c, ha), Equal.cong(Nat, Nat, z => M.gcd(c, z), v(x), 1n+ni, ex))) 1274 +au = I.u32_op(NM.Quot{r, gu}) 1275 +ea = Equal.trans(Nat, v(au), Nat.div(c, CN.gg(c, ni)), CN.wl(c, ni), quot_v(r, gu, c, CN.gg(c, ni), ha, eg, CN.g_pos(c, ni)), CN.div_c(c, ni)) 1276 +ju = I.u32_op(NM.Quot{x, gu}) 1277 +ej = Equal.trans(Nat, v(ju), Nat.div(1n+ni, CN.gg(c, ni)), CN.wr(c, ni), quot_v(x, gu, 1n+ni, CN.gg(c, ni), ex, eg, CN.g_pos(c, ni)), CN.div_j(c, ni)) 1278 +bu = I.u32_op(NM.Quot{t, ju}) 1279 +eb = Equal.trans(Nat, v(bu), Nat.div(tn, CN.wr(c, ni)), CN.sq(c, ni, tn, c1), quot_v(t, ju, tn, CN.wr(c, ni), et, ej, CN.wr_pos(c, ni)), CN.div_t(c, ni, tn, c1, ce)) 1280 +hpn = Equal.trans(Nat, Nat.mul(v(au), v(bu)), Nat.mul(CN.wl(c, ni), CN.sq(c, ni, tn, c1)), c1, nmul(v(au), v(bu), CN.wl(c, ni), CN.sq(c, ni, tn, c1), ea, eb), CN.prod_eq(c, ni, tn, c1, ce)) 1281 +hf2 = L.subst(Nat, z => {Nat.is_le(1n+K, z) == True{} : Bool}, 1n+Nat.add(g, ni), Nat.add(g, 1n+ni), Equal.sym(Nat, Nat.add(g, 1n+ni), 1n+Nat.add(g, ni), NA.add_succ(g, ni)), hf) 1282 combsim(g, n, x, k, I.u32_op(NM.Mul{au, bu}), nn, 1n+ni, k0, K, Bool.not(I.u32_is(NM.MulOver{au, bu})), I.u32_is(NM.Lt{x, k}), cn, hK, hn, ex, hk, h2, succ_le(ni, k0, hlt), hf2, ok_mul(au, bu, c1, hpn), fv_mul(au, bu, c1, hpn, C.fits(32n, c1), {==}), ltv(x, k, 1n+ni, k0, ex, hk), hcn) 1283 1284 def min_le_a(+a: Nat, +b: Nat, +c: Bool, +hc: {Nat.is_lt(a, b) == c : Bool}) -> {Nat.is_le(Nat.min(a, b), a) == True{} : Bool}: 1285 match c: 1286 case True{}: 1287 L.subst(Nat, z => {Nat.is_le(z, a) == True{} : Bool}, a, Nat.min(a, b), Equal.sym(Nat, Nat.min(a, b), a, N.min_left(a, b, hc)), N.le_refl(a)) 1288 case False{}: 1289 L.subst(Nat, z => {Nat.is_le(z, a) == True{} : Bool}, b, Nat.min(a, b), Equal.sym(Nat, Nat.min(a, b), b, N.min_right(a, b, hc)), N.not_lt_le(a, b, hc)) 1290 1291 def min_le_b(+a: Nat, +b: Nat, +c: Bool, +hc: {Nat.is_lt(a, b) == c : Bool}) -> {Nat.is_le(Nat.min(a, b), b) == True{} : Bool}: 1292 match c: 1293 case True{}: 1294 L.subst(Nat, z => {Nat.is_le(z, b) == True{} : Bool}, a, Nat.min(a, b), Equal.sym(Nat, Nat.min(a, b), a, N.min_left(a, b, hc)), N.lt_le(a, b, hc)) 1295 case False{}: 1296 L.subst(Nat, z => {Nat.is_le(z, b) == True{} : Bool}, b, Nat.min(a, b), Equal.sym(Nat, Nat.min(a, b), b, N.min_right(a, b, hc)), N.le_refl(b)) 1297 1298 def le_add_rr(+a: Nat, +b: Nat, +c: Nat, +h: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.is_le(Nat.add(a, c), Nat.add(b, c)) == True{} : Bool}: 1299 +h1 = L.subst(Nat, z => {Nat.is_le(z, Nat.add(c, b)) == True{} : Bool}, Nat.add(c, a), Nat.add(a, c), N.add_comm(c, a), N.le_add_left(a, b, c, h)) 1300 L.subst(Nat, z => {Nat.is_le(Nat.add(a, c), z) == True{} : Bool}, Nat.add(c, b), Nat.add(b, c), N.add_comm(c, b), h1) 1301 1302 def comb_top(+K: Nat, +hK: {K == 32n : Nat}, +n: U32, +k: U32, +big: Bool, +hbig: {I.u32_is(NM.Lt{n, k}) == big : Bool}) -> {G.comb_big(~U32, ~I.u32_op, ~I.u32_is, n, k, big) == SG.checked(~U32, ~SG.u32_of, 32n, S.choose(v(n), v(k))) : Result<&2, &2, NM.NumError, U32>}: 1303 match big: 1304 case True{}: 1305 +cz = FA.choose_eq_zero(v(n), v(k), lt_of(n, k, True{}, hbig)) 1306 Equal.trans(Result<&2, &2, NM.NumError, U32>, Done{I.u32_op(NM.ZeroOp{})}, SG.checked(~U32, ~SG.u32_of, 32n, 0n), SG.checked(~U32, ~SG.u32_of, 32n, S.choose(v(n), v(k))), Equal.cong(U32, Result<&2, &2, NM.NumError, U32>, t => Done{t}, I.u32_op(NM.ZeroOp{}), of(0n), as_of(I.u32_op(NM.ZeroOp{}), 0n, zero_v())), Equal.cong(Nat, Result<&2, &2, NM.NumError, U32>, t => SG.checked(~U32, ~SG.u32_of, 32n, t), 0n, S.choose(v(n), v(k)), Equal.sym(Nat, S.choose(v(n), v(k)), 0n, cz))) 1307 case False{}: 1308 +hkn = N.not_lt_le(v(n), v(k), lt_of(n, k, False{}, hbig)) 1309 +s = I.u32_op(NM.Sub{n, k}) 1310 +sn = Nat.sub(v(n), v(k)) 1311 +es = Equal.trans(Nat, v(s), Nat.sub(v(n), v(k)), sn, LW.ops_sub(n, k, hkn), {==}) 1312 +k0 = Nat.min(v(k), sn) 1313 +kk = G.min(~U32, ~I.u32_op, ~I.u32_is, k, s) 1314 +hk0a = min_le_a(v(k), sn, Nat.is_lt(v(k), sn), {==}) 1315 +hk0b = min_le_b(v(k), sn, Nat.is_lt(v(k), sn), {==}) 1316 +hkK = L.subst(Nat, z => {Nat.is_lt(z, C.pow2(K)) == True{} : Bool}, v(k), v(k), {==}, U32P.val_lt(1n, {==}, K, hK, k)) 1317 +ekk0 = min_c(k, s, I.u32_is(NM.Lt{s, k}), {==}) 1318 +ekk1 = Equal.cong(U32, Nat, t => v(t), kk, of(Nat.min(v(k), v(s))), ekk0) 1319 +ekk2 = Equal.cong(Nat, Nat, t => Nat.min(v(k), t), v(s), sn, es) 1320 +hfk = fits32(K, hK, k0, N.le_lt_trans(k0, v(k), C.pow2(K), hk0a, hkK)) 1321 +ekk = Equal.trans(Nat, v(kk), v(of(Nat.min(v(k), v(s)))), k0, ekk1, Equal.trans(Nat, v(of(Nat.min(v(k), v(s)))), v(of(k0)), k0, Equal.cong(Nat, Nat, t => v(of(t)), Nat.min(v(k), v(s)), k0, ekk2), LW.vo(k0, hfk))) 1322 +hsum = N.le_trans(Nat.add(k0, k0), Nat.add(v(k), k0), v(n), le_add_rr(k0, v(k), k0, hk0a), L.subst(Nat, z => {Nat.is_le(Nat.add(v(k), k0), z) == True{} : Bool}, Nat.add(v(k), sn), v(n), N.sub_add(v(n), v(k), hkn), N.le_add_left(k0, sn, v(k), hk0b))) 1323 +h2 = L.subst(Nat, z => {Nat.is_le(z, v(n)) == True{} : Bool}, Nat.add(k0, k0), Nat.double(k0), Equal.sym(Nat, Nat.double(k0), Nat.add(k0, k0), NA.double_self(k0)), hsum) 1324 +one = I.u32_op(NM.One{}) 1325 +zero = I.u32_op(NM.ZeroOp{}) 1326 +c0 = FA.choose_zero_right(v(n)) 1327 +hf0 = L.subst(Nat, z => {Nat.is_le(1n+z, 140n) == True{} : Bool}, 32n, K, Equal.sym(Nat, K, 32n, hK), {==}) 1328 +hok = L.subst(Nat, z => {C.fits(32n, z) == True{} : Bool}, 1n, S.choose(v(n), 0n), Equal.sym(Nat, S.choose(v(n), 0n), 1n, c0), {==}) 1329 +ha = Equal.trans(Nat, v(one), 1n, S.choose(v(n), 0n), one_v(), Equal.sym(Nat, S.choose(v(n), 0n), 1n, c0)) 1330 +D = S.choose(v(n), k0) 1331 +sm = combsim(140n, n, zero, kk, one, v(n), 0n, k0, K, True{}, I.u32_is(NM.Lt{zero, kk}), C.fits(32n, D), hK, {==}, zero_v(), ekk, h2, N.zero_le(k0), hf0, hok, ha, ltv(zero, kk, 0n, k0, zero_v(), ekk), {==}) 1332 +g = G.comb_go(~U32, ~I.u32_op, ~I.u32_is, 140n, n, zero, kk, (one, True{}), I.u32_is(NM.Lt{zero, kk})) 1333 +em = FA.comb_min(v(n), v(k), hkn, Nat.is_lt(v(k), sn), {==}) 1334 Equal.trans(Result<&2, &2, NM.NumError, U32>, G.ok(U32, g), SG.checked(~U32, ~SG.u32_of, 32n, D), SG.checked(~U32, ~SG.u32_of, 32n, S.choose(v(n), v(k))), Equal.trans(Result<&2, &2, NM.NumError, U32>, G.ok(U32, g), G.ok(U32, G.fits(U32, Bool.not(C.fits(32n, D)), of(D))), SG.checked(~U32, ~SG.u32_of, 32n, D), Equal.cong(Maybe<&2, U32>, Result<&2, &2, NM.NumError, U32>, t => G.ok(U32, t), g, G.fits(U32, Bool.not(C.fits(32n, D)), of(D)), sm), okfits(D, C.fits(32n, D))), Equal.cong(Nat, Result<&2, &2, NM.NumError, U32>, t => SG.checked(~U32, ~SG.u32_of, 32n, t), D, S.choose(v(n), v(k)), em)) 1335 1336 def comb_checked(+n: U32, +k: U32) -> SG.Comb.checked(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 32n, n, k): 1337 Equal.trans(Result<&2, &2, NM.NumError, U32>, G.comb_big(~U32, ~I.u32_op, ~I.u32_is, n, k, I.u32_is(NM.Lt{n, k})), SG.checked(~U32, ~SG.u32_of, 32n, S.choose(v(n), v(k))), SG.checked(~U32, ~SG.u32_of, 32n, M.comb(v(n), v(k))), comb_top(32n, {==}, n, k, I.u32_is(NM.Lt{n, k}), {==}), Equal.cong(Nat, Result<&2, &2, NM.NumError, U32>, t => SG.checked(~U32, ~SG.u32_of, 32n, t), S.choose(v(n), v(k)), M.comb(v(n), v(k)), Equal.sym(Nat, M.comb(v(n), v(k)), S.choose(v(n), v(k)), FA.comb_ok(v(n), v(k)))))