def sqg

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64sqf.bend:42

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/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqv.bend as QV
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqr.bend as QR
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqs.bend as QS
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqx.bend as QX

42# the generic even-exponent root
43def sqg(+one: Nat, +h1: {one == 1n : Nat}, +nh: WU.U64, +h62: {C.fits(62n, SW.value(nh)) == True{} : Bool}, +h60: {C.fits(60n, SW.value(nh)) == False{} : Bool}, +MX: Nat, +sa: Nat, +ci: Nat, +cs: Nat, +hnh: {SW.value(nh) == C.shift(8n, C.shift(Nat.add(sa, ci), MX)) : Nat}, +Ep: Nat, +p: Nat, +hp: {Nat.add(Nat.add(p, p), 1075n) == Nat.add(Ep, 4096n) : Nat}, +hpe: {Nat.div(Nat.sub(Nat.add(Ep, F.off()), 1075n), 2n) == p : Nat}, +EN: Nat, +hE: {Nat.add(Ep, ci) == EN : Nat}, +XX: Nat, +hEN: {Nat.add(EN, sa) == Nat.add(XX, 2171n) : Nat}, +Mq: Nat, +hMq: {C.shift(200n, Mq) == C.shift(Nat.add(200n, cs), MX) : Nat}, +Xq: Nat, +q: Nat, +hq: {Nat.add(Nat.add(q, q), cs) == XX : Nat}, +hqd: {Nat.div(Xq, 2n) == q : Nat}, +j: Nat, +hj: {Nat.add(Nat.add(j, j), Nat.add(72n, Nat.add(sa, ci))) == Nat.add(200n, cs) : Nat}) -> {F.sq_root(Nat.add(Nat.div(Nat.sub(Nat.add(Ep, F.off()), 1075n), 2n), 1048n), nh) == SF.sqrt_even(Mq, Xq) : F.F64}:
44  +hpv = Equal.cong(Nat, Nat, z => Nat.add(z, 1048n), Nat.div(Nat.sub(Nat.add(Ep, F.off()), 1075n), 2n), p, hpe)
45  +pge = N.not_lt_le(p, 1132n, p_ge(p, Ep, hp, Nat.is_lt(p, 1132n), {==}))
46  +hle = Equal.trans(Bool, Nat.is_le(Nat.add(1132n, 1048n), Nat.add(p, 1048n)), Nat.is_le(1132n, p), True{}, FR.le_cancel_r(1132n, p, 1048n), pge)
47  +hxs = Equal.trans(Nat, Nat.add(Nat.sub(Nat.add(p, 1048n), 2180n), 2180n), Nat.add(2180n, Nat.sub(Nat.add(p, 1048n), 2180n)), Nat.add(p, 1048n), NA.add_comm(Nat.sub(Nat.add(p, 1048n), 2180n), 2180n), N.sub_add(Nat.add(p, 1048n), 2180n, hle))
48  +hx = Equal.trans(Nat, Nat.add(Nat.sub(Nat.add(p, 1048n), 2180n), 2180n), Nat.add(p, 1048n), Nat.add(Nat.div(Nat.sub(Nat.add(Ep, F.off()), 1075n), 2n), 1048n), hxs, Equal.sym(Nat, Nat.add(Nat.div(Nat.sub(Nat.add(Ep, F.off()), 1075n), 2n), 1048n), Nat.add(p, 1048n), hpv))
49  +r1 = QR.sqr_root_v(one, h1, nh, h62, h60, Nat.add(Nat.div(Nat.sub(Nat.add(Ep, F.off()), 1075n), 2n), 1048n), Nat.sub(Nat.add(p, 1048n), 2180n), hx)
50  +hEs = Equal.trans(Nat, Nat.sub(Nat.add(Nat.div(Xq, 2n), 1500n), 101n), Nat.sub(Nat.add(q, 1500n), 101n), Nat.add(q, 1399n), Equal.cong(Nat, Nat, z => Nat.sub(Nat.add(z, 1500n), 101n), Nat.div(Xq, 2n), q, hqd), FR.sub_add_a(q, 1500n, 101n, {==}))
51  +g = QX.sqexp(q, p, j, Nat.sub(Nat.add(p, 1048n), 2180n), XX, EN, Ep, sa, ci, cs, hq, hp, hE, hEN, hj, hxs)
52  +hEx = Equal.trans(Nat, Nat.add(Nat.sub(Nat.add(Nat.div(Xq, 2n), 1500n), 101n), 1n+j), Nat.add(Nat.add(q, 1399n), 1n+j), Nat.sub(Nat.add(p, 1048n), 2180n), Equal.cong(Nat, Nat, z => Nat.add(z, 1n+j), Nat.sub(Nat.add(Nat.div(Xq, 2n), 1500n), 101n), Nat.add(q, 1399n), hEs), g)
53  +r2 = QS.sq_spec(one, h1, C.shift(64n, SW.value(nh)), j, QV.s62(one, h1, nh, h62, h60), Nat.sub(Nat.add(Nat.div(Xq, 2n), 1500n), 101n), Nat.sub(Nat.add(p, 1048n), 2180n), hEx)
54  +e1 = Equal.cong(Nat, Nat, z => C.shift(j, C.shift(j, C.shift(64n, z))), SW.value(nh), C.shift(8n, C.shift(Nat.add(sa, ci), MX)), hnh)
55  +e2 = shift_nest(j, Nat.add(sa, ci), MX)
56  +e3 = Equal.cong(Nat, Nat, z => C.shift(z, MX), Nat.add(Nat.add(j, j), Nat.add(72n, Nat.add(sa, ci))), Nat.add(200n, cs), hj)
57  +eN = Equal.trans(Nat, C.shift(j, C.shift(j, C.shift(64n, SW.value(nh)))), C.shift(j, C.shift(j, C.shift(64n, C.shift(8n, C.shift(Nat.add(sa, ci), MX))))), C.shift(Nat.add(200n, cs), MX), e1, Equal.trans(Nat, C.shift(j, C.shift(j, C.shift(64n, C.shift(8n, C.shift(Nat.add(sa, ci), MX))))), C.shift(Nat.add(Nat.add(j, j), Nat.add(72n, Nat.add(sa, ci))), MX), C.shift(Nat.add(200n, cs), MX), e2, e3))
58  +eNs = Equal.trans(Nat, C.shift(200n, Mq), C.shift(Nat.add(200n, cs), MX), C.shift(j, C.shift(j, C.shift(64n, SW.value(nh)))), hMq, Equal.sym(Nat, C.shift(j, C.shift(j, C.shift(64n, SW.value(nh)))), C.shift(Nat.add(200n, cs), MX), eN))
59  +r3 = Equal.cong(Nat, F.F64, z => SF.round(False{}, Nat.add(Nat.mul(2n, M.isqrt(z)), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(z), 2n), z)))), Nat.sub(Nat.add(Nat.div(Xq, 2n), 1500n), 101n)), C.shift(200n, Mq), C.shift(j, C.shift(j, C.shift(64n, SW.value(nh)))), eNs)
60  Equal.trans(F.F64, F.sq_root(Nat.add(Nat.div(Nat.sub(Nat.add(Ep, F.off()), 1075n), 2n), 1048n), nh), SF.round(False{}, SW.jam(M.isqrt(C.shift(64n, SW.value(nh))), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(C.shift(64n, SW.value(nh))), M.isqrt(C.shift(64n, SW.value(nh)))), C.shift(64n, SW.value(nh)))))), Nat.sub(Nat.add(p, 1048n), 2180n)), SF.round(False{}, Nat.add(Nat.mul(2n, M.isqrt(C.shift(200n, Mq))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(200n, Mq)), 2n), C.shift(200n, Mq))))), Nat.sub(Nat.add(Nat.div(Xq, 2n), 1500n), 101n)), r1, Equal.trans(F.F64, SF.round(False{}, SW.jam(M.isqrt(C.shift(64n, SW.value(nh))), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(C.shift(64n, SW.value(nh))), M.isqrt(C.shift(64n, SW.value(nh)))), C.shift(64n, SW.value(nh)))))), Nat.sub(Nat.add(p, 1048n), 2180n)), SF.round(False{}, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, C.shift(64n, SW.value(nh)))))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, C.shift(64n, SW.value(nh))))), 2n), C.shift(j, C.shift(j, C.shift(64n, SW.value(nh)))))))), Nat.sub(Nat.add(Nat.div(Xq, 2n), 1500n), 101n)), SF.round(False{}, Nat.add(Nat.mul(2n, M.isqrt(C.shift(200n, Mq))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(200n, Mq)), 2n), C.shift(200n, Mq))))), Nat.sub(Nat.add(Nat.div(Xq, 2n), 1500n), 101n)), Equal.sym(F.F64, SF.round(False{}, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, C.shift(64n, SW.value(nh)))))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, C.shift(64n, SW.value(nh))))), 2n), C.shift(j, C.shift(j, C.shift(64n, SW.value(nh)))))))), Nat.sub(Nat.add(Nat.div(Xq, 2n), 1500n), 101n)), SF.round(False{}, SW.jam(M.isqrt(C.shift(64n, SW.value(nh))), SF.b2n(Bool.not(Nat.is_eq(Nat.mul(M.isqrt(C.shift(64n, SW.value(nh))), M.isqrt(C.shift(64n, SW.value(nh)))), C.shift(64n, SW.value(nh)))))), Nat.sub(Nat.add(p, 1048n), 2180n)), r2), Equal.sym(F.F64, SF.round(False{}, Nat.add(Nat.mul(2n, M.isqrt(C.shift(200n, Mq))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(200n, Mq)), 2n), C.shift(200n, Mq))))), Nat.sub(Nat.add(Nat.div(Xq, 2n), 1500n), 101n)), SF.round(False{}, Nat.add(Nat.mul(2n, M.isqrt(C.shift(j, C.shift(j, C.shift(64n, SW.value(nh)))))), SF.b2n(Bool.not(Nat.is_eq(Nat.pow(M.isqrt(C.shift(j, C.shift(j, C.shift(64n, SW.value(nh))))), 2n), C.shift(j, C.shift(j, C.shift(64n, SW.value(nh)))))))), Nat.sub(Nat.add(Nat.div(Xq, 2n), 1500n), 101n)), r3)))