feat: equations <num> = 0 in grind ring (#9062)
This PR implements support for equations `<num> = 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 ```
This commit is contained in:
Leonardo de Moura
GitHub
parent
22152b8bfb
commit
5ca6eadd50
7 changed files with 122 additions and 36 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
/--
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
/--
|
||||
|
|
|
|||
|
|
@ -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
|
||||
22
tests/lean/run/grind_field_norm_2.lean
Normal file
22
tests/lean/run/grind_field_norm_2.lean
Normal file
|
|
@ -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
|
||||
Loading…
Add table
Reference in a new issue