def up_stop

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

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/u32div.bend as UD
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend as AR
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/u64/u64div.bend as PD
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mul.bend as WM

126# where the up loop stops, x < (r + 1)^2
127def up_stop(+one: Nat, +h1: {one == 1n : Nat}, +x: U32, +r: U32, +m: U32, +pm: {m == U32{WD.mask(32n, 16n)} : U32}, +hle: {Nat.is_le(v(r), v(m)) == True{} : Bool}, +b: Bool, +hb2: {U32.is_le(U32.mul(U32.add(r, 1), U32.add(r, 1)), x) == b : Bool}, +a: Bool, +ha: {U32.is_lt(r, m) == a : Bool}, +hstop: {Bool.and(a, b) == False{} : Bool}) -> {Nat.is_lt(v(x), sq(1n+v(r))) == True{} : Bool}:
128  match a:
129    case False{}:
130      +em = m16(one, h1, m, pm)
131      +nl = Equal.trans(Bool, Nat.is_lt(v(r), v(m)), U32.is_lt(r, m), False{}, Equal.sym(Bool, U32.is_lt(r, m), Nat.is_lt(v(r), v(m)), U.is_lt_nat(r, m)), ha)
132      +er = N.le_antisym(v(r), v(m), hle, N.not_lt_le(v(r), v(m), nl))
133      +e1 = Equal.trans(Nat, 1n+v(r), 1n+v(m), WD.sc(16n, one), N.succ_cong(v(r), v(m), er), em)
134      +ex = L.subst(Nat, z => {Nat.is_lt(v(x), z) == True{} : Bool}, WD.sc(32n, one), sq(1n+v(r)), Equal.sym(Nat, sq(1n+v(r)), WD.sc(32n, one), Equal.trans(Nat, sq(1n+v(r)), Nat.mul(WD.sc(16n, one), WD.sc(16n, one)), WD.sc(32n, one), Equal.trans(Nat, sq(1n+v(r)), Nat.mul(WD.sc(16n, one), 1n+v(r)), Nat.mul(WD.sc(16n, one), WD.sc(16n, one)), Equal.cong(Nat, Nat, t => Nat.mul(t, 1n+v(r)), 1n+v(r), WD.sc(16n, one), e1), Equal.cong(Nat, Nat, t => Nat.mul(WD.sc(16n, one), t), 1n+v(r), WD.sc(16n, one), e1)), WM.sq_sc(16n, one, h1))), UD.vb(one, h1, x))
135      ex
136    case True{}:
137      +em = m16(one, h1, m, pm)
138      +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)
139      +b16 = N.lt_le_trans(v(r), v(m), WD.sc(16n, one), lt, N.lt_le(v(m), WD.sc(16n, one), 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)))))
140      +r1 = U32.add(r, 1)
141      +bs = 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))))
142      +a1 = Equal.trans(Nat, Nat.add(v(r), 1n), 1n+Nat.add(v(r), 0n), 1n+v(r), NA.add_succ(v(r), 0n), N.succ_cong(Nat.add(v(r), 0n), v(r), N.add_zero(v(r))))
143      +lt32 = N.lt_le_trans(Nat.add(v(r), 1n), WD.sc(16n, one), WD.sc(32n, one), L.subst(Nat, z => {Nat.is_lt(z, WD.sc(16n, one)) == True{} : Bool}, 1n+v(r), Nat.add(v(r), 1n), Equal.sym(Nat, Nat.add(v(r), 1n), 1n+v(r), a1), bs), AR.le_sc(16n, WD.sc(16n, one)))
144      +e1 = Equal.trans(Nat, v(r1), Nat.add(v(r), 1n), 1n+v(r), PD.add32(one, h1, r, 1, lt32), a1)
145      +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), bs)
146      +esq = Equal.trans(Nat, v(U32.mul(r1, r1)), sq(v(r1)), sq(1n+v(r)), sq_exact(one, h1, r1, bs1), Equal.cong(Nat, Nat, t => sq(t), v(r1), 1n+v(r), e1))
147      +nb = Equal.trans(Bool, Nat.is_le(sq(1n+v(r)), v(x)), U32.is_le(U32.mul(r1, r1), x), False{}, Equal.sym(Bool, U32.is_le(U32.mul(r1, r1), x), Nat.is_le(sq(1n+v(r)), v(x)), L.subst(Nat, z => {U32.is_le(U32.mul(r1, r1), x) == Nat.is_le(z, v(x)) : Bool}, v(U32.mul(r1, r1)), sq(1n+v(r)), esq, is_le_nat(U32.mul(r1, r1), x))), Equal.trans(Bool, U32.is_le(U32.mul(r1, r1), x), b, False{}, hb2, hstop))
148      N.not_le_lt(sq(1n+v(r)), v(x), nb)