nat.bend source

nat.bend on the hub · documented module

import Base# Nat.add — the first two lemmas: a + 0 == a, and (a + b) + c == a + (b + c).## Base ships a rich term library and no reasoning library; these are the two# facts every proof over Nat.add ends up writing by hand.  A lemma is a def# whose return type is an equation; import this file and call one by name.##   add_zero:   a + 0 == a       (Nat.add recurses on its first argument, so#                                 Nat.add(a, 0n) is stuck when a is a variable)#   add_assoc:  (a + b) + c == a + (b + c)def add_zero(a: Nat) -> {Nat.add(a, 0n) == a : Nat}:  match a:    case 0n:      {==}    case 1n+p:      %add_zero(p) : {1n+Nat.add(p, 0n) == 1n+_ : Nat}      {==}def add_assoc(a: Nat, -b: Nat, -c: Nat) -> {Nat.add(Nat.add(a, b), c) == Nat.add(a, Nat.add(b, c)) : Nat}:  match a:    case 0n:      {==}    case 1n+p:      %add_assoc(p, b, c) : {1n+Nat.add(Nat.add(p, b), c) == 1n+_ : Nat}      {==}