diff --git a/src/Init/Grind/Tactics.lean b/src/Init/Grind/Tactics.lean index 956c7e622e..60e9976de2 100644 --- a/src/Init/Grind/Tactics.lean +++ b/src/Init/Grind/Tactics.lean @@ -102,11 +102,6 @@ structure Config where ring := true ringSteps := 10000 /-- - When `true` (default: `false`), the commutative ring procedure in `grind` constructs stepwise - proof terms, instead of a single-step Nullstellensatz certificate - -/ - ringNull := false - /-- When `true` (default: `true`), uses procedure for handling linear arithmetic for `IntModule`, and `CommRing`. -/ diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean index bbdc5a3767..e117b0624a 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean @@ -341,7 +341,6 @@ def processNewEqImpl (a b : Expr) : GoalM Unit := do let p ← (ra.sub rb).toPolyM addNewEq (← mkEqCnstr p (.core a b ra rb)) else if let some semiringId ← inSameSemiring? a b then SemiringM.run semiringId do - if (← getConfig).ringNull then return () -- TODO: remove after we add Nullstellensatz certificates for semiring adapter trace_goal[grind.ring.assert] "{← mkEq a b}" let some sa ← toSemiringExpr? a | return () let some sb ← toSemiringExpr? b | return () @@ -405,7 +404,6 @@ def processNewDiseqImpl (a b : Expr) : GoalM Unit := do } else if let some semiringId ← inSameSemiring? a b then SemiringM.run semiringId do if (← getAddRightCancelInst?).isSome then - if (← getConfig).ringNull then return () -- TODO: remove after we add Nullstellensatz certificates for semiring adapter trace_goal[grind.ring.assert] "{mkNot (← mkEq a b)}" let some sa ← toSemiringExpr? a | return () let some sb ← toSemiringExpr? b | return () diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean index f44e81afda..85b8204d6b 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean @@ -19,181 +19,27 @@ import Lean.Meta.Tactic.Grind.Arith.CommRing.VarRename public section namespace Lean.Meta.Grind.Arith.CommRing - -def toContextExprCore (vars : Array Expr) : RingM Expr := do +/-- +Returns a context of type `RArray α` containing the variables `vars` where +`α` is the type of the ring. +-/ +private def toContextExpr (vars : Array Expr) : RingM Expr := do let ring ← getRing if h : 0 < vars.size then RArray.toExpr ring.type id (RArray.ofFn (vars[·]) h) else RArray.toExpr ring.type id (RArray.leaf (mkApp (← getNatCastFn) (toExpr 0))) -/-- -Returns a context of type `RArray α` containing the variables of the given ring. -`α` is the type of the ring. --/ -def toContextExpr : RingM Expr := do - toContextExprCore (← getRing).vars.toArray - -private def toSContextExprCore' (vars : Array Expr) : SemiringM Expr := do +private def toSContextExpr' (vars : Array Expr) : SemiringM Expr := do let semiring ← getSemiring if h : 0 < vars.size then RArray.toExpr semiring.type id (RArray.ofFn (vars[·]) h) else RArray.toExpr semiring.type id (RArray.leaf (mkApp (← getNatCastFn') (toExpr 0))) -private def toSContextExpr' : SemiringM Expr := do - toSContextExprCore' (← getSemiring).vars.toArray - /-- Similar to `toContextExpr`, but for semirings. -/ private def toSContextExpr (semiringId : Nat) (vars : Array Expr) : RingM Expr := do - SemiringM.run semiringId do toSContextExprCore' vars - -def throwNoNatZeroDivisors : RingM α := do - throwError "`grind` internal error, `NoNatZeroDivisors` instance is needed, but it is not available for{indentExpr (← getRing).type}" - -def getPolyConst (p : Poly) : RingM Int := do - let .num k := p - | throwError "`grind` internal error, constant polynomial expected {indentExpr (← p.denoteExpr)}" - return k - -namespace Null -/-! -Proof term for a Nullstellensatz certificate. --/ - -/-- -A "pre" Nullstellensatz certificate. -Recall that, given the hypotheses `h₁ : lhs₁ = rhs₁` ... `hₙ : lhsₙ = rhsₙ`, -a Nullstellensatz certificate is of the form -``` -q₁*(lhs₁ - rhs₁) + ... + qₙ*(lhsₙ - rhsₙ) -``` -Each hypothesis is an `EqCnstr` justified by a `.core ..` `EqnCnstrProof`. -We dynamically associate them with unique indices based on the order we find them -during traversal. -For the other `EqCnstr`s we compute a "pre" certificate as a dense array -containing `q₁` ... `qₙ` needed to create the `EqCnstr`. - -We are assuming the number of hypotheses used to derive a conclusion is small -and a dense array is a reasonable representation. --/ -structure PreNullCert where - qs : Array Poly - /-- - We don't use rational coefficients in the polynomials. - Thus, we need to track a denominator to justify the proof step `div`. - -/ - 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) - { qs } - -def PreNullCert.div (c : PreNullCert) (k : Int) : RingM PreNullCert := do - return { c with d := c.d * k } - -def PreNullCert.mul (c : PreNullCert) (k : Int) : RingM PreNullCert := do - if k == 1 then - return c - else - let g := Int.gcd k c.d - let k := k / g - let d := c.d / g - if k == 1 then - return { c with d } - else - let qs ← c.qs.mapM fun q => q.mulConstM k - return { qs, d } - -def PreNullCert.combine (k₁ : Int) (m₁ : Mon) (c₁ : PreNullCert) (k₂ : Int) (m₂ : Mon) (c₂ : PreNullCert) : RingM PreNullCert := do - let d₁ := c₁.d - let d₂ := c₂.d - let k₁_d₂ := k₁*d₂ - let k₂_d₁ := k₂*d₁ - let d₁_d₂ := d₁*d₂ - let g := Int.gcd (Int.gcd k₁_d₂ k₂_d₁) d₁_d₂ - let k₁ := k₁_d₂ / g - let k₂ := k₂_d₁ / g - let d := d₁_d₂ / g - let qs₁ := c₁.qs - let qs₂ := c₂.qs - let n := Nat.max qs₁.size qs₂.size - let mut qs : Vector Poly n := Vector.replicate n (.num 0) - for h : i in *...n do - if h₁ : i < qs₁.size then - let q₁ ← qs₁[i].mulMonM k₁ m₁ - if h₂ : i < qs₂.size then - let q₂ ← qs₂[i].mulMonM k₂ m₂ - qs := qs.set i (← q₁.combineM q₂) - else - qs := qs.set i q₁ - else - have : i < n := Std.PRange.lt_upper_of_mem h - have : qs₁.size = n ∨ qs₂.size = n := by simp +zetaDelta only [Nat.max_def, right_eq_ite_iff]; split <;> simp [*] - have : i < qs₂.size := by omega - let q₂ ← qs₂[i].mulMonM k₂ m₂ - qs := qs.set i q₂ - return { qs := qs.toArray, d } - -structure NullCertHypothesis where - h : Expr - lhs : RingExpr - rhs : RingExpr - -structure ProofM.State where - /-- Mapping from `EqCnstr` to `PreNullCert` -/ - cache : Std.HashMap UInt64 PreNullCert := {} - hyps : Array NullCertHypothesis := #[] - -abbrev ProofM := StateRefT ProofM.State RingM - -private abbrev caching (c : α) (k : ProofM PreNullCert) : ProofM PreNullCert := do - let addr := unsafe (ptrAddrUnsafe c).toUInt64 >>> 2 - if let some h := (← get).cache[addr]? then - return h - else - let h ← k - modify fun s => { s with cache := s.cache.insert addr h } - return h - -structure NullCertExt where - d : Int - qhs : Array (Poly × NullCertHypothesis) - -end Null - -section -open Null -partial def EqCnstr.toPreNullCert (c : EqCnstr) : ProofM PreNullCert := caching c do - match c.h with - | .core a b lhs rhs => - let i := (← get).hyps.size - let h ← mkEqProof a b - 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 "`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 - | .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) - | .normEq0 .. => - throwError "`grind +ringNull` is not supported yet for this goal" + SemiringM.run semiringId do toSContextExpr' vars /-- Returns the multiplier `k` for the input polynomial. See comment at `PolyDerivation.step`. -/ def PolyDerivation.getMultiplier (d : PolyDerivation) : Int := @@ -205,126 +51,13 @@ where | .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 {} - return { d := nc.d, qhs := nc.qs.zip s.hyps } +private def throwNoNatZeroDivisors : RingM α := do + throwError "`grind` internal error, `NoNatZeroDivisors` instance is needed, but it is not available for{indentExpr (← getRing).type}" -def PolyDerivation.mkNullCertExt (d : PolyDerivation) : RingM NullCertExt := do - let (nc, s) ← d.toPreNullCert.run {} - return { d := nc.d, qhs := nc.qs.zip s.hyps } - -def DiseqCnstr.mkNullCertExt (c : DiseqCnstr) : RingM NullCertExt := - c.d.mkNullCertExt -end - -namespace Null -def NullCertExt.toPoly (nc : NullCertExt) : RingM Poly := do - let mut p : Poly := .num 0 - for (q, h) in nc.qhs do - p ← p.combineM (← q.mulM (← (h.lhs.sub h.rhs).toPolyM)) - return p - -def NullCertExt.check (c : EqCnstr) (nc : NullCertExt) : RingM Bool := do - let p₁ := c.p.mulConst' nc.d (← nonzeroChar?) - let p₂ ← nc.toPoly - return p₁ == p₂ - -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 - -/-- -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? | throwNoNatZeroDivisors - return some inst - -def setEqUnsat (c : EqCnstr) : RingM Unit := do - trace_goal[grind.ring.assert.unsat] "{← c.denoteExpr}" - let k ← getPolyConst c.p - 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` instance is needed, but it is not available for{indentExpr (← getRing).type}\nconsider not using `+ringNull`" - 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) eagerReflBoolTrue - closeGoal <| ncx.applyEqs h - -def setDiseqUnsat (c : DiseqCnstr) : RingM Unit := do - trace_goal[grind.ring.assert.unsat] "{← c.denoteExpr}" - let ncx ← c.mkNullCertExt - trace_goal[grind.ring.assert.unsat] "multiplier: {c.d.getMultiplier}, {ncx.d}*({← c.d.p.denoteExpr}), {← (← ncx.toPoly).denoteExpr}" - let nc := toExpr (ncx.toNullCert) - let ring ← getRing - let ctx ← toContextExpr - let k := c.d.getMultiplier * ncx.d - 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) eagerReflBoolTrue (← mkDiseqProof c.lhs c.rhs) - closeGoal <| ncx.applyEqs h - -def propagateEq (a b : Expr) (ra rb : RingExpr) (d : PolyDerivation) : RingM Unit := do - let ncx ← d.mkNullCertExt - let nc := toExpr (ncx.toNullCert) - let ring ← getRing - let ctx ← toContextExpr - let k := d.getMultiplier * ncx.d - let h := match (← nonzeroCharInst?), (← getNoZeroDivInstIfNeeded? k) with - | some (charInst, char), some nzDivInst => - mkApp8 (mkConst ``Grind.CommRing.NullCert.eq_nzdivC [ring.u]) ring.type (toExpr char) ring.commRingInst charInst nzDivInst ctx nc (toExpr k) - | some (charInst, char), none => - mkApp6 (mkConst ``Grind.CommRing.NullCert.eqC [ring.u]) ring.type (toExpr char) ring.commRingInst charInst ctx nc - | none, some nzDivInst => - mkApp6 (mkConst ``Grind.CommRing.NullCert.eq_nzdiv [ring.u]) ring.type ring.commRingInst nzDivInst ctx nc (toExpr k) - | none, none => - mkApp4 (mkConst ``Grind.CommRing.NullCert.eq [ring.u]) ring.type ring.commRingInst ctx nc - let h := mkApp3 h (toExpr ra) (toExpr rb) eagerReflBoolTrue - trace_goal[grind.debug.ring.impEq] "{a}, {b}" - let eq := mkApp3 (mkConst ``Eq [.succ ring.u]) ring.type a b - pushEq a b <| mkExpectedPropHint (ncx.applyEqs h) eq - -end Null - -namespace Stepwise -/-! -Alternative proof term construction where we generate a sub-term for each step in -the derivation. --/ +private def getPolyConst (p : Poly) : RingM Int := do + let .num k := p + | throwError "`grind` internal error, constant polynomial expected {indentExpr (← p.denoteExpr)}" + return k structure ProofM.State where cache : Std.HashMap UInt64 Expr := {} @@ -369,16 +102,16 @@ local macro "declare! " decls:ident a:ident : term => modify fun s => { s with $decls:ident := (s.$decls).insert $a x }; return x) -def mkPolyDecl (p : Poly) : ProofM Expr := do +private def mkPolyDecl (p : Poly) : ProofM Expr := do declare! polyDecls p -def mkExprDecl (e : RingExpr) : ProofM Expr := do +private def mkExprDecl (e : RingExpr) : ProofM Expr := do declare! exprDecls e -def mkSExprDecl (e : SemiringExpr) : ProofM Expr := do +private def mkSExprDecl (e : SemiringExpr) : ProofM Expr := do declare! sexprDecls e -def mkMonDecl (m : Mon) : ProofM Expr := do +private def mkMonDecl (m : Mon) : ProofM Expr := do declare! monDecls m private def mkStepBasicPrefix (declName : Name) : ProofM Expr := do @@ -516,7 +249,7 @@ private def mkContext (h : Expr) : ProofM Expr := do if h.hasLooseBVars then let ring ← getRing let ctxType := mkApp (mkConst ``RArray [ring.u]) ring.type - let ctxVal ← toContextExprCore vars + let ctxVal ← toContextExpr vars return .letE `ctx ctxType ctxVal h (nondep := false) else return h @@ -549,7 +282,7 @@ where mkSemiringContext h open Lean.Grind.CommRing in -def setEqUnsat (c : EqCnstr) : RingM Unit := do +def EqCnstr.setUnsat (c : EqCnstr) : RingM Unit := do let h ← withProofContext do let ring ← getRing if let some (charInst, char) := ring.charInst? then @@ -565,7 +298,7 @@ def setEqUnsat (c : EqCnstr) : RingM Unit := do throwError "`grind ring` internal error, unexpected unsat eq proof {← c.denoteExpr}" closeGoal h -def setDiseqUnsat (c : DiseqCnstr) : RingM Unit := do +def DiseqCnstr.setUnsat (c : DiseqCnstr) : RingM Unit := do let h ← withProofContext do let heq ← mkImpEqExprProof c.rlhs c.rrhs c.d let hne ← if let some (sa, sb) := c.ofSemiring? then @@ -583,34 +316,21 @@ def propagateEq (a b : Expr) (ra rb : RingExpr) (d : PolyDerivation) : RingM Uni let eq := mkApp3 (mkConst ``Eq [.succ ring.u]) ring.type a b pushEq a b <| mkExpectedPropHint heq eq -end Stepwise - -def EqCnstr.setUnsat (c : EqCnstr) : RingM Unit := do - if (← getConfig).ringNull then - Null.setEqUnsat c - else - Stepwise.setEqUnsat c - -def DiseqCnstr.setUnsat (c : DiseqCnstr) : RingM Unit := do - if (← getConfig).ringNull then - Null.setDiseqUnsat c - else - Stepwise.setDiseqUnsat c - -def propagateEq (a b : Expr) (ra rb : RingExpr) (d : PolyDerivation) : RingM Unit := do - if (← getConfig).ringNull then - Null.propagateEq a b ra rb d - else - Stepwise.propagateEq a b ra rb d - /-- Given `a` and `b`, such that `a ≠ b` in the core and `sa` and `sb` their reified semiring terms s.t. `sa.toPoly == sb.toPoly`, close the goal. -/ def setSemiringDiseqUnsat (a b : Expr) (sa sb : SemiringExpr) : SemiringM Unit := do - let ctx ← toSContextExpr' let semiring ← getSemiring let hne ← mkDiseqProof a b + let usedVars := sa.collectVars >> sb.collectVars <| {} + let vars' := usedVars.toArray + let varRename := mkVarRename vars' + let vars := (← getSemiring).vars + let vars := vars'.map fun x => vars[x]! + let sa := sa.renameVars varRename + let sb := sb.renameVars varRename + let ctx ← toSContextExpr' vars let h := mkApp3 (mkConst ``Grind.Ring.OfSemiring.eq_normS [semiring.u]) semiring.type semiring.commSemiringInst ctx let h := mkApp3 h (toExpr sa) (toExpr sb) eagerReflBoolTrue closeGoal (mkApp hne h) diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index 79a0e58edd..ad491b0de1 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -1,3 +1,4 @@ +// update me! #include "util/options.h" namespace lean { diff --git a/tests/lean/run/grind_ring_2.lean b/tests/lean/run/grind_ring_2.lean index 7ada566541..9289ed7e9b 100644 --- a/tests/lean/run/grind_ring_2.lean +++ b/tests/lean/run/grind_ring_2.lean @@ -40,15 +40,9 @@ example [CommRing α] [NoNatZeroDivisors α] (x y : α) : 600000*x = 1 → 300*y example (x y : Int) : y = 0 → (x + 1)*(x - 1) + y = x^2 → False := by grind -example (x y : Int) : y = 0 → (x + 1)*(x - 1) + y = x^2 → False := by - grind +ringNull - example (x y z : BitVec 8) : z = y → (x + 1)*(x - 1)*y + y = z*x^2 + 1 → False := by grind -example (x y z : BitVec 8) : z = y → (x + 1)*(x - 1)*y + y = z*x^2 + 1 → False := by - grind +ringNull - example [CommRing α] (x y : α) : x*y*x = 1 → x*y*y = y → y = 1 := by grind diff --git a/tests/lean/run/grind_semiring_norm.lean b/tests/lean/run/grind_semiring_norm.lean index 5815af7b44..33c2469330 100644 --- a/tests/lean/run/grind_semiring_norm.lean +++ b/tests/lean/run/grind_semiring_norm.lean @@ -11,4 +11,18 @@ example (a b : R) : (a + 2 * b)^2 = 4 * b^2 + b * 4 * a + a^2 := by grind example (a b : R) : (a + b)^2 ≠ a^2 + 2 * a * b + b^2 → False := by grind +/-- +trace: [grind.debug.proof] fun h h_1 => + h_1 + (Ring.OfSemiring.eq_normS (RArray.branch 1 (RArray.leaf a) (RArray.leaf b)) + (((Ring.OfSemiring.Expr.var 0).add (Ring.OfSemiring.Expr.var 1)).pow 2) + ((((Ring.OfSemiring.Expr.var 0).pow 2).add + (((Ring.OfSemiring.Expr.num 2).mul (Ring.OfSemiring.Expr.var 0)).mul (Ring.OfSemiring.Expr.var 1))).add + ((Ring.OfSemiring.Expr.var 1).pow 2)) + (eagerReduce (Eq.refl true))) +-/ +#guard_msgs in -- context should contain only `a` and `b` +set_option trace.grind.debug.proof true in +example (a b c d : R) : c + d = d → (a + b)^2 ≠ a^2 + 2 * a * b + b^2 → False := by grind + end CommSemiring