feat: improve linarith markVars

This PR improves the linarith `markVars`, and ensures it does not
produce spurious issue messages.

src/Lean/Meta/Tactic/Grind/Arith/Linear/Internalize.lean

@@ -45,9 +45,47 @@ private def isForbiddenParent (parent? : Option Expr) : Bool :=
   else
     true
 
-def markVars (e : Expr) : LinearM Unit := do
-  -- TODO: avoid creation of auxiliary reified expression
-  discard <| reify? e (skipVar := true)
+partial def markVars (e : Expr) : LinearM Unit := do
+  match_expr e with
+  | HAdd.hAdd _ _ _ i a b =>
+    if isAddInst (← getStruct) i then markVars a; markVars b else markVar e
+  | HSub.hSub _ _ _ i a b => if isSubInst (← getStruct) i then markVars a; markVars b else markVar e
+  | HMul.hMul _ _ _ i a b =>
+    if isHMulInst (← getStruct) i then
+      if (← getIntValue? a).isSome then
+        return (← markVar b)
+    if isHMulNatInst (← getStruct) i then
+      if (← getNatValue? a).isSome then
+        return (← markVar b)
+    if isHomoMulInst (← getStruct) i then
+      if isNumeral a then
+        return (← markVar b)
+      else if isNumeral b then
+        return (← markVar a)
+      else
+        markVar a; markVar b; markVar e
+        return
+    markVar e
+  | HSMul.hSMul _ _ _ i a b =>
+    if isHSMulInst (← getStruct) i then
+      if (← getIntValue? a).isSome then
+        return (← markVar b)
+    if isHSMulNatInst (← getStruct) i then
+      if (← getNatValue? a).isSome then
+        return (← markVar b)
+    markVar e
+  | Neg.neg _ _ a => markVars a
+  | Zero.zero _ _ => return ()
+  | OfNat.ofNat _ _ _ => return ()
+  | _ => markVar e
+where
+  markVar (e : Expr) : LinearM Unit :=
+    discard <| mkVar e
+  isNumeral (e : Expr) : Bool :=
+    match_expr e with
+    | Neg.neg _ _ a => isNumeral a
+    | OfNat.ofNat _ n _ => isNatNum n
+    | _ => false
 
 def internalize (e : Expr) (parent? : Option Expr) : GoalM Unit := do
   unless (← getConfig).linarith do return ()

src/Lean/Meta/Tactic/Grind/Arith/Linear/Reify.lean

@@ -17,6 +17,8 @@ def isHMulInst (struct : Struct) (inst : Expr) : Bool :=
   isSameExpr struct.hmulFn.appArg! inst
 def isHMulNatInst (struct : Struct) (inst : Expr) : Bool :=
   isSameExpr struct.hmulNatFn.appArg! inst
+def isHomoMulInst (struct : Struct) (inst : Expr) : Bool :=
+  if let some homomulFn := struct.homomulFn? then isSameExpr homomulFn inst else false
 def isHSMulInst (struct : Struct) (inst : Expr) : Bool :=
   if let some smulFn := struct.hsmulFn? then isSameExpr smulFn.appArg! inst else false
 def isHSMulNatInst (struct : Struct) (inst : Expr) : Bool :=
@@ -108,5 +110,4 @@ where
       if (← isOfNatZero e) then return .zero else toVar e
     | _ => toVar e
 
-
 end  Lean.Meta.Grind.Arith.Linear

src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean

@@ -177,6 +177,11 @@ where
       return some one
     let one? ← getOne?
     let commRingInst? ← getInst? ``Grind.CommRing
+    let homomulFn? ← if commRingInst?.isSome then
+      let mulInst ← getBinHomoInst ``HMul
+      pure <| some (← internalizeFn <| mkApp4 (mkConst ``HMul.hMul [u, u, u]) type type type mulInst)
+    else
+      pure none
     let getOrderedRingInst? : GoalM (Option Expr) := do
       let some semiringInst := semiringInst? | return none
       let some preorderInst := preorderInst? | return none
@@ -197,7 +202,7 @@ where
     let struct : Struct := {
       id, type, u, intModuleInst, preorderInst?, orderedAddInst?, partialInst?, linearInst?, noNatDivInst?
       leFn?, ltFn?, addFn, subFn, negFn, hmulFn, hmulNatFn, hsmulFn?, hsmulNatFn?, zero, one?
-      ringInst?, commRingInst?, orderedRingInst?, charInst?, ringId?, fieldInst?, ofNatZero
+      ringInst?, commRingInst?, orderedRingInst?, charInst?, ringId?, fieldInst?, ofNatZero, homomulFn?
     }
     modify' fun s => { s with structs := s.structs.push struct }
     if let some one := one? then

src/Lean/Meta/Tactic/Grind/Arith/Linear/Types.lean

@@ -123,6 +123,7 @@ structure Struct where
   hmulNatFn        : Expr
   hsmulFn?         : Option Expr
   hsmulNatFn?      : Option Expr
+  homomulFn?       : Option Expr -- homogeneous multiplication if structure is a ring
   subFn            : Expr
   negFn            : Expr
   /--

tests/lean/run/grind_linarith_spurious_issues.lean

@@ -0,0 +1,7 @@
+open Lean Grind
+
+-- Should not produced spurious issues.
+#guard_msgs (drop error, trace) in
+set_option trace.grind.issues true in
+example [Field α] (a b : α) : a*b + b*c = 2 → b = a⁻¹ := by
+  grind