proofs/math/natural/misc.bend checks

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

5 imports

import Base
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../../src/math/natural.bend as M
import ./arith.bend as R

Definitions

def divmod_done source · line 13 · raw

@+a:Nat -> @+bp:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.divmod(a, 1n+bp) == Done{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.QR{Nat.div(a, 1n+bp), Nat.mod(a, 1n+bp)}} : Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.MathError, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.QuotRem>}

def divmod_eq source · line 16 · raw

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

def divmod_lt source · line 19 · raw

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

def divmod_zero source · line 22 · raw

@+a:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.divmod(a, 0n) == Fail{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.ZeroDivision{}} : Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.MathError, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.QuotRem>}

def le_max_r source · line 27 · raw

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

def max_eq_l source · line 36 · raw

@+x:Nat -> @+lo:Nat -> @+h:{Nat.is_le(lo, x) == True{} : Bool} -> {Nat.max(x, lo) == x : Nat}

def min_le_r source · line 47 · raw

@+y:Nat -> @+hi:Nat -> {Nat.is_le(Nat.min(y, hi), hi) == True{} : Bool}

def le_min source · line 56 · raw

@+lo:Nat -> @+y:Nat -> @+hi:Nat -> @+h1:{Nat.is_le(lo, y) == True{} : Bool} -> @+h2:{Nat.is_le(lo, hi) == True{} : Bool} -> {Nat.is_le(lo, Nat.min(y, hi)) == True{} : Bool}

def min_eq_l source · line 67 · raw

@+y:Nat -> @+hi:Nat -> @+h:{Nat.is_le(y, hi) == True{} : Bool} -> {Nat.min(y, hi) == y : Nat}

def clamp_done source · line 78 · raw

@+x:Nat -> @+lo:Nat -> @+hi:Nat -> @+h:{Nat.is_le(lo, hi) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.clamp(x, lo, hi) == Done{Nat.min(Nat.max(x, lo), hi)} : Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.MathError, Nat>}

def clamp_domain source · line 82 · raw

@+x:Nat -> @+lo:Nat -> @+hi:Nat -> @+h:{Nat.is_lt(hi, lo) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.clamp(x, lo, hi) == Fail{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.Domain{}} : Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.MathError, Nat>}

def clamp_ge source · line 87 · raw

@+x:Nat -> @+lo:Nat -> @+hi:Nat -> @+h:{Nat.is_le(lo, hi) == True{} : Bool} -> {Nat.is_le(lo, Nat.min(Nat.max(x, lo), hi)) == True{} : Bool}

lo <= clamp and clamp <= hi

def clamp_le source · line 90 · raw

@+x:Nat -> @+lo:Nat -> @+hi:Nat -> {Nat.is_le(Nat.min(Nat.max(x, lo), hi), hi) == True{} : Bool}

def clamp_id source · line 94 · raw

@+x:Nat -> @+lo:Nat -> @+hi:Nat -> @+h1:{Nat.is_le(lo, x) == True{} : Bool} -> @+h2:{Nat.is_le(x, hi) == True{} : Bool} -> {Nat.min(Nat.max(x, lo), hi) == x : Nat}

x in [lo, hi] is left alone