U64int.dm: def of bend-collections-laws-math@1.0.0.0 Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64int.bend as U64int Lines 61-77 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64int.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64int.bend&start_line=61&end_line=77 import Base import bend-collections-laws-math@1.0.0.0/spec/math/generic.bend as SG import bend-collections-laws-math@1.0.0.0/src/math/generic.bend as G import bend-collections-laws-math@1.0.0.0/src/math/num.bend as NM import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M import bend-collections-laws-math@1.0.0.0/src/math/instances.bend as I import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64laws.bend as LW import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU def dm(+a: WU.U64, +b: WU.U64, +c: Bool, +hc: {I.u64_is(NM.IsZero{b}) == c : Bool}, +nb: Nat, +hnb: {v(b) == nb : Nat}) -> {G.divmod_ok(~WU.U64, ~I.u64_op, a, b, c) == SG.lift_qr(~WU.U64, ~SG.u64_of, M.divmod(v(a), nb)) : Result<&2, &2, NM.NumError, G.QuotRem>}: match c nb: case True{} 0n: {==} case False{} 0n: +hz = Equal.trans(Bool, False{}, I.u64_is(NM.IsZero{b}), Nat.is_eq(0n, 0n), Equal.sym(Bool, I.u64_is(NM.IsZero{b}), False{}, hc), Equal.trans(Bool, I.u64_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))) Empty.absurd({G.divmod_ok(~WU.U64, ~I.u64_op, a, b, False{}) == SG.lift_qr(~WU.U64, ~SG.u64_of, M.divmod(v(a), 0n)) : Result<&2, &2, NM.NumError, G.QuotRem>}, true_ne_false(Equal.sym(Bool, False{}, True{}, hz))) case True{} 1n+ +bp: +hz = Equal.trans(Bool, True{}, I.u64_is(NM.IsZero{b}), Nat.is_eq(1n+bp, 0n), Equal.sym(Bool, I.u64_is(NM.IsZero{b}), True{}, hc), Equal.trans(Bool, I.u64_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))) Empty.absurd({G.divmod_ok(~WU.U64, ~I.u64_op, a, b, True{}) == SG.lift_qr(~WU.U64, ~SG.u64_of, M.divmod(v(a), 1n+bp)) : Result<&2, &2, NM.NumError, G.QuotRem>}, true_ne_false(hz)) case False{} 1n+ +bp: +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), {==}) +eq = as_of(I.u64_op(NM.Quot{a, b}), Nat.div(v(a), 1n+bp), Equal.trans(Nat, v(I.u64_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))) +er = as_of(I.u64_op(NM.Rem{a, b}), Nat.mod(v(a), 1n+bp), Equal.trans(Nat, v(I.u64_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))) %Equal.sym(WU.U64, I.u64_op(NM.Quot{a, b}), of(Nat.div(v(a), 1n+bp)), eq) : {Done{G.TQR{_, I.u64_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>} %Equal.sym(WU.U64, I.u64_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>} {==} Uses (28): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.div https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64int.bend&name=as_of https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64int.bend&name=of https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64int.bend&name=true_ne_false https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64int.bend&name=v https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64laws.bend&name=ops_quot https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64laws.bend&name=ops_rem https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64laws.bend&name=tests_is_zero https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/generic.bend&name=lift_qr https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/generic.bend&name=u64_of https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/generic.bend&name=QuotRem https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/generic.bend&name=divmod_ok https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/instances.bend&name=u64_is https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/instances.bend&name=u64_op https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/natural.bend&name=divmod https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/num.bend&name=NumError https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/num.bend&name=Op https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/num.bend&name=Test https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/u64.bend&name=U64