~/bend-docscommunity

proofs/crypto/secp256k1/ineq.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ineq.bend as Ineq

GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/ineq.src; edit the .src

7 imports
import Base
import ../../../spec/lib/common.bend as C
import ../../lib/nat.bend as N
import ../../lib/logic.bend as Lg
import ../../lib/arith.bend as AR
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../../math/typed/width.bend as WW

Definitions

def le_subst_r source · line 13 · raw

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

def le_subst_l source · line 16 · raw

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

def lt_subst_r source · line 19 · raw

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

def lt_subst_l source · line 22 · raw

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

def le_add_l source · line 26 · raw

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

b <= a + b

def le_add2 source · line 30 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+d:Nat -> @+h1:{Nat.is_le(a, c) == True{} : Bool} -> @+h2:{Nat.is_le(b, d) == True{} : Bool} -> {Nat.is_le(Nat.add(a, b), Nat.add(c, d)) == True{} : Bool}

a <= c, b <= d: a + b <= c + d

def lt_le_add source · line 34 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+d:Nat -> @+h1:{Nat.is_lt(a, c) == True{} : Bool} -> @+h2:{Nat.is_le(b, d) == True{} : Bool} -> {Nat.is_lt(Nat.add(a, b), Nat.add(c, d)) == True{} : Bool}

a < c, b <= d: a + b < c + d

def le_lt_add source · line 38 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+d:Nat -> @+h1:{Nat.is_le(a, c) == True{} : Bool} -> @+h2:{Nat.is_lt(b, d) == True{} : Bool} -> {Nat.is_lt(Nat.add(a, b), Nat.add(c, d)) == True{} : Bool}

a <= c, b < d: a + b < c + d

def le_mul_r source · line 42 · raw

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

b <= c: a b <= a c

def le_mul2 source · line 48 · raw

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

a <= c, b <= d: a b <= c d

def shift_le source · line 51 · raw

@k:Nat -> @+a:Nat -> @+b:Nat -> @+h:{Nat.is_le(a, b) == True{} : Bool} -> {Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(k, a), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(k, b)) == True{} : Bool}

def shift_lt source · line 58 · raw

@+k:Nat -> @+a:Nat -> @+b:Nat -> @+h:{Nat.is_lt(a, b) == True{} : Bool} -> {Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(k, a), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(k, b)) == True{} : Bool}

def lt_succ_le source · line 62 · raw

@+a:Nat -> @+b:Nat -> @+h:{Nat.is_lt(a, b) == True{} : Bool} -> {Nat.is_le(Nat.add(a, 1n), b) == True{} : Bool}

a < b gives a + 1 <= b

def digit_lt source · line 67 · raw

@+k:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:Nat -> @+e:Nat -> @+pp:Nat -> @+ha:{Nat.is_lt(a, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(k, one)) == True{} : Bool} -> @+he:{Nat.is_lt(e, pp) == True{} : Bool} -> {Nat.is_lt(Nat.add(a, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(k, e)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(k, pp)) == True{} : Bool}

a < 2^k and e < P: a + 2^k e < 2^k P (2^k written C.shift(k, one))

def lt_of_le_lt source · line 74 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+h1:{Nat.is_le(a, b) == True{} : Bool} -> @+h2:{Nat.is_lt(b, c) == True{} : Bool} -> {Nat.is_lt(a, c) == True{} : Bool}

x < b and b <= c: x < c, and friends with rewriting

def lt_add_pos source · line 78 · raw

@+a:Nat -> @+b:Nat -> @+h:{Nat.is_lt(0n, b) == True{} : Bool} -> {Nat.is_lt(a, Nat.add(a, b)) == True{} : Bool}

0 < b: a < a + b

def le_mul_pos source · line 83 · raw

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

a <= a + b, and a <= a * b for b >= 1