nat.bend checks

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

nat.bend: laws of Base's Nat.add, Nat.mul and Nat.double, as typed defs. Rewrites follow Bend's rule: %e : P with e : {a == b} takes the goal P[b/_] to P[a/_].

1 import

import Base

Definitions

def add_zero source · line 10 · raw

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

def add_succ source · line 18 · raw

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

def add_comm source · line 26 · raw

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

def add_assoc source · line 36 · raw

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

def add_swap source · line 45 · raw

@+x:Nat -> @+y:Nat -> @+z:Nat -> {Nat.add(x, Nat.add(y, z)) == Nat.add(y, Nat.add(x, z)) : Nat}

the first two summands of a triple sum swap

def add_4 source · line 55 · raw

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

the middle summands of two pairs swap

def double_add_self source · line 64 · raw

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

def mul_add_r source · line 76 · raw

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

def pred source · line 88 · raw

@n:Nat -> Nat

def succ_inj source · line 95 · raw

@+x:Nat -> @+y:Nat -> @e:{1n+x == 1n+y : Nat} -> {x == y : Nat}

def disc source · line 99 · raw

@n:Nat -> Type

a motive for refuting 1n+x == 0n: it sends 0n to Empty

def succ_ne_zero source · line 106 · raw

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

def double_inj source · line 110 · raw

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

def parity source · line 123 · raw

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

no even Nat is odd

def add_cancel_l source · line 135 · raw

@+p:Nat -> @+x:Nat -> @+y:Nat -> @e:{Nat.add(p, x) == Nat.add(p, y) : Nat} -> {x == y : Nat}

def add_cancel_r source · line 142 · raw

@+x:Nat -> @+y:Nat -> @+p:Nat -> @e:{Nat.add(x, p) == Nat.add(y, p) : Nat} -> {x == y : Nat}

def bdisc source · line 152 · raw

@b:Bool -> Type

a motive for refuting False{} == True{}: it sends True{} to Empty

def false_ne_true source · line 159 · raw

@e:{False{} == True{} : Bool} -> Empty

def le_sub source · line 164 · raw

@+x:Nat -> @+y:Nat -> @h:{Nat.is_le(x, y) == True{} : Bool} -> {y == Nat.add(x, Nat.sub(y, x)) : Nat}

x <= y leaves room for the difference: y == x + (y - x)