-- Natural-number recursion and computation
-- Part of the Grace17 proof assistant for mathematics based on set theory.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Core.Nat
namespace Grace.Core.Nat

namespace Rec

def add (x y : Nat) -> Nat
  | zero, y => y
  | succ(x), y => succ(add(x, y))

notation infixl 60 "+" => add for Nat

theorem add.left_unit (y : Nat)
  shows add(0, y) = y
proof
  simp [add]

def mul (x y : Nat) -> Nat
  | zero, y => zero
  | succ(x), y => y + mul(x, y)

notation infixl 70 "*" => mul for Nat

def factorial (n : Nat) -> Nat
  | zero => succ(zero)
  | succ(n) => mul(succ(n), factorial(n))

notation postfix 90 "!" => factorial for Nat

def predecessor (n : Nat) -> Nat
  | zero => zero
  | succ(n) => n

theorem mul.six_seven
  shows mul(6, 7) = 42
proof
  compute

theorem factorial.five
  shows factorial(5) = 120
proof
  compute

end Rec

export open Grace.Core.Nat.Rec

end Grace.Core.Nat