From e38b8a0a7a0652ca4e45dcce9c118d6b59635335 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 8 Jun 2025 19:38:03 -0400 Subject: [PATCH] feat: proof terms generation for `CommRing` and linarith interface (#8689) This PR implements proof term generation for the `CommRing` and `linarith` interface. It also fixes the `CommRing` helper theorems. --- src/Init/Grind/CommRing/Poly.lean | 16 +++--- .../Tactic/Grind/Arith/Linear/DenoteExpr.lean | 15 +----- .../Tactic/Grind/Arith/Linear/IneqCnstr.lean | 4 +- .../Meta/Tactic/Grind/Arith/Linear/Proof.lean | 49 ++++++++++++++++++- .../Meta/Tactic/Grind/Arith/Linear/Types.lean | 4 +- .../Meta/Tactic/Grind/Arith/Linear/Util.lean | 15 ++++++ tests/lean/run/grind_linarith_1.lean | 21 ++++++++ 7 files changed, 98 insertions(+), 26 deletions(-) diff --git a/src/Init/Grind/CommRing/Poly.lean b/src/Init/Grind/CommRing/Poly.lean index 53bbe98605..23d1f2478b 100644 --- a/src/Init/Grind/CommRing/Poly.lean +++ b/src/Init/Grind/CommRing/Poly.lean @@ -1178,31 +1178,31 @@ theorem lt_norm {α} [CommRing α] [Preorder α] [Ring.IsOrdered α] (ctx : Cont assumption theorem not_le_norm {α} [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) - : core_cert rhs lhs p → ¬ lhs.denote ctx ≤ rhs.denote ctx → p.denote ctx < 0 := by - simp [core_cert]; intro _ h₁; subst p; simp [Expr.denote_toPoly, Expr.denote] + : core_cert rhs lhs p → ¬ lhs.denote ctx ≤ rhs.denote ctx → p.denoteAsIntModule ctx < 0 := by + simp [core_cert, Poly.denoteAsIntModule_eq_denote]; intro _ h₁; subst p; simp [Expr.denote_toPoly, Expr.denote] replace h₁ := LinearOrder.lt_of_not_le h₁ replace h₁ := add_lt_left h₁ (-lhs.denote ctx) simp [← sub_eq_add_neg, sub_self] at h₁ assumption theorem not_lt_norm {α} [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) - : core_cert rhs lhs p → ¬ lhs.denote ctx < rhs.denote ctx → p.denote ctx ≤ 0 := by - simp [core_cert]; intro _ h₁; subst p; simp [Expr.denote_toPoly, Expr.denote] + : core_cert rhs lhs p → ¬ lhs.denote ctx < rhs.denote ctx → p.denoteAsIntModule ctx ≤ 0 := by + simp [core_cert, Poly.denoteAsIntModule_eq_denote]; intro _ h₁; subst p; simp [Expr.denote_toPoly, Expr.denote] replace h₁ := LinearOrder.le_of_not_lt h₁ replace h₁ := add_le_left h₁ (-lhs.denote ctx) simp [← sub_eq_add_neg, sub_self] at h₁ assumption theorem not_le_norm' {α} [CommRing α] [Preorder α] [Ring.IsOrdered α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) - : core_cert lhs rhs p → ¬ lhs.denote ctx ≤ rhs.denote ctx → ¬ p.denote ctx ≤ 0 := by - simp [core_cert]; intro _ h₁; subst p; simp [Expr.denote_toPoly, Expr.denote]; intro h + : core_cert lhs rhs p → ¬ lhs.denote ctx ≤ rhs.denote ctx → ¬ p.denoteAsIntModule ctx ≤ 0 := by + simp [core_cert, Poly.denoteAsIntModule_eq_denote]; intro _ h₁; subst p; simp [Expr.denote_toPoly, Expr.denote]; intro h replace h := add_le_right (rhs.denote ctx) h rw [sub_eq_add_neg, add_left_comm, ← sub_eq_add_neg, sub_self] at h; simp [add_zero] at h contradiction theorem not_lt_norm' {α} [CommRing α] [Preorder α] [Ring.IsOrdered α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) - : core_cert lhs rhs p → ¬ lhs.denote ctx < rhs.denote ctx → ¬ p.denote ctx < 0 := by - simp [core_cert]; intro _ h₁; subst p; simp [Expr.denote_toPoly, Expr.denote]; intro h + : core_cert lhs rhs p → ¬ lhs.denote ctx < rhs.denote ctx → ¬ p.denoteAsIntModule ctx < 0 := by + simp [core_cert, Poly.denoteAsIntModule_eq_denote]; intro _ h₁; subst p; simp [Expr.denote_toPoly, Expr.denote]; intro h replace h := add_lt_right (rhs.denote ctx) h rw [sub_eq_add_neg, add_left_comm, ← sub_eq_add_neg, sub_self] at h; simp [add_zero] at h contradiction diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Linear/DenoteExpr.lean b/src/Lean/Meta/Tactic/Grind/Arith/Linear/DenoteExpr.lean index 5d7afb3df7..c819bf1542 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/DenoteExpr.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/DenoteExpr.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ prelude +import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr import Lean.Meta.Tactic.Grind.Arith.Linear.Util import Lean.Meta.Tactic.Grind.Arith.Linear.Var @@ -86,18 +87,6 @@ where def _root_.Lean.Grind.CommRing.Poly.denoteAsIntModuleExpr (p : Grind.CommRing.Poly) : LinearM Expr := do match p with | .num k => denoteNum k - | .add k m p => go p (← denoteTerm k m) -where - denoteTerm (k : Int) (m : Grind.CommRing.Mon) : LinearM Expr := do - if k == 1 then - m.denoteAsIntModuleExpr - else - return mkApp2 (← getStruct).hmulFn (mkIntLit k) (← m.denoteAsIntModuleExpr) - - go (p : Grind.CommRing.Poly) (acc : Expr) : LinearM Expr := do - match p with - | .num 0 => return acc - | .num k => return mkApp2 (← getStruct).addFn acc (← denoteNum k) - | .add k m p => go p (mkApp2 (← getStruct).addFn acc (← denoteTerm k m)) + | .add k m p => return mkApp2 (← getStruct).addFn (mkApp2 (← getRing).mulFn (mkIntLit k) (← m.denoteExpr)) (← denoteAsIntModuleExpr p) end Lean.Meta.Grind.Arith.Linear diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Linear/IneqCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/Linear/IneqCnstr.lean index 44f5217d49..8f26190d3e 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/IneqCnstr.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/IneqCnstr.lean @@ -50,7 +50,7 @@ def propagateCommRingIneq (e : Expr) (lhs rhs : Expr) (strict : Bool) (eqTrue : let lhs' ← p'.denoteAsIntModuleExpr let some lhs' ← reify? lhs' (skipVar := false) | return () let p := lhs'.norm - let c : IneqCnstr := { p, strict, h := .coreCommRing e lhs rhs lhs' } + let c : IneqCnstr := { p, strict, h := .coreCommRing e lhs rhs p' lhs' } c.assert else if (← isLinearOrder) then let p' := (rhs.sub lhs).toPoly @@ -58,7 +58,7 @@ def propagateCommRingIneq (e : Expr) (lhs rhs : Expr) (strict : Bool) (eqTrue : let lhs' ← p'.denoteAsIntModuleExpr let some lhs' ← reify? lhs' (skipVar := false) | return () let p := lhs'.norm - let c : IneqCnstr := { p, strict, h := .notCoreCommRing e lhs rhs lhs' } + let c : IneqCnstr := { p, strict, h := .notCoreCommRing e lhs rhs p' lhs' } c.assert else let p' := (lhs.sub rhs).toPoly diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Proof.lean b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Proof.lean index 6f9c401f59..33452fd061 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Proof.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Proof.lean @@ -43,6 +43,7 @@ structure ProofM.State where cache : Std.HashMap UInt64 Expr := {} polyMap : Std.HashMap Poly Expr := {} exprMap : Std.HashMap LinExpr Expr := {} + ringPolyMap : Std.HashMap CommRing.Poly Expr := {} ringExprMap : Std.HashMap RingExpr Expr := {} structure ProofM.Context where @@ -86,6 +87,13 @@ def mkExprDecl (e : LinExpr) : ProofM Expr := do modify fun s => { s with exprMap := s.exprMap.insert e x } return x +def mkRingPolyDecl (p : CommRing.Poly) : ProofM Expr := do + if let some x := (← get).ringPolyMap[p]? then + return x + let x := mkFVar (← mkFreshFVarId) + modify fun s => { s with ringPolyMap := s.ringPolyMap.insert p x } + return x + def mkRingExprDecl (e : RingExpr) : ProofM Expr := do if let some x := (← get).ringExprMap[e]? then return x @@ -103,7 +111,8 @@ where let h ← x let h ← mkLetOfMap (← get).polyMap h `p (mkConst ``Grind.Linarith.Poly) toExpr let h ← mkLetOfMap (← get).exprMap h `e (mkConst ``Grind.Linarith.Expr) toExpr - let h ← mkLetOfMap (← get).ringExprMap h `r (mkConst ``Grind.CommRing.Expr) toExpr + let h ← mkLetOfMap (← get).ringPolyMap h `rp (mkConst ``Grind.CommRing.Poly) toExpr + let h ← mkLetOfMap (← get).ringExprMap h `re (mkConst ``Grind.CommRing.Expr) toExpr mkLetFVars #[(← getContext), (← getRingContext)] h /-- @@ -131,6 +140,31 @@ private def mkIntModPreOrdThmPrefix (declName : Name) : ProofM Expr := do let s ← getStruct return mkApp5 (mkConst declName [s.u]) s.type s.intModuleInst s.preorderInst s.isOrdInst (← getContext) +/-- +Returns the prefix of a theorem with name `declName` where the first five arguments are +`{α} [IntModule α] [LinearOrder α] [IntModule.IsOrdered α] (ctx : Context α)` +This is the most common theorem prefix at `Linarith.lean` +-/ +private def mkIntModLinOrdThmPrefix (declName : Name) : ProofM Expr := do + let s ← getStruct + return mkApp5 (mkConst declName [s.u]) s.type s.intModuleInst (← getLinearOrderInst) s.isOrdInst (← getContext) + +/-- +Returns the prefix of a theorem with name `declName` where the first five arguments are +`{α} [CommRing α] [Preorder α] [Ring.IsOrdered α] (rctx : Context α)` +-/ +private def mkCommRingPreOrdThmPrefix (declName : Name) : ProofM Expr := do + let s ← getStruct + return mkApp5 (mkConst declName [s.u]) s.type (← getCommRingInst) s.preorderInst (← getRingIsOrdInst) (← getRingContext) + +/-- +Returns the prefix of a theorem with name `declName` where the first five arguments are +`{α} [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (rctx : Context α)` +-/ +private def mkCommRingLinOrdThmPrefix (declName : Name) : ProofM Expr := do + let s ← getStruct + return mkApp5 (mkConst declName [s.u]) s.type (← getCommRingInst) (← getLinearOrderInst) (← getRingIsOrdInst) (← getRingContext) + mutual partial def EqCnstr.toExprProof (c' : EqCnstr) : ProofM Expr := caching c' do throwError "NIY" @@ -140,6 +174,19 @@ partial def IneqCnstr.toExprProof (c' : IneqCnstr) : ProofM Expr := caching c' d | .core e lhs rhs => let h ← mkIntModPreOrdThmPrefix (if c'.strict then ``Grind.Linarith.lt_norm else ``Grind.Linarith.le_norm) return mkApp5 h (← mkExprDecl lhs) (← mkExprDecl rhs) (← mkPolyDecl c'.p) reflBoolTrue (mkOfEqTrueCore e (← mkEqTrueProof e)) + | .notCore e lhs rhs => + let h ← mkIntModLinOrdThmPrefix (if c'.strict then ``Grind.Linarith.not_le_norm else ``Grind.Linarith.not_lt_norm) + return mkApp5 h (← mkExprDecl lhs) (← mkExprDecl rhs) (← mkPolyDecl c'.p) reflBoolTrue (mkOfEqFalseCore e (← mkEqFalseProof e)) + | .coreCommRing e lhs rhs p' lhs' => + let h' ← mkCommRingPreOrdThmPrefix (if c'.strict then ``Grind.CommRing.lt_norm else ``Grind.CommRing.le_norm) + let h' := mkApp5 h' (← mkRingExprDecl lhs) (← mkRingExprDecl rhs) (← mkRingPolyDecl p') reflBoolTrue (mkOfEqTrueCore e (← mkEqTrueProof e)) + let h ← mkIntModPreOrdThmPrefix (if c'.strict then ``Grind.Linarith.lt_norm else ``Grind.Linarith.le_norm) + return mkApp5 h (← mkExprDecl lhs') (← mkExprDecl .zero) (← mkPolyDecl c'.p) reflBoolTrue h' + | .notCoreCommRing e lhs rhs p' lhs' => + let h' ← mkCommRingLinOrdThmPrefix (if c'.strict then ``Grind.CommRing.not_le_norm else ``Grind.CommRing.not_lt_norm) + let h' := mkApp5 h' (← mkRingExprDecl lhs) (← mkRingExprDecl rhs) (← mkRingPolyDecl p') reflBoolTrue (mkOfEqFalseCore e (← mkEqFalseProof e)) + let h ← mkIntModPreOrdThmPrefix (if c'.strict then ``Grind.Linarith.lt_norm else ``Grind.Linarith.le_norm) + return mkApp5 h (← mkExprDecl lhs') (← mkExprDecl .zero) (← mkPolyDecl c'.p) reflBoolTrue h' | _ => throwError "NIY" partial def DiseqCnstr.toExprProof (c' : DiseqCnstr) : ProofM Expr := caching c' do diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Types.lean b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Types.lean index d969f63c3b..56d942a493 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Types.lean @@ -40,8 +40,8 @@ structure IneqCnstr where inductive IneqCnstrProof where | core (e : Expr) (lhs rhs : LinExpr) | notCore (e : Expr) (lhs rhs : LinExpr) - | coreCommRing (e : Expr) (lhs rhs : Grind.CommRing.Expr) (lhs' : LinExpr) - | notCoreCommRing (e : Expr) (lhs rhs : Grind.CommRing.Expr) (lhs' : LinExpr) + | coreCommRing (e : Expr) (lhs rhs : Grind.CommRing.Expr) (p : Grind.CommRing.Poly) (lhs' : LinExpr) + | notCoreCommRing (e : Expr) (lhs rhs : Grind.CommRing.Expr) (p : Grind.CommRing.Poly) (lhs' : LinExpr) | combine (c₁ : IneqCnstr) (c₂ : IneqCnstr) | combineEq (c₁ : IneqCnstr) (c₂ : EqCnstr) | norm (c₁ : IneqCnstr) (k : Nat) diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Util.lean b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Util.lean index fbbe0cb527..425aee099f 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Util.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Util.lean @@ -104,6 +104,21 @@ def setTermStructId (e : Expr) : LinearM Unit := do return () modify' fun s => { s with exprToStructId := s.exprToStructId.insert { expr := e } structId } +def getLinearOrderInst : LinearM Expr := do + let some inst := (← getStruct).linearInst? + | throwError "`grind linarith` internal error, structure is not a linear order" + return inst + +def getCommRingInst : LinearM Expr := do + let some inst := (← getStruct).commRingInst? + | throwError "`grind linarith` internal error, structure is not a commutative ring" + return inst + +def getRingIsOrdInst : LinearM Expr := do + let some inst := (← getStruct).ringIsOrdInst? + | throwError "`grind linarith` internal error, structure is not an ordered ring" + return inst + /-- Tries to evaluate the polynomial `p` using the partial model/assignment built so far. The result is `none` if the polynomial contains variables that have not been assigned. diff --git a/tests/lean/run/grind_linarith_1.lean b/tests/lean/run/grind_linarith_1.lean index 387cca1043..f8b71a206e 100644 --- a/tests/lean/run/grind_linarith_1.lean +++ b/tests/lean/run/grind_linarith_1.lean @@ -14,3 +14,24 @@ example [IntModule α] [Preorder α] [IntModule.IsOrdered α] (a b : α) : (2:Int)*a + b < b + a + a → False := by fail_if_success grind -linarith grind + +example [IntModule α] [LinearOrder α] [IntModule.IsOrdered α] (a b : α) + : (2:Int)*a + b ≥ b + a + a := by + grind + +#guard_msgs (drop error) in +example [IntModule α] [Preorder α] [IntModule.IsOrdered α] (a b : α) + : (2:Int)*a + b ≥ b + a + a := by + fail_if_success grind + +example [CommRing α] [Preorder α] [Ring.IsOrdered α] (a b : α) + : 2*a + b < b + a + a → False := by + grind + +example [CommRing α] [Preorder α] [Ring.IsOrdered α] (a b : α) + : 2 + 2*a + b + 1 < b + a + a + 3 → False := by + grind + +example [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (a b : α) + : 2 + 2*a + b + 1 <= b + a + a + 3 := by + grind