nat.bend checks

Nat.add — the laws of Base's Nat.add, as a callable lemma set.

Base ships a term library and no reasoning library: not one fact about Nat.add is stated anywhere in it. These six defs are the facts every proof over Nat.add ends up writing by hand — zero, succ, assoc, comm — plus the two that fall out of the first two by one rewrite. (First written for the Life proofs of bend2-from-zero; extracted here so the next proof can import them.)

The rewrite rule, because it decides each statement's orientation: %lem(args) : P P is the goal AFTER the rewrite, with _ at the position the lemma's LEFT side was put in. So a lemma is written {target == what-the-goal-holds-now}: its right side is the form being eliminated, its left side replaces it.

add_zero {a + 0 == a} replaces a with a + 0 add_zero_r {a == a + 0} replaces a + 0 with a add_succ {a + (1+p) == 1+(a+p)} replaces 1+(a+p) with a + (1+p) add_succ_r {1+(a+p) == a + (1+p)} replaces a + (1+p) with 1+(a+p) add_assoc {(a+b)+c == a+(b+c)} replaces a+(b+c) with (a+b)+c add_comm {a + b == b + a} replaces b + a with a + b