~/bend-docscommunity

proofs/lib/nat.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as MNat

5 imports
import Base
import ./logic.bend as L
import ./lemmas/proofs/nat_algebra.bend as NA
import ../../spec/lib/common.bend as SC
import ./lemmas/spec/numeric.bend as S

Definitions

def pred source · line 10 · raw

@n:Nat -> Nat

def succ_inj source · line 17 · raw

@+a:Nat -> @+b:Nat -> @e:{1n+a == 1n+b : Nat} -> {a == b : Nat}

def succ_cong source · line 20 · raw

@+a:Nat -> @+b:Nat -> @e:{a == b : Nat} -> {1n+a == 1n+b : Nat}

def is_zero source · line 23 · raw

@n:Nat -> Bool

def zero_succ source · line 30 · raw

@+n:Nat -> @e:{0n == 1n+n : Nat} -> Empty

def succ_zero source · line 34 · raw

@+n:Nat -> @e:{1n+n == 0n : Nat} -> Empty

def add_zero source · line 37 · raw

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

def add_succ source · line 40 · raw

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

def add_comm source · line 43 · raw

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

def add_assoc source · line 46 · raw

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

def lt_irrefl source · line 51 · raw

@+n:Nat -> {Nat.is_lt(n, n) == False{} : Bool}

def le_refl source · line 58 · raw

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

def lt_succ source · line 65 · raw

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

def le_succ source · line 72 · raw

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

def zero_le source · line 79 · raw

@+n:Nat -> {Nat.is_le(0n, n) == True{} : Bool}

def not_lt_zero source · line 86 · raw

@+n:Nat -> {Nat.is_lt(n, 0n) == False{} : Bool}

def lt_zero_absurd source · line 93 · raw

@+n:Nat -> @e:{Nat.is_lt(n, 0n) == True{} : Bool} -> Empty

def lt_le source · line 96 · raw

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

def le_lt_succ source · line 107 · raw

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

def lt_succ_le source · line 116 · raw

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

def succ_le_lt source · line 125 · raw

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

def lt_succ_le_succ source · line 134 · raw

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

def le_trans source · line 143 · raw

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

def lt_le_trans source · line 154 · raw

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

def le_lt_trans source · line 157 · raw

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

def lt_trans source · line 160 · raw

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

def not_lt_le source · line 164 · raw

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

is_lt(a, b) == False gives b <= a.

def le_not_lt source · line 173 · raw

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

def lt_not_le source · line 182 · raw

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

def not_le_lt source · line 191 · raw

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

def lt_asym source · line 202 · raw

@+a:Nat -> @+b:Nat -> @ab:{Nat.is_lt(a, b) == True{} : Bool} -> @ba:{Nat.is_lt(b, a) == True{} : Bool} -> Empty

def le_antisym source · line 205 · raw

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

def eq_le source · line 216 · raw

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

def lt_ne source · line 220 · raw

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

def eq_from_is_eq source · line 223 · raw

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

def is_eq_refl source · line 234 · raw

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

def is_eq_lt source · line 241 · raw

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

def lt_or_eq source · line 250 · raw

@+a:Nat -> @+b:Nat -> @e:{Nat.is_le(a, b) == True{} : Bool} -> @ne:{Nat.is_eq(a, b) == False{} : Bool} -> {Nat.is_lt(a, b) == True{} : Bool}

def add_sub_cancel source · line 263 · raw

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

def sub_add source · line 272 · raw

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

def sub_zero source · line 283 · raw

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

def sub_self source · line 290 · raw

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

def sub_succ_left source · line 297 · raw

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

def sub_lt source · line 307 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @le:{Nat.is_le(b, a) == True{} : Bool} -> @lt:{Nat.is_lt(a, Nat.add(b, c)) == True{} : Bool} -> {Nat.is_lt(Nat.sub(a, b), c) == True{} : Bool}

def le_add_right source · line 317 · raw

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

def lt_add_left source · line 324 · raw

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

def le_add_left source · line 331 · raw

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

def double_inj source · line 340 · raw

@+a:Nat -> @+b:Nat -> @e:{Nat.double(a) == Nat.double(b) : Nat} -> {a == b : Nat}

def even_odd source · line 351 · raw

@+a:Nat -> @+b:Nat -> @e:{Nat.double(a) == 1n+Nat.double(b) : Nat} -> Empty

def bit_split_bit source · line 361 · raw

@+b:Bool -> @+c:Bool -> @+u:Nat -> @+v:Nat -> @e:{Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.bit_value(b), Nat.double(u)) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.bit_value(c), Nat.double(v)) : Nat} -> {b == c : Bool}

bit + 2u == bit' + 2v determines both parts.

def bit_split_val source · line 372 · raw

@+b:Bool -> @+c:Bool -> @+u:Nat -> @+v:Nat -> @e:{Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.bit_value(b), Nat.double(u)) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.bit_value(c), Nat.double(v)) : Nat} -> {u == v : Nat}

def double_lt source · line 383 · raw

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

def double_le source · line 392 · raw

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

def bit_double_lt source · line 402 · raw

@+b:Bool -> @+u:Nat -> @+v:Nat -> @e:{Nat.is_lt(Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.bit_value(b), Nat.double(u)), Nat.double(v)) == True{} : Bool} -> {Nat.is_lt(u, v) == True{} : Bool}

bit + 2u < 2v gives u < v.

def double_lt_bit source · line 413 · raw

@+b:Bool -> @+u:Nat -> @+v:Nat -> @e:{Nat.is_lt(u, v) == True{} : Bool} -> {Nat.is_lt(Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.bit_value(b), Nat.double(u)), Nat.double(v)) == True{} : Bool}

def double_self_le source · line 426 · raw

@+n:Nat -> {Nat.is_le(n, Nat.double(n)) == True{} : Bool}

def double_succ_le source · line 433 · raw

@+n:Nat -> @e:{Nat.is_le(1n, n) == True{} : Bool} -> {Nat.is_le(1n+n, Nat.double(n)) == True{} : Bool}

def pow2_pos source · line 440 · raw

@+k:Nat -> {Nat.is_le(1n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(k)) == True{} : Bool}

def pow2_lt_succ source · line 447 · raw

@+k:Nat -> {Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(k), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(1n+k)) == True{} : Bool}

def pow2_mono source · line 451 · raw

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

1 <= n gives 1 + n <= 2n.

def pow2_strict source · line 460 · raw

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

def pred_double source · line 468 · raw

@+v:Nat -> @e:{Nat.is_le(1n, v) == True{} : Bool} -> {Nat.sub(Nat.double(v), 1n) == 1n+Nat.double(Nat.sub(v, 1n)) : Nat}

pred(2v) == 1 + 2 pred(v) for v >= 1.

def add_double source · line 476 · raw

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

def bump2 source · line 490 · raw

@p:Pair(Nat, Nat) -> Pair(Nat, Nat)

def acc2 source · line 494 · raw

@i:Nat -> @m:Nat -> @+d:Nat -> @+r:Nat -> {Nat.divmod.go(i, m, 1n+d, r) == bump2(Nat.divmod.go(i, m, d, r)) : Pair(Nat, Nat)}

def peel2 source · line 503 · raw

@+i:Nat -> @+d:Nat -> {Nat.divmod.go(Nat.add(2n, i), 1n, d, 0n) == Nat.divmod.go(i, 1n, 1n+d, 0n) : Pair(Nat, Nat)}

def fst_bump2 source · line 506 · raw

@p:Pair(Nat, Nat) -> {Pair.fst(Nat, Nat, bump2(p)) == 1n+Pair.fst(Nat, Nat, p) : Nat}

def div2_step source · line 510 · raw

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

def double_succ source · line 517 · raw

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

def div2_double source · line 522 · raw

@x:Nat -> {Nat.div(Nat.double(x), 2n) == x : Nat}

def div2_pow2 source · line 532 · raw

@+r:Nat -> {Nat.div(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(1n+r), 2n) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(r) : Nat}

2^(1+r) / 2 = 2^r

def min_left source · line 535 · raw

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

def min_right source · line 544 · raw

@+a:Nat -> @+b:Nat -> @+h:{Nat.is_lt(a, b) == False{} : Bool} -> {Nat.min(a, b) == b : Nat}

def is_eq_sym_false source · line 555 · raw

@+a:Nat -> @+b:Nat -> @+h:{Nat.is_eq(a, b) == False{} : Bool} -> {Nat.is_eq(b, a) == False{} : Bool}

def lt_add_r2 source · line 567 · raw

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

a < b ==> a + c < b + c