~/bend-docscommunity

nat.bend checks

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

lib/nat.bend -- the arithmetic of Base's Nat, as theorems.

Every lemma here is about the operators Base ships (Nat.add, Nat.mul, Nat.double, Nat.cmp), so a program that uses +n gets these laws for free. A claim is a def whose return type is the proposition and whose body is the proof; bend nat.bend --check verifies all of them.

Reading a proof: match x refines the goal per constructor, a recursive call is the induction hypothesis, {==} closes a goal whose two sides compute to the same term, and %e : P rewrites with an equation e : {a == b}: the goal must be P with b at the _ marks, and what follows proves P with a there. So %e REPLACES b BY a in the goal; to replace X by Y you need an equation {Y == X}, and Equal.sym flips one that points the other way.

1 import
import Base

Definitions

def Nat.pred source · line 22 · raw

@n:Nat -> Nat

def Nat.is_succ source · line 31 · raw

@n:Nat -> Type

a Type computed from a Nat: Empty at zero, Unit above. Rewriting an equation {1n+a == 0n} into it turns Unit into Empty.

def Nat.succ_neq_zero source · line 38 · raw

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

def Nat.zero_neq_succ source · line 42 · raw

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

def Nat.succ_inj source · line 45 · raw

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

def Nat.add_zero source · line 52 · raw

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

def Nat.add_succ source · line 60 · raw

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

def Nat.add_comm source · line 68 · raw

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

def Nat.add_assoc source · line 78 · raw

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

def Nat.add_swap source · line 87 · 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 Nat.add_add_swap source · line 93 · 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}

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

def Nat.mul_zero source · line 102 · raw

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

def Nat.mul_one source · line 109 · raw

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

def Nat.one_mul source · line 117 · raw

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

def Nat.mul_succ source · line 121 · raw

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

a * (1 + b) = a + a * b

def Nat.mul_comm source · line 131 · raw

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

def Nat.add_mul source · line 142 · 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}

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

def Nat.mul_add source · line 151 · 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}

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

def Nat.mul_assoc source · line 160 · raw

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

def Nat.double_add source · line 174 · raw

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

def Nat.two_mul source · line 184 · raw

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

def Nat.double_inj source · line 189 · raw

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

def Nat.add_cancel_l source · line 204 · raw

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

def Nat.add_cancel_r source · line 211 · raw

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

def Nat.add_eq_zero_l source · line 214 · raw

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

def Nat.add_eq_zero_r source · line 221 · raw

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

def Nat.Le source · line 230 · raw

@a:Nat -> @b:Nat -> Type

def Nat.Lt source · line 241 · raw

@a:Nat -> @b:Nat -> Type

def Nat.le_refl source · line 244 · raw

@a:Nat -> Nat.Le(a, a)

def Nat.le_succ source · line 251 · raw

@a:Nat -> @b:Nat -> @h:Nat.Le(a, b) -> Nat.Le(a, 1n+b)

def Nat.lt_le source · line 263 · raw

@a:Nat -> @b:Nat -> @h:Nat.Lt(a, b) -> Nat.Le(a, b)

a < b implies a <= b

def Nat.le_trans source · line 270 · raw

@a:Nat -> @b:Nat -> @c:Nat -> @h1:Nat.Le(a, b) -> @h2:Nat.Le(b, c) -> Nat.Le(a, c)

def Nat.le_antisym source · line 285 · raw

@a:Nat -> @b:Nat -> @h1:Nat.Le(a, b) -> @h2:Nat.Le(b, a) -> {a == b : Nat}

def Nat.lt_irrefl source · line 296 · raw

@a:Nat -> @h:Nat.Lt(a, a) -> Empty

def Nat.eq_le source · line 303 · raw

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

def Nat.le_add_r source · line 307 · raw

@a:Nat -> @-b:Nat -> Nat.Le(a, Nat.add(a, b))

def Nat.le_add_l source · line 314 · raw

@+a:Nat -> @+b:Nat -> Nat.Le(b, Nat.add(a, b))

def Nat.le_add_both source · line 318 · raw

@a:Nat -> @+b:Nat -> @+c:Nat -> @+d:Nat -> @h1:Nat.Le(a, b) -> @h2:Nat.Le(c, d) -> Nat.Le(Nat.add(a, c), Nat.add(b, d))

def Nat.le_add_mono_l source · line 329 · raw

@c:Nat -> @-a:Nat -> @-b:Nat -> @h:Nat.Le(a, b) -> Nat.Le(Nat.add(c, a), Nat.add(c, b))

def Nat.le_diff.con source · line 337 · raw

@-ap:Nat -> @-bp:Nat -> @w:(&c:Nat -> {Nat.add(ap, c) == bp : Nat}) -> &c:Nat -> {Nat.add(1n+ap, c) == 1n+bp : Nat}

a <= b exactly when b = a + c for some c

def Nat.le_diff source · line 341 · raw

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

def Bool.is_true source · line 356 · raw

@b:Bool -> Type

def Bool.is_false source · line 363 · raw

@b:Bool -> Type

def Bool.false_ne_true source · line 370 · raw

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

def Bool.true_ne_false source · line 374 · raw

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

def Bool.not_not source · line 378 · raw

@b:Bool -> {Bool.not(Bool.not(b)) == b : Bool}

def Bool.or_idem source · line 385 · raw

@b:Bool -> {Bool.or(b, b) == b : Bool}

def Bool.same source · line 393 · raw

@a:Bool -> @b:Bool -> Bool

Bool.same(a, b): True when a and b agree

def Bool.same_true source · line 404 · raw

@b:Bool -> {Bool.same(True{}, b) == b : Bool}

def Bool.not_same_l source · line 411 · raw

@a:Bool -> @b:Bool -> {Bool.not(Bool.same(a, b)) == Bool.same(Bool.not(a), b) : Bool}

def Bool.same_or source · line 422 · raw

@a:Bool -> @b:Bool -> {Bool.same(b, Bool.or(a, b)) == Bool.or(Bool.not(a), b) : Bool}

def Cmp.is_LT source · line 433 · raw

@c:Cmp -> Type

def Cmp.is_EQ source · line 442 · raw

@c:Cmp -> Type

def Cmp.is_GT source · line 451 · raw

@c:Cmp -> Type

def Cmp.eq_ne_lt source · line 460 · raw

@e:{EQ{} == LT{} : Cmp} -> Empty

def Cmp.gt_ne_lt source · line 464 · raw

@e:{GT{} == LT{} : Cmp} -> Empty

def Cmp.lt_ne_eq source · line 468 · raw

@e:{LT{} == EQ{} : Cmp} -> Empty

def Cmp.gt_ne_eq source · line 472 · raw

@e:{GT{} == EQ{} : Cmp} -> Empty

def Nat.cmp_lt source · line 478 · raw

@a:Nat -> @b:Nat -> @e:{Nat.cmp(a, b) == LT{} : Cmp} -> Nat.Lt(a, b)

Nat.cmp answers LT only when a < b, and EQ only when a = b: the run-time comparison is faithful to the proposition.

def Nat.cmp_eq source · line 489 · raw

@a:Nat -> @b:Nat -> @e:{Nat.cmp(a, b) == EQ{} : Cmp} -> {a == b : Nat}

def Nat.is_lt_true source · line 500 · raw

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

def Nat.even source · line 515 · raw

@n:Nat -> Bool

def Nat.half source · line 522 · raw

@n:Nat -> Nat

def Nat.even_add source · line 531 · raw

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

def Nat.even_mul source · line 540 · raw

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

def Nat.even_sq source · line 551 · raw

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

a square has the parity of its root

def Nat.even_double source · line 555 · raw

@a:Nat -> {Nat.even(Nat.double(a)) == True{} : Bool}

def Nat.even_half source · line 564 · raw

@n:Nat -> @e:{Nat.even(n) == True{} : Bool} -> {n == Nat.double(Nat.half(n)) : Nat}

an even number is the double of its half