Grace/Core/Nat.g17

Open in Workbench Download source

Imports

None

Declarations

• add def
• add.left_unit theorem derivation
• mul def
• factorial def
• predecessor def
• mul.six_seven theorem derivation
• factorial.five theorem derivation

Source

1-- Natural-number recursion and computation2-- Part of the Grace17 proof assistant for mathematics based on set theory.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Core.Nat8namespace Grace.Core.Nat910namespace Rec1112def add (x y : Nat) -> Nat13  | zero, y => y14  | succ(x), y => succ(add(x, y))1516notation infixl 60 "+" => add for Nat1718theorem add.left_unit (y : Nat)19  shows add(0, y) = y20proof21  simp [add]2223def mul (x y : Nat) -> Nat24  | zero, y => zero25  | succ(x), y => y + mul(x, y)2627notation infixl 70 "*" => mul for Nat2829def factorial (n : Nat) -> Nat30  | zero => succ(zero)31  | succ(n) => mul(succ(n), factorial(n))3233notation postfix 90 "!" => factorial for Nat3435def predecessor (n : Nat) -> Nat36  | zero => zero37  | succ(n) => n3839theorem mul.six_seven40  shows mul(6, 7) = 4241proof42  compute4344theorem factorial.five45  shows factorial(5) = 12046proof47  compute4849end Rec5051export open Grace.Core.Nat.Rec5253end Grace.Core.Nat54