From d64ae32965fe10024410ffd401cfab5277537a5e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 26 Apr 2025 15:52:00 -0700 Subject: [PATCH] feat: generate Nullstellensatz proof terms in `grind` (#8122) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR implements the generation of compact proof terms for Nullstellensatz certificates in the new commutative ring procedure in `grind`. Some examples: ```lean example [CommRing α] (x y : α) : x = 1 → y = 2 → 2*x + y = 4 := by grind +ring example [CommRing α] [IsCharP α 7] (x y : α) : 3*x = 1 → 3*y = 2 → x + y = 1 := by grind +ring example [CommRing α] [NoZeroNatDivisors α] (x y : α) : 3*x = 1 → 3*y = 2 → x + y = 1 := by grind +ring example (x y z : BitVec 8) : z = y → (x + 1)*(x - 1)*y + y = z*x^2 + 1 → False := by grind +ring ``` --- src/Init/Grind/CommRing/Basic.lean | 2 +- src/Init/Grind/CommRing/Poly.lean | 135 ++++++++++-------- .../Meta/Tactic/Grind/Arith/CommRing.lean | 1 + .../Grind/Arith/CommRing/DenoteExpr.lean | 3 + .../Tactic/Grind/Arith/CommRing/EqCnstr.lean | 51 ++++--- .../Tactic/Grind/Arith/CommRing/Proof.lean | 116 +++++++++++---- .../Tactic/Grind/Arith/CommRing/ToExpr.lean | 9 ++ .../Tactic/Grind/Arith/CommRing/Types.lean | 28 +++- .../Tactic/Grind/Arith/CommRing/Util.lean | 3 + tests/lean/run/grind_ring_2.lean | 44 ++++++ tests/lean/run/grind_som1.lean | 2 +- 11 files changed, 281 insertions(+), 113 deletions(-) create mode 100644 tests/lean/run/grind_ring_2.lean diff --git a/src/Init/Grind/CommRing/Basic.lean b/src/Init/Grind/CommRing/Basic.lean index 51d4475b79..5153edd3d4 100644 --- a/src/Init/Grind/CommRing/Basic.lean +++ b/src/Init/Grind/CommRing/Basic.lean @@ -325,7 +325,7 @@ class NoZeroNatDivisors (α : Type u) [CommRing α] where export NoZeroNatDivisors (no_zero_nat_divisors) -theorem no_zero_int_divisors (α : Type u) [CommRing α] [NoZeroNatDivisors α] {k : Int} (a : α) +theorem no_zero_int_divisors {α : Type u} [CommRing α] [NoZeroNatDivisors α] {k : Int} {a : α} : k ≠ 0 → k * a = 0 → a = 0 := by match k with | (k : Nat) => diff --git a/src/Init/Grind/CommRing/Poly.lean b/src/Init/Grind/CommRing/Poly.lean index e945bdfcc6..f217c67f32 100644 --- a/src/Init/Grind/CommRing/Poly.lean +++ b/src/Init/Grind/CommRing/Poly.lean @@ -700,33 +700,6 @@ theorem Expr.eq_of_toPoly_eq {α} [CommRing α] (ctx : Context α) (a b : Expr) simp [denote_toPoly] at h assumption -def ne_unsat_cert (a b : Expr) : Bool := - (a.sub b).toPoly == .num 0 - -theorem ne_unsat {α} [CommRing α] (ctx : Context α) (a b : Expr) - : ne_unsat_cert a b → a.denote ctx ≠ b.denote ctx → False := by - simp [ne_unsat_cert] - intro h - replace h := congrArg (Poly.denote ctx .) h - simp [Poly.denote, Expr.denote, Expr.denote_toPoly, intCast_zero, sub_eq_zero_iff] at h - assumption - -def eq_unsat_cert (a b : Expr) (k : Int) : Bool := - k != 0 && (a.sub b).toPoly == .num k - --- Remark: `[IsCharP α 0]` after `(ctx : Context α)` is not a mistake. --- The `grind` procedure assumes that support theorems start with `{α} [CommRing α] (ctx : Context α)` -theorem eq_unsat {α} [CommRing α] (ctx : Context α) [IsCharP α 0] (a b : Expr) (k : Int) - : eq_unsat_cert a b k → a.denote ctx = b.denote ctx → False := by - simp [eq_unsat_cert] - intro h₁ h₂ - replace h₂ := congrArg (Poly.denote ctx .) h₂ - simp [Poly.denote, Expr.denote, Expr.denote_toPoly, intCast_zero, sub_eq_iff] at h₂ - have := IsCharP.intCast_eq_zero_iff (α := α) 0 k - simp [h₁] at this - rw [h₂, Eq.comm, ← sub_eq_iff, sub_self, Eq.comm] - assumption - /-- Helper theorem for proving `NullCert` theorems. -/ theorem NullCert.eqsImplies_helper {α} [CommRing α] (ctx : Context α) (nc : NullCert) (p : Prop) : (nc.denote ctx = 0 → p) → nc.eqsImplies ctx p := by induction nc <;> simp [denote, eqsImplies] @@ -742,7 +715,7 @@ theorem NullCert.denote_toPoly {α} [CommRing α] (ctx : Context α) (nc : NullC def NullCert.eq_cert (nc : NullCert) (lhs rhs : Expr) := (lhs.sub rhs).toPoly == nc.toPoly -theorem NullCert.eq {α} [CommRing α] (ctx : Context α) (nc : NullCert) (lhs rhs : Expr) +theorem NullCert.eq {α} [CommRing α] (ctx : Context α) (nc : NullCert) {lhs rhs : Expr} : nc.eq_cert lhs rhs → nc.eqsImplies ctx (lhs.denote ctx = rhs.denote ctx) := by simp [eq_cert]; intro h₁ apply eqsImplies_helper @@ -751,6 +724,46 @@ theorem NullCert.eq {α} [CommRing α] (ctx : Context α) (nc : NullCert) (lhs r simp [Expr.denote_toPoly, denote_toPoly, h₂, Expr.denote, sub_eq_zero_iff] at h₁ assumption +theorem NullCert.eqsImplies_helper' {α} [CommRing α] {ctx : Context α} {nc : NullCert} {p q : Prop} : nc.eqsImplies ctx p → (p → q) → nc.eqsImplies ctx q := by + induction nc <;> simp [denote, eqsImplies] + next => intro h₁ h₂; exact h₂ h₁ + next ih => intro h₁ h₂ h₃; exact ih (h₁ h₃) h₂ + +theorem NullCert.ne_unsat {α} [CommRing α] (ctx : Context α) (nc : NullCert) (lhs rhs : Expr) + : nc.eq_cert lhs rhs → lhs.denote ctx ≠ rhs.denote ctx → nc.eqsImplies ctx False := by + intro h₁ h₂ + exact eqsImplies_helper' (eq ctx nc h₁) h₂ + +def NullCert.ne_nzdiv_unsat_cert (nc : NullCert) (k : Int) (lhs rhs : Expr) : Bool := + k ≠ 0 && (lhs.sub rhs).toPoly.mulConst k == nc.toPoly + +theorem NullCert.ne_nzdiv_unsat {α} [CommRing α] [NoZeroNatDivisors α] (ctx : Context α) (nc : NullCert) (k : Int) (lhs rhs : Expr) + : nc.ne_nzdiv_unsat_cert k lhs rhs → lhs.denote ctx ≠ rhs.denote ctx → nc.eqsImplies ctx False := by + simp [ne_nzdiv_unsat_cert] + intro h₁ h₂ h₃ + apply eqsImplies_helper + intro h₄ + replace h₂ := congrArg (Poly.denote ctx) h₂ + simp [Expr.denote_toPoly, Poly.denote_mulConst, denote_toPoly, h₄, Expr.denote] at h₂ + replace h₂ := no_zero_int_divisors h₁ h₂ + rw [sub_eq_zero_iff] at h₂ + exact h₃ h₂ + +def NullCert.eq_unsat_cert (nc : NullCert) (k : Int) : Bool := + k ≠ 0 && nc.toPoly == .num k + +theorem NullCert.eq_unsat {α} [CommRing α] [IsCharP α 0] (ctx : Context α) (nc : NullCert) (k : Int) + : nc.eq_unsat_cert k → nc.eqsImplies ctx False := by + simp [eq_unsat_cert] + intro h₁ h₂ + apply eqsImplies_helper + intro h₃ + replace h₂ := congrArg (Poly.denote ctx) h₂ + simp [Expr.denote_toPoly, Poly.denote_mulConst, denote_toPoly, Expr.denote, h₃, Poly.denote] at h₂ + have := IsCharP.intCast_eq_zero_iff (α := α) 0 k + simp [← h₂] at this + contradiction + /-! Theorems for justifying the procedure for commutative rings with a characteristic in `grind`. -/ @@ -877,45 +890,55 @@ theorem Expr.eq_of_toPolyC_eq {α c} [CommRing α] [IsCharP α c] (ctx : Context simp [denote_toPolyC] at h assumption -def ne_unsatC_cert (a b : Expr) (c : Nat) : Bool := - (a.sub b).toPolyC c == .num 0 - -theorem ne_unsatC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (a b : Expr) - : ne_unsatC_cert a b c → a.denote ctx ≠ b.denote ctx → False := by - simp [ne_unsatC_cert] - intro h - replace h := congrArg (Poly.denote ctx .) h - simp [Poly.denote, Expr.denote, Expr.denote_toPolyC, intCast_zero, sub_eq_zero_iff] at h - assumption - -def eq_unsatC_cert (a b : Expr) (c : Nat) (k : Int) : Bool := - k != 0 && k % c != 0 && (a.sub b).toPolyC c == .num k - -theorem eq_unsatC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (a b : Expr) (k : Int) - : eq_unsatC_cert a b c k → a.denote ctx = b.denote ctx → False := by - simp [eq_unsatC_cert] - intro h₁ h₂ h₃ - replace h₃ := congrArg (Poly.denote ctx .) h₃ - simp [Poly.denote, Expr.denote, Expr.denote_toPolyC, intCast_zero, sub_eq_iff] at h₃ - have := IsCharP.intCast_eq_zero_iff (α := α) c k - simp [h₁, h₂] at this - rw [h₃, Eq.comm, ← sub_eq_iff, sub_self, Eq.comm] - assumption - theorem NullCert.denote_toPolyC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (nc : NullCert) : (nc.toPolyC c).denote ctx = nc.denote ctx := by induction nc <;> simp [toPolyC, denote, Poly.denote, intCast_zero, Poly.denote_combineC, Poly.denote_mulC, Expr.denote_toPolyC, Expr.denote, *] def NullCert.eq_certC (nc : NullCert) (lhs rhs : Expr) (c : Nat) := - (lhs.sub rhs).toPolyC c == nc.toPoly + (lhs.sub rhs).toPolyC c == nc.toPolyC c -theorem NullCert.eqC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (nc : NullCert) (lhs rhs : Expr) +theorem NullCert.eqC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (nc : NullCert) {lhs rhs : Expr} : nc.eq_certC lhs rhs c → nc.eqsImplies ctx (lhs.denote ctx = rhs.denote ctx) := by simp [eq_certC]; intro h₁ apply eqsImplies_helper intro h₂ replace h₁ := congrArg (Poly.denote ctx) h₁ - simp [Expr.denote_toPolyC, denote_toPoly, h₂, Expr.denote, sub_eq_zero_iff] at h₁ + simp [Expr.denote_toPolyC, denote_toPolyC, h₂, Expr.denote, sub_eq_zero_iff] at h₁ assumption +theorem NullCert.ne_unsatC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (nc : NullCert) (lhs rhs : Expr) + : nc.eq_certC lhs rhs c → lhs.denote ctx ≠ rhs.denote ctx → nc.eqsImplies ctx False := by + intro h₁ h₂ + exact eqsImplies_helper' (eqC ctx nc h₁) h₂ + +def NullCert.ne_nzdiv_unsat_certC (nc : NullCert) (k : Int) (lhs rhs : Expr) (c : Nat) : Bool := + k ≠ 0 && ((lhs.sub rhs).toPolyC c).mulConstC k c == nc.toPolyC c + +theorem NullCert.ne_nzdiv_unsatC {α c} [CommRing α] [IsCharP α c] [NoZeroNatDivisors α] (ctx : Context α) (nc : NullCert) (k : Int) (lhs rhs : Expr) + : nc.ne_nzdiv_unsat_certC k lhs rhs c → lhs.denote ctx ≠ rhs.denote ctx → nc.eqsImplies ctx False := by + simp [ne_nzdiv_unsat_certC] + intro h₁ h₂ h₃ + apply eqsImplies_helper + intro h₄ + replace h₂ := congrArg (Poly.denote ctx) h₂ + simp [Expr.denote_toPolyC, Poly.denote_mulConstC, denote_toPolyC, h₄, Expr.denote] at h₂ + replace h₂ := no_zero_int_divisors h₁ h₂ + rw [sub_eq_zero_iff] at h₂ + exact h₃ h₂ + +def NullCert.eq_unsat_certC (nc : NullCert) (k : Int) (c : Nat) : Bool := + k % c != 0 && nc.toPolyC c == .num k + +theorem NullCert.eq_unsatC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (nc : NullCert) (k : Int) + : nc.eq_unsat_certC k c → nc.eqsImplies ctx False := by + simp [eq_unsat_certC] + intro h₁ h₂ + apply eqsImplies_helper + intro h₃ + replace h₂ := congrArg (Poly.denote ctx) h₂ + simp [Expr.denote_toPolyC, Poly.denote_mulConstC, denote_toPolyC, h₃, Poly.denote] at h₂ + have := IsCharP.intCast_eq_zero_iff (α := α) c k + simp [h₂] at this + contradiction + 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 8e703e62d3..bef5352c15 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing.lean @@ -30,5 +30,6 @@ builtin_initialize registerTraceClass `grind.ring.simp builtin_initialize registerTraceClass `grind.ring.superpose builtin_initialize registerTraceClass `grind.debug.ring.simp +builtin_initialize registerTraceClass `grind.debug.ring.proof end Lean diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/DenoteExpr.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/DenoteExpr.lean index 4e531a8889..e1003246bd 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/DenoteExpr.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/DenoteExpr.lean @@ -74,4 +74,7 @@ def EqCnstr.denoteExpr (c : EqCnstr) : RingM Expr := do def PolyDerivation.denoteExpr (d : PolyDerivation) : RingM Expr := do d.p.denoteExpr +def DiseqCnstr.denoteExpr (c : DiseqCnstr) : RingM Expr := do + return mkNot (← mkEq (← c.d.denoteExpr) (← denoteNum 0)) + end Lean.Meta.Grind.Arith.CommRing diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean index 10e0de2990..a80f9ca504 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean @@ -130,7 +130,7 @@ def EqCnstr.checkConstant (c : EqCnstr) : RingM Bool := do if k == 0 then trace_goal[grind.ring.assert.trivial] "{← c.denoteExpr}" else if (← hasChar) then - setUnsatEq c + c.setUnsat else -- Remark: we currently don't do anything if the characteristic is not known. trace_goal[grind.ring.assert.discard] "{← c.denoteExpr}" @@ -219,6 +219,28 @@ def addNewEq (c : EqCnstr) : RingM Unit := do 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 + trace_goal[grind.ring.assert.trivial] "{← c.denoteExpr}" + return true + +def DiseqCnstr.simplify (c : DiseqCnstr) : RingM DiseqCnstr := do + return { c with d := (← c.d.simplify) } + +def saveDiseq (c : DiseqCnstr) : RingM Unit := do + trace_goal[grind.ring.assert.store] "{← c.denoteExpr}" + modifyRing fun s => { s with diseqs := s.diseqs.push c } + +def addNewDiseq (c : DiseqCnstr) : RingM Unit := do + let c ← c.simplify + if (← c.checkConstant) then + return () + saveDiseq c + @[export lean_process_ring_eq] def processNewEqImpl (a b : Expr) : GoalM Unit := do if isSameExpr a b then return () -- TODO: check why this is needed @@ -228,17 +250,6 @@ def processNewEqImpl (a b : Expr) : GoalM Unit := do let some ra ← toRingExpr? a | return () let some rb ← toRingExpr? b | return () let p ← (ra.sub rb).toPolyM - -- TODO: delete this `if` after simplifier is fully integrated - if let .num k := p then - if k == 0 then - trace_goal[grind.ring.assert.trivial] "{← p.denoteExpr} = 0" - else if (← hasChar) then - trace_goal[grind.ring.assert.unsat] "{← p.denoteExpr} = 0" - setEqUnsat k a b ra rb - else - -- Remark: we currently don't do anything if the characteristic is not known. - trace_goal[grind.ring.assert.discard] "{← p.denoteExpr} = 0" - return () addNewEq (← mkEqCnstr p (.core a b ra rb)) @[export lean_process_ring_diseq] @@ -249,16 +260,10 @@ def processNewDiseqImpl (a b : Expr) : GoalM Unit := do let some ra ← toRingExpr? a | return () let some rb ← toRingExpr? b | return () let p ← (ra.sub rb).toPolyM - if let .num k := p then - if k == 0 then - trace_goal[grind.ring.assert.unsat] "{← p.denoteExpr} ≠ 0" - setNeUnsat a b ra rb - else - -- Remark: if the characteristic is known, it is trivial. - -- Otherwise, we don't do anything. - trace_goal[grind.ring.assert.trivial] "{← p.denoteExpr} ≠ 0" - return () - trace_goal[grind.ring.assert.store] "{← p.denoteExpr} ≠ 0" - -- TODO: save disequalitys + addNewDiseq { + lhs := a, rhs := b + rlhs := ra, rrhs := rb + d := .input p + } end Lean.Meta.Grind.Arith.CommRing diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean index 21b41d4cbc..73a6d00056 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean @@ -47,6 +47,9 @@ structure PreNullCert where d : Int := 1 deriving Inhabited +def PreNullCert.zero : PreNullCert := + { qs := #[] } + def PreNullCert.unit (i : Nat) (n : Nat) : PreNullCert := let qs := Array.replicate n (.num 0) let qs := qs.set! i (.num 1) @@ -131,6 +134,23 @@ partial def EqCnstr.toPreNullCert (c : EqCnstr) : ProofM PreNullCert := caching | .mul k c => (← c.toPreNullCert).mul k | .div k c => (← c.toPreNullCert).div k +def PolyDerivation.toPreNullCert (d : PolyDerivation) : ProofM PreNullCert := do + match d with + | .input _ => return .zero + | .step _p k₁ d k₂ m₂ c₂ => + -- 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) + +/-- Returns the multiplier `k` for the input polynomial. See comment at `PolyDerivation.step`. -/ +def PolyDerivation.getMultiplier (d : PolyDerivation) : Int := + go d 1 +where + go (d : PolyDerivation) (acc : Int) : Int := + match d with + | .input _ => acc + | .step _ k₁ d .. => go d (k₁ * acc) + structure NullCertExt where d : Int qhs : Array (Poly × NullCertHypothesis) @@ -139,6 +159,10 @@ def EqCnstr.mkNullCertExt (c : EqCnstr) : RingM NullCertExt := do let (nc, s) ← c.toPreNullCert.run {} return { d := nc.d, qhs := nc.qs.zip s.hyps } +def DiseqCnstr.mkNullCertExt (c : DiseqCnstr) : RingM NullCertExt := do + let (nc, s) ← c.d.toPreNullCert.run {} + return { d := nc.d, qhs := nc.qs.zip s.hyps } + def NullCertExt.toPoly (nc : NullCertExt) : RingM Poly := do let mut p : Poly := .num 0 for (q, h) in nc.qhs do @@ -150,33 +174,75 @@ def NullCertExt.check (c : EqCnstr) (nc : NullCertExt) : RingM Bool := do let p₂ ← nc.toPoly return p₁ == p₂ -def setUnsatEq (c : EqCnstr) : RingM Unit := do - trace_goal[grind.ring.assert.unsat] "{← c.denoteExpr}" - let nc ← c.mkNullCertExt - trace_goal[grind.ring.assert.unsat] "{nc.d}*({← c.p.denoteExpr}), {← (← nc.toPoly).denoteExpr}" - trace_goal[grind.ring.assert.unsat] "{nc.d}*({← c.p.denoteExpr}), {← nc.qhs.mapM fun (p, h) => return (← p.denoteExpr, ← h.lhs.denoteExpr, ← h.rhs.denoteExpr) }" - -- TODO +def NullCertExt.toNullCert (nc : NullCertExt) : Grind.CommRing.NullCert := + go nc.qhs.size .empty (by omega) +where + go (i : Nat) (acc : Grind.CommRing.NullCert) (h : i ≤ nc.qhs.size) : Grind.CommRing.NullCert := + if h : i > 0 then + let i := i - 1 + let (p, h) := nc.qhs[i] + go i (.add p h.lhs h.rhs acc) (by omega) + else + acc -private def mkLemmaPrefix (declName declNameC : Name) : RingM Expr := do +/-- +Given a `pr`, returns `pr h₁ ... hₙ`, where `n` is size `nc.qhs.size`, and `hᵢ`s +are the equalities in the certificate. +-/ +def NullCertExt.applyEqs (pr : Expr) (nc : NullCertExt) : Expr := + go 0 pr +where + go (i : Nat) (pr : Expr) : Expr := + if _ : i < nc.qhs.size then + let (_, h) := nc.qhs[i] + go (i + 1) (mkApp pr h.h) + else + pr + +private def getNoZeroDivInstIfNeeded? (k : Int) : RingM (Option Expr) := do + if k == 1 then + return none + else + let some inst ← noZeroDivisorsInst? + | throwError "`grind` internal error, `NoZeroNatDivisors` instance is needed, but it is not available for{indentExpr (← getRing).type}" + return some inst + +def EqCnstr.setUnsat (c : EqCnstr) : RingM Unit := do + trace_goal[grind.ring.assert.unsat] "{← c.denoteExpr}" + let .num k := c.p + | throwError "`grind` internal error, constant polynomial expected {indentExpr (← c.p.denoteExpr)}" + let ncx ← c.mkNullCertExt + trace_goal[grind.ring.assert.unsat] "{ncx.d}*({← c.p.denoteExpr}), {← (← ncx.toPoly).denoteExpr}" + let ring ← getRing + let some (charInst, char) := ring.charInst? + | throwError "`grind` internal error, `IsCharP` insrtance is needed, but it is not available for{indentExpr (← getRing).type}" + let h := if char == 0 then + mkApp (mkConst ``Grind.CommRing.NullCert.eq_unsat [ring.u]) ring.type + else + mkApp2 (mkConst ``Grind.CommRing.NullCert.eq_unsatC [ring.u]) ring.type (toExpr char) + let ctx ← toContextExpr + let nc := toExpr (ncx.toNullCert) + let h := mkApp6 h ring.commRingInst charInst ctx nc (toExpr k) reflBoolTrue + closeGoal <| ncx.applyEqs h + +def DiseqCnstr.setUnsat (c : DiseqCnstr) : RingM Unit := do + trace_goal[grind.ring.assert.unsat] "{← c.denoteExpr}" + let ncx ← c.mkNullCertExt + trace_goal[grind.ring.assert.unsat] "{ncx.d}*({← c.d.p.denoteExpr}), {← (← ncx.toPoly).denoteExpr}" + let nc := toExpr (ncx.toNullCert) let ring ← getRing let ctx ← toContextExpr - if let some (charInst, c) ← nonzeroCharInst? then - return mkApp5 (mkConst declNameC [ring.u]) ring.type (toExpr c) ring.commRingInst charInst ctx - else - return mkApp3 (mkConst declName [ring.u]) ring.type ring.commRingInst ctx - --- TODO: delete -def setNeUnsat (a b : Expr) (ra rb : RingExpr) : RingM Unit := do - let h ← mkLemmaPrefix ``Grind.CommRing.ne_unsat ``Grind.CommRing.ne_unsatC - closeGoal <| mkApp4 h (toExpr ra) (toExpr rb) reflBoolTrue (← mkDiseqProof a b) - --- TODO: delete -def setEqUnsat (k : Int) (a b : Expr) (ra rb : RingExpr) : RingM Unit := do - let mut h ← mkLemmaPrefix ``Grind.CommRing.eq_unsat ``Grind.CommRing.eq_unsatC - let (charInst, c) ← getCharInst - if c == 0 then - h := mkApp h charInst - closeGoal <| mkApp5 h (toExpr ra) (toExpr rb) (toExpr k) reflBoolTrue (← mkEqProof a b) - + let k := c.d.getMultiplier + let h := match (← nonzeroCharInst?), (← getNoZeroDivInstIfNeeded? k) with + | some (charInst, char), some nzDivInst => + mkApp8 (mkConst ``Grind.CommRing.NullCert.ne_nzdiv_unsatC [ring.u]) ring.type (toExpr char) ring.commRingInst charInst nzDivInst ctx nc (toExpr k) + | some (charInst, char), none => + mkApp6 (mkConst ``Grind.CommRing.NullCert.ne_unsatC [ring.u]) ring.type (toExpr char) ring.commRingInst charInst ctx nc + | none, some nzDivInst => + mkApp6 (mkConst ``Grind.CommRing.NullCert.ne_nzdiv_unsat [ring.u]) ring.type ring.commRingInst nzDivInst ctx nc (toExpr k) + | none, none => + mkApp4 (mkConst ``Grind.CommRing.NullCert.ne_unsat [ring.u]) ring.type ring.commRingInst ctx nc + let h := mkApp4 h (toExpr c.rlhs) (toExpr c.rrhs) reflBoolTrue (← mkDiseqProof c.lhs c.rhs) + closeGoal <| ncx.applyEqs h end Lean.Meta.Grind.Arith.CommRing diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/ToExpr.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/ToExpr.lean index 698affe3d5..5d8ce04d1b 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/ToExpr.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/ToExpr.lean @@ -54,4 +54,13 @@ instance : ToExpr CommRing.Expr where toExpr := ofRingExpr toTypeExpr := mkConst ``CommRing.Expr +def ofNullCert (nc : NullCert) : Expr := + match nc with + | .empty => mkConst ``CommRing.NullCert.empty + | .add q lhs rhs nc => mkApp4 (mkConst ``CommRing.NullCert.add) (toExpr q) (toExpr lhs) (toExpr rhs) (ofNullCert nc) + +instance : ToExpr CommRing.NullCert where + toExpr := ofNullCert + toTypeExpr := mkConst ``CommRing.NullCert + end Lean.Meta.Grind.Arith.CommRing diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean index 4bf269047c..489aaa2159 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean @@ -54,13 +54,13 @@ using the equations `x - 1 = 0` (`c₁`) and `y - 2 = 0` (`c₂`). ``` 2*x^2 + x*y | s₁ := .input (2*x^2 + x*y) = - 2*x*(x - 1) -(2*x + x*y) | s₂ := .simp (2*x + x*y) c₁ 1 (-2) x s₁ +(2*x + x*y) | s₂ := .step (2*x + x*y) 1 s₁ (-2) x c₁ = - 2*1*(x - 1) -(x*y + 2) | s₃ := .simp (x*y + 2) c₁ 1 (-2) 1 s₂ +(x*y + 2) | s₃ := .step (x*y + 2) 1 s₂ (-2) 1 c₁ = - 1*y*(x - 1) -(y + 2) | s₄ := .simp (y+2) c₁ 1 (-1) y s₃ +(y + 2) | s₄ := .step (y+2) 1 s₃ (-1) y c₁ = - 1*1*(y - 2) -4 | s₅ := .simp 4 c₂ 1 1 1 s₄ +4 | s₅ := .step 4 1 s₄ 1 1 c₂ ``` From the chain above, we build the certificate ``` @@ -88,12 +88,12 @@ inductive PolyDerivation where x + y + z | s₁ := .input (x + y + z) *2 = - 1*1*(2*x - 1) - 2*y + 2*z + 1 | s₂ := .simp (2*y + 2*z + 1) c₁ 2 (-1) 1 s₁ + 2*y + 2*z + 1 | s₂ := .step (2*y + 2*z + 1) 2 s₁ (-1) 1 c₁ *3 = - 2*1*(3*y - 1) - 6*z + 5 | s₃ := .simp (6*z + 5) c₂ 3 (-2) 1 s₂ + 6*z + 5 | s₃ := .step (6*z + 5) 3 s₂ (-2) 1 c₂ = - 1*1*(6*z + 5) - 0 | s₄ := .simp (0) c₃ 1 (-1) 1 s₃ + 0 | s₄ := .step (0) 1 s₃ (-1) 1 c₃ ``` For this chain, we build the certificate ``` @@ -115,6 +115,17 @@ def PolyDerivation.p : PolyDerivation → Poly | .input p => p | .step p .. => p +/-- A disequality `lhs ≠ rhs` asserted by the core. -/ +structure DiseqCnstr where + lhs : Expr + rhs : Expr + /-- Reified `lhs` -/ + rlhs : RingExpr + /-- Reified `rhs` -/ + rrhs : RingExpr + /-- `lhs - rhs` simplication chain. If it becomes `0` we have an inconsistency. -/ + d : PolyDerivation + /-- State for each `CommRing` processed by this module. -/ structure Ring where id : Nat @@ -154,6 +165,9 @@ structure Ring where in the leading monomial is `x`. -/ varToBasis : PArray (List EqCnstr) := {} + /-- Disequalities. -/ + -- TODO: add indexing + diseqs : PArray DiseqCnstr := {} deriving Inhabited /-- State for all `CommRing` types detected by `grind`. -/ diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Util.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Util.lean index d2754cae14..1bdcc58aee 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Util.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Util.lean @@ -61,6 +61,9 @@ def nonzeroCharInst? : RingM (Option (Expr × Nat)) := do return some (inst, c) return none +def noZeroDivisorsInst? : RingM (Option Expr) := do + return (← getRing).noZeroDivInst? + /-- Returns `true` if the current ring satifies the property ``` diff --git a/tests/lean/run/grind_ring_2.lean b/tests/lean/run/grind_ring_2.lean new file mode 100644 index 0000000000..8580e82993 --- /dev/null +++ b/tests/lean/run/grind_ring_2.lean @@ -0,0 +1,44 @@ +set_option grind.warning false +open Lean.Grind + +example [CommRing α] [NoZeroNatDivisors α] (x y : α) : 3*x = 1 → 3*y = 2 → x + y = 1 := by + grind +ring + +example [CommRing α] (x y : α) : 3*x = 1 → 3*y = 2 → x + y = 1 := by + fail_if_success grind +ring + sorry + +example [CommRing α] (x y : α) : x = 1 → y = 2 → 2*x + y = 4 := by + grind +ring + +example [CommRing α] [IsCharP α 7] (x y : α) : 3*x = 1 → 3*y = 2 → x + y = 1 := by + grind +ring + +example [CommRing α] [IsCharP α 7] (x y : α) : 2*x = 1 → 2*y = 1 → x + y = 1 := by + grind +ring + +example [CommRing α] [IsCharP α 8] (x y : α) : 2*x = 1 → 2*y = 1 → x + y = 1 := by + fail_if_success grind +ring + sorry + +example [CommRing α] [IsCharP α 8] [NoZeroNatDivisors α] (x y : α) : 2*x = 1 → 2*y = 1 → x + y = 1 := by + grind +ring + +example (x y : UInt8) : 3*x = 1 → 3*y = 2 → x + y = 1 := by + grind +ring + +example (x y : UInt8) : 3*x = 1 → 3*y = 2 → False := by + fail_if_success grind +ring + sorry + +example [CommRing α] [NoZeroNatDivisors α] (x y : α) : 6*x = 1 → 3*y = 2 → 2*x + y = 1 := by + grind +ring + +example [CommRing α] [NoZeroNatDivisors α] (x y : α) : 600000*x = 1 → 300*y = 2 → 200000*x + 100*y = 1 := by + grind +ring + +example (x y : Int) : y = 0 → (x + 1)*(x - 1) + y = x^2 → False := by + grind +ring + +example (x y z : BitVec 8) : z = y → (x + 1)*(x - 1)*y + y = z*x^2 + 1 → False := by + grind +ring diff --git a/tests/lean/run/grind_som1.lean b/tests/lean/run/grind_som1.lean index ec13618942..bd4b000213 100644 --- a/tests/lean/run/grind_som1.lean +++ b/tests/lean/run/grind_som1.lean @@ -37,4 +37,4 @@ def nc : NullCert := .add q₁ lhs₁ rhs₁ (.add q₂ lhs₂ rhs₂ .empty) example (x y : Int) : x = y → y - x*y + y^2 = 1 → y = 1 := let ctx := #R[x, y] - nc.eq ctx lhs rhs (Eq.refl true) + nc.eq ctx (lhs := lhs) (rhs := rhs) (Eq.refl true)