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>
This PR sets up the new integrated test/bench suite. It then migrates
all benchmarks and some related tests to the new suite. There's also
some documentation and some linting.
For now, a lot of the old tests are left alone so this PR doesn't become
even larger than it already is. Eventually, all tests should be migrated
to the new suite though so there isn't a confusing mix of two systems.
