def sim_dbl

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u64bgcd.bend:93

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/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/instances.bend as I
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64laws.bend as UL
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/bgcdnat.bend as BN

93def sim_dbl(c: Nat, +x: WU.U64, +hfit: {C.fits(64n, BN.ndbl(c, v(x))) == True{} : Bool}) -> {v(G.dbl(~WU.U64, ~I.u64_op, c, x)) == BN.ndbl(c, v(x)) : Nat}:
94  match c:
95    case 0n:
96      {==}
97    case 1n+ +k:
98      +hf2 = fits_mono(Nat.add(v(x), v(x)), BN.ndbl(k, Nat.add(v(x), v(x))), ndbl_ge(k, Nat.add(v(x), v(x))), hfit)
99      +hno = Equal.trans(Bool, I.u64_is(NM.AddOver{x, x}), Bool.not(C.fits(64n, Nat.add(v(x), v(x)))), False{}, UL.tests_add_over(x, x), Equal.cong(Bool, Bool, t => Bool.not(t), C.fits(64n, Nat.add(v(x), v(x))), True{}, hf2))
100      +s = I.u64_op(NM.Add{x, x})
101      +hfit2 = Equal.trans(Bool, C.fits(64n, BN.ndbl(k, v(s))), C.fits(64n, BN.ndbl(k, Nat.add(v(x), v(x)))), True{}, Equal.cong(Nat, Bool, t => C.fits(64n, BN.ndbl(k, t)), v(s), Nat.add(v(x), v(x)), UL.ops_add(x, x, hno)), hfit)
102      Equal.trans(Nat, v(G.dbl(~WU.U64, ~I.u64_op, k, s)), BN.ndbl(k, v(s)), BN.ndbl(k, Nat.add(v(x), v(x))), sim_dbl(k, s, hfit2), Equal.cong(Nat, Nat, t => BN.ndbl(k, t), v(s), Nat.add(v(x), v(x)), UL.ops_add(x, x, hno)))