proofs/math/typed/montnat.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/math/typed/montnat.bend as Montnat

7 imports

import Base
import ../../../spec/lib/common.bend as C
import ../../lib/nat.bend as N
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../natural/arith.bend as NR
import ./width.bend as WW
import ./natlight.bend as QN

Definitions

def low_addlow source · line 14 · raw

@+kk:Nat -> @+a:Nat -> @+b:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(kk, Nat.add(a, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(kk, b))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(kk, Nat.add(a, b)) : Nat}

def low_mullow source · line 17 · raw

@+kk:Nat -> @+a:Nat -> @+b:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(kk, Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(kk, a), b)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(kk, Nat.mul(a, b)) : Nat}

def low_zero source · line 20 · raw

@k:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, 0n) == 0n : Nat}

def low_shift0 source · line 27 · raw

@+kk:Nat -> @+z:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(kk, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(kk, z)) == 0n : Nat}

def redc0 source · line 31 · raw

@+kk:Nat -> @+one:Nat -> @+tl:Nat -> @+M:Nat -> @+mp:Nat -> @+hinv:{1n+0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(kk, Nat.mul(M, mp)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(kk, one) : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(kk, Nat.add(tl, Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(kk, Nat.mul(tl, mp)), M))) == 0n : Nat}

t + (t mp mod R) m == 0 (mod R) for m mp == -1 (mod R)

def half_inv source · line 35 · raw

@+bp:Nat -> @+hh:Nat -> @+hM:{2n+bp == Nat.add(hh, hh) : Nat} -> @+x:Nat -> {Nat.mod(x, 1n+bp) == Nat.mod(Nat.mul(Nat.mod(Nat.double(x), 1n+bp), hh), 1n+bp) : Nat}

x == 2 x (m + 1) / 2 (mod m)

def cancel2 source · line 39 · raw

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

2 x == 2 y (mod m) gives x == y (mod m) for odd m

def cancel source · line 43 · raw

@+bp:Nat -> @+hh:Nat -> @+hM:{2n+bp == Nat.add(hh, hh) : Nat} -> @k:Nat -> @+x:Nat -> @+y:Nat -> @+h:{Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, x), 1n+bp) == Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, y), 1n+bp) : Nat} -> {Nat.mod(x, 1n+bp) == Nat.mod(y, 1n+bp) : Nat}

x 2^k == y 2^k (mod m) gives x == y (mod m) for odd m

def mod_shift source · line 51 · raw

@+bp:Nat -> @+k:Nat -> @+z0:Nat -> {Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, Nat.mod(z0, 1n+bp)), 1n+bp) == Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, z0), 1n+bp) : Nat}

(z mod m) 2^k == z 2^k (mod m)

def plus1 source · line 54 · raw

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

def odd_hh source · line 58 · raw

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

m + 1 == 2 hh for odd m, hh = m / 2 + 1