From 5ca6eadd504975eef91a31b31fbf659e8127287d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 28 Jun 2025 07:28:42 -0700 Subject: [PATCH] feat: equations ` = 0` in `grind ring` (#9062) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR implements support for equations ` = 0` in rings and fields of unknown characteristic. Examples: ```lean example [Field α] (a : α) : (2 * a)⁻¹ = a⁻¹ / 2 := by grind example [Field α] (a : α) : (2 : α) ≠ 0 → 1 / a + 1 / (2 * a) = 3 / (2 * a) := by grind example [CommRing α] (a b : α) (h₁ : a + 2 = a) (h₂ : 2*b + a = 0) : a = 0 := by grind example [CommRing α] (a b : α) (h₁ : a + 6 = a) (h₂ : b + 9 = b) (h₂ : 3*b + a = 0) : a = 0 := by grind example [CommRing α] (a b : α) (h₁ : a + 6 = a) (h₂ : b + 9 = b) (h₂ : 3*b + a = 0) : a = 0 := by grind example [CommRing α] (a b : α) (h₁ : a + 2 = a) (h₂ : b = 0) : 4*a + b = 0 := by grind example [CommRing α] (a b c : α) (h₁ : a + 6 = a) (h₂ : c = c + 9) (h : b + 3*c = 0) : 27*a + b = 0 := by grind ``` --- src/Init/Grind/Ring/Poly.lean | 13 ++-- .../Meta/Tactic/Grind/Arith/CommRing.lean | 1 - .../Tactic/Grind/Arith/CommRing/EqCnstr.lean | 73 ++++++++++++++----- .../Tactic/Grind/Arith/CommRing/Proof.lean | 24 +++++- .../Tactic/Grind/Arith/CommRing/Types.lean | 16 ++++ .../grind/algebra/field_normalization.lean | 9 --- tests/lean/run/grind_field_norm_2.lean | 22 ++++++ 7 files changed, 122 insertions(+), 36 deletions(-) delete mode 100644 tests/lean/grind/algebra/field_normalization.lean create mode 100644 tests/lean/run/grind_field_norm_2.lean diff --git a/src/Init/Grind/Ring/Poly.lean b/src/Init/Grind/Ring/Poly.lean index 92224a3700..8c2aba7cda 100644 --- a/src/Init/Grind/Ring/Poly.lean +++ b/src/Init/Grind/Ring/Poly.lean @@ -1385,11 +1385,6 @@ theorem eq_normEq0 {α} [CommRing α] (ctx : Context α) (c : Nat) (p₁ p₂ p simp [eq_normEq0_cert]; intro _ _; subst p₁ p; simp [Poly.denote]; intro h₁ h₂ rw [p₂.normEq0_eq] <;> assumption -theorem diseq_normEq0 {α} [CommRing α] (ctx : Context α) (c : Nat) (p₁ p₂ p : Poly) - : eq_normEq0_cert c p₁ p₂ p → p₁.denote ctx = 0 → p₂.denote ctx ≠ 0 → p.denote ctx ≠ 0 := by - simp [eq_normEq0_cert]; intro _ _; subst p₁ p; simp [Poly.denote]; intro h₁ h₂ - rw [p₂.normEq0_eq] <;> assumption - theorem gcd_eq_0 [CommRing α] (g n m a b : Int) (h : g = a * n + b * m) (h₁ : Int.cast (R := α) n = 0) (h₂ : Int.cast (R := α) m = 0) : Int.cast (R := α) g = 0 := by rw [← Ring.intCast_ofNat] at * @@ -1418,5 +1413,13 @@ theorem eq_gcd {α} [CommRing α] (ctx : Context α) (a b : Int) (p₁ p₂ p : next n m g => apply gcd_eq_0 g n m a b +def d_normEq0_cert (c : Nat) (p₁ p₂ p : Poly) : Bool := + p₂ == .num c && p == p₁.normEq0 c + +theorem d_normEq0 {α} [CommRing α] (ctx : Context α) (k : Int) (c : Nat) (init : Poly) (p₁ p₂ p : Poly) + : d_normEq0_cert c p₁ p₂ p → k * init.denote ctx = p₁.denote ctx → p₂.denote ctx = 0 → k * init.denote ctx = p.denote ctx := by + simp [d_normEq0_cert]; intro _ h₁ h₂; subst p p₂; simp [Poly.denote] + intro h; rw [p₁.normEq0_eq] <;> assumption + end CommRing end Lean.Grind diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing.lean index 2999714f5a..360aed8293 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing.lean @@ -28,7 +28,6 @@ builtin_initialize registerTraceClass `grind.ring.assert.trivial (inherited := t builtin_initialize registerTraceClass `grind.ring.assert.queue (inherited := true) builtin_initialize registerTraceClass `grind.ring.assert.basis (inherited := true) builtin_initialize registerTraceClass `grind.ring.assert.store (inherited := true) -builtin_initialize registerTraceClass `grind.ring.assert.discard (inherited := true) builtin_initialize registerTraceClass `grind.ring.simp builtin_initialize registerTraceClass `grind.ring.superpose builtin_initialize registerTraceClass `grind.ring.impEq diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean index b68cc29fef..573a79af46 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean @@ -96,10 +96,16 @@ def PolyDerivation.simplifyWith (d : PolyDerivation) (c : EqCnstr) : RingM PolyD trace_goal[grind.ring.simp] "{← r.p.denoteExpr}" return .step r.p r.k₁ d r.k₂ r.m₂ c +def PolyDerivation.simplifyNumEq0 (d : PolyDerivation) : RingM PolyDerivation := do + let some numEq0 := (← getRing).numEq0? | return d + let .num k := numEq0.p | return d + return .normEq0 (d.p.normEq0 k.natAbs) d numEq0 + /-- Simplified `d.p` using the current basis, and returns the extended polynomial derivation. -/ def PolyDerivation.simplify (d : PolyDerivation) : RingM PolyDerivation := do let mut d := d repeat + d ← d.simplifyNumEq0 if (← checkMaxSteps) then return d let some c ← d.p.findSimp? | trace_goal[grind.debug.ring.simp] "simplified{indentD (← d.denoteExpr)}" @@ -128,10 +134,16 @@ partial def EqCnstr.simplifyWithExhaustively (c₁ c₂ : EqCnstr) : RingM EqCns let some c ← c₁.simplifyWithCore c₂ | return c₁ c.simplifyWithExhaustively c₂ +def EqCnstr.simplifyUsingNumEq0 (c : EqCnstr) : RingM EqCnstr := do + let some c' := (← getRing).numEq0? | return c + let .num k := c'.p | return c + return { c with p := c.p.normEq0 k.natAbs, h := .numEq0 k.natAbs c' c } + /-- Simplify the given equation constraint using the current basis. -/ def EqCnstr.simplify (c : EqCnstr) : RingM EqCnstr := do let mut c := c repeat + c ← simplifyUsingNumEq0 c if (← checkMaxSteps) then return c let some c' ← c.p.findSimp? | trace_goal[grind.debug.ring.simp] "simplified{indentD (← c.denoteExpr)}" @@ -141,21 +153,25 @@ def EqCnstr.simplify (c : EqCnstr) : RingM EqCnstr := do /-- Returns `true` if `c.p` is the constant polynomial. -/ def EqCnstr.checkConstant (c : EqCnstr) : RingM Bool := do - let .num k := c.p | return false - if k == 0 then + let .num n := c.p | return false + if n == 0 then trace_goal[grind.ring.assert.trivial] "{← c.denoteExpr}" else if (← hasChar) then c.setUnsat - else if k.natAbs == 1 then - if (← isField) then - c.setUnsat - else - -- Remark: we currently don't do anything if the ring characteristic is not known. - -- TODO: we could set all terms of this ring `0` if `1 = 0`. - trace_goal[grind.ring.assert.discard] "{← c.denoteExpr}" + else if (← pure (n.natAbs == 1) <&&> isField) then + c.setUnsat else - -- TODO: we could save the equation for and use it to simplify polynomials - trace_goal[grind.ring.assert.discard] "{← c.denoteExpr}" + let mut c := c + let mut n := n + if n < 0 then + n := -n + c := { c with p := .num n, h := .mul (-1) c } + if let some c' := (← getRing).numEq0? then + let .num m := c'.p | unreachable! + let (g, a, b) := gcdExt n m + c := { c with p := .num g, h := .gcd a b c c' } + modifyRing fun s => { s with numEq0? := some c, numEq0Updated := true } + trace_goal[grind.ring.assert.store] "{← c.denoteExpr}" return true /-- @@ -259,23 +275,39 @@ def EqCnstr.addToBasisAfterSimp (c : EqCnstr) : RingM Unit := do trace_goal[grind.ring.assert.basis] "{← c.denoteExpr}" addToBasisCore c +private def checkNumEq0Updated : RingM Unit := do + if (← getRing).numEq0Updated then + -- `numEq0?` was updated, then we must move the basis back to the queue to be simplified. + let basis := (← getRing).basis + modifyRing fun s => { s with numEq0Updated := false, basis := {} } + for c in basis do + c.addToQueue + +abbrev withCheckingNumEq0 (k : RingM Unit) : RingM Unit := do + try + k + finally + checkNumEq0Updated + def EqCnstr.addToBasis (c : EqCnstr) : RingM Unit := do - let some c ← c.simplifyAndCheck | return () - c.addToBasisAfterSimp + withCheckingNumEq0 do + let some c ← c.simplifyAndCheck | return () + c.addToBasisAfterSimp def addNewEq (c : EqCnstr) : RingM Unit := do - let some c ← c.simplifyAndCheck | return () - if c.p.degree == 1 then - c.addToBasisAfterSimp - else - c.addToQueue + withCheckingNumEq0 do + let some c ← c.simplifyAndCheck | return () + if c.p.degree == 1 then + c.addToBasisAfterSimp + else + c.addToQueue /-- Returns `true` if `c.d.p` is the constant polynomial. -/ def DiseqCnstr.checkConstant (c : DiseqCnstr) : RingM Bool := do let .num k := c.d.p | return false if k == 0 then c.setUnsat - else + else if (← hasChar) then trace_goal[grind.ring.assert.trivial] "{← c.denoteExpr}" return true @@ -292,6 +324,7 @@ def addNewDiseq (c : DiseqCnstr) : RingM Unit := do let c ← c.simplify if (← c.checkConstant) then return () + trace[grind.ring.assert.store] "{← c.denoteExpr}" saveDiseq c @[export lean_process_ring_eq] @@ -354,7 +387,7 @@ def processNewDiseqImpl (a b : Expr) : GoalM Unit := do let some rb ← toRingExpr? b | return () let p ← (ra.sub rb).toPolyM if (← isField) then - unless p matches .num _ do + if !(p matches .num _) || !(← hasChar) then if rb matches .num 0 then diseqZeroToEq a b else diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean index 1fce5cd78c..441c94dd8e 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean @@ -164,11 +164,13 @@ partial def EqCnstr.toPreNullCert (c : EqCnstr) : ProofM PreNullCert := caching modify fun s => { s with hyps := s.hyps.push { h, lhs, rhs } } return PreNullCert.unit i (i+1) | .coreS _a _b _sa _sb _ra _rb => - throwError "NIY" + throwError "`grind +ringNull` is not supported yet for this goal" | .superpose k₁ m₁ c₁ k₂ m₂ c₂ => (← c₁.toPreNullCert).combine k₁ m₁ k₂ m₂ (← c₂.toPreNullCert) | .simp k₁ c₁ k₂ m₂ c₂ => (← c₁.toPreNullCert).combine k₁ .unit k₂ m₂ (← c₂.toPreNullCert) | .mul k c => (← c.toPreNullCert).mul k | .div k c => (← c.toPreNullCert).div k + | .gcd .. | .numEq0 .. => + throwError "`grind +ringNull` is not supported yet for this goal" def PolyDerivation.toPreNullCert (d : PolyDerivation) : ProofM PreNullCert := do match d with @@ -177,6 +179,8 @@ def PolyDerivation.toPreNullCert (d : PolyDerivation) : ProofM PreNullCert := do -- Recall that _p = k₁*d.getPoly + k₂*m₂*c.p trace[grind.debug.ring.proof] ">> k₁: {k₁}, {(← d.toPreNullCert).d}, {(← c₂.toPreNullCert).d}" (← d.toPreNullCert).combine k₁ .unit (-k₂) m₂ (← c₂.toPreNullCert) + | .normEq0 .. => + throwError "`grind +ringNull` is not supported yet for this goal" /-- Returns the multiplier `k` for the input polynomial. See comment at `PolyDerivation.step`. -/ def PolyDerivation.getMultiplier (d : PolyDerivation) : Int := @@ -186,6 +190,7 @@ where match d with | .input _ => acc | .step _ k₁ d .. => go d (k₁ * acc) + | .normEq0 _ d .. => go d acc def EqCnstr.mkNullCertExt (c : EqCnstr) : RingM NullCertExt := do let (nc, s) ← c.toPreNullCert.run {} @@ -432,6 +437,14 @@ partial def _root_.Lean.Meta.Grind.Arith.CommRing.EqCnstr.toExprProof (c : EqCns let some nzInst ← noZeroDivisorsInst? | throwNoNatZeroDivisors return mkApp6 h nzInst (← mkPolyDecl c₁.p) (toExpr k) (← mkPolyDecl c.p) reflBoolTrue (← toExprProof c₁) + | .gcd a b c₁ c₂ => + let h ← mkStepBasicPrefix ``Grind.CommRing.eq_gcd + return mkApp8 h (toExpr a) (toExpr b) (← mkPolyDecl c₁.p) (← mkPolyDecl c₂.p) (← mkPolyDecl c.p) + reflBoolTrue (← toExprProof c₁) (← toExprProof c₂) + | .numEq0 k c₁ c₂ => + let h ← mkStepBasicPrefix ``Grind.CommRing.eq_normEq0 + return mkApp7 h (toExpr k) (← mkPolyDecl c₁.p) (← mkPolyDecl c₂.p) (← mkPolyDecl c.p) + reflBoolTrue (← toExprProof c₁) (← toExprProof c₂) open Lean.Grind.CommRing in /-- @@ -455,6 +468,15 @@ private def derivToExprProof (d : PolyDerivation) : ProofM (Int × Poly × Expr) (toExpr k₂) (← mkMonDecl m₂) (← mkPolyDecl c₂.p) (← mkPolyDecl p) reflBoolTrue h₁ h₂ return (k₁*k, p₀, h) + | .normEq0 p d c => + let (k, p₀, h₁) ← derivToExprProof d + let h₂ ← c.toExprProof + let .num a := c.p | unreachable! + let h ← mkStepBasicPrefix ``Grind.CommRing.d_normEq0 + let h := mkApp9 h + (toExpr k) (toExpr a.natAbs) (← mkPolyDecl p₀) (← mkPolyDecl d.p) + (← mkPolyDecl c.p) (← mkPolyDecl p) reflBoolTrue h₁ h₂ + return (k, p₀, h) open Lean.Grind.CommRing in /-- diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean index ebc4acbfbe..8590389193 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean @@ -30,6 +30,8 @@ inductive EqCnstrProof where | simp (k₁ : Int) (c₁ : EqCnstr) (k₂ : Int) (m₂ : Mon) (c₂ : EqCnstr) | mul (k : Int) (e : EqCnstr) | div (k : Int) (e : EqCnstr) + | gcd (a b : Int) (c₁ c₂ : EqCnstr) + | numEq0 (k : Nat) (c₁ c₂ : EqCnstr) end instance : Inhabited EqCnstrProof where @@ -109,10 +111,18 @@ inductive PolyDerivation where grind can deduce that `x+y+z = 0` -/ step (p : Poly) (k₁ : Int) (d : PolyDerivation) (k₂ : Int) (m₂ : Mon) (c : EqCnstr) + | /-- + Given `c.p == .num k` + ``` + p = d.getPoly.normEq0 k + ``` + -/ + normEq0 (p : Poly) (d : PolyDerivation) (c : EqCnstr) def PolyDerivation.p : PolyDerivation → Poly | .input p => p | .step p .. => p + | .normEq0 p .. => p /-- A disequality `lhs ≠ rhs` asserted by the core. -/ structure DiseqCnstr where @@ -196,6 +206,12 @@ structure Ring where recheck : Bool := false /-- Inverse theorems that have been already asserted. -/ invSet : PHashSet Expr := {} + /-- + An equality of the form `c = 0`. It is used to simplify polynomial coefficients. + -/ + numEq0? : Option EqCnstr := none + /-- Flag indicating whether `numEq0?` has been updated. -/ + numEq0Updated : Bool := false deriving Inhabited /-- diff --git a/tests/lean/grind/algebra/field_normalization.lean b/tests/lean/grind/algebra/field_normalization.lean deleted file mode 100644 index 6b6a19992d..0000000000 --- a/tests/lean/grind/algebra/field_normalization.lean +++ /dev/null @@ -1,9 +0,0 @@ -open Lean.Grind - -variable (R : Type u) [Field R] --- We need to store equalities/disequalities such as `2 = 0` when characteristic is not unknown. --- The current implementation discards them. - -example (a : R) : (2 * a)⁻¹ = a⁻¹ / 2 := by grind - -example (a : R) (_ : (2 : R) ≠ 0) : 1 / a + 1 / (2 * a) = 3 / (2 * a) := by grind diff --git a/tests/lean/run/grind_field_norm_2.lean b/tests/lean/run/grind_field_norm_2.lean new file mode 100644 index 0000000000..a917cb202c --- /dev/null +++ b/tests/lean/run/grind_field_norm_2.lean @@ -0,0 +1,22 @@ +open Lean.Grind + +variable (R : Type u) [Field R] + +example (a : R) : (2 * a)⁻¹ = a⁻¹ / 2 := by grind + +example (a : R) (_ : (2 : R) ≠ 0) : 1 / a + 1 / (2 * a) = 3 / (2 * a) := by grind + +example [CommRing α] (a b : α) (h₁ : a + 2 = a) (h₂ : 2*b + a = 0) : a = 0 := by + grind + +example [CommRing α] (a b : α) (h₁ : a + 6 = a) (h₂ : b + 9 = b) (h₂ : 3*b + a = 0) : a = 0 := by + grind + +example [CommRing α] (a b : α) (h₁ : a + 6 = a) (h₂ : b + 9 = b) (h₂ : 3*b + a = 0) : a = 0 := by + grind + +example [CommRing α] (a b : α) (h₁ : a + 2 = a) (h₂ : b = 0) : 4*a + b = 0 := by + grind + +example [CommRing α] (a b c : α) (h₁ : a + 6 = a) (h₂ : c = c + 9) (h : b + 3*c = 0) : 27*a + b = 0 := by + grind