def ilog_stop

bend-collections-laws-math@1.0.0.0 · proofs/math/natural/logs.bend:37

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/proofs/lib/lemmas/proofs/nat_algebra.bend as A

37# the loop stops at k: b^k == p <= n < p b
38def ilog_stop(+n: Nat, +bq: Nat, +k: Nat, +p: Nat, +hp: {p == Nat.pow(2n+bq, k) : Nat}, +hpn: {Nat.is_le(p, n) == True{} : Bool}, +hu: {False{} == Nat.is_le(Nat.mul(p, 2n+bq), n) : Bool}) -> {Nat.is_le(Nat.pow(2n+bq, k), n) == True{} : Bool} & {Nat.is_lt(n, Nat.pow(2n+bq, 1n+k)) == True{} : Bool}:
39  +b = {2n+bq : Nat}
40  +lt = N.not_le_lt(Nat.mul(p, b), n, Equal.sym(Bool, False{}, Nat.is_le(Nat.mul(p, b), n), hu))
41  (Equal.trans(Bool, Nat.is_le(Nat.pow(b, k), n), Nat.is_le(p, n), True{}, Equal.cong(Nat, Bool, z => Nat.is_le(z, n), Nat.pow(b, k), p, Equal.sym(Nat, p, Nat.pow(b, k), hp)), hpn),
42   Equal.trans(Bool, Nat.is_lt(n, Nat.mul(b, Nat.pow(b, k))), Nat.is_lt(n, Nat.mul(p, b)), True{}, Equal.cong(Nat, Bool, z => Nat.is_lt(n, z), Nat.mul(b, Nat.pow(b, k)), Nat.mul(p, b), Equal.trans(Nat, Nat.mul(b, Nat.pow(b, k)), Nat.mul(b, p), Nat.mul(p, b), Equal.cong(Nat, Nat, z => Nat.mul(b, z), Nat.pow(b, k), p, Equal.sym(Nat, p, Nat.pow(b, k), hp)), A.mul_comm(b, p))), lt))