~/bend-docscommunity

proofs/lib/lemmas/proofs/nat_algebra.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as Nat_algebra

1 import
import Base

Definitions

def succ_equal source · line 5 · raw

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

Commutative-semiring laws of Base Nat.add/Nat.mul, by induction on the actual definitions. Used by the host decimal/word conversion proofs.

def add_zero source · line 8 · raw

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

def add_succ source · line 13 · raw

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

def add_comm source · line 18 · raw

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

def add_assoc source · line 23 · raw

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

def add_swap source · line 29 · raw

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

a + (b + c) == b + (a + c)

def mul_zero source · line 36 · raw

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

def mul_succ source · line 41 · raw

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

def mul_comm source · line 48 · raw

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

def mul_one source · line 55 · raw

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

def mul_add_right source · line 58 · raw

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

def mul_add_left source · line 65 · raw

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

def mul_assoc source · line 71 · raw

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

def double_add source · line 78 · raw

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

def double_self source · line 83 · raw

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

def double_mul source · line 90 · raw

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