feat: wire PowIdentity into grind ring solver (#13088)

This PR wires the `PowIdentity` typeclass (from
https://github.com/leanprover/lean4/pull/13086) into the `grind` ring
solver's Groebner basis engine.

When a ring has a `PowIdentity α p` instance, the solver pushes `x ^ p =
x` as a new fact for each variable `x`, which becomes `x^p - x = 0` in
the Groebner basis. Since `p` is an `outParam`, instance discovery is
decoupled from `IsCharP` — the solver synthesizes `PowIdentity α ?p`
with a fresh metavar and lets instance search find both the instance and
the exponent.

This correctly handles non-prime finite fields: for `F_4` (char 2, 4
elements), Mathlib would provide `PowIdentity F_4 4` and the solver
would discover `p = 4`, not `p = 2`.

Note: the original motivating example `(x + y)^2 = x^128 + y^2` from
https://github.com/leanprover/lean4/issues/12842 does not yet work
because the `ToInt` module lifts `Fin 2` expressions to integers and
expands `x^128` via the binomial theorem before the ring solver can
reduce it. Addressing that is a separate deeper change.

🤖 Prepared with Claude Code

---------

Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Internalize.lean

@@ -112,6 +112,25 @@ private def processInv (e inst a : Expr) : RingM Unit := do
       return ()
   pushNewFact <| mkApp3 (mkConst ``Grind.CommRing.inv_split [ring.u]) ring.type fieldInst a
 
+/--
+For each new variable `x` in a ring with `PowIdentity α p`,
+push the equation `x ^ p = x` as a new fact into grind.
+-/
+private def processPowIdentityVars : RingM Unit := do
+  let ring ← getCommRing
+  let some (powIdentityInst, csInst, p) := ring.powIdentityInst? | return ()
+  let startIdx := ring.powIdentityVarCount
+  let vars := ring.toRing.vars
+  if startIdx >= vars.size then return ()
+  for i in [startIdx:vars.size] do
+    let x := vars[i]!
+    trace_goal[grind.ring] "PowIdentity: pushing x^{p} = x for {x}"
+    -- Construct proof: @PowIdentity.pow_eq α csInst p powIdentityInst x
+    let proof := mkApp5 (mkConst ``Grind.PowIdentity.pow_eq [ring.u])
+      ring.type csInst (mkNatLit p) powIdentityInst x
+    pushNewFact proof
+  modifyCommRing fun s => { s with powIdentityVarCount := vars.size }
+
 /-- Returns `true` if `e` is a term `a⁻¹`. -/
 private def internalizeInv (e : Expr) : GoalM Bool := do
   match_expr e with
@@ -138,6 +157,7 @@ def internalize (e : Expr) (parent? : Option Expr) : GoalM Unit := do
       denote := s.denote.insert { expr := e } re
       denoteEntries := s.denoteEntries.push (e, re)
     }
+    processPowIdentityVars
   else if let some semiringId ← getCommSemiringId? type then SemiringM.run semiringId do
     let some re ← sreify? e | return ()
     trace_goal[grind.ring.internalize] "semiring [{semiringId}]: {e}"

src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.lean

@@ -38,11 +38,13 @@ where
     let noZeroDivInst? ← getNoZeroDivInst? u type
     trace_goal[grind.ring] "NoNatZeroDivisors available: {noZeroDivInst?.isSome}"
     let fieldInst? ← synthInstance? <| mkApp (mkConst ``Grind.Field [u]) type
+    let powIdentityInst? ← getPowIdentityInst? u type
+    trace_goal[grind.ring] "PowIdentity available: {powIdentityInst?.isSome}"
     let semiringId? := none
     let id := (← get').rings.size
     let ring : CommRing := {
       id, semiringId?, type, u, semiringInst, ringInst, commSemiringInst,
-      commRingInst, charInst?, noZeroDivInst?, fieldInst?,
+      commRingInst, charInst?, noZeroDivInst?, fieldInst?, powIdentityInst?,
     }
     modify' fun s => { s with rings := s.rings.push ring }
     return some id

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean

@@ -214,6 +214,8 @@ structure CommRing extends Ring where
   noZeroDivInst? : Option Expr
   /-- `Field` instance for `type` if available. -/
   fieldInst?     : Option Expr
+  /-- `PowIdentity` instance, the synthesized `CommSemiring` instance, and exponent `p` if available. -/
+  powIdentityInst? : Option (Expr × Expr × Nat) := none
   /-- `denoteEntries` is `denote` as a `PArray` for deterministic traversal. -/
   denoteEntries  : PArray (Expr × RingExpr) := {}
   /-- Next unique id for `EqCnstr`s. -/
@@ -238,6 +240,8 @@ structure CommRing extends Ring where
   recheck        : Bool := false
   /-- Inverse theorems that have been already asserted. -/
   invSet         : PHashSet Expr := {}
+  /-- Number of variables for which `PowIdentity` equations have been pushed. -/
+  powIdentityVarCount : Nat := 0
   /--
   An equality of the form `c = 0`. It is used to simplify polynomial coefficients.
   -/

src/Lean/Meta/Tactic/Grind/Arith/Insts.lean

@@ -19,6 +19,20 @@ def getIsCharInst? (u : Level) (type : Expr) (semiringInst : Expr) : GoalM (Opti
   let some n ← evalNat? n | return none
   return some (charInst, n)
 
+def getPowIdentityInst? (u : Level) (type : Expr) : GoalM (Option (Expr × Expr × Nat)) := do withNewMCtxDepth do
+  -- We use a fresh metavar for `CommSemiring` (unlike `getIsCharInst?` which pins the semiring)
+  -- because `PowIdentity` instances may be declared against a canonical `CommSemiring` instance
+  -- that is not definitionally equal to `CommRing.toCommSemiring`. The synthesized `csInst` is
+  -- stored and used in proof terms to ensure type-correctness.
+  let csInst ← mkFreshExprMVar (mkApp (mkConst ``Grind.CommSemiring [u]) type)
+  let p ← mkFreshExprMVar (mkConst ``Nat)
+  let powIdentityType := mkApp3 (mkConst ``Grind.PowIdentity [u]) type csInst p
+  let some inst ← synthInstance? powIdentityType | return none
+  let csInst ← instantiateMVars csInst
+  let p ← instantiateMVars p
+  let some pVal ← evalNat? p | return none
+  return some (inst, csInst, pVal)
+
 def getNoZeroDivInst? (u : Level) (type : Expr) : GoalM (Option Expr) := do
   let natModuleType := mkApp (mkConst ``Grind.NatModule [u]) type
   let some natModuleInst ← synthInstance? natModuleType | return none

tests/elab/grind_pow_identity.lean

@@ -0,0 +1,18 @@
+module
+-- Test that grind can solve equations over Fin 2 using PowIdentity
+-- The PowIdentity instance for Fin 2 gives x^2 = x, which the ring solver
+-- uses to reduce high-degree polynomials.
+
+example (x y : Fin 2) : (x + y)^2 = x + y := by grind
+example (x : Fin 2) : x^2 = x := by grind
+example (x y : Fin 2) : x^2 + y^2 = x + y := by grind
+example (x y : Fin 2) : x * y + x * y = 0 := by grind
+example (x y : Fin 2) : (x + y)^2 = x^2 + y^2 := by grind
+
+-- Higher powers reduced by PowIdentity
+example (x : Fin 2) : x^4 = x := by grind
+example (x : Fin 2) : x^8 = x := by grind
+
+-- Note: `(x + y)^2 = x^128 + y^2` (the motivating example from #12842) does not yet work.
+-- The `ToInt` module lifts `Fin 2` expressions to integers and expands `x^128` via the
+-- binomial theorem before the `Fin 2` ring solver can reduce it, causing blowup.

tests/elab/grind_ring_1.lean

@@ -18,6 +18,7 @@ example (x : UInt8) : (x + 16)*(x - 16) = x^2 := by
 /--
 trace: [grind.ring] new ring: Int
 [grind.ring] NoNatZeroDivisors available: true
+[grind.ring] PowIdentity available: false
 -/
 #guard_msgs (trace) in
 set_option trace.grind.ring true in
@@ -30,10 +31,13 @@ example (x : BitVec 8) : (x + 16)*(x - 16) = x^2 := by
 /--
 trace: [grind.ring] new ring: Ring.OfSemiring.Q Nat
 [grind.ring] NoNatZeroDivisors available: true
+[grind.ring] PowIdentity available: false
 [grind.ring] new ring: Int
 [grind.ring] NoNatZeroDivisors available: true
+[grind.ring] PowIdentity available: false
 [grind.ring] new ring: BitVec 8
 [grind.ring] NoNatZeroDivisors available: false
+[grind.ring] PowIdentity available: false
 -/
 #guard_msgs (trace) in
 set_option trace.grind.ring true in

tests/elab/grind_ring_1.lean.out.expected

@@ -1,2 +1,2 @@
-grind_ring_1.lean:55:0-55:7: warning: declaration uses `sorry`
-grind_ring_1.lean:68:0-68:7: warning: declaration uses `sorry`
+grind_ring_1.lean:59:0-59:7: warning: declaration uses `sorry`
+grind_ring_1.lean:72:0-72:7: warning: declaration uses `sorry`