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.

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

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}"

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

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

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 }

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

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"