def ba.adv2

bend-osdev-algo@0.1.0.0 · PROOF.bend:1298

import Base
import bend-osdev-algo@0.1.0.0/proof_u32.bend as U
import bend-osdev-algo@0.1.0.0/proof_bsearch.bend as Q

1298# one halving, with the element at mid below the key (b) or not
1299def ba.adv2(b: Bool, +g: Nat, +d: Nat, +l: List<&2, U32>, +key: U32, +n: U32, +lo: U32, +hi: U32, +eb: {Nat.is_lt(Q.bq.m(lo, hi), Q.bq.lb(l, n, key)) == b : Bool}, +i1: {Nat.is_le(U32.to_nat(lo), Q.bq.lb(l, n, key)) == True{} : Bool}, +i2: {Nat.is_le(Q.bq.lb(l, n, key), U32.to_nat(hi)) == True{} : Bool}, +i3: {Nat.is_le(U32.to_nat(hi), U32.to_nat(n)) == True{} : Bool}, +hz: {Nat.is_lt(Q.bq.s(lo, hi), U.uq.pw(1n+g)) == True{} : Bool}, +eM: {U32.to_nat(Q.bq.mid(lo, hi)) == Q.bq.m(lo, hi) : Nat}, +ehs: {Nat.add(U32.to_nat(lo), Q.bq.s(lo, hi)) == U32.to_nat(hi) : Nat}, +hmh: {Nat.is_lt(Q.bq.m(lo, hi), U32.to_nat(hi)) == True{} : Bool}, ih: @lo2: U32 -> @hi2: U32 -> @j1: {Nat.is_le(U32.to_nat(lo2), Q.bq.lb(l, n, key)) == True{} : Bool} -> @j2: {Nat.is_le(Q.bq.lb(l, n, key), U32.to_nat(hi2)) == True{} : Bool} -> @j3: {Nat.is_le(U32.to_nat(hi2), U32.to_nat(n)) == True{} : Bool} -> @jz: {Nat.is_lt(Q.bq.s(lo2, hi2), U.uq.pw(g)) == True{} : Bool} -> {U32.to_nat(Q.bq.run(g, d, l, lo2, hi2, key)) == Q.bq.lb(l, n, key) : Nat}) -> {U32.to_nat(Q.bq.run(g, d, l, Q.bq.lo_b(b, lo, Q.bq.mid(lo, hi)), Q.bq.hi_b(b, hi, Q.bq.mid(lo, hi)), key)) == Q.bq.lb(l, n, key) : Nat}:
1300  match b:
1301    case True{}:
1302      +h0 = U32.to_nat(hi)
1303      +l0 = U32.to_nat(lo)
1304      +s = Q.bq.s(lo, hi)
1305      +m = Q.bq.m(lo, hi)
1306      +mid = Q.bq.mid(lo, hi)
1307      +lb = Q.bq.lb(l, n, key)
1308      +hinc = Q.bq.le_rw(1n+m, h0, 1n+U32.to_nat(mid), h0, U.uq.succ_cong(m, U32.to_nat(mid), Equal.sym(Nat, U32.to_nat(mid), m, eM)), {==}, Equal.trans(Bool, Nat.is_le(1n+m, h0), Nat.is_lt(m, h0), True{}, U.uq.le_succ(m, h0), hmh))
1309      +eI = Equal.trans(Nat, U32.to_nat(U32.inc(mid)), 1n+U32.to_nat(mid), 1n+m, U.uq.u32_inc(mid, hi, hinc), U.uq.succ_cong(U32.to_nat(mid), m, eM))
1310      +j1 = Q.bq.le_rw(1n+m, lb, U32.to_nat(U32.inc(mid)), lb, Equal.sym(Nat, U32.to_nat(U32.inc(mid)), 1n+m, eI), {==}, Equal.trans(Bool, Nat.is_le(1n+m, lb), Nat.is_lt(m, lb), True{}, U.uq.le_succ(m, lb), eb))
1311      +jz = Q.bq.lt_rw(Nat.sub(s, 1n+U.uq.half(s)), U.uq.pw(g), Q.bq.s(U32.inc(mid), hi), U.uq.pw(g), ba.jz_eq(lo, hi, eI, ehs), {==}, Q.bq.hr_lt_pw(s, U.uq.pw(g), hz))
1312      ih(U32.inc(mid), hi, j1, i2, i3, jz)
1313    case False{}:
1314      +h0 = U32.to_nat(hi)
1315      +l0 = U32.to_nat(lo)
1316      +s = Q.bq.s(lo, hi)
1317      +m = Q.bq.m(lo, hi)
1318      +mid = Q.bq.mid(lo, hi)
1319      +lb = Q.bq.lb(l, n, key)
1320      +j2 = Q.bq.le_rw(lb, m, lb, U32.to_nat(mid), {==}, Equal.sym(Nat, U32.to_nat(mid), m, eM), Q.bq.not_lt(m, lb, eb))
1321      +j3 = Q.bq.le_rw(m, U32.to_nat(n), U32.to_nat(mid), U32.to_nat(n), Equal.sym(Nat, U32.to_nat(mid), m, eM), {==}, Q.bq.le_trans(m, h0, U32.to_nat(n), Q.bq.lt_le(m, h0, hmh), i3))
1322      +e2 = Equal.trans(Nat, U.uq.half(s), Nat.sub(Nat.add(l0, U.uq.half(s)), l0), Nat.sub(U32.to_nat(mid), l0), Equal.sym(Nat, Nat.sub(Nat.add(l0, U.uq.half(s)), l0), U.uq.half(s), U.uq.sub_add_l(l0, U.uq.half(s))), Equal.cong(Nat, Nat, z => Nat.sub(z, l0), m, U32.to_nat(mid), Equal.sym(Nat, U32.to_nat(mid), m, eM)))
1323      +jz = Q.bq.lt_rw(U.uq.half(s), U.uq.pw(g), Q.bq.s(lo, mid), U.uq.pw(g), e2, {==}, Q.bq.half_lt_pw(s, U.uq.pw(g), hz))
1324      ih(lo, mid, i1, j2, j3, jz)