def up

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64sqrt.bend:180

import Base
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/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend as U
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD

180def up(+fu: Nat, +one: Nat, +h1: {one == 1n : Nat}, +x: U32, +r: U32, +m: U32, +pm: {m == U32{WD.mask(32n, 16n)} : U32}, +hf: {Nat.is_lt(Nat.sub(v(m), v(r)), fu) == True{} : Bool}, +hle: {Nat.is_le(v(r), v(m)) == True{} : Bool}, +hs: {Nat.is_le(sq(v(r)), v(x)) == True{} : Bool}, +ub: Bool, +hub: {up_okg(x, r, m) == ub : Bool}) -> {Nat.is_le(sq(v(up32g(fu, x, r, ub, m))), v(x)) == True{} : Bool} & {Nat.is_lt(v(x), sq(1n+v(up32g(fu, x, r, ub, m)))) == True{} : Bool}:
181  match fu:
182    case 0n:
183      Empty.absurd({Nat.is_le(sq(v(up32g(0n, x, r, ub, m))), v(x)) == True{} : Bool} & {Nat.is_lt(v(x), sq(1n+v(up32g(0n, x, r, ub, m)))) == True{} : Bool}, N.lt_zero_absurd(Nat.sub(v(m), v(r)), hf))
184    case 1n+ +g:
185      match ub:
186        case False{}:
187          (hs, up_stop(one, h1, x, r, m, pm, hle, U32.is_le(U32.mul(U32.add(r, 1), U32.add(r, 1)), x), {==}, U32.is_lt(r, m), {==}, hub))
188        case True{}:
189          +r1 = U32.add(r, 1)
190          +ha = and_l(U32.is_lt(r, m), U32.is_le(U32.mul(r1, r1), x), hub)
191          +hb = and_r(U32.is_lt(r, m), U32.is_le(U32.mul(r1, r1), x), hub)
192          +lt = Equal.trans(Bool, Nat.is_lt(v(r), v(m)), U32.is_lt(r, m), True{}, Equal.sym(Bool, U32.is_lt(r, m), Nat.is_lt(v(r), v(m)), U.is_lt_nat(r, m)), ha)
193          +e1 = succ_v(one, h1, r, m, pm, lt)
194          +em = m16(one, h1, m, pm)
195          +bs1 = L.subst(Nat, z => {Nat.is_lt(z, WD.sc(16n, one)) == True{} : Bool}, 1n+v(r), v(r1), Equal.sym(Nat, v(r1), 1n+v(r), e1), N.le_lt_trans(1n+v(r), v(m), WD.sc(16n, one), lt_to_le(v(r), v(m), lt), L.subst(Nat, z => {Nat.is_lt(v(m), z) == True{} : Bool}, 1n+v(m), WD.sc(16n, one), em, N.lt_succ(v(m)))))
196          +esq = sq_exact(one, h1, r1, bs1)
197          +hs1 = L.subst(Nat, z => {Nat.is_le(z, v(x)) == True{} : Bool}, v(U32.mul(r1, r1)), sq(v(r1)), esq, Equal.trans(Bool, Nat.is_le(v(U32.mul(r1, r1)), v(x)), U32.is_le(U32.mul(r1, r1), x), True{}, Equal.sym(Bool, U32.is_le(U32.mul(r1, r1), x), Nat.is_le(v(U32.mul(r1, r1)), v(x)), is_le_nat(U32.mul(r1, r1), x)), hb))
198          +hle1 = L.subst(Nat, z => {Nat.is_le(z, v(m)) == True{} : Bool}, 1n+v(r), v(r1), Equal.sym(Nat, v(r1), 1n+v(r), e1), lt_to_le(v(r), v(m), lt))
199          +hf0 = L.subst(Nat, z => {Nat.is_lt(z, 1n+g) == True{} : Bool}, Nat.sub(v(m), v(r)), 1n+Nat.sub(v(m), 1n+v(r)), sub_succ_r(v(r), v(m), lt), hf)
200          +hf1 = L.subst(Nat, z => {Nat.is_lt(Nat.sub(v(m), z), g) == True{} : Bool}, 1n+v(r), v(r1), Equal.sym(Nat, v(r1), 1n+v(r), e1), hf0)
201          up(g, one, h1, x, r1, m, pm, hf1, hle1, hs1, up_okg(x, r1, m), {==})