def gcd_sim

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

import Base
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

159def 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)))