~/bend-docscommunity

tinygrad/nat.bend checks

raw source on the hub · import 0xe6b82fa6c4c459c7023adf4b12a3ac46/tinygrad/nat.bend as MNat

tinygrad/nat.bend -- arithmetic lemmas over Nat used by PROOF.bend. Textbook Peano arithmetic, structural inductions only.

1 import
import Base

Definitions

def add_zero_right source · line 7 · raw

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

x + 0 == x

def add_succ_right source · line 16 · raw

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

a + (1n+b) == 1n + (a + b)

def sub_diag source · line 24 · raw

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

x - x == 0

def succ1 source · line 33 · raw

@n:Nat -> Nat

a + b == b + a

def add_comm source · line 36 · raw

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

def add_assoc source · line 49 · raw

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

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

def sub_add_cancel source · line 57 · raw

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

(n + k) - k == n