def ba.fd

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

import Base
import bend-osdev-algo@0.1.0.0/bsearch.bend as S
import bend-osdev-array@0.1.0.0/array.bend as AR
import bend-osdev-array@0.1.0.0/LAWS.bend as AL
import bend-osdev-algo@0.1.0.0/proof_bsearch.bend as Q
import bend-osdev-algo@0.1.0.0/LAWS.bend as Laws

1395def ba.fd(c: Bool, +d: Nat, +l: List<&2, U32>, +hl: {List.length(&2, U32, l) == AR.Arrays.slots(d) : Nat}, +key: U32, +n: U32, +hn: {Nat.is_le(U32.to_nat(n), AR.Arrays.slots(d)) == True{} : Bool}, +r: U32, +ec: {U32.is_lt(r, n) == c : Bool}, +er: {U32.to_nat(r) == Q.bq.lb(l, n, key) : Nat}) -> {Laws.algo_index_nat(Pair.snd(Array<U32>, Maybe<&2, U32>, S.bsearch.array.found(c, (AR.Arrays.of_list(U32, d, l, 0), AR.Arrays.nth(U32, l, AR.Arrays.index(d, r), 0)), r, key))) == S.bsearch.find(Q.bq.pre(l, n), key) : Maybe<&2, Nat>}:
1396  match c:
1397    case True{}:
1398      +lb = Q.bq.lb(l, n, key)
1399      +nn = U32.to_nat(n)
1400      +pre = Q.bq.pre(l, n)
1401      +hnl = Q.bq.le_rw(nn, AR.Arrays.slots(d), nn, List.length(&2, U32, l), {==}, Equal.sym(Nat, List.length(&2, U32, l), AR.Arrays.slots(d), hl), hn)
1402      +hc = Equal.trans(Bool, Nat.is_lt(lb, nn), Nat.is_lt(U32.to_nat(r), nn), True{}, Equal.cong(Nat, Bool, z => Nat.is_lt(z, nn), lb, U32.to_nat(r), Equal.sym(Nat, U32.to_nat(r), lb, er)), u32.mv_lt(r, n, True{}, ec))
1403      +hls = Q.bq.lt_le_trans(lb, nn, AR.Arrays.slots(d), hc, hn)
1404      +ei = Equal.trans(Nat, AR.Arrays.index(d, r), U32.to_nat(r), lb, AL.index_of_u32(d, r, Q.bq.lt_rw(lb, AR.Arrays.slots(d), U32.to_nat(r), AR.Arrays.slots(d), Equal.sym(Nat, U32.to_nat(r), lb, er), {==}, hls)), er)
1405      +hll = Q.bq.lt_rw(lb, AR.Arrays.slots(d), lb, List.length(&2, U32, l), {==}, Equal.sym(Nat, List.length(&2, U32, l), AR.Arrays.slots(d), hl), hls)
1406      +eg = Equal.trans(Maybe<&2, U32>, List.get(&2, U32, pre, lb), List.get(&2, U32, l, lb), Some{AR.Arrays.nth(U32, l, lb, 0)}, Q.bq.get_take(l, nn, lb, hc), Q.bq.get_nth(l, lb, hll))
1407      %Equal.sym(Nat, AR.Arrays.index(d, r), lb, ei) : {Laws.algo_index_nat(Pair.snd(Array<U32>, Maybe<&2, U32>, S.bsearch.array.found(True{}, (AR.Arrays.of_list(U32, d, l, 0), AR.Arrays.nth(U32, l, _, 0)), r, key))) == S.bsearch.find(pre, key) : Maybe<&2, Nat>}
1408      %Equal.sym(Maybe<&2, U32>, List.get(&2, U32, pre, lb), Some{AR.Arrays.nth(U32, l, lb, 0)}, eg) : {Laws.algo_index_nat(Pair.snd(Array<U32>, Maybe<&2, U32>, S.bsearch.array.found(True{}, (AR.Arrays.of_list(U32, d, l, 0), AR.Arrays.nth(U32, l, lb, 0)), r, key))) == S.bsearch.find.check(lb, _, key) : Maybe<&2, Nat>}
1409      ba.hit(U32.is_eq(AR.Arrays.nth(U32, l, lb, 0), key), r, lb, er)
1410    case False{}:
1411      +lb = Q.bq.lb(l, n, key)
1412      +nn = U32.to_nat(n)
1413      +pre = Q.bq.pre(l, n)
1414      +hnl = Q.bq.le_rw(nn, AR.Arrays.slots(d), nn, List.length(&2, U32, l), {==}, Equal.sym(Nat, List.length(&2, U32, l), AR.Arrays.slots(d), hl), hn)
1415      +hc = Equal.trans(Bool, Nat.is_lt(lb, nn), Nat.is_lt(U32.to_nat(r), nn), False{}, Equal.cong(Nat, Bool, z => Nat.is_lt(z, nn), lb, U32.to_nat(r), Equal.sym(Nat, U32.to_nat(r), lb, er)), u32.mv_lt(r, n, False{}, ec))
1416      +eln = Q.bq.le_antisym(lb, nn, ba.lb_le(d, l, n, key, hl, hn), Q.bq.not_lt(lb, nn, hc))
1417      +eg = Equal.trans(Maybe<&2, U32>, List.get(&2, U32, pre, lb), List.get(&2, U32, pre, List.length(&2, U32, pre)), None{}, Equal.cong(Nat, Maybe<&2, U32>, z => List.get(&2, U32, pre, z), lb, List.length(&2, U32, pre), Equal.trans(Nat, lb, nn, List.length(&2, U32, pre), eln, Equal.sym(Nat, List.length(&2, U32, pre), nn, Q.bq.len_take(l, nn, hnl)))), Q.bq.get_len(pre))
1418      %Equal.sym(Maybe<&2, U32>, List.get(&2, U32, pre, lb), None{}, eg) : {Laws.algo_index_nat(Pair.snd(Array<U32>, Maybe<&2, U32>, S.bsearch.array.found(False{}, (AR.Arrays.of_list(U32, d, l, 0), AR.Arrays.nth(U32, l, AR.Arrays.index(d, r), 0)), r, key))) == S.bsearch.find.check(lb, _, key) : Maybe<&2, Nat>}
1419      {==}