From ac0c59caae30cf9354d97176bf8d90af8e1b901e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 14 Jun 2025 21:20:49 -0400 Subject: [PATCH] feat: enable `linarith` even if no order is available (#8791) This PR ensures the `grind linarith` module is activated for any type that implements only `IntModule`. That is, the type does not need to be a preorder anymore. --- .../Tactic/Grind/Arith/Linear/DenoteExpr.lean | 6 +-- .../Tactic/Grind/Arith/Linear/IneqCnstr.lean | 11 +++- .../Meta/Tactic/Grind/Arith/Linear/Proof.lean | 12 ++--- .../Grind/Arith/Linear/PropagateEq.lean | 2 + .../Tactic/Grind/Arith/Linear/StructId.lean | 50 +++++++++++-------- .../Meta/Tactic/Grind/Arith/Linear/Types.lean | 15 +++--- .../Meta/Tactic/Grind/Arith/Linear/Util.lean | 23 +++++++++ 7 files changed, 81 insertions(+), 38 deletions(-) diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Linear/DenoteExpr.lean b/src/Lean/Meta/Tactic/Grind/Arith/Linear/DenoteExpr.lean index 832f602522..51d84d2398 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/DenoteExpr.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/DenoteExpr.lean @@ -14,7 +14,7 @@ namespace Lean.Meta.Grind.Arith.Linear Helper functions for converting reified terms back into their denotations. -/ -variable [Monad M] [MonadGetStruct M] +variable [Monad M] [MonadGetStruct M] [MonadError M] def _root_.Lean.Grind.Linarith.Poly.denoteExpr (p : Poly) : M Expr := do match p with @@ -52,9 +52,9 @@ def DiseqCnstr.denoteExpr (c : DiseqCnstr) : M Expr := do private def denoteIneq (p : Poly) (strict : Bool) : M Expr := do if strict then - return mkApp2 (← getStruct).ltFn (← p.denoteExpr) (← getStruct).ofNatZero + return mkApp2 (← getLtFn) (← p.denoteExpr) (← getStruct).ofNatZero else - return mkApp2 (← getStruct).leFn (← p.denoteExpr) (← getStruct).ofNatZero + return mkApp2 (← getLeFn) (← p.denoteExpr) (← getStruct).ofNatZero def IneqCnstr.denoteExpr (c : IneqCnstr) : M Expr := do denoteIneq c.p c.strict diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Linear/IneqCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/Linear/IneqCnstr.lean index d033e93dea..54cd772723 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/IneqCnstr.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/IneqCnstr.lean @@ -16,9 +16,16 @@ import Lean.Meta.Tactic.Grind.Arith.Linear.Proof namespace Lean.Meta.Grind.Arith.Linear def isLeInst (struct : Struct) (inst : Expr) : Bool := - isSameExpr struct.leFn.appArg! inst + if let some leFn := struct.leFn? then + isSameExpr leFn.appArg! inst + else + false + def isLtInst (struct : Struct) (inst : Expr) : Bool := - isSameExpr struct.ltFn.appArg! inst + if let some ltFn := struct.ltFn? then + isSameExpr ltFn.appArg! inst + else + false def IneqCnstr.assert (c : IneqCnstr) : LinearM Unit := do trace[grind.linarith.assert] "{← c.denoteExpr}" diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Proof.lean b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Proof.lean index 865a64c0dc..d5bbf6b14f 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Proof.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Proof.lean @@ -131,7 +131,7 @@ Returns the prefix of a theorem with name `declName` where the first four argume -/ private def mkIntModPreThmPrefix (declName : Name) : ProofM Expr := do let s ← getStruct - return mkApp4 (mkConst declName [s.u]) s.type s.intModuleInst s.preorderInst (← getContext) + return mkApp4 (mkConst declName [s.u]) s.type s.intModuleInst (← getPreorderInst) (← getContext) /-- Returns the prefix of a theorem with name `declName` where the first five arguments are @@ -140,7 +140,7 @@ This is the most common theorem prefix at `Linarith.lean` -/ 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) + return mkApp5 (mkConst declName [s.u]) s.type s.intModuleInst (← getPreorderInst) (← getIsOrdInst) (← getContext) /-- Returns the prefix of a theorem with name `declName` where the first five arguments are @@ -149,7 +149,7 @@ 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) + return mkApp5 (mkConst declName [s.u]) s.type s.intModuleInst (← getLinearOrderInst) (← getIsOrdInst) (← getContext) /-- Returns the prefix of a theorem with name `declName` where the first three arguments are @@ -165,7 +165,7 @@ Returns the prefix of a theorem with name `declName` where the first five argume -/ private def mkCommRingPreOrdThmPrefix (declName : Name) : ProofM Expr := do let s ← getStruct - return mkApp5 (mkConst declName [s.u]) s.type (← getCommRingInst) s.preorderInst (← getRingIsOrdInst) (← getRingContext) + return mkApp5 (mkConst declName [s.u]) s.type (← getCommRingInst) (← getPreorderInst) (← getRingIsOrdInst) (← getRingContext) /-- Returns the prefix of a theorem with name `declName` where the first five arguments are @@ -205,7 +205,7 @@ partial def IneqCnstr.toExprProof (c' : IneqCnstr) : ProofM Expr := caching c' d (← c₁.toExprProof) (← c₂.toExprProof) | .oneGtZero => let s ← getStruct - let h := mkApp5 (mkConst ``Grind.Linarith.zero_lt_one [s.u]) s.type (← getRingInst) s.preorderInst (← getRingIsOrdInst) (← getContext) + let h := mkApp5 (mkConst ``Grind.Linarith.zero_lt_one [s.u]) s.type (← getRingInst) (← getPreorderInst) (← getRingIsOrdInst) (← getContext) return mkApp3 h (← mkPolyDecl c'.p) reflBoolTrue (← mkEqRefl (← getOne)) | .ofEq a b la lb => let h ← mkIntModPreOrdThmPrefix ``Grind.Linarith.le_of_eq @@ -218,7 +218,7 @@ partial def IneqCnstr.toExprProof (c' : IneqCnstr) : ProofM Expr := caching c' d | .dec h => return mkFVar h | .ofDiseqSplit c₁ fvarId h _ => let hFalse ← h.toExprProofCore - let lt := (← getStruct).ltFn + let lt ← getLtFn let hNot := mkLambda `h .default (mkApp2 lt (← c₁.p.denoteExpr) (← getZero)) (hFalse.abstract #[mkFVar fvarId]) let h ← mkIntModLinOrdThmPrefix ``Grind.Linarith.diseq_split_resolve return mkApp5 h (← mkPolyDecl c₁.p) (← mkPolyDecl c'.p) reflBoolTrue (← c₁.toExprProof) hNot diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Linear/PropagateEq.lean b/src/Lean/Meta/Tactic/Grind/Arith/Linear/PropagateEq.lean index 98dec889f6..5d55067c3a 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/PropagateEq.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/PropagateEq.lean @@ -56,6 +56,8 @@ def processNewEqImpl (a b : Expr) : GoalM Unit := do if isSameExpr a b then return () -- TODO: check why this is needed let some structId ← inSameStruct? a b | return () LinearM.run structId do + -- TODO: support non ordered case + unless (← isOrdered) do return () trace_goal[grind.linarith.assert] "{← mkEq a b}" if (← isCommRing) then processNewCommRingEq a b diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean b/src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean index 5bbb60adf9..2fb27fbc07 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean @@ -39,6 +39,7 @@ private def ensureDefEq (a b : Expr) : MetaM Unit := do throwError (← mkExpectedDefEqMsg a b) def getStructId? (type : Expr) : GoalM (Option Nat) := do + unless (← getConfig).linarith do return none if (← getConfig).cutsat && Cutsat.isSupportedType type then -- If `type` is supported by cutsat, let it handle return none @@ -51,30 +52,30 @@ def getStructId? (type : Expr) : GoalM (Option Nat) := do where go? : GoalM (Option Nat) := do let u ← getDecLevel type - let getInst? (declName : Name) : GoalM (Option Expr) := do + let rec getInst? (declName : Name) : GoalM (Option Expr) := do let instType := mkApp (mkConst declName [u]) type return LOption.toOption (← trySynthInstance instType) - let getInst (declName : Name) : GoalM Expr := do + let rec getInst (declName : Name) : GoalM Expr := do let instType := mkApp (mkConst declName [u]) type let .some inst ← trySynthInstance instType | throwError "`grind linarith` failed to find instance{indentExpr instType}" return inst - let getBinHomoInst (declName : Name) : GoalM Expr := do + let rec getBinHomoInst (declName : Name) : GoalM Expr := do let instType := mkApp3 (mkConst declName [u, u, u]) type type type let .some inst ← trySynthInstance instType | throwError "`grind linarith` failed to find instance{indentExpr instType}" return inst - let getHMulInst : GoalM Expr := do + let rec getHMulInst : GoalM Expr := do let instType := mkApp3 (mkConst ``HMul [0, u, u]) Int.mkType type type let .some inst ← trySynthInstance instType | throwError "`grind linarith` failed to find instance{indentExpr instType}" return inst - let getHMulNatInst : GoalM Expr := do + let rec getHMulNatInst : GoalM Expr := do let instType := mkApp3 (mkConst ``HMul [0, u, u]) Nat.mkType type type let .some inst ← trySynthInstance instType | throwError "`grind linarith` failed to find instance{indentExpr instType}" return inst - let checkToFieldDefEq? (parentInst? : Option Expr) (inst? : Option Expr) (toFieldName : Name) : GoalM (Option Expr) := do + let rec checkToFieldDefEq? (parentInst? : Option Expr) (inst? : Option Expr) (toFieldName : Name) : GoalM (Option Expr) := do let some parentInst := parentInst? | return none let some inst := inst? | return none let toField := mkApp2 (mkConst toFieldName [u]) type inst @@ -82,10 +83,10 @@ where reportIssue! (← mkExpectedDefEqMsg parentInst toField) return none return some inst - let ensureToFieldDefEq (parentInst : Expr) (inst : Expr) (toFieldName : Name) : GoalM Unit := do + let rec ensureToFieldDefEq (parentInst : Expr) (inst : Expr) (toFieldName : Name) : GoalM Unit := do let toField := mkApp2 (mkConst toFieldName [u]) type inst ensureDefEq parentInst toField - let ensureToHomoFieldDefEq (parentInst : Expr) (inst : Expr) (toFieldName : Name) (toHeteroName : Name) : GoalM Unit := do + let rec ensureToHomoFieldDefEq (parentInst : Expr) (inst : Expr) (toFieldName : Name) (toHeteroName : Name) : GoalM Unit := do let toField := mkApp2 (mkConst toFieldName [u]) type inst let heteroToField := mkApp2 (mkConst toHeteroName [u]) type toField ensureDefEq parentInst heteroToField @@ -112,17 +113,25 @@ where ensureToHomoFieldDefEq subInst intModuleInst ``Grind.IntModule.toSub ``instHSub ensureToFieldDefEq negInst intModuleInst ``Grind.IntModule.toNeg ensureToFieldDefEq hmulInst intModuleInst ``Grind.IntModule.toHMul - let some preorderInst ← getInst? ``Grind.Preorder | return none - let leInst ← getInst ``LE - let ltInst ← getInst ``LT - let leFn ← internalizeFn <| mkApp2 (mkConst ``LE.le [u]) type leInst - let ltFn ← internalizeFn <| mkApp2 (mkConst ``LT.lt [u]) type ltInst - ensureToFieldDefEq leInst preorderInst ``Grind.Preorder.toLE - ensureToFieldDefEq ltInst preorderInst ``Grind.Preorder.toLT - let partialInst? ← checkToFieldDefEq? (some preorderInst) (← getInst? ``Grind.PartialOrder) ``Grind.PartialOrder.toPreorder + let preorderInst? ← getInst? ``Grind.Preorder + let isOrdInst? ← if let some preorderInst := preorderInst? then + let isOrderedType := mkApp3 (mkConst ``Grind.IntModule.IsOrdered [u]) type preorderInst intModuleInst + pure <| LOption.toOption (← trySynthInstance isOrderedType) + else + pure none + let preorderInst? := if isOrdInst?.isNone then none else preorderInst? + let partialInst? ← checkToFieldDefEq? preorderInst? (← getInst? ``Grind.PartialOrder) ``Grind.PartialOrder.toPreorder let linearInst? ← checkToFieldDefEq? partialInst? (← getInst? ``Grind.LinearOrder) ``Grind.LinearOrder.toPartialOrder - let isOrderedType := mkApp3 (mkConst ``Grind.IntModule.IsOrdered [u]) type preorderInst intModuleInst - let .some isOrdInst ← trySynthInstance isOrderedType | return none + let (leFn?, ltFn?) ← if let some preorderInst := preorderInst? then + let leInst ← getInst ``LE + let ltInst ← getInst ``LT + let leFn ← internalizeFn <| mkApp2 (mkConst ``LE.le [u]) type leInst + let ltFn ← internalizeFn <| mkApp2 (mkConst ``LT.lt [u]) type ltInst + ensureToFieldDefEq leInst preorderInst ``Grind.Preorder.toLE + ensureToFieldDefEq ltInst preorderInst ``Grind.Preorder.toLT + pure (some leFn, some ltFn) + else + pure (none, none) let getSMulFn? : GoalM (Option Expr) := do let smulType := mkApp3 (mkConst ``HSMul [0, u, u]) Int.mkType type type let .some smulInst ← trySynthInstance smulType | return none @@ -144,6 +153,7 @@ where let commRingInst? ← getInst? ``Grind.CommRing let getRingIsOrdInst? : GoalM (Option Expr) := do let some ringInst := ringInst? | return none + let some preorderInst := preorderInst? | return none let isOrdType := mkApp3 (mkConst ``Grind.Ring.IsOrdered [u]) type ringInst preorderInst let .some inst ← trySynthInstance isOrdType | reportIssue! "type is an ordered `IntModule` and a `Ring`, but is not an ordered ring, failed to synthesize{indentExpr isOrdType}" @@ -158,8 +168,8 @@ where let noNatDivInst? ← getNoNatZeroDivInst? let id := (← get').structs.size let struct : Struct := { - id, type, u, intModuleInst, preorderInst, isOrdInst, partialInst?, linearInst?, noNatDivInst? - leFn, ltFn, addFn, subFn, negFn, hmulFn, hmulNatFn, smulFn?, zero, one? + id, type, u, intModuleInst, preorderInst?, isOrdInst?, partialInst?, linearInst?, noNatDivInst? + leFn?, ltFn?, addFn, subFn, negFn, hmulFn, hmulNatFn, smulFn?, zero, one? ringInst?, commRingInst?, ringIsOrdInst?, ringId?, ofNatZero } modify' fun s => { s with structs := s.structs.push struct } diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Types.lean b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Types.lean index 1de5db8f17..21281599c7 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Types.lean @@ -60,7 +60,8 @@ instance : Inhabited DiseqCnstr where /-- State for each algebraic structure by this module. -Each type must be at least implement the instances `IntModule`, `Preorder`, and `IntModule.IsOrdered` +Each type must at least implement the instance `IntModule`. +For being able to process inequalities, it must at least implement `Preorder`, and `IntModule.IsOrdered` -/ structure Struct where id : Nat @@ -71,10 +72,10 @@ structure Struct where u : Level /-- `IntModule` instance -/ intModuleInst : Expr - /-- `Preorder` instance -/ - preorderInst : Expr - /-- `IntModule.IsOrdered` instance with `Preorder` -/ - isOrdInst : Expr + /-- `Preorder` instance if available -/ + preorderInst? : Option Expr + /-- `IntModule.IsOrdered` instance with `Preorder` if available -/ + isOrdInst? : Option Expr /-- `PartialOrder` instance if available -/ partialInst? : Option Expr /-- `LinearOrder` instance if available -/ @@ -90,8 +91,8 @@ structure Struct where zero : Expr ofNatZero : Expr one? : Option Expr - leFn : Expr - ltFn : Expr + leFn? : Option Expr + ltFn? : Option Expr addFn : Expr hmulFn : Expr hmulNatFn : Expr diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Util.lean b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Util.lean index c1d41f6443..5794059bb0 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Util.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Util.lean @@ -110,6 +110,29 @@ def setTermStructId (e : Expr) : LinearM Unit := do return () modify' fun s => { s with exprToStructId := s.exprToStructId.insert { expr := e } structId } +def getPreorderInst : LinearM Expr := do + let some inst := (← getStruct).preorderInst? + | throwError "`grind linarith` internal error, structure is not a preorder" + return inst + +def getIsOrdInst : LinearM Expr := do + let some inst := (← getStruct).isOrdInst? + | throwError "`grind linarith` internal error, structure is not an ordered module" + return inst + +def isOrdered : LinearM Bool := + return (← getStruct).isOrdInst?.isSome + +def getLtFn [Monad m] [MonadError m] [MonadGetStruct m] : m Expr := do + let some lt := (← getStruct).ltFn? + | throwError "`grind linarith` internal error, structure is not an ordered module" + return lt + +def getLeFn [Monad m] [MonadError m] [MonadGetStruct m] : m Expr := do + let some le := (← getStruct).leFn? + | throwError "`grind linarith` internal error, structure is not an ordered int module" + return le + def getLinearOrderInst : LinearM Expr := do let some inst := (← getStruct).linearInst? | throwError "`grind linarith` internal error, structure is not a linear order"