chore: remove tests that are working

I have already moved them to `run`

src/Init/Grind/Module/Basic.lean

@@ -51,6 +51,12 @@ instance toNatModule (M : Type u) [i : IntModule M] : NatModule M :=
 
 variable {M : Type u} [IntModule M]
 
+instance (priority := 100) (M : Type u) [IntModule M] : SMul Nat M where
+  smul a x := (a : Int) * x
+
+instance (priority := 100) (M : Type u) [IntModule M] : SMul Int M where
+  smul a x := a * x
+
 theorem zero_add (a : M) : 0 + a = a := by
   rw [add_comm, add_zero]
 

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

@@ -45,6 +45,10 @@ 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)
+
 def internalize (e : Expr) (parent? : Option Expr) : GoalM Unit := do
   unless (← getConfig).linarith do return ()
   if isIntModuleVirtualParent parent? then
@@ -57,5 +61,6 @@ def internalize (e : Expr) (parent? : Option Expr) : GoalM Unit := do
     trace[grind.linarith.internalize] "{e}"
     setTermStructId e
     markAsLinarithTerm e
+    markVars e
 
 end Lean.Meta.Grind.Arith.Linear

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

@@ -17,11 +17,10 @@ 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 isSMulInst (struct : Struct) (inst : Expr) : Bool :=
-  if let some smulFn := struct.smulFn? then
-    isSameExpr smulFn.appArg! 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 :=
+  if let some smulFn := struct.hsmulNatFn? then isSameExpr smulFn.appArg! inst else false
 def isSubInst (struct : Struct) (inst : Expr) : Bool :=
   isSameExpr struct.subFn.appArg! inst
 def isNegInst (struct : Struct) (inst : Expr) : Bool :=
@@ -46,10 +45,8 @@ partial def reify? (e : Expr) (skipVar : Bool) : LinearM (Option LinExpr) := do
     let some r ← processHMul i a b | asTopVar e
     return some r
   | HSMul.hSMul _ _ _ i a b =>
-    if isSMulInst (← getStruct) i then
-      let some k ← getIntValue? a | pure ()
-      return some (.mul k (← go b))
-    asTopVar e
+    let some r ← processHSMul i a b | asTopVar e
+    return some r
   | Neg.neg _ i a =>
     if isNegInst (← getStruct  ) i then return some (.neg (← go a)) else asTopVar e
   | Zero.zero _ i =>
@@ -83,6 +80,14 @@ where
       let some k ← getNatValue? a | return none
       return some (.mul k (← go b))
     return none
+  processHSMul (i a b : Expr) : LinearM (Option LinExpr) := do
+    if isHSMulInst (← getStruct) i then
+      let some k ← getIntValue? a | return none
+      return some (.mul k (← go b))
+    else if isHSMulNatInst (← getStruct) i then
+      let some k ← getNatValue? a | return none
+      return some (.mul k (← go b))
+    return none
   go (e : Expr) : LinearM LinExpr := do
     match_expr e with
     | HAdd.hAdd _ _ _ i a b =>
@@ -93,10 +98,8 @@ where
       let some r ← processHMul i a b | asVar e
       return r
     | HSMul.hSMul _ _ _ i a b =>
-      if isSMulInst (← getStruct) i then
-        let some k ← getIntValue? a | pure ()
-        return .mul k (← go b)
-      asVar e
+      let some r ← processHSMul i a b | asVar e
+      return r
     | Neg.neg _ i a =>
       if isNegInst (← getStruct) i then return .neg (← go a) else asVar e
     | Zero.zero _ i =>

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

@@ -132,15 +132,16 @@ where
       pure (some leFn, some ltFn)
     else
       pure (none, none)
-    let getSMulFn? : GoalM (Option Expr) := do
+    let getHSMulFn? : GoalM (Option Expr) := do
       let smulType := mkApp3 (mkConst ``HSMul [0, u, u]) Int.mkType type type
       let .some smulInst ← trySynthInstance smulType | return none
-      let smulFn ← internalizeFn <| mkApp4 (mkConst ``HSMul.hSMul [0, u, u]) Int.mkType type smulInst smulInst
-      if (← withDefault <| isDefEq hmulFn smulFn) then
-        return smulFn
-      reportIssue! (← mkExpectedDefEqMsg hmulFn smulFn)
-      return none
-    let smulFn? ← getSMulFn?
+      internalizeFn <| mkApp4 (mkConst ``HSMul.hSMul [0, u, u]) Int.mkType type smulInst smulInst
+    let getHSMulNatFn? : GoalM (Option Expr) := do
+      let smulType := mkApp3 (mkConst ``HSMul [0, u, u]) Nat.mkType type type
+      let .some smulInst ← trySynthInstance smulType | return none
+      internalizeFn <| mkApp4 (mkConst ``HSMul.hSMul [0, u, u]) Nat.mkType type smulInst smulInst
+    let hsmulFn? ← getHSMulFn?
+    let hsmulNatFn? ← getHSMulNatFn?
     let ringId? ← CommRing.getRingId? type
     let ringInst? ← getInst? ``Grind.Ring
     let getOne? : GoalM (Option Expr) := do
@@ -169,7 +170,7 @@ where
     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?
+      leFn?, ltFn?, addFn, subFn, negFn, hmulFn, hmulNatFn, hsmulFn?, hsmulNatFn?, 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

@@ -96,7 +96,8 @@ structure Struct where
   addFn            : Expr
   hmulFn           : Expr
   hmulNatFn        : Expr
-  smulFn?          : Option Expr
+  hsmulFn?         : Option Expr
+  hsmulNatFn?      : Option Expr
   subFn            : Expr
   negFn            : Expr
   /--

tests/lean/grind/algebra/module_normalization.lean

@@ -14,19 +14,3 @@ example (a : R) : 2 * a = a + a := by grind
 example (a b : R) : 2 * (b + c) = c + 2 * b + c := by grind
 
 end NatModule
-
-section IntModule
-
-variable (R : Type u) [IntModule R]
-
-example (a b : R) : a + b = b + a := by grind
-example (a : R) : a + 0 = a := by grind
-example (a : R) : 0 + a = a := by grind
-example (a b c : R) : a + b + c = a + (b + c) := by grind
-example (a : R) : 2 * a = a + a := by grind
-example (a : R) : (-2 : Int) * a = -a - a := by grind
-example (a b : R) : 2 * (b + c) = c + 2 * b + c := by grind
-example (a b c : R) : 2 * (b + c) - 3 * c + b + b = c + 5 * b - 2 * c := by grind
-example (a b c : R) : 2 * (b + c) + (-3 : Int) * c + b + b = c + (5 : Int) * b - 2 • c := by grind
-
-end IntModule

tests/lean/run/grind_linarith_2.lean

@@ -6,7 +6,7 @@ example [IntModule α] [Preorder α] [IntModule.IsOrdered α] (a b : α)
 
 /--
 trace: [grind.debug.proof] Classical.byContradiction fun h =>
-      let ctx := RArray.leaf One.one;
+      let ctx := RArray.branch 1 (RArray.leaf One.one) (RArray.branch 2 (RArray.leaf a) (RArray.leaf b));
       let rctx := RArray.branch 1 (RArray.leaf a) (RArray.leaf b);
       let re_1 := (CommRing.Expr.var 1).add (CommRing.Expr.var 0);
       let re_2 := (CommRing.Expr.var 0).add (CommRing.Expr.var 1);

tests/lean/run/grind_module_normalization.lean

@@ -0,0 +1,16 @@
+open Lean Grind
+variable (R : Type u) [IntModule R]
+
+example (a b : R) : a + b = b + a := by grind
+example (a : R) : a + 0 = a := by grind
+example (a : R) : 0 + a = a := by grind
+example (a b c : R) : a + b + c = a + (b + c) := by grind
+example (a : R) : 2 * a = a + a := by grind
+example (a : R) : (-2 : Int) * a = -a - a := by grind
+example (b c : R) : 2 * (b + c) = c + 2 * b + c := by grind
+example (b c : R) : 2 * (b + c) - 3 * c + b + b = c + 5 * b - 2 * c - b := by grind
+example (b c : R) : 2 * (b + c) + (-3 : Int) * c + b + b = c + (5 : Int) * b - 2 • c - b := by grind
+example (b : R) : 2•b = 1•b + b := by grind
+
+example [CommRing α] (b : α) : 2•b = 1•b + b := by grind -ring
+example [CommRing α] (b : α) : 2•b = 1•b + b := by grind