1 import Base 2 import ./lemmas/spec/numeric.bend as S 3 import ./nat.bend as N 4 import ./logic.bend as L 5 import ./u32.bend as U 6 import ./u32alg.bend as A 7 import ./lemmas/proofs/nat_algebra.bend as NA 8 import ./lemmas/proofs/natural_products.bend as PR 9 import ./lemmas/proofs/division_bounds.bend as DB 10 import ./lemmas/proofs/division_quotient.bend as DQ 11 import ./lemmas/proofs/natural_division.bend as ND 12 import ./lemmas/proofs/word_comparison.bend as WC 13 import ./word.bend as WD 14 15 # Base's U32.div and U32.mod (binary long division, U32.divmod.go) against 16 # Nat division, for every nonzero divisor, the remainder's shift carry 17 # included: 18 # div_mod: to_nat(div(a, b)) * to_nat(b) + to_nat(mod(a, b)) == to_nat(a) 19 # and to_nat(mod(a, b)) < to_nat(b) 20 # div_nat: to_nat(div(a, b)) == Nat.div(to_nat(a), to_nat(b)) 21 # mod_nat: to_nat(mod(a, b)) == Nat.mod(to_nat(a), to_nat(b)) 22 23 def v(+x: U32) -> Nat: 24 U32.to_nat(x) 25 26 def dq(-m: Nat, r: Word(m) & U32) -> Word(m): 27 (q, s) = r 28 q 29 30 def dr(-m: Nat, r: Word(m) & U32) -> U32: 31 (q, s) = r 32 s 33 34 # the long-division invariant of a partial result r for the prefix a 35 def inv(+m: Nat, +a: Word(m), +bn: Nat, r: Word(m) & U32) -> Type: 36 {Nat.add(Nat.mul(S.unsigned(m, dq(m, r)), bn), v(dr(m, r))) == S.unsigned(m, a) : Nat} & {Nat.is_lt(v(dr(m, r)), bn) == True{} : Bool} 37 38 # ---- digit algebra ---- 39 40 # a subtracting digit: (1 + 2q) b + d == a + 2 (q b + r) when b + d == a + 2 r 41 def digit_one(+q: Nat, +bn: Nat, +r: Nat, +a: Nat, +d: Nat, +h: {Nat.add(bn, d) == Nat.add(a, Nat.double(r)) : Nat}) -> {Nat.add(Nat.mul(1n+Nat.double(q), bn), d) == Nat.add(a, Nat.double(Nat.add(Nat.mul(q, bn), r))) : Nat}: 42 +x = Nat.double(Nat.mul(q, bn)) 43 +rhs = Nat.add(a, Nat.double(Nat.add(Nat.mul(q, bn), r))) 44 %Equal.sym(Nat, Nat.mul(Nat.double(q), bn), x, PR.double_product(q, bn)) : {Nat.add(Nat.add(bn, _), d) == rhs : Nat} 45 %Equal.sym(Nat, Nat.add(Nat.add(bn, x), d), Nat.add(Nat.add(bn, d), x), A.add_rot(bn, x, d)) : {_ == rhs : Nat} 46 %N.add_comm(x, Nat.add(bn, d)) : {_ == rhs : Nat} 47 %Equal.sym(Nat, Nat.add(bn, d), Nat.add(a, Nat.double(r)), h) : {Nat.add(x, _) == rhs : Nat} 48 %NA.add_swap(a, x, Nat.double(r)) : {_ == rhs : Nat} 49 Equal.cong(Nat, Nat, z => Nat.add(a, z), Nat.add(x, Nat.double(r)), Nat.double(Nat.add(Nat.mul(q, bn), r)), N.add_double(Nat.mul(q, bn), r)) 50 51 # a zero digit: 2q b + (a + 2 r) == a + 2 (q b + r) 52 def digit_zero(+q: Nat, +bn: Nat, +r: Nat, +a: Nat) -> {Nat.add(Nat.mul(Nat.double(q), bn), Nat.add(a, Nat.double(r))) == Nat.add(a, Nat.double(Nat.add(Nat.mul(q, bn), r))) : Nat}: 53 +x = Nat.double(Nat.mul(q, bn)) 54 +rhs = Nat.add(a, Nat.double(Nat.add(Nat.mul(q, bn), r))) 55 %Equal.sym(Nat, Nat.mul(Nat.double(q), bn), x, PR.double_product(q, bn)) : {Nat.add(_, Nat.add(a, Nat.double(r))) == rhs : Nat} 56 %NA.add_swap(a, x, Nat.double(r)) : {_ == rhs : Nat} 57 Equal.cong(Nat, Nat, z => Nat.add(a, z), Nat.add(x, Nat.double(r)), Nat.double(Nat.add(Nat.mul(q, bn), r)), N.add_double(Nat.mul(q, bn), r)) 58 59 # ---- U32 views of the width-generic word facts ---- 60 61 def vw(+w: Word(32n)) -> {v(U32{w}) == WD.uw(32n, w) : Nat}: 62 U.to_nat_word(w) 63 64 def vb(+one: Nat, +h1: {one == 1n : Nat}, +x: U32) -> {Nat.is_lt(v(x), WD.sc(32n, one)) == True{} : Bool}: 65 match x: 66 case U32{+w}: 67 %Equal.sym(Nat, v(U32{w}), WD.uw(32n, w), vw(w)) : {Nat.is_lt(_, WD.sc(32n, one)) == True{} : Bool} 68 WD.wb(32n, one, h1, w) 69 70 def sub32(+one: Nat, +h1: {one == 1n : Nat}, +x: U32, +b: U32, +d: Nat, +e: {Nat.add(v(x), WD.sc(32n, one)) == Nat.add(d, v(b)) : Nat}, +hd: {Nat.is_lt(d, WD.sc(32n, one)) == True{} : Bool}) -> {v(U32.sub(x, b)) == d : Nat}: 71 match x b: 72 case U32{+xw} U32{+bw}: 73 +e2 = Equal.trans(Nat, Nat.add(WD.uw(32n, xw), WD.sc(32n, one)), Nat.add(v(U32{xw}), WD.sc(32n, one)), Nat.add(d, WD.uw(32n, bw)), 74 Equal.cong(Nat, Nat, z => Nat.add(z, WD.sc(32n, one)), WD.uw(32n, xw), v(U32{xw}), Equal.sym(Nat, v(U32{xw}), WD.uw(32n, xw), vw(xw))), 75 Equal.trans(Nat, Nat.add(v(U32{xw}), WD.sc(32n, one)), Nat.add(d, v(U32{bw})), Nat.add(d, WD.uw(32n, bw)), e, Equal.cong(Nat, Nat, z => Nat.add(d, z), v(U32{bw}), WD.uw(32n, bw), vw(bw)))) 76 %Equal.sym(Nat, v(U32{Word.sub(32n, xw, bw)}), WD.uw(32n, Word.sub(32n, xw, bw)), vw(Word.sub(32n, xw, bw))) : {_ == d : Nat} 77 WD.sub_wrap(32n, one, h1, xw, bw, d, e2, hd) 78 79 # ---- one long-division step ---- 80 81 def fin_true(+p: Nat, +q: Word(p), +s: U32, +b: U32, +a0: Bool, +hi: Word(p), +r: Nat, +one: Nat, +h1: {one == 1n : Nat}, +he: {Nat.add(Nat.mul(S.unsigned(p, q), v(b)), r) == S.unsigned(p, hi) : Nat}, +hr: {Nat.is_lt(r, v(b)) == True{} : Bool}, +hts: {Nat.add(v(s), WD.sc(32n, one)) == Nat.add(S.bit_value(a0), Nat.double(r)) : Nat}) -> inv(1n+p, WCon{a0, hi}, v(b), U32.divmod.go.fin(p, q, s, b, True{})): 82 +bn = v(b) 83 +k = WD.sc(32n, one) 84 +t = Nat.add(S.bit_value(a0), Nat.double(r)) 85 +hbk = vb(one, h1, b) 86 +hkt = L.subst(Nat, z => {Nat.is_le(k, z) == True{} : Bool}, Nat.add(k, v(s)), t, Equal.trans(Nat, Nat.add(k, v(s)), Nat.add(v(s), k), t, N.add_comm(k, v(s)), hts), N.le_add_right(k, v(s))) 87 +hbt = N.lt_le(bn, t, N.lt_le_trans(bn, k, t, hbk, hkt)) 88 +d = Nat.sub(t, bn) 89 +hsum = N.sub_add(t, bn, hbt) 90 +htb = L.subst(Nat, z => {Nat.is_lt(t, z) == True{} : Bool}, Nat.double(bn), Nat.add(bn, bn), NA.double_self(bn), N.double_lt_bit(a0, r, bn, hr)) 91 +hdb = N.sub_lt(t, bn, bn, hbt, htb) 92 +hdk = N.lt_trans(d, bn, k, hdb, hbk) 93 +e = Equal.trans(Nat, Nat.add(v(s), k), t, Nat.add(d, bn), hts, Equal.trans(Nat, t, Nat.add(bn, d), Nat.add(d, bn), Equal.sym(Nat, Nat.add(bn, d), t, hsum), N.add_comm(bn, d))) 94 +hsub = sub32(one, h1, s, b, d, e, hdk) 95 +eq = Equal.trans(Nat, Nat.add(Nat.mul(1n+Nat.double(S.unsigned(p, q)), bn), v(U32.sub(s, b))), Nat.add(Nat.mul(1n+Nat.double(S.unsigned(p, q)), bn), d), Nat.add(S.bit_value(a0), Nat.double(S.unsigned(p, hi))), 96 Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(1n+Nat.double(S.unsigned(p, q)), bn), z), v(U32.sub(s, b)), d, hsub), 97 %he : {Nat.add(Nat.mul(1n+Nat.double(S.unsigned(p, q)), bn), d) == Nat.add(S.bit_value(a0), Nat.double(_)) : Nat} 98 digit_one(S.unsigned(p, q), bn, r, S.bit_value(a0), d, hsum)) 99 +lt = L.subst(Nat, z => {Nat.is_lt(z, bn) == True{} : Bool}, d, v(U32.sub(s, b)), Equal.sym(Nat, v(U32.sub(s, b)), d, hsub), hdb) 100 (eq, lt) 101 102 def fin_ge(+p: Nat, +q: Word(p), +s: U32, +b: U32, +a0: Bool, +hi: Word(p), +r: Nat, +he: {Nat.add(Nat.mul(S.unsigned(p, q), v(b)), r) == S.unsigned(p, hi) : Nat}, +hr: {Nat.is_lt(r, v(b)) == True{} : Bool}, +hs: {v(s) == Nat.add(S.bit_value(a0), Nat.double(r)) : Nat}, +hge: {Nat.is_ge(v(s), v(b)) == True{} : Bool}) -> inv(1n+p, WCon{a0, hi}, v(b), U32.divmod.go.fin(p, q, s, b, True{})): 103 +bn = v(b) 104 +t = Nat.add(S.bit_value(a0), Nat.double(r)) 105 +htb = L.subst(Nat, z => {Nat.is_lt(t, z) == True{} : Bool}, Nat.double(bn), Nat.add(bn, bn), NA.double_self(bn), N.double_lt_bit(a0, r, bn, hr)) 106 +hle = Equal.trans(Bool, Nat.is_le(bn, v(s)), Nat.is_ge(v(s), bn), True{}, Equal.sym(Bool, Nat.is_ge(v(s), bn), Nat.is_le(bn, v(s)), DB.ge_reverse(v(s), bn)), hge) 107 +d = Nat.sub(v(s), bn) 108 +hsub = U.sub_nat(s, b, hle) 109 +hsum = Equal.trans(Nat, Nat.add(bn, d), v(s), t, N.sub_add(v(s), bn, hle), hs) 110 +hsb = L.subst(Nat, z => {Nat.is_lt(z, Nat.add(bn, bn)) == True{} : Bool}, t, v(s), Equal.sym(Nat, v(s), t, hs), htb) 111 +hdb = N.sub_lt(v(s), bn, bn, hle, hsb) 112 +eq = Equal.trans(Nat, Nat.add(Nat.mul(1n+Nat.double(S.unsigned(p, q)), bn), v(U32.sub(s, b))), Nat.add(Nat.mul(1n+Nat.double(S.unsigned(p, q)), bn), d), Nat.add(S.bit_value(a0), Nat.double(S.unsigned(p, hi))), 113 Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(1n+Nat.double(S.unsigned(p, q)), bn), z), v(U32.sub(s, b)), d, hsub), 114 %he : {Nat.add(Nat.mul(1n+Nat.double(S.unsigned(p, q)), bn), d) == Nat.add(S.bit_value(a0), Nat.double(_)) : Nat} 115 digit_one(S.unsigned(p, q), bn, r, S.bit_value(a0), d, hsum)) 116 +lt = L.subst(Nat, z => {Nat.is_lt(z, bn) == True{} : Bool}, d, v(U32.sub(s, b)), Equal.sym(Nat, v(U32.sub(s, b)), d, hsub), hdb) 117 (eq, lt) 118 119 def fin_lt(+p: Nat, +q: Word(p), +s: U32, +b: U32, +a0: Bool, +hi: Word(p), +r: Nat, +he: {Nat.add(Nat.mul(S.unsigned(p, q), v(b)), r) == S.unsigned(p, hi) : Nat}, +hs: {v(s) == Nat.add(S.bit_value(a0), Nat.double(r)) : Nat}, +hge: {Nat.is_ge(v(s), v(b)) == False{} : Bool}) -> inv(1n+p, WCon{a0, hi}, v(b), U32.divmod.go.fin(p, q, s, b, False{})): 120 +bn = v(b) 121 +t = Nat.add(S.bit_value(a0), Nat.double(r)) 122 +lt = DB.not_ge(v(s), bn, hge) 123 +eq = Equal.trans(Nat, Nat.add(Nat.mul(Nat.double(S.unsigned(p, q)), bn), v(s)), Nat.add(Nat.mul(Nat.double(S.unsigned(p, q)), bn), t), Nat.add(S.bit_value(a0), Nat.double(S.unsigned(p, hi))), 124 Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(Nat.double(S.unsigned(p, q)), bn), z), v(s), t, hs), 125 %he : {Nat.add(Nat.mul(Nat.double(S.unsigned(p, q)), bn), t) == Nat.add(S.bit_value(a0), Nat.double(_)) : Nat} 126 digit_zero(S.unsigned(p, q), bn, r, S.bit_value(a0))) 127 (eq, lt) 128 129 def fin_false(+p: Nat, +q: Word(p), +s: U32, +b: U32, +a0: Bool, +hi: Word(p), +r: Nat, +he: {Nat.add(Nat.mul(S.unsigned(p, q), v(b)), r) == S.unsigned(p, hi) : Nat}, +hr: {Nat.is_lt(r, v(b)) == True{} : Bool}, +hs: {v(s) == Nat.add(S.bit_value(a0), Nat.double(r)) : Nat}, +g: Bool, +hg: {U32.is_ge(s, b) == g : Bool}) -> inv(1n+p, WCon{a0, hi}, v(b), U32.divmod.go.fin(p, q, s, b, g)): 130 match g: 131 case True{}: 132 fin_ge(p, q, s, b, a0, hi, r, he, hr, hs, Equal.trans(Bool, Nat.is_ge(v(s), v(b)), U32.is_ge(s, b), True{}, Equal.sym(Bool, U32.is_ge(s, b), Nat.is_ge(v(s), v(b)), WC.u32_ge(s, b)), hg)) 133 case False{}: 134 fin_lt(p, q, s, b, a0, hi, r, he, hs, Equal.trans(Bool, Nat.is_ge(v(s), v(b)), U32.is_ge(s, b), False{}, Equal.sym(Bool, U32.is_ge(s, b), Nat.is_ge(v(s), v(b)), WC.u32_ge(s, b)), hg)) 135 136 def shl_ts(+p: Nat, +q: Word(p), +b: U32, +t: Bool, +s: Word(32n), +a0: Bool, +hi: Word(p), +r: Nat, +one: Nat, +h1: {one == 1n : Nat}, +he: {Nat.add(Nat.mul(S.unsigned(p, q), v(b)), r) == S.unsigned(p, hi) : Nat}, +hr: {Nat.is_lt(r, v(b)) == True{} : Bool}, +hts: {Nat.add(WD.uw(32n, s), WD.sc(32n, WD.bo(t, one))) == Nat.add(S.bit_value(a0), Nat.double(r)) : Nat}) -> inv(1n+p, WCon{a0, hi}, v(b), U32.divmod.go.fin(p, q, U32{s}, b, Bool.or(t, U32.is_ge(U32{s}, b)))): 137 match t: 138 case True{}: 139 fin_true(p, q, U32{s}, b, a0, hi, r, one, h1, he, hr, L.subst(Nat, z => {Nat.add(z, WD.sc(32n, one)) == Nat.add(S.bit_value(a0), Nat.double(r)) : Nat}, WD.uw(32n, s), v(U32{s}), Equal.sym(Nat, v(U32{s}), WD.uw(32n, s), vw(s)), hts)) 140 case False{}: 141 +hs = Equal.trans(Nat, v(U32{s}), WD.uw(32n, s), Nat.add(S.bit_value(a0), Nat.double(r)), vw(s), Equal.trans(Nat, WD.uw(32n, s), Nat.add(WD.uw(32n, s), 0n), Nat.add(S.bit_value(a0), Nat.double(r)), Equal.sym(Nat, Nat.add(WD.uw(32n, s), 0n), WD.uw(32n, s), N.add_zero(WD.uw(32n, s))), hts)) 142 fin_false(p, q, U32{s}, b, a0, hi, r, he, hr, hs, U32.is_ge(U32{s}, b), {==}) 143 144 def shl_ok(+p: Nat, +q: Word(p), +b: U32, ts: Bool & Word(32n), +a0: Bool, +hi: Word(p), +r: Nat, +one: Nat, +h1: {one == 1n : Nat}, +he: {Nat.add(Nat.mul(S.unsigned(p, q), v(b)), r) == S.unsigned(p, hi) : Nat}, +hr: {Nat.is_lt(r, v(b)) == True{} : Bool}, hts: {Nat.add(WD.uw(32n, WD.ow(32n, ts)), WD.sc(32n, WD.bo(WD.ob(32n, ts), one))) == Nat.add(S.bit_value(a0), Nat.double(r)) : Nat}) -> inv(1n+p, WCon{a0, hi}, v(b), U32.divmod.go.shl(p, q, b, ts)): 145 match ts: 146 case (+t, +s): 147 shl_ts(p, q, b, t, s, a0, hi, r, one, h1, he, hr, hts) 148 149 def rec_ok(+p: Nat, +a0: Bool, +b: U32, +hi: Word(p), qr: Word(p) & U32, ih: inv(p, hi, v(b), qr), +one: Nat, +h1: {one == 1n : Nat}) -> inv(1n+p, WCon{a0, hi}, v(b), U32.divmod.go.rec(p, a0, b, qr)): 150 match qr: 151 case (+q, +r): 152 match r: 153 case U32{+rw}: 154 (he, hr) = ih 155 +hts = Equal.trans(Nat, Nat.add(WD.uw(32n, WD.ow(32n, Word.shl.out(32n, a0, rw))), WD.sc(32n, WD.bo(WD.ob(32n, Word.shl.out(32n, a0, rw)), one))), Nat.add(S.bit_value(a0), Nat.double(WD.uw(32n, rw))), Nat.add(S.bit_value(a0), Nat.double(v(U32{rw}))), 156 WD.shl_out1(32n, one, h1, a0, rw), 157 Equal.cong(Nat, Nat, z => Nat.add(S.bit_value(a0), Nat.double(z)), WD.uw(32n, rw), v(U32{rw}), Equal.sym(Nat, v(U32{rw}), WD.uw(32n, rw), vw(rw)))) 158 shl_ok(p, q, b, Word.shl.out(32n, a0, rw), a0, hi, v(U32{rw}), one, h1, he, hr, hts) 159 160 # the invariant holds for every prefix of the dividend 161 def go_ok(+m: Nat, +a: Word(m), +b: U32, +hb: {Nat.is_lt(0n, v(b)) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}) -> inv(m, a, v(b), U32.divmod.go(m, a, b)): 162 match m a: 163 case 0n WNil{}: 164 ({==}, hb) 165 case 1n+p WCon{a0, hi}: 166 rec_ok(p, a0, b, hi, U32.divmod.go(p, hi, b), go_ok(p, hi, b, hb, one, h1), one, h1) 167 168 # ---- the division theorems ---- 169 170 def pos_nat(+x: Nat, +h: {Cmp.is_eq(Nat.cmp(x, 0n)) == False{} : Bool}) -> {Nat.is_lt(0n, x) == True{} : Bool}: 171 match x: 172 case 0n: 173 Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, L.true_false(h)) 174 case 1n+k: 175 {==} 176 177 def pos(+b: U32, +hb: {U32.is_zero(b) == False{} : Bool}) -> {Nat.is_lt(0n, v(b)) == True{} : Bool}: 178 pos_nat(v(b), L.subst(Cmp, c => {Cmp.is_eq(c) == False{} : Bool}, U32.cmp(b, 0), Nat.cmp(v(b), 0n), U.u32_cmp(b, 0), hb)) 179 180 def dm_fin(+aw: Word(32n), +b: U32, qr: Word(32n) & U32, h: inv(32n, aw, v(b), qr)) -> {Nat.add(Nat.mul(v(U32.div.fin(qr)), v(b)), v(U32.mod.fin(qr))) == v(U32{aw}) : Nat} & {Nat.is_lt(v(U32.mod.fin(qr)), v(b)) == True{} : Bool}: 181 match qr: 182 case (+q, +r): 183 (he, hr) = h 184 +eq = Equal.trans(Nat, Nat.add(Nat.mul(v(U32{q}), v(b)), v(r)), Nat.add(Nat.mul(S.unsigned(32n, q), v(b)), v(r)), v(U32{aw}), 185 Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(z, v(b)), v(r)), v(U32{q}), S.unsigned(32n, q), vw(q)), 186 Equal.trans(Nat, Nat.add(Nat.mul(S.unsigned(32n, q), v(b)), v(r)), S.unsigned(32n, aw), v(U32{aw}), he, Equal.sym(Nat, v(U32{aw}), S.unsigned(32n, aw), vw(aw)))) 187 (eq, hr) 188 189 def dm_if(+aw: Word(32n), +b: U32, +z: Bool, +hz: {z == False{} : Bool}, +hb: {Nat.is_lt(0n, v(b)) == True{} : Bool}) -> {Nat.add(Nat.mul(v(U32.div.if(aw, b, z)), v(b)), v(U32.mod.if(aw, b, z))) == v(U32{aw}) : Nat} & {Nat.is_lt(v(U32.mod.if(aw, b, z)), v(b)) == True{} : Bool}: 190 match z: 191 case True{}: 192 Empty.absurd({Nat.add(Nat.mul(v(U32.div.if(aw, b, True{})), v(b)), v(U32.mod.if(aw, b, True{}))) == v(U32{aw}) : Nat} & {Nat.is_lt(v(U32.mod.if(aw, b, True{})), v(b)) == True{} : Bool}, L.true_false(hz)) 193 case False{}: 194 dm_fin(aw, b, U32.divmod.go(32n, aw, b), go_ok(32n, aw, b, hb, 1n, {==})) 195 196 # THEOREM: div and mod are Euclidean division by any nonzero divisor. 197 def div_mod(+a: U32, +b: U32, +hb: {U32.is_zero(b) == False{} : Bool}) -> {Nat.add(Nat.mul(v(U32.div(a, b)), v(b)), v(U32.mod(a, b))) == v(a) : Nat} & {Nat.is_lt(v(U32.mod(a, b)), v(b)) == True{} : Bool}: 198 match a b: 199 case U32{+aw} U32{+bw}: 200 dm_if(aw, U32{bw}, U32.is_zero(U32{bw}), hb, pos(U32{bw}, hb)) 201 202 def mod_identify(+q: Nat, +d: Nat, +r: Nat, +bound: {Nat.is_lt(r, d) == True{} : Bool}) -> {Nat.mod(Nat.add(Nat.mul(q, d), r), d) == r : Nat}: 203 match d: 204 case 0n: 205 Empty.absurd({Nat.mod(Nat.add(Nat.mul(q, 0n), r), 0n) == r : Nat}, N.lt_zero_absurd(r, bound)) 206 case 1n+p: 207 ND.remainder(q, p, r, N.lt_succ_le(r, p, bound)) 208 209 def dm_type(+a: U32, +b: U32) -> Type: 210 {Nat.add(Nat.mul(v(U32.div(a, b)), v(b)), v(U32.mod(a, b))) == v(a) : Nat} & {Nat.is_lt(v(U32.mod(a, b)), v(b)) == True{} : Bool} 211 212 def div_of(+a: U32, +b: U32, h: dm_type(a, b)) -> {v(U32.div(a, b)) == Nat.div(v(a), v(b)) : Nat}: 213 (e, lt) = h 214 %e : {v(U32.div(a, b)) == Nat.div(_, v(b)) : Nat} 215 Equal.sym(Nat, Nat.div(Nat.add(Nat.mul(v(U32.div(a, b)), v(b)), v(U32.mod(a, b))), v(b)), v(U32.div(a, b)), DQ.identify(v(U32.div(a, b)), v(b), v(U32.mod(a, b)), lt)) 216 217 def mod_of(+a: U32, +b: U32, h: dm_type(a, b)) -> {v(U32.mod(a, b)) == Nat.mod(v(a), v(b)) : Nat}: 218 (e, lt) = h 219 %e : {v(U32.mod(a, b)) == Nat.mod(_, v(b)) : Nat} 220 Equal.sym(Nat, Nat.mod(Nat.add(Nat.mul(v(U32.div(a, b)), v(b)), v(U32.mod(a, b))), v(b)), v(U32.mod(a, b)), mod_identify(v(U32.div(a, b)), v(b), v(U32.mod(a, b)), lt)) 221 222 # THEOREM: div is Nat division. 223 def div_nat(+a: U32, +b: U32, +hb: {U32.is_zero(b) == False{} : Bool}) -> {v(U32.div(a, b)) == Nat.div(v(a), v(b)) : Nat}: 224 div_of(a, b, div_mod(a, b, hb)) 225 226 # THEOREM: mod is Nat remainder. 227 def mod_nat(+a: U32, +b: U32, +hb: {U32.is_zero(b) == False{} : Bool}) -> {v(U32.mod(a, b)) == Nat.mod(v(a), v(b)) : Nat}: 228 mod_of(a, b, div_mod(a, b, hb))