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}
      {==}