~/bend-docscommunity

proofs/math/natural/arith.bend checks

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

5 imports
import Base
import ../../lib/nat.bend as N
import ../../lib/lemmas/proofs/nat_algebra.bend as A
import ../../lib/lemmas/proofs/word_value.bend as WV
import ../../lib/lemmas/proofs/natural_division.bend as ND

Definitions

def dm_e2 source · line 15 · raw

@+bp:Nat -> @+v:Nat -> @g:0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/word_value.go_equation(bp, v, bp, 0n, 0n) -> {v == Nat.add(Nat.mul(Nat.div(v, 1n+bp), 1n+bp), Nat.mod(v, 1n+bp)) : Nat}

def dm_l2 source · line 19 · raw

@+bp:Nat -> @+v:Nat -> @g:0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/word_value.go_equation(bp, v, bp, 0n, 0n) -> {Nat.is_lt(Nat.mod(v, 1n+bp), 1n+bp) == True{} : Bool}

def dm_eq source · line 24 · raw

@+bp:Nat -> @+v:Nat -> {v == Nat.add(Nat.mul(Nat.div(v, 1n+bp), 1n+bp), Nat.mod(v, 1n+bp)) : Nat}

v == (v / n) n + v mod n (Mathlib Nat.div_add_mod)

def dm_lt source · line 28 · raw

@+bp:Nat -> @+v:Nat -> {Nat.is_lt(Nat.mod(v, 1n+bp), 1n+bp) == True{} : Bool}

v mod n < n (Mathlib Nat.mod_lt)

def div_of source · line 32 · raw

@+q:Nat -> @+bp:Nat -> @+r:Nat -> @+h:{Nat.is_lt(r, 1n+bp) == True{} : Bool} -> {Nat.div(Nat.add(Nat.mul(q, 1n+bp), r), 1n+bp) == q : Nat}

the quotient and remainder are unique

def mod_of source · line 35 · raw

@+q:Nat -> @+bp:Nat -> @+r:Nat -> @+h:{Nat.is_lt(r, 1n+bp) == True{} : Bool} -> {Nat.mod(Nat.add(Nat.mul(q, 1n+bp), r), 1n+bp) == r : Nat}

def add_cancel source · line 41 · raw

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

c + a == c + b gives a == b (Mathlib Nat.add_left_cancel)

def mul_cancel source · line 49 · raw

@+x:Nat -> @+y:Nat -> @+bp:Nat -> @+e:{Nat.mul(x, 1n+bp) == Nat.mul(y, 1n+bp) : Nat} -> {x == y : Nat}

x c == y c with c > 0 gives x == y (Mathlib Nat.eq_of_mul_eq_mul_right)

def le_add_cancel source · line 63 · raw

@+d:Nat -> @+x:Nat -> @+y:Nat -> {Nat.is_le(Nat.add(d, x), Nat.add(d, y)) == Nat.is_le(x, y) : Bool}

d + x <= d + y is x <= y

def le_div_g source · line 70 · raw

@+x:Nat -> @+q:Nat -> @+bp:Nat -> @+r:Nat -> @+hr:{Nat.is_lt(r, 1n+bp) == True{} : Bool} -> {Nat.is_le(x, q) == Nat.is_le(Nat.mul(x, 1n+bp), Nat.add(Nat.mul(q, 1n+bp), r)) : Bool}

def le_div source · line 83 · raw

@+bp:Nat -> @+x:Nat -> @+n:Nat -> {Nat.is_le(x, Nat.div(n, 1n+bp)) == Nat.is_le(Nat.mul(x, 1n+bp), n) : Bool}

x <= n / d is x d <= n (Mathlib Nat.le_div_iff_mul_le)

def zsub source · line 90 · raw

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

def sub_cancel_l source · line 97 · raw

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

def mul_sub source · line 105 · raw

@+x:Nat -> @+y:Nat -> @+c:Nat -> {Nat.mul(Nat.sub(x, y), c) == Nat.sub(Nat.mul(x, c), Nat.mul(y, c)) : Nat}

(x - y) c == x c - y c (Mathlib Nat.mul_sub_right_distrib)

def absorb source · line 120 · raw

@+bp:Nat -> @+q:Nat -> @+r:Nat -> {Nat.mod(Nat.add(Nat.mul(q, 1n+bp), r), 1n+bp) == Nat.mod(r, 1n+bp) : Nat}

(q n + r) mod n == r mod n (Mathlib Nat.mul_add_mod)

def mod_mod source · line 132 · raw

@+bp:Nat -> @+x:Nat -> {Nat.mod(Nat.mod(x, 1n+bp), 1n+bp) == Nat.mod(x, 1n+bp) : Nat}

(x mod n) mod n == x mod n (Mathlib Nat.mod_mod)

def mod_add_r source · line 136 · raw

@+bp:Nat -> @+x:Nat -> @+y:Nat -> {Nat.mod(Nat.add(x, Nat.mod(y, 1n+bp)), 1n+bp) == Nat.mod(Nat.add(x, y), 1n+bp) : Nat}

(x + y mod n) mod n == (x + y) mod n (Mathlib Nat.add_mod)

def mod_add_l source · line 145 · raw

@+bp:Nat -> @+x:Nat -> @+y:Nat -> {Nat.mod(Nat.add(Nat.mod(x, 1n+bp), y), 1n+bp) == Nat.mod(Nat.add(x, y), 1n+bp) : Nat}

def mod_mul_r source · line 151 · raw

@+bp:Nat -> @+x:Nat -> @+y:Nat -> {Nat.mod(Nat.mul(x, Nat.mod(y, 1n+bp)), 1n+bp) == Nat.mod(Nat.mul(x, y), 1n+bp) : Nat}

(x (y mod n)) mod n == (x y) mod n (Mathlib Nat.mul_mod)

def mod_mul_l source · line 162 · raw

@+bp:Nat -> @+x:Nat -> @+y:Nat -> {Nat.mod(Nat.mul(Nat.mod(x, 1n+bp), y), 1n+bp) == Nat.mod(Nat.mul(x, y), 1n+bp) : Nat}

def pow_add source · line 170 · raw

@+a:Nat -> @+x:Nat -> @+y:Nat -> {Nat.pow(a, Nat.add(x, y)) == Nat.mul(Nat.pow(a, x), Nat.pow(a, y)) : Nat}

a^(x + y) == a^x a^y (Mathlib pow_add)

def mul_swap4 source · line 179 · raw

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

(a b)(c d) == (a c)(b d)

def mul_pow source · line 188 · raw

@+x:Nat -> @+y:Nat -> @+k:Nat -> {Nat.pow(Nat.mul(x, y), k) == Nat.mul(Nat.pow(x, k), Nat.pow(y, k)) : Nat}

(x y)^k == x^k y^k (Mathlib mul_pow)