def lcmc

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

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
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/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW

244def 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), {==})