feat: wire PowIdentity into grind ring solver

src/Init/Grind/Ring/Basic.lean

@@ -564,6 +564,28 @@ end Ring
 
 end IsCharP
 
+/--
+`PowIdentity α p` states that `x ^ p = x` holds for all elements of `α`.
+
+The primary source of instances is Fermat's little theorem: for a finite field with `q` elements,
+`x ^ q = x` for every `x`. For `Fin p` or `ZMod p` with prime `p`, this gives `x ^ p = x`.
+
+The `grind` ring solver uses this typeclass to add the relation `x ^ p - x = 0` to the
+Groebner basis, which allows it to reduce high-degree polynomials. Mathlib can provide
+instances for general finite fields via `FiniteField.pow_card`.
+-/
+class PowIdentity (α : Type u) [CommSemiring α] (p : outParam Nat) : Prop where
+  /-- Every element satisfies `x ^ p = x`. -/
+  pow_eq (x : α) : x ^ p = x
+
+namespace PowIdentity
+
+variable [CommSemiring α] [PowIdentity α p]
+
+theorem pow (x : α) : x ^ p = x := pow_eq x
+
+end PowIdentity
+
 open AddCommGroup
 
 theorem no_int_zero_divisors {α : Type u} [IntModule α] [NoNatZeroDivisors α] {k : Int} {a : α}

src/Init/GrindInstances/Ring/Fin.lean

@@ -156,6 +156,12 @@ instance [i : NeZero n] : ToInt.Pow (Fin n) (.co 0 n) where
       rw [pow_succ, ToInt.Mul.toInt_mul, ih, ← ToInt.wrap_toInt,
         ← IntInterval.wrap_mul (by simp), Int.pow_succ, ToInt.wrap_toInt]
 
+instance : PowIdentity (Fin 2) 2 where
+  pow_eq x := by
+    match x with
+    | ⟨0, _⟩ => rfl
+    | ⟨1, _⟩ => rfl
+
 end Fin
 
 end Lean.Grind

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`