proofs/math/natural/logs.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/math/natural/logs.bend as Logs

7 imports

import Base
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/lemmas/proofs/nat_algebra.bend as A
import ../../../src/math/natural.bend as M
import ./arith.bend as R
import ./roots.bend as RT

Definitions

def le_add_r source · line 15 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+h:{Nat.is_le(a, b) == True{} : Bool} -> {Nat.is_le(Nat.add(a, c), Nat.add(b, c)) == True{} : Bool}

a <= b gives a + c <= b + c

def lt_add_pos source · line 21 · raw

@+a:Nat -> @+c:Nat -> @+h:{Nat.is_lt(0n, c) == True{} : Bool} -> {Nat.is_lt(a, Nat.add(a, c)) == True{} : Bool}

a < a + c for c > 0

def pow_gt source · line 26 · raw

@+bq:Nat -> @+k:Nat -> {Nat.is_lt(k, Nat.pow(2n+bq, k)) == True{} : Bool}

k < b^k for b >= 2

def ilog_stop source · line 38 · raw

@+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} -> Pair({Nat.is_le(Nat.pow(2n+bq, k), n) == True{} : Bool}, {Nat.is_lt(n, Nat.pow(2n+bq, 1n+k)) == True{} : Bool})

the loop stops at k: b^k == p <= n < p b

def ilog_absurd source · line 45 · raw

@+n:Nat -> @+bq:Nat -> @+k:Nat -> @+p:Nat -> @+hp:{p == Nat.pow(2n+bq, k) : Nat} -> @+hu:{True{} == Nat.is_le(Nat.mul(p, 2n+bq), n) : Bool} -> @+hf:{k == n : Nat} -> Empty

with no fuel left k == n, and p b <= n is impossible: n == k < p <= p b

def ilog_ok source · line 53 · raw

@fuel:Nat -> @+n:Nat -> @+bq:Nat -> @+k:Nat -> @+p:Nat -> @+up:Bool -> @+hp:{p == Nat.pow(2n+bq, k) : Nat} -> @+hpn:{Nat.is_le(p, n) == True{} : Bool} -> @+hup:{up == Nat.is_le(p, Nat.div(n, 2n+bq)) : Bool} -> @+hf:{Nat.add(fuel, k) == n : Nat} -> Pair({Nat.is_le(Nat.pow(2n+bq, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.ilog_go(fuel, n, 2n+bq, k, p, up)), n) == True{} : Bool}, {Nat.is_lt(n, Nat.pow(2n+bq, 1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.ilog_go(fuel, n, 2n+bq, k, p, up))) == True{} : Bool})

the loop: p == b^k <= n, up is p b <= n, fuel + k == n

def lt_two source · line 67 · raw

@+bq:Nat -> {Nat.is_lt(2n+bq, 2n) == False{} : Bool}

def ilog_value source · line 75 · raw

@+np:Nat -> @+bq:Nat -> Nat

the value ilog(n, b) returns for n >= 1, b >= 2

def ilog_done source · line 78 · raw

@+np:Nat -> @+bq:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.ilog(1n+np, 2n+bq) == Done{ilog_value(np, bq)} : Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.MathError, Nat>}

def ilog_bounds source · line 82 · raw

@+np:Nat -> @+bq:Nat -> Pair({Nat.is_le(Nat.pow(2n+bq, ilog_value(np, bq)), 1n+np) == True{} : Bool}, {Nat.is_lt(1n+np, Nat.pow(2n+bq, 1n+ilog_value(np, bq))) == True{} : Bool})

def fst_b source · line 86 · raw

@-P:Type -> @-Q:Type -> @p:Pair(P, Q) -> P

b^ilog(n, b) <= n (Mathlib Nat.pow_log_le_self)

def snd_b source · line 90 · raw

@-P:Type -> @-Q:Type -> @p:Pair(P, Q) -> Q

def pow_ilog_le source · line 94 · raw

@+np:Nat -> @+bq:Nat -> {Nat.is_le(Nat.pow(2n+bq, ilog_value(np, bq)), 1n+np) == True{} : Bool}

def lt_pow_succ_ilog source · line 98 · raw

@+np:Nat -> @+bq:Nat -> {Nat.is_lt(1n+np, Nat.pow(2n+bq, 1n+ilog_value(np, bq))) == True{} : Bool}

n < b^(ilog(n, b) + 1) (Mathlib Nat.lt_pow_succ_log_self)

def ilog_zero source · line 101 · raw

@+b:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.ilog(0n, b) == Fail{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.Domain{}} : Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.MathError, Nat>}

def or_true source · line 104 · raw

@+n:Nat -> @+b:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.ilog_ok(n, b, Bool.or(Nat.is_eq(n, 0n), True{})) == Fail{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.Domain{}} : Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.MathError, Nat>}

def ilog_small_base source · line 111 · raw

@+n:Nat -> @+b:Nat -> @+hb:{Nat.is_lt(b, 2n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.ilog(n, b) == Fail{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.Domain{}} : Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.MathError, Nat>}