def dm

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32int.bend:59

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/u32laws.bend as LW

59def 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<U32>>}:
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<U32>>}, 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<U32>>}, 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<U32>>}
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<U32>>}
75      {==}