def gcd_sim

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u64int.bend:161

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/u64laws.bend as LW
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU

161def gcd_sim(+f: Nat, +a: WU.U64, +b: WU.U64, +cz: Bool, +nb: Nat, +hcz: {I.u64_is(NM.IsZero{b}) == cz : Bool}, +hnb: {v(b) == nb : Nat}) -> {v(G.gcd_go(~WU.U64, ~I.u64_op, ~I.u64_is, f, a, (b, cz))) == M.gcd_go(f, v(a), nb) : Nat}:
162  match f cz nb:
163    case 0n _ _:
164      {==}
165    case 1n+g True{} 0n:
166      {==}
167    case 1n+g True{} 1n+bp:
168      +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{}, hcz), 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)))
169      Empty.absurd({v(G.gcd_go(~WU.U64, ~I.u64_op, ~I.u64_is, 1n+g, a, (b, True{}))) == M.gcd_go(1n+g, v(a), 1n+bp) : Nat}, true_ne_false(hz))
170    case 1n+g False{} 0n:
171      +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{}, hcz), 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)))
172      Empty.absurd({v(G.gcd_go(~WU.U64, ~I.u64_op, ~I.u64_is, 1n+g, a, (b, False{}))) == M.gcd_go(1n+g, v(a), 0n) : Nat}, true_ne_false(Equal.sym(Bool, False{}, True{}, hz)))
173    case 1n+ +g False{} 1n+ +bp:
174      +rm = I.u64_op(NM.Rem{a, b})
175      +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), {==})
176      +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))
177      +ih = gcd_sim(g, b, rm, I.u64_is(NM.IsZero{rm}), v(rm), {==}, {==})
178      Equal.trans(Nat, v(G.gcd_go(~WU.U64, ~I.u64_op, ~I.u64_is, g, b, (rm, I.u64_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)))