proofs/lib/arith.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend as Arith

7 imports

import Base
import ./lemmas/spec/numeric.bend as S
import ./nat.bend as N
import ./logic.bend as L
import ./u32alg.bend as A
import ./lemmas/proofs/nat_algebra.bend as NA
import ./lemmas/proofs/natural_products.bend as PR

Definitions

def sc source · line 13 · raw

@+n:Nat -> @+k:Nat -> Nat

def mul_sc source · line 16 · raw

@+k:Nat -> @+x:Nat -> {Nat.mul(x, sc(k, 1n)) == sc(k, x) : Nat}

def mul_sc1 source · line 23 · raw

@+k:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:Nat -> {Nat.mul(x, sc(k, one)) == sc(k, x) : Nat}

def sc_mul source · line 26 · raw

@+k:Nat -> @+q:Nat -> @+d:Nat -> {sc(k, Nat.mul(q, d)) == Nat.mul(sc(k, q), d) : Nat}

def sc_le source · line 33 · raw

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

def sc_lt source · line 40 · raw

@+k:Nat -> @+a:Nat -> @+b:Nat -> @+h:{Nat.is_lt(a, b) == True{} : Bool} -> {Nat.is_lt(sc(k, a), sc(k, b)) == True{} : Bool}

def sc_lt_cancel_g source · line 47 · raw

@+k:Nat -> @+a:Nat -> @+b:Nat -> @+c:Bool -> @+hc:{Nat.is_lt(a, b) == c : Bool} -> @+h:{Nat.is_lt(sc(k, a), sc(k, b)) == True{} : Bool} -> {Nat.is_lt(a, b) == True{} : Bool}

def sc_lt_cancel source · line 54 · raw

@+k:Nat -> @+a:Nat -> @+b:Nat -> @+h:{Nat.is_lt(sc(k, a), sc(k, b)) == True{} : Bool} -> {Nat.is_lt(a, b) == True{} : Bool}

def le_sc source · line 57 · raw

@+k:Nat -> @+x:Nat -> {Nat.is_le(x, sc(k, x)) == True{} : Bool}

def digit_lt source · line 65 · raw

@+k:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:Nat -> @+y:Nat -> @+b:Nat -> @+hx:{Nat.is_lt(x, sc(k, one)) == True{} : Bool} -> @+hy:{Nat.is_lt(y, b) == True{} : Bool} -> {Nat.is_lt(Nat.add(sc(k, y), x), sc(k, b)) == True{} : Bool}

a digit x below 2^k after y < b scaled by 2^k stays below b scaled

def mul_le source · line 72 · raw

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

def one_mul source · line 78 · raw

@+d:Nat -> {Nat.mul(1n, d) == d : Nat}

def quot_lt_g source · line 81 · raw

@+k:Nat -> @+q:Nat -> @+d:Nat -> @+r:Nat -> @+c:Bool -> @+hc:{Nat.is_lt(q, sc(k, 1n)) == c : Bool} -> @+h:{Nat.is_lt(Nat.add(Nat.mul(q, d), r), sc(k, d)) == True{} : Bool} -> {Nat.is_lt(q, sc(k, 1n)) == True{} : Bool}

def quot_lt source · line 93 · raw

@+k:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+q:Nat -> @+d:Nat -> @+r:Nat -> @+h:{Nat.is_lt(Nat.add(Nat.mul(q, d), r), sc(k, d)) == True{} : Bool} -> {Nat.is_lt(q, sc(k, one)) == True{} : Bool}

q d + r < 2^k d forces q < 2^k

def step source · line 98 · raw

@+k:Nat -> @+q:Nat -> @+r:Nat -> @+d:Nat -> @+y:Nat -> @+q2:Nat -> @+r2:Nat -> @+x:Nat -> @+hx:{x == Nat.add(Nat.mul(q, d), r) : Nat} -> @+h2:{Nat.add(sc(k, r), y) == Nat.add(Nat.mul(q2, d), r2) : Nat} -> {Nat.add(sc(k, x), y) == Nat.add(Nat.mul(Nat.add(sc(k, q), q2), d), r2) : Nat}

one long-division step: if x == q d + r and 2^k r + y == q2 d + r2 then 2^k x + y == (2^k q + q2) d + r2

def go_le source · line 108 · raw

@+n:Nat -> @+m:Nat -> @+d:Nat -> @+r:Nat -> {Nat.is_le(Pair.fst(Nat, Nat, Nat.divmod.go(n, m, d, r)), Nat.add(d, n)) == True{} : Bool}

def div_le source · line 122 · raw

@+a:Nat -> @+d:Nat -> {Nat.is_le(Nat.div(a, d), a) == True{} : Bool}

a quotient never exceeds its dividend

def zsub source · line 129 · raw

@+b:Nat -> {Nat.sub(0n, b) == 0n : Nat}

def sub_cancel_l source · line 136 · raw

@+c:Nat -> @+a:Nat -> @+b:Nat -> {Nat.sub(Nat.add(c, a), Nat.add(c, b)) == Nat.sub(a, b) : Nat}

def sc_idx source · line 144 · raw

@+k:Nat -> @+j:Nat -> @+x:Nat -> {sc(Nat.add(k, j), x) == sc(k, sc(j, x)) : Nat}

2^(k + j) x == 2^k (2^j x)

def sc_sub source · line 152 · raw

@+k:Nat -> @+a:Nat -> @+b:Nat -> {sc(k, Nat.sub(a, b)) == Nat.sub(sc(k, a), sc(k, b)) : Nat}

2^k (a - b) == 2^k a - 2^k b

def sub_le2 source · line 169 · raw

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

a - b <= a