def search_ok

bend-collections-laws-math@1.0.0.0 · proofs/math/natural/roots.bend:152

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/src/math/natural.bend as M

152def search_ok(fuel: Nat, +n: Nat, +k: Nat, +lo: Nat, +hi: Nat, +more: Bool, +ok: Bool, +hlo: {M.root_le(n, k, lo) == True{} : Bool}, +hhi: {M.root_le(n, k, hi) == False{} : Bool}, +hlt: {Nat.is_lt(lo, hi) == True{} : Bool}, +hf: {Nat.is_le(Nat.sub(hi, lo), fuel) == True{} : Bool}, +hm: {more == Nat.is_lt(1n+lo, hi) : Bool}, +hok: {ok == M.root_le(n, k, M.mid(lo, hi)) : Bool}) -> root_ok(n, k, M.search_go(fuel, n, k, lo, hi, more, ok)):
153  match fuel more ok:
154    case 0n False{} False{}:
155      Empty.absurd(root_ok(n, k, M.search_go(0n, n, k, lo, hi, False{}, False{})), no_fuel(lo, hi, hlt, hf))
156    case 0n False{} True{}:
157      Empty.absurd(root_ok(n, k, M.search_go(0n, n, k, lo, hi, False{}, True{})), no_fuel(lo, hi, hlt, hf))
158    case 0n True{} False{}:
159      Empty.absurd(root_ok(n, k, M.search_go(0n, n, k, lo, hi, True{}, False{})), no_fuel(lo, hi, hlt, hf))
160    case 0n True{} True{}:
161      Empty.absurd(root_ok(n, k, M.search_go(0n, n, k, lo, hi, True{}, True{})), no_fuel(lo, hi, hlt, hf))
162    case 1n+f False{} False{}:
163      done_ok(n, k, lo, hi, hlo, hhi, hlt, hm)
164    case 1n+f False{} True{}:
165      done_ok(n, k, lo, hi, hlo, hhi, hlt, hm)
166    case 1n+ +f True{} True{}:
167      +m = M.mid(lo, hi)
168      +hml = lo_lt_mid(lo, hi, Equal.sym(Bool, True{}, Nat.is_lt(1n+lo, hi), hm))
169      +hmh = mid_lt_hi(lo, hi, hlt)
170      search_ok(f, n, k, m, hi, Nat.is_lt(1n+m, hi), M.root_le(n, k, M.mid(m, hi)), Equal.sym(Bool, True{}, M.root_le(n, k, m), hok), hhi, hmh, shrink(Nat.sub(hi, m), Nat.sub(hi, lo), f, lt_sub(hi, lo, m, hml, N.lt_le(m, hi, hmh)), hf), {==}, {==})
171    case 1n+ +f True{} False{}:
172      +m = M.mid(lo, hi)
173      +hml = lo_lt_mid(lo, hi, Equal.sym(Bool, True{}, Nat.is_lt(1n+lo, hi), hm))
174      +hmh = mid_lt_hi(lo, hi, hlt)
175      search_ok(f, n, k, lo, m, Nat.is_lt(1n+lo, m), M.root_le(n, k, M.mid(lo, m)), hlo, Equal.sym(Bool, False{}, M.root_le(n, k, m), hok), hml, shrink(Nat.sub(m, lo), Nat.sub(hi, lo), f, lt_sub2(m, hi, lo, hmh, N.lt_le(lo, m, hml)), hf), {==}, {==})