From 3cde12567f8156e91a13e87a224ba696cc5ecdcc Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Thu, 24 Jul 2025 16:00:11 +1000
Subject: [PATCH] feat: add HPow Int field to Field (#9500)

This PR adds a `HPow \a Int \a` field to `Lean.Grind.Field`, and
sufficient axioms to connect it to the operations, so that in future we
can reason about exponents in `grind`. To avoid collisions, we also move
the `HPow \a Nat \a` field in `Semiring` from the extends clause to a
field. Finally, we add some failing tests about normalizing exponents.
---
 src/Init/Grind/Ring/Basic.lean                |  6 ++--
 src/Init/Grind/Ring/Envelope.lean             | 11 +++----
 src/Init/Grind/Ring/Field.lean                | 18 +++++++++++-
 .../Tactic/Grind/Arith/CommRing/Util.lean     |  2 +-
 tests/lean/grind/algebra/exponents.lean       | 29 +++++++++++++++++++
 .../grind/algebra/module_normalization.lean   |  2 +-
 tests/lean/grind/algebra/nat_module.lean      |  2 +-
 7 files changed, 59 insertions(+), 11 deletions(-)
 create mode 100644 tests/lean/grind/algebra/exponents.lean

diff --git a/src/Init/Grind/Ring/Basic.lean b/src/Init/Grind/Ring/Basic.lean
index 380f8b7747..3a129ef147 100644
--- a/src/Init/Grind/Ring/Basic.lean
+++ b/src/Init/Grind/Ring/Basic.lean
@@ -41,7 +41,7 @@ Use `Ring` instead if the type also has negation,
 `CommSemiring` if the multiplication is commutative,
 or `CommRing` if the type has negation and multiplication is commutative.
 -/
-class Semiring (α : Type u) extends Add α, Mul α, HPow α Nat α where
+class Semiring (α : Type u) extends Add α, Mul α where
   /--
   In every semiring there is a canonical map from the natural numbers to the semiring,
   providing the values of `0` and `1`. Note that this function need not be injective.
@@ -54,6 +54,8 @@ class Semiring (α : Type u) extends Add α, Mul α, HPow α Nat α where
   [ofNat : ∀ n, OfNat α n]
   /-- Scalar multiplication by natural numbers. -/
   [nsmul : HMul Nat α α]
+  /-- Exponentiation by a natural number. -/
+  [npow : HPow α Nat α]
   /-- Zero is the right identity for addition. -/
   add_zero : ∀ a : α, a + 0 = a
   /-- Addition is commutative. -/
@@ -129,7 +131,7 @@ class CommRing (α : Type u) extends Ring α, CommSemiring α
 -- so that in downstream libraries with their own `CommRing` class,
 -- the path `CommRing -> Add` is found before `CommRing -> Lean.Grind.CommRing -> Add`.
 -- (And similarly for the other parents.)
-attribute [instance 100] Semiring.toAdd Semiring.toMul Semiring.toHPow Ring.toNeg Ring.toSub
+attribute [instance 100] Semiring.toAdd Semiring.toMul Semiring.npow Ring.toNeg Ring.toSub
 
 -- This is a low-priority instance, to avoid conflicts with existing `OfNat`, `NatCast`, and `IntCast` instances.
 attribute [instance 100] Semiring.ofNat
diff --git a/src/Init/Grind/Ring/Envelope.lean b/src/Init/Grind/Ring/Envelope.lean
index 6f2e2b0449..b614140dcd 100644
--- a/src/Init/Grind/Ring/Envelope.lean
+++ b/src/Init/Grind/Ring/Envelope.lean
@@ -227,14 +227,14 @@ theorem right_distrib (a b c : Q α) : mul (add a b) c = add (mul a c) (mul b c)
   cases a; cases b; cases c; simp; apply Quot.sound
   simp [Semiring.right_distrib]; refine ⟨0, ?_⟩; ac_rfl
 
-def hPow (a : Q α) (n : Nat)  : Q α :=
+def npow (a : Q α) (n : Nat)  : Q α :=
   match n with
   | 0 => natCast 1
-  | n+1 => mul (hPow a n) a
+  | n+1 => mul (npow a n) a
 
-private theorem pow_zero (a : Q α) : hPow a 0 = natCast 1 := rfl
+private theorem pow_zero (a : Q α) : npow a 0 = natCast 1 := rfl
 
-private theorem pow_succ (a : Q α) (n : Nat) : hPow a (n+1) = mul (hPow a n) a := rfl
+private theorem pow_succ (a : Q α) (n : Nat) : npow a (n+1) = mul (npow a n) a := rfl
 
 def nsmul (n : Nat) (a : Q α) : Q α :=
   mul (natCast n) a
@@ -261,7 +261,8 @@ def ofSemiring : Ring (Q α) := {
   ofNat   := fun n => ⟨natCast n⟩
   natCast := ⟨natCast⟩
   intCast := ⟨intCast⟩
-  add, sub, mul, neg, hPow
+  npow := ⟨npow⟩
+  add, sub, mul, neg,
   add_comm, add_assoc, add_zero
   neg_add_cancel, sub_eq_add_neg
   mul_one, one_mul, zero_mul, mul_zero, mul_assoc,
diff --git a/src/Init/Grind/Ring/Field.lean b/src/Init/Grind/Ring/Field.lean
index e7e27bf5a1..c5ac5c7c8e 100644
--- a/src/Init/Grind/Ring/Field.lean
+++ b/src/Init/Grind/Ring/Field.lean
@@ -16,6 +16,7 @@ namespace Lean.Grind
 A field is a commutative ring with inverses for all non-zero elements.
 -/
 class Field (α : Type u) extends CommRing α, Inv α, Div α where
+  [zpow : HPow α Int α]
   /-- Division is multiplication by the inverse. -/
   div_eq_mul_inv : ∀ a b : α, a / b = a * b⁻¹
   /-- Zero is not equal to one: fields are non trivial.-/
@@ -24,8 +25,14 @@ class Field (α : Type u) extends CommRing α, Inv α, Div α where
   inv_zero : (0 : α)⁻¹ = 0
   /-- The inverse of a non-zero element is a right inverse. -/
   mul_inv_cancel : ∀ {a : α}, a ≠ 0 → a * a⁻¹ = 1
+  /-- The zeroth power of any element is one. -/
+  zpow_zero : ∀ a : α, a ^ (0 : Int) = 1
+  /-- The first power of any element is the element itself. -/
+  zpow_one : ∀ a : α, a ^ (1 : Int) = a
+  /-- Power to a sum is the product of the powers. -/
+  zpow_add : ∀ a : α, ∀ n m : Int, a ^ (n + m) = a ^ n * a ^ m
 
-attribute [instance 100] Field.toInv Field.toDiv
+attribute [instance 100] Field.toInv Field.toDiv Field.zpow
 
 namespace Field
 
@@ -119,6 +126,15 @@ theorem of_pow_eq_zero (a : α) (n : Nat) : a^n = 0 → a = 0 := by
     have := ih h
     contradiction
 
+theorem zpow_neg (a : α) (n : Int) : a ^ (-n) = (a ^ n)⁻¹ := by
+  apply eq_inv_of_mul_eq_one
+  rw [← zpow_add, Int.add_left_neg, zpow_zero]
+
+theorem zpow_natCast (a : α) (n : Nat) : a ^ (n : Int) = a ^ n := by
+  induction n
+  next => simp [zpow_zero, Semiring.pow_zero]
+  next n ih => rw [Int.natCast_add_one, zpow_add, ih, zpow_one, Semiring.pow_succ]
+
 instance [IsCharP α 0] : NoNatZeroDivisors α := NoNatZeroDivisors.mk' <| by
   intro a b h w
   have := IsCharP.natCast_eq_zero_iff (α := α) 0 a
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Util.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Util.lean
index 28a9cbc756..3e7dd5740e 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Util.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Util.lean
@@ -258,7 +258,7 @@ def getInvFn : m Expr := do
 
 private def mkPowFn (u : Level) (type : Expr) (semiringInst : Expr) : m Expr := do
   let inst ← MonadRing.synthInstance <| mkApp3 (mkConst ``HPow [u, 0, u]) type Nat.mkType type
-  let inst' := mkApp2 (mkConst ``Grind.Semiring.toHPow [u]) type semiringInst
+  let inst' := mkApp2 (mkConst ``Grind.Semiring.npow [u]) type semiringInst
   checkInst inst inst'
   canonExpr <| mkApp4 (mkConst ``HPow.hPow [u, 0, u]) type Nat.mkType type inst
 where
diff --git a/tests/lean/grind/algebra/exponents.lean b/tests/lean/grind/algebra/exponents.lean
new file mode 100644
index 0000000000..d6be041c02
--- /dev/null
+++ b/tests/lean/grind/algebra/exponents.lean
@@ -0,0 +1,29 @@
+open Lean.Grind
+
+section CommRing
+
+variable (R : Type) [CommRing R]
+
+example (a : R) (n : Nat) : a^(n + 1) = a^n * a := by grind
+example (a : R) (n m : Nat) : a^(n + m) = a^n * a^m := by grind
+example (a : R) (n m : Nat) : a^(n + m) = a^m * a^n := by grind
+example (a : R) (n m : Nat) : a^(n + m + n) = a^m * a^(2*n) := by grind
+
+example (n m : Nat) : (n+m)^2 = n^2 + 2*n*m + m^2 := by grind
+example (a : R) (n m : Nat) : a^((n+m)^2) = a^(n^2 + 2*n*m + m^2) := by grind
+example (a : R) (n m : Nat) : a^((n+m)^2) = a^(n^2) * a^(2*n*m) * a^(m^2) := by grind
+
+end CommRing
+
+
+section Field
+
+variable (F : Type) [Field F]
+
+example (a : F) (n m : Int) : a^(n + m - n) = a^m := by grind
+
+example (a : F) (n m : Int) : a^(n - m) = a^n / a^m := by grind
+
+example (a : F) (n m : Int) : a^((n - m) * (n + m)) = a^(n^2) / a^(m^2) := by grind
+
+end Field
diff --git a/tests/lean/grind/algebra/module_normalization.lean b/tests/lean/grind/algebra/module_normalization.lean
index 4a51eb7a03..fadc89d433 100644
--- a/tests/lean/grind/algebra/module_normalization.lean
+++ b/tests/lean/grind/algebra/module_normalization.lean
@@ -1,4 +1,4 @@
--- Tests for `grind` as a module normalization tactic, when only `NatModule`, `IntModule`, or `RatModule` is available.
+-- Tests for `grind` as a module normalization tactic, when only `NatModule` is available.
 
 open Lean.Grind
 
diff --git a/tests/lean/grind/algebra/nat_module.lean b/tests/lean/grind/algebra/nat_module.lean
index 1e0608adc7..68c20ae7d8 100644
--- a/tests/lean/grind/algebra/nat_module.lean
+++ b/tests/lean/grind/algebra/nat_module.lean
@@ -15,7 +15,7 @@ end IntModule
 -- We could solve these problems by embedding the NatModule in its Grothendieck completion.
 section NatModule
 
-variable (M : Type) [NatModule M]
+variable (M : Type) [NatModule M] [AddRightCancel M]
 
 example (x y : M) : 2 * x + 3 * y + x = 3 * (x + y) := by grind