proofs/math/typed/natcmp.bend checks

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

8 imports

import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/math/f64.bend as SF
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ./width.bend as WW
import ./u32laws.bend as LW

Definitions

def absurd_tf source · line 13 · raw

@-T:Type -> @+h:{False{} == True{} : Bool} -> T

def lex source · line 16 · raw

@c:Cmp -> @d:Cmp -> Cmp

def cmp_dbl source · line 25 · raw

@+a:Nat -> @+b:Nat -> {Nat.cmp(Nat.double(a), Nat.double(b)) == Nat.cmp(a, b) : Cmp}

def cmp_shift source · line 36 · raw

@+k:Nat -> @+a:Nat -> @+b:Nat -> {Nat.cmp(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, a), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, b)) == Nat.cmp(a, b) : Cmp}

def cmp_add source · line 43 · raw

@+d:Nat -> @+a:Nat -> @+b:Nat -> {Nat.cmp(Nat.add(d, a), Nat.add(d, b)) == Nat.cmp(a, b) : Cmp}

def cmp_addr source · line 50 · raw

@+a:Nat -> @+b:Nat -> @+s:Nat -> {Nat.cmp(Nat.add(a, s), Nat.add(b, s)) == Nat.cmp(a, b) : Cmp}

def lt_c source · line 55 · raw

@+c:Cmp -> @+h:{Cmp.is_lt(c) == True{} : Bool} -> {c == LT{} : Cmp}

def eq_c source · line 64 · raw

@+c:Cmp -> @+h:{Cmp.is_eq(c) == True{} : Bool} -> {c == EQ{} : Cmp}

def cmp_lt source · line 73 · raw

@+a:Nat -> @+b:Nat -> @+h:{Nat.is_lt(a, b) == True{} : Bool} -> {Nat.cmp(a, b) == LT{} : Cmp}

def cmp_flip source · line 76 · raw

@+a:Nat -> @+b:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.flip(Nat.cmp(a, b)) == Nat.cmp(b, a) : Cmp}

def cmp_gt source · line 87 · raw

@+a:Nat -> @+b:Nat -> @+h:{Nat.is_lt(b, a) == True{} : Bool} -> {Nat.cmp(a, b) == GT{} : Cmp}

def cmp_refl source · line 90 · raw

@+a:Nat -> {Nat.cmp(a, a) == EQ{} : Cmp}

def eq_of_cmp source · line 93 · raw

@+a:Nat -> @+b:Nat -> @+h:{Nat.cmp(a, b) == EQ{} : Cmp} -> {a == b : Nat}

def lt_of_cmp source · line 96 · raw

@+a:Nat -> @+b:Nat -> @+h:{Nat.cmp(a, b) == LT{} : Cmp} -> {Nat.is_lt(a, b) == True{} : Bool}

def lt_of_gt source · line 99 · raw

@+a:Nat -> @+b:Nat -> @+h:{Nat.cmp(a, b) == GT{} : Cmp} -> {Nat.is_lt(b, a) == True{} : Bool}

def cl_c source · line 103 · raw

@+k:Nat -> @+x1:Nat -> @+y1:Nat -> @+x2:Nat -> @+y2:Nat -> @+hx1:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, x1) == True{} : Bool} -> @+hx2:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, x2) == True{} : Bool} -> @+c:Cmp -> @+hc:{Nat.cmp(y1, y2) == c : Cmp} -> {Nat.cmp(Nat.add(x1, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, y1)), Nat.add(x2, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, y2))) == lex(c, Nat.cmp(x1, x2)) : Cmp}

two limbs compare lexicographically

def cmp_limbs source · line 112 · raw

@+k:Nat -> @+x1:Nat -> @+y1:Nat -> @+x2:Nat -> @+y2:Nat -> @+hx1:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, x1) == True{} : Bool} -> @+hx2:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, x2) == True{} : Bool} -> {Nat.cmp(Nat.add(x1, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, y1)), Nat.add(x2, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, y2))) == lex(Nat.cmp(y1, y2), Nat.cmp(x1, x2)) : Cmp}

def min_le_l source · line 115 · raw

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

def min_le_r source · line 124 · raw

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

def sh_split source · line 134 · raw

@+a:Nat -> @+m:Nat -> @+p:Nat -> @+h:{Nat.is_le(m, a) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(a, p) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(m, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.sub(a, m), p)) : Nat}

shift(a, p) = shift(m, shift(a - m, p)) for m <= a

def cmp_min source · line 138 · raw

@+a:Nat -> @+b:Nat -> @+p:Nat -> @+q:Nat -> {Nat.cmp(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.sub(a, Nat.min(a, b)), p), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.sub(b, Nat.min(a, b)), q)) == Nat.cmp(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(a, p), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(b, q)) : Cmp}

a common scale 2^min cancels