def srch

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32int.bend:1150

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/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/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as NR
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natfuel.bend as NF
import bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend as AR2
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/roots.bend as RT

1150def srch(+f: Nat, +n: U32, +k: Nat, +lo: U32, +hi: U32, +m: U32, +more: Bool, +hit: Bool, +j: Nat, +nlo: Nat, +w: Nat, +R: Nat, +K: Nat, +hK: {K == 32n : Nat}, +hlo: {v(lo) == nlo : Nat}, +hhi: {v(hi) == Nat.add(nlo, w) : Nat}, +hm: {v(m) == Nat.add(nlo, Nat.div(w, 2n)) : Nat}, +hR1: {Nat.is_le(Nat.pow(R, k), v(n)) == True{} : Bool}, +hR2: {Nat.is_lt(v(n), Nat.pow(1n+R, k)) == True{} : Bool}, +hl: {Nat.is_le(nlo, R) == True{} : Bool}, +hr: {Nat.is_lt(R, Nat.add(nlo, w)) == True{} : Bool}, +hmore: {more == Nat.is_lt(1n, w) : Bool}, +hhit: {hit == Nat.is_le(Nat.pow(Nat.add(nlo, Nat.div(w, 2n)), k), v(n)) : Bool}, +hw: {Nat.is_le(w, C.pow2(j)) == True{} : Bool}, +hf: {Nat.is_le(1n+j, f) == True{} : Bool}) -> {v(G.search_go(~U32, ~I.u32_op, ~I.u32_is, f, n, k, lo, hi, m, more, hit)) == R : Nat}:
1151  match f more hit j:
1152    case 0n _ _ _:
1153      Empty.absurd({v(G.search_go(~U32, ~I.u32_op, ~I.u32_is, 0n, n, k, lo, hi, m, more, hit)) == R : Nat}, true_ne_false(Equal.sym(Bool, False{}, True{}, hf)))
1154    case 1n+g False{} _ _:
1155      +hw1 = N.not_lt_le(1n, w, Equal.sym(Bool, False{}, Nat.is_lt(1n, w), hmore))
1156      +h1 = L.subst(Nat, z => {Nat.is_le(Nat.add(nlo, w), z) == True{} : Bool}, Nat.add(nlo, 1n), 1n+nlo, plus1(nlo), N.le_add_left(w, 1n, nlo, hw1))
1157      +hrl = N.lt_succ_le(R, nlo, N.lt_le_trans(R, Nat.add(nlo, w), 1n+nlo, hr, h1))
1158      Equal.trans(Nat, v(lo), nlo, R, hlo, N.le_antisym(nlo, R, hl, hrl))
1159    case 1n+g True{} _ 0n:
1160      Empty.absurd({v(G.search_go(~U32, ~I.u32_op, ~I.u32_is, 1n+g, n, k, lo, hi, m, True{}, hit)) == R : Nat}, true_ne_false(Equal.trans(Bool, True{}, Nat.is_lt(1n, w), False{}, hmore, N.le_not_lt(1n, w, hw))))
1161    case 1n+ +g True{} True{} 1n+ +jp:
1162      +q = Nat.div(w, 2n)
1163      +X = Nat.add(nlo, q)
1164      +w2 = Nat.sub(w, q)
1165      +hqw = Equal.trans(Nat, Nat.add(q, w2), w, w, N.sub_add(w, q, AR2.div_le(w, 2n)), {==})
1166      +ehi = Equal.trans(Nat, Nat.add(X, w2), Nat.add(nlo, Nat.add(q, w2)), Nat.add(nlo, w), N.add_assoc(nlo, q, w2), Equal.cong(Nat, Nat, t => Nat.add(nlo, t), Nat.add(q, w2), w, hqw))
1167      +hhi2 = Equal.trans(Nat, v(hi), Nat.add(nlo, w), Nat.add(X, w2), hhi, Equal.sym(Nat, Nat.add(X, w2), Nat.add(nlo, w), ehi))
1168      +hw0 = N.lt_trans(0n, 1n, w, {==}, Equal.sym(Bool, True{}, Nat.is_lt(1n, w), hmore))
1169      +hdw = L.subst(Nat, z => {Nat.is_lt(w, z) == True{} : Bool}, Nat.add(w, w), Nat.double(w), Equal.sym(Nat, Nat.double(w), Nat.add(w, w), NA.double_self(w)), lt_add_r(w, w, hw0))
1170      +hpos = RT.sub_pos(q, w, NF.half_below(w, w, hdw))
1171      +m2 = G.imid(~U32, ~I.u32_op, m, hi)
1172      +hm2 = imid_v(K, hK, m, hi, X, w2, hm, hhi2)
1173      +hmore2 = more_v(K, hK, m, hi, X, w2, hm, hhi2, hpos)
1174      +hhit2 = Equal.trans(Bool, G.root_le(~U32, ~I.u32_op, ~I.u32_is, n, k, m2), Nat.is_le(Nat.pow(v(m2), k), v(n)), Nat.is_le(Nat.pow(Nat.add(X, Nat.div(w2, 2n)), k), v(n)), rl_v(K, hK, n, k, m2), Equal.cong(Nat, Bool, t => Nat.is_le(Nat.pow(t, k), v(n)), v(m2), Nat.add(X, Nat.div(w2, 2n)), hm2))
1175      +hl2 = NF.root_below(R, X, k, v(n), Equal.sym(Bool, True{}, Nat.is_le(Nat.pow(X, k), v(n)), hhit), hR2)
1176      +hr2 = L.subst(Nat, z => {Nat.is_lt(R, z) == True{} : Bool}, Nat.add(nlo, w), Nat.add(X, w2), Equal.sym(Nat, Nat.add(X, w2), Nat.add(nlo, w), ehi), hr)
1177      +hw3 = NF.w_hi(w, C.pow2(jp), hw)
1178      srch(g, n, k, m, hi, m2, I.u32_is(NM.Lt{G.inc(~U32, ~I.u32_op, m), hi}), G.root_le(~U32, ~I.u32_op, ~I.u32_is, n, k, m2), jp, X, w2, R, K, hK, hm, hhi2, hm2, hR1, hR2, hl2, hr2, Equal.sym(Bool, Nat.is_lt(1n, w2), I.u32_is(NM.Lt{G.inc(~U32, ~I.u32_op, m), hi}), Equal.sym(Bool, I.u32_is(NM.Lt{G.inc(~U32, ~I.u32_op, m), hi}), Nat.is_lt(1n, w2), hmore2)), hhit2, hw3, hf)
1179    case 1n+ +g True{} False{} 1n+ +jp:
1180      +q = Nat.div(w, 2n)
1181      +X = Nat.add(nlo, q)
1182      +h2w = N.lt_succ_le_succ(1n, w, Equal.sym(Bool, True{}, Nat.is_lt(1n, w), hmore))
1183      +hq1 = Equal.trans(Bool, Nat.is_le(1n, q), Nat.is_le(Nat.mul(1n, 2n), w), True{}, NR.le_div(1n, 1n, w), h2w)
1184      +hpos = pos_of(q, hq1)
1185      +m2 = G.imid(~U32, ~I.u32_op, lo, m)
1186      +hm2 = imid_v(K, hK, lo, m, nlo, q, hlo, hm)
1187      +hmore2 = more_v(K, hK, lo, m, nlo, q, hlo, hm, hpos)
1188      +hhit2 = Equal.trans(Bool, G.root_le(~U32, ~I.u32_op, ~I.u32_is, n, k, m2), Nat.is_le(Nat.pow(v(m2), k), v(n)), Nat.is_le(Nat.pow(Nat.add(nlo, Nat.div(q, 2n)), k), v(n)), rl_v(K, hK, n, k, m2), Equal.cong(Nat, Bool, t => Nat.is_le(Nat.pow(t, k), v(n)), v(m2), Nat.add(nlo, Nat.div(q, 2n)), hm2))
1189      +hr2 = NF.root_above(R, X, k, v(n), Equal.sym(Bool, False{}, Nat.is_le(Nat.pow(X, k), v(n)), hhit), hR1)
1190      +hw3 = NF.w_lo(w, C.pow2(jp), hw)
1191      srch(g, n, k, lo, m, m2, I.u32_is(NM.Lt{G.inc(~U32, ~I.u32_op, lo), m}), G.root_le(~U32, ~I.u32_op, ~I.u32_is, n, k, m2), jp, nlo, q, R, K, hK, hlo, hm, hm2, hR1, hR2, hl, hr2, Equal.sym(Bool, Nat.is_lt(1n, q), I.u32_is(NM.Lt{G.inc(~U32, ~I.u32_op, lo), m}), Equal.sym(Bool, I.u32_is(NM.Lt{G.inc(~U32, ~I.u32_op, lo), m}), Nat.is_lt(1n, q), hmore2)), hhit2, hw3, hf)