Grace/Cumulus/Nat/Pow.g17

Open in Workbench Download source

Imports

Core

Declarations

• pow def
• pow.zero theorem derivation
• pow.succ theorem derivation
• pow.closed theorem derivation
• pow.add theorem derivation
• pow.sample lemma derivation

Source

1-- Natural-number exponentiation2-- Part of Cumulus, the Grace17 mathematics library.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.Cumulus.Nat.Pow8import Core910def pow (base exponent : Nat) → Nat11  | base, zero => 112  | base, succ(n) => mul(base, pow(base, n))1314notation infixr 80 "^" => pow for Nat1516theorem pow.zero (a : Nat)17  shows a ^ 0 = 118proof19  simp [pow]2021theorem pow.succ (a n : Nat)22  shows a ^ succ(n) = mul(a, a ^ n)23proof24  simp [pow]2526theorem pow.closed (a : Nat, n : Nat)27  shows Nat(a ^ n)28proof29  induction n30  | zero => settle with pow, Naturals.constructor.zero, Naturals.constructor.succ31  | succ(k) using ih => settle with pow, mul.closed, ih3233theorem pow.add (a n : Nat, m : Nat)34  shows a ^ add(m, n) = mul(a ^ m, a ^ n)35proof36  induction m37  | zero => settle with pow, add, mul, add.right_unit38  | succ(k) using ih => settle with pow, add, mul.associative, pow.closed, ih3940lemma pow.sample41  shows 12 ^ 8 = 42998169642proof43  compute4445eval 12 ^ 2046