Grace/Cumulus/Algebra/Group/Power.g17

Open in Workbench Download source

Imports

Core · Nat.Core

Declarations

• monoidPow def
• monoidPow.zero theorem derivation
• monoidPow.succ theorem derivation
• monoidPow.closed theorem derivation
• monoidPow.add theorem derivation
• monoidPow.one theorem derivation
• monoidPow.succ_right theorem derivation
• monoidPow.succ_left theorem derivation
• monoidPow.commute theorem derivation
• monoidPow.add_commute theorem derivation
• monoidPow.unit theorem derivation
• monoidPow.mul theorem derivation

Source

1-- Natural powers in a monoid2-- 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.Algebra.Group.Power8import Core9import Nat.Core1011-- Natural powers belong to every monoid.  The carrier and its multiplication12-- remain explicit here so all concrete algebraic structures share one13-- recursion and one collection of laws.14def monoidPow (op unit x : Set, n : Nat) → Set15  | op, unit, x, zero => unit16  | op, unit, x, succ(n) => op(x, monoidPow(op, unit, x, n))1718notation scoped monoidPow(R, x, n) => monoidPow(R.mul, R.one, x, n)1920theorem monoidPow.zero (op unit x : Set)21  shows monoidPow(op, unit, x, 0) = unit22proof23  simp [monoidPow]2425theorem monoidPow.succ (op unit x : Set, n : Nat)26  shows monoidPow(op, unit, x, succ(n)) =27    op(x, monoidPow(op, unit, x, n))28proof29  simp [monoidPow]3031theorem monoidPow.closed (A op unit x : Set, n : Nat)32  requires monoid : IsMonoid(A, op, unit)33  requires xInA : x ∈ A34  shows monoidPow(op, unit, x, n) ∈ A35proof36  induction n37  | zero =>38    rw monoidPow.zero39    exact IsMonoid.unit_in_carrier with monoid40  | succ(k) using ih =>41    rw monoidPow.succ42    exact IsMonoid.closed with monoid, xInA, ih4344theorem monoidPow.add (A op unit x : Set, m n : Nat)45  requires monoid : IsMonoid(A, op, unit)46  requires xInA : x ∈ A47  shows monoidPow(op, unit, x, m + n) =48    op(monoidPow(op, unit, x, m), monoidPow(op, unit, x, n))49proof50  induction m51  | zero =>52    have powerNInA := monoidPow.closed with monoid, xInA53    rw [add.left_unit, monoidPow.zero]54    have leftIdentity := IsMonoid.left_identity with monoid, powerNInA55    rw leftIdentity56    rfl57  | succ(k) using ih =>58    have powerKInA := monoidPow.closed at A, op, unit, x, k with59      monoid, xInA60    have powerNInA := monoidPow.closed at A, op, unit, x, n with61      monoid, xInA62    have associative := IsMonoid.associative with monoid63    rw [add, monoidPow.succ, monoidPow.succ, ih]64    have reassociate := Associative.law with associative, xInA, powerKInA, powerNInA65    rw reassociate66    rfl6768theorem monoidPow.one (A op unit x : Set)69  requires monoid : IsMonoid(A, op, unit)70  requires hx : x ∈ A71  shows monoidPow(op, unit, x, 1) = x72proof73  have identity := IsMonoid.right_identity with monoid, hx74  simp [monoidPow, identity]7576theorem monoidPow.succ_right (A op unit x : Set, n : Nat)77  requires monoid : IsMonoid(A, op, unit)78  requires hx : x ∈ A79  shows monoidPow(op, unit, x, n + 1) =80    op(monoidPow(op, unit, x, n), x)81proof82  have split := monoidPow.add at A, op, unit, x, n, 1 with monoid, hx83  have one := monoidPow.one with monoid, hx84  rw [split, one]85  rfl8687theorem monoidPow.succ_left (A op unit x : Set, n : Nat)88  requires monoid : IsMonoid(A, op, unit)89  requires hx : x ∈ A90  shows monoidPow(op, unit, x, n + 1) =91    op(x, monoidPow(op, unit, x, n))92proof93  rw add.right_one94  exact monoidPow.succ9596theorem monoidPow.commute (A op unit x : Set, n : Nat)97  requires monoid : IsMonoid(A, op, unit)98  requires hx : x ∈ A99  shows op(x, monoidPow(op, unit, x, n)) =100    op(monoidPow(op, unit, x, n), x)101proof102  have left := monoidPow.succ_left with monoid, hx103  have right := monoidPow.succ_right with monoid, hx104  cc105106theorem monoidPow.add_commute (A op unit x : Set, m n : Nat)107  requires monoid : IsMonoid(A, op, unit)108  requires hx : x ∈ A109  shows op(monoidPow(op, unit, x, m), monoidPow(op, unit, x, n)) =110    op(monoidPow(op, unit, x, n), monoidPow(op, unit, x, m))111proof112  have first := monoidPow.add at A, op, unit, x, m, n with monoid, hx113  have second := monoidPow.add at A, op, unit, x, n, m with monoid, hx114  have swap := add.commutative at n, m115  rw [← first, ← second, swap]116  rfl117118theorem monoidPow.unit (A op unit : Set, n : Nat)119  requires monoid : IsMonoid(A, op, unit)120  shows monoidPow(op, unit, unit, n) = unit121proof122  induction n123  | zero =>124    exact monoidPow.zero at op, unit, unit125  | succ(k) using ih =>126    have unitIn := IsMonoid.unit_in_carrier with monoid127    have identity := IsMonoid.left_identity with monoid, unitIn128    rw [monoidPow.succ, ih]129    exact identity130131theorem monoidPow.mul (A op unit x : Set, m n : Nat)132  requires monoid : IsMonoid(A, op, unit)133  requires hx : x ∈ A134  shows monoidPow(op, unit, x, mul(m, n)) =135    monoidPow(op, unit, monoidPow(op, unit, x, m), n)136proof137  induction n138  | zero =>139    rw [mul.right_zero, monoidPow.zero, monoidPow.zero]140    rfl141  | succ(k) using ih =>142    have powerM := monoidPow.closed at A, op, unit, x, m with monoid, hx143    have step := mul.succ_right at k, m144    have split := monoidPow.add at A, op, unit, x, m, mul(m, k) with monoid, hx145    rw [step, split, ih, monoidPow.succ]146    rfl147