8353964e55
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>
101 lines
2.8 KiB
Text
101 lines
2.8 KiB
Text
module
|
||
set_option grind.debug true
|
||
|
||
open Std Lean.Grind
|
||
|
||
example [CommRing α] (x : α) : (x + 1)*(x - 1) = x^2 - 1 := by
|
||
grind
|
||
|
||
example [CommRing α] [IsCharP α 256] (x : α) : (x + 16)*(x - 16) = x^2 := by
|
||
grind
|
||
|
||
example (x : Int) : (x + 1)*(x - 1) = x^2 - 1 := by
|
||
grind
|
||
|
||
example (x : UInt8) : (x + 16)*(x - 16) = x^2 := by
|
||
grind
|
||
|
||
/--
|
||
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
|
||
example (x : Int) : (x + 1)^2 - 1 = x^2 + 2*x := by
|
||
grind
|
||
|
||
example (x : BitVec 8) : (x + 16)*(x - 16) = x^2 := by
|
||
grind
|
||
|
||
/--
|
||
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
|
||
example (x : BitVec 8) : (x + 1)^2 - 1 = x^2 + 2*x := by
|
||
grind
|
||
|
||
example (x : Int) : (x + 1)*(x - 1) = x^2 → False := by
|
||
grind
|
||
|
||
example (x y : Int) : (x + 1)*(x - 1)*y + y = y*x^2 + 1 → False := by
|
||
grind
|
||
|
||
example (x : UInt8) : (x + 1)*(x - 1) = x^2 → False := by
|
||
grind
|
||
|
||
example (x y : BitVec 8) : (x + 1)*(x - 1)*y + y = y*x^2 + 1 → False := by
|
||
grind
|
||
|
||
example [CommRing α] (x : α) : (x + 1)*(x - 1) = x^2 → False := by
|
||
fail_if_success grind
|
||
sorry
|
||
|
||
example [CommRing α] [IsCharP α 0] (x : α) : (x + 1)*(x - 1) = x^2 → False := by
|
||
grind
|
||
|
||
example [CommRing α] [IsCharP α 8] (x : α) : (x + 1)*(x - 1) = x^2 → False := by
|
||
grind
|
||
|
||
/-- trace: [grind.ring.assert.queue] -7 * x ^ 2 + 16 * y ^ 2 + x = 0 -/
|
||
#guard_msgs (trace) in
|
||
set_option trace.grind.ring.assert.queue true in
|
||
example (x y : Int) : x + 16*y^2 - 7*x^2 = 0 → False := by
|
||
fail_if_success grind -lia
|
||
sorry
|
||
|
||
/--
|
||
trace: [grind.debug.ring.basis] a ^ 2 * b + -1 = 0
|
||
[grind.debug.ring.basis] a * b ^ 2 + -1 * b = 0
|
||
[grind.debug.ring.basis] a * b + -1 * b = 0
|
||
[grind.debug.ring.basis] b + -1 = 0
|
||
[grind.debug.ring.basis] a + -1 = 0
|
||
-/
|
||
#guard_msgs (drop error, trace) in
|
||
set_option trace.grind.debug.ring.basis true in
|
||
example [CommRing α] (a b c : α)
|
||
: a^2*b = 1 → a*b^2 = b → False := by
|
||
grind
|
||
|
||
|
||
/--
|
||
trace: [grind.ring.assert.basis] a ^ 2 * b + -1 = 0
|
||
[grind.ring.assert.basis] a * b ^ 2 + -1 * b = 0
|
||
[grind.ring.assert.basis] a * b + -1 * b = 0
|
||
[grind.ring.assert.basis] b + -1 = 0
|
||
[grind.ring.assert.basis] a + -1 = 0
|
||
-/
|
||
#guard_msgs (drop error, trace) in
|
||
set_option trace.grind.ring.assert.basis true in
|
||
example [CommRing α] [LE α] [LT α] [IsPreorder α] [OrderedRing α] (a b c : α)
|
||
: a^2*b = 1 → a*b^2 = b → False := by
|
||
grind
|