def ilb

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/natfuel.bend:324

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/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

324# q < 2^K, 2^s <= p, t + s == K: the loop from p stops within t rounds
325def ilb(+t: Nat, +f: Nat, +c: Bool, +q: Nat, +bq: Nat, +s: Nat, +p: Nat, +K: Nat, +hK: {Nat.add(t, s) == K : Nat}, +hq: {Nat.is_lt(q, C.pow2(K)) == True{} : Bool}, +hs: {Nat.is_le(C.pow2(s), p) == True{} : Bool}, +ht: {Nat.is_le(t, f) == True{} : Bool}, +hc: {c == Nat.is_le(p, q) : Bool}) -> {ilends(f, q, 2n+bq, p, c) == True{} : Bool}:
326  match t f c:
327    case 0n _ True{}:
328      +hqs = L.subst(Nat, z => {Nat.is_lt(q, C.pow2(z)) == True{} : Bool}, K, s, Equal.sym(Nat, s, K, hK), hq)
329      Empty.absurd({ilends(f, q, 2n+bq, p, True{}) == True{} : Bool}, true_ne_false(Equal.trans(Bool, True{}, Nat.is_le(p, q), False{}, hc, N.lt_not_le(q, p, N.lt_le_trans(q, C.pow2(s), p, hqs, hs)))))
330    case 0n _ False{}:
331      il_false(f, q, 2n+bq, p)
332    case 1n+tp _ False{}:
333      il_false(f, q, 2n+bq, p)
334    case 1n+tp 0n True{}:
335      Empty.absurd({ilends(0n, q, 2n+bq, p, True{}) == True{} : Bool}, true_ne_false(Equal.sym(Bool, False{}, True{}, ht)))
336    case 1n+ +tp 1n+ +g True{}:
337      +hK2 = Equal.trans(Nat, Nat.add(tp, 1n+s), 1n+Nat.add(tp, s), K, NA.add_succ(tp, s), hK)
338      +hs2 = N.le_trans(Nat.double(C.pow2(s)), Nat.double(p), Nat.mul(p, 2n+bq), N.double_le(C.pow2(s), p, hs), dbl_le_mul(p, bq))
339      ilb(tp, g, Nat.is_le(Nat.mul(p, 2n+bq), q), q, bq, 1n+s, Nat.mul(p, 2n+bq), K, hK2, hq, hs2, ht, {==})