From 8353964e5527df2bb6b406a14e07f01bcd421aef Mon Sep 17 00:00:00 2001 From: Kim Morrison <477956+kim-em@users.noreply.github.com> Date: Wed, 8 Apr 2026 20:14:10 +1000 Subject: [PATCH] feat: wire `PowIdentity` into `grind` ring solver (#13088) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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) --- .../Grind/Arith/CommRing/Internalize.lean | 20 +++++++++++++++++++ .../Tactic/Grind/Arith/CommRing/RingId.lean | 4 +++- .../Tactic/Grind/Arith/CommRing/Types.lean | 4 ++++ src/Lean/Meta/Tactic/Grind/Arith/Insts.lean | 14 +++++++++++++ tests/elab/grind_pow_identity.lean | 18 +++++++++++++++++ tests/elab/grind_ring_1.lean | 4 ++++ tests/elab/grind_ring_1.lean.out.expected | 4 ++-- 7 files changed, 65 insertions(+), 3 deletions(-) create mode 100644 tests/elab/grind_pow_identity.lean diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Internalize.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Internalize.lean index b52f0c5f65..ae846b6afe 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Internalize.lean +++ b/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}" diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.lean index 34ce52afad..df6f1b5b94 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean index 486a787764..9be02fd2c7 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean +++ b/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. -/ diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Insts.lean b/src/Lean/Meta/Tactic/Grind/Arith/Insts.lean index 09056ef447..1ea4ac8649 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Insts.lean +++ b/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 diff --git a/tests/elab/grind_pow_identity.lean b/tests/elab/grind_pow_identity.lean new file mode 100644 index 0000000000..6d83e6c8d8 --- /dev/null +++ b/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. diff --git a/tests/elab/grind_ring_1.lean b/tests/elab/grind_ring_1.lean index ec64e93611..e767c88a97 100644 --- a/tests/elab/grind_ring_1.lean +++ b/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 diff --git a/tests/elab/grind_ring_1.lean.out.expected b/tests/elab/grind_ring_1.lean.out.expected index 6f30193f46..a83fcb54fe 100644 --- a/tests/elab/grind_ring_1.lean.out.expected +++ b/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`