chore: a few missing grind typeclass docstrings

.gitignore

@@ -6,6 +6,7 @@
 lake-manifest.json
 /build
 /src/lakefile.toml
+/tests/lakefile.toml
 /lakefile.toml
 GPATH
 GRTAGS

src/Init/Grind/Module/Basic.lean

@@ -48,11 +48,7 @@ satisfying appropriate compatibilities.
 
 Equivalently, an additive commutative group.
 -/
-class IntModule (M : Type u) extends Zero M, Add M, Neg M, Sub M where
-  /-- Scalar multiplication by natural numbers. -/
-  [hmulNat : HMul Nat M M]
-  /-- Scalar multiplication by integers. -/
-  [hmulInt : HMul Int M M]
+class IntModule (M : Type u) extends Zero M, Add M, Neg M, Sub M, HMul Int M M where
   /-- Zero is the right identity for addition. -/
   add_zero : ∀ a : M, a + 0 = a
   /-- Addition is commutative. -/
@@ -73,8 +69,6 @@ class IntModule (M : Type u) extends Zero M, Add M, Neg M, Sub M where
   neg_add_cancel : ∀ a : M, -a + a = 0
   /-- Subtraction is addition of the negative. -/
   sub_eq_add_neg : ∀ a b : M, a - b = a + -b
-  /-- Scalar multiplication by natural numbers is consistent with scalar multiplication by integers. -/
-  hmul_nat : ∀ n : Nat, ∀ a : M, (n : Int) * a = n * a
 
 namespace NatModule
 
@@ -89,33 +83,27 @@ theorem mul_hmul (n m : Nat) (a : M) : (n * m) * a = n * (m * a) := by
   | succ n ih =>
     rw [Nat.add_one_mul, add_hmul, ih, add_hmul, one_hmul]
 
-instance (priority := 100) (M : Type u) [NatModule M] : SMul Nat M where
-  smul a x := a * x
-
 end NatModule
 
 namespace IntModule
 
-attribute [instance 100] IntModule.toZero IntModule.toAdd IntModule.toNeg IntModule.toSub
-  IntModule.hmulNat IntModule.hmulInt
+attribute [instance 100] IntModule.toZero IntModule.toAdd IntModule.toNeg IntModule.toSub IntModule.toHMul
 
 instance toNatModule (M : Type u) [i : IntModule M] : NatModule M :=
   { i with
-    hMul := i.hmulNat.hMul
-    zero_hmul := by simp [← hmul_nat, zero_hmul]
-    one_hmul := by simp [← hmul_nat, one_hmul]
-    hmul_zero := by simp [← hmul_nat, hmul_zero]
-    add_hmul := by simp [← hmul_nat, add_hmul]
-    hmul_add := by simp [← hmul_nat, hmul_add] }
+    hMul a x := (a : Int) * x
+    hmul_zero := by simp [IntModule.hmul_zero]
+    add_hmul := by simp [IntModule.add_hmul]
+    hmul_add := by simp [IntModule.hmul_add] }
+
+variable {M : Type u} [IntModule M]
 
 instance (priority := 100) (M : Type u) [IntModule M] : SMul Nat M where
-  smul a x := a * x
+  smul a x := (a : Int) * x
 
 instance (priority := 100) (M : Type u) [IntModule M] : SMul Int M where
   smul a x := a * x
 
-variable {M : Type u} [IntModule M]
-
 theorem zero_add (a : M) : 0 + a = a := by
   rw [add_comm, add_zero]
 
@@ -183,9 +171,6 @@ theorem hmul_sub (k : Int) (a b : M) : k * (a - b) = k * a - k * b := by
 theorem sub_hmul (k₁ k₂ : Int) (a : M) : (k₁ - k₂) * a = k₁ * a - k₂ * a := by
   rw [Int.sub_eq_add_neg, add_hmul, neg_hmul, ← sub_eq_add_neg]
 
-theorem nat_zero_hmul (a : M) : (0 : Nat) * a = 0 := by
-  rw [← hmul_nat, Int.natCast_zero, zero_hmul]
-
 private theorem nat_mul_hmul (n : Nat) (m : Int) (a : M) :
     ((n : Int) * m) * a = (n : Int) * (m * a) := by
   induction n with
@@ -203,30 +188,16 @@ end IntModule
 
 /--
 We say a module has no natural number zero divisors if
-`k ≠ 0` and `k * a = k * b` implies `a = b` (here `k` is a natural number and `a` and `b` are element of the module).
+`k * a = 0` implies `k = 0` or `a = 0` (here `k` is a natural number and `a` is an element of the module).
+
+This is a special case of Mathlib's `NoZeroSMulDivisors Nat α`.
 -/
-class NoNatZeroDivisors (α : Type u) [HMul Nat α α] where
-  no_nat_zero_divisors : ∀ (k : Nat) (a b : α), k ≠ 0 → k * a = k * b → a = b
+class NoNatZeroDivisors (α : Type u) [Zero α] [HMul Nat α α] where
+  /-- If `k * a = 0` (for `k : Nat` and `a : α`), then `k = 0` or `a = 0`. -/
+  no_nat_zero_divisors : ∀ (k : Nat) (a : α), k ≠ 0 → k * a = 0 → a = 0
 
 export NoNatZeroDivisors (no_nat_zero_divisors)
 
-namespace NoNatZeroDivisors
-
-/-- Alternative constructor for `NoNatZeroDivisors` when we have an `IntModule`. -/
-def mk' {α} [IntModule α] (eq_zero_of_mul_eq_zero : ∀ (k : Nat) (a : α), k ≠ 0 → k * a = 0 → a = 0) : NoNatZeroDivisors α where
-  no_nat_zero_divisors k a b h₁ h₂ := by
-    rw [← IntModule.sub_eq_zero_iff, ← IntModule.hmul_nat, ← IntModule.hmul_nat, ← IntModule.hmul_sub, IntModule.hmul_nat] at h₂
-    rw [← IntModule.sub_eq_zero_iff]
-    apply eq_zero_of_mul_eq_zero k (a - b) h₁ h₂
-
-theorem eq_zero_of_mul_eq_zero {α : Type u} [NatModule α] [NoNatZeroDivisors α] {k : Nat} {a : α}
-    : k ≠ 0 → k * a = 0 → a = 0 := by
-  intro h₁ h₂
-  replace h₁ : k ≠ 0 := by intro h; simp [h] at h₁
-  exact no_nat_zero_divisors k a 0 h₁ (by rwa [NatModule.hmul_zero])
-
-end NoNatZeroDivisors
-
 instance [ToInt α (some lo) (some hi)] [IntModule α] [ToInt.Zero α (some lo) (some hi)] [ToInt.Add α (some lo) (some hi)] : ToInt.Neg α (some lo) (some hi) where
   toInt_neg x := by
     have := (ToInt.Add.toInt_add (-x) x).symm

src/Init/Grind/Ordered/Linarith.lean

@@ -20,7 +20,7 @@ namespace Lean.Grind.Linarith
 abbrev Var := Nat
 open IntModule
 
-attribute [local simp] add_zero zero_add zero_hmul nat_zero_hmul hmul_zero one_hmul
+attribute [local simp] add_zero zero_add zero_hmul hmul_zero one_hmul
 
 inductive Expr where
   | zero
@@ -28,9 +28,8 @@ inductive Expr where
   | add  (a b : Expr)
   | sub  (a b : Expr)
   | neg  (a : Expr)
-  | natMul  (k : Nat) (a : Expr)
-  | intMul  (k : Int) (a : Expr)
-  deriving Inhabited, BEq, Repr
+  | mul  (k : Int) (a : Expr)
+  deriving Inhabited, BEq
 
 abbrev Context (α : Type u) := RArray α
 
@@ -42,14 +41,13 @@ def Expr.denote {α} [IntModule α] (ctx : Context α) : Expr → α
   | .var v    => v.denote ctx
   | .add a b  => denote ctx a + denote ctx b
   | .sub a b  => denote ctx a - denote ctx b
-  | .natMul k a  => k * denote ctx a
-  | .intMul k a  => k * denote ctx a
+  | .mul k a  => k * denote ctx a
   | .neg a    => -denote ctx a
 
 inductive Poly where
   | nil
   | add (k : Int) (v : Var) (p : Poly)
-  deriving BEq, Repr
+  deriving BEq
 
 def Poly.denote {α} [IntModule α] (ctx : Context α) (p : Poly) : α :=
   match p with
@@ -146,8 +144,7 @@ where
     | .var v    => (.add coeff v ·)
     | .add a b  => go coeff a ∘ go coeff b
     | .sub a b  => go coeff a ∘ go (-coeff) b
-    | .natMul k a  => bif k == 0 then id else go (Int.mul coeff k) a
-    | .intMul k a  => bif k == 0 then id else go (Int.mul coeff k) a
+    | .mul k a  => bif k == 0 then id else go (Int.mul coeff k) a
     | .neg a    => go (-coeff) a
 
 /-- Converts the given expression into a polynomial, and then normalizes it. -/
@@ -218,8 +215,6 @@ theorem Expr.denote_toPoly'_go {α} [IntModule α] {k p} (ctx : Context α) (e :
   next => ac_rfl
   next => rw [sub_eq_add_neg, neg_hmul, hmul_add, hmul_neg]; ac_rfl
   next h => simp at h; subst h; simp
-  next ih => simp at ih; rw [ih, mul_hmul, IntModule.hmul_nat]
-  next ih => simp at ih; simp [ih]
   next ih => simp at ih; rw [ih, mul_hmul]
   next => rw [hmul_neg, neg_hmul]
 
@@ -476,8 +471,8 @@ def eq_coeff_cert (p₁ p₂ : Poly) (k : Nat) :=
 
 theorem eq_coeff {α} [IntModule α] [NoNatZeroDivisors α] (ctx : Context α) (p₁ p₂ : Poly) (k : Nat)
     : eq_coeff_cert p₁ p₂ k → p₁.denote' ctx = 0 → p₂.denote' ctx = 0 := by
-  simp [eq_coeff_cert]; intro h _; subst p₁; simp [*, hmul_nat]
-  exact NoNatZeroDivisors.eq_zero_of_mul_eq_zero h
+  simp [eq_coeff_cert]; intro h _; subst p₁; simp [*]
+  exact no_nat_zero_divisors k (p₂.denote ctx) h
 
 def coeff_cert (p₁ p₂ : Poly) (k : Nat) :=
   k > 0 && p₁ == p₂.mul k
@@ -521,8 +516,8 @@ theorem eq_diseq_subst {α} [IntModule α] [NoNatZeroDivisors α] (ctx : Context
       cases Int.natAbs_eq_iff.mp (Eq.refl k₁.natAbs)
       next h => rw [← h]; assumption
       next h => replace h := congrArg (- ·) h; simp at h; rw [← h, IntModule.neg_hmul, h₃, IntModule.neg_zero]
-    simpa [hmul_nat] using this
-  have := NoNatZeroDivisors.eq_zero_of_mul_eq_zero hne this
+    exact this
+  have := no_nat_zero_divisors (k₁.natAbs) (p₂.denote ctx) hne this
   contradiction
 
 def eq_diseq_subst1_cert (k : Int) (p₁ p₂ p₃ : Poly) : Bool :=

src/Init/Grind/Ordered/Module.lean

@@ -146,7 +146,8 @@ instance : IntModule.IsOrdered M where
     match k with
     | (k + 1 : Nat) => by
       intro h
-      simpa [hmul_zero, ← hmul_nat] using hmul_lt_hmul_iff (k := k + 1) h
+      have := hmul_lt_hmul_iff (k := k + 1) h
+      simpa [NatModule.hmul_zero] using hmul_lt_hmul_iff (k := k + 1) h
     | (0 : Nat) => by simp [zero_hmul]; intro h; exact Preorder.lt_irrefl 0
     | -(k + 1 : Nat) => by
       intro h
@@ -157,11 +158,11 @@ instance : IntModule.IsOrdered M where
       simp
       intro h'
       rw [NatModule.IsOrdered.neg_le_iff, neg_zero]
-      simpa [hmul_zero, ← hmul_nat] using hmul_le_hmul (k := k + 1) (Preorder.le_of_lt h)
+      simpa [NatModule.hmul_zero] using hmul_le_hmul (k := k + 1) (Preorder.le_of_lt h)
   hmul_nonneg {k a} h :=
     match k, h with
     | (k : Nat), _ => by
-      simpa [hmul_nat] using NatModule.IsOrdered.hmul_nonneg
+      simpa using NatModule.IsOrdered.hmul_nonneg
 
 end
 

src/Init/Grind/Ordered/Ring.lean

@@ -15,7 +15,7 @@ namespace Lean.Grind
 A ring which is also equipped with a preorder is considered a strict ordered ring if addition, negation,
 and multiplication are compatible with the preorder, and `0 < 1`.
 -/
-class Ring.IsOrdered (R : Type u) [Ring R] [Preorder R] extends NatModule.IsOrdered R where
+class Ring.IsOrdered (R : Type u) [Ring R] [Preorder R] extends IntModule.IsOrdered R where
   /-- In a strict ordered semiring, we have `0 < 1`. -/
   zero_lt_one : (0 : R) < 1
   /-- In a strict ordered semiring, we can multiply an inequality `a < b` on the left
@@ -35,7 +35,7 @@ variable [Preorder R] [Ring.IsOrdered R]
 
 theorem neg_one_lt_zero : (-1 : R) < 0 := by
   have h := zero_lt_one (R := R)
-  have := NatModule.IsOrdered.add_lt_left h (-1)
+  have := IntModule.IsOrdered.add_lt_left h (-1)
   rw [Semiring.zero_add, Ring.add_neg_cancel] at this
   assumption
 
@@ -45,7 +45,7 @@ theorem ofNat_nonneg (x : Nat) : (OfNat.ofNat x : R) ≥ 0 := by
   next n ih =>
     have := Ring.IsOrdered.zero_lt_one (R := R)
     rw [Semiring.ofNat_succ]
-    replace ih := NatModule.IsOrdered.add_le_left ih 1
+    replace ih := IntModule.IsOrdered.add_le_left ih 1
     rw [Semiring.zero_add] at ih
     have := Preorder.lt_of_lt_of_le this ih
     exact Preorder.le_of_lt this

src/Init/Grind/Ring/Basic.lean

@@ -125,9 +125,6 @@ attribute [instance 100] Semiring.ofNat
 
 attribute [local instance] Semiring.natCast Ring.intCast
 
--- Verify that the diamond from `CommRing` to `Semiring` via either `CommSemiring` or `Ring` is defeq.
-example [CommRing α] : (CommSemiring.toSemiring : Semiring α) = (Ring.toSemiring : Semiring α) := rfl
-
 namespace Semiring
 
 variable {α : Type u} [Semiring α]
@@ -337,11 +334,7 @@ theorem intCast_pow (x : Int) (k : Nat) : ((x ^ k : Int) : α) = (x : α) ^ k :=
   next k ih => simp [pow_succ, Int.pow_succ, intCast_mul, *]
 
 instance : IntModule α where
-  hmulInt := ⟨fun a x => a * x⟩
-  hmulNat := ⟨fun a x => a * x⟩
-  hmul_nat n x := by
-    change ((n : Int) : α) * x = (n : α) * x
-    rw [intCast_natCast]
+  hMul a x := a * x
   add_zero := by simp [add_zero]
   add_assoc := by simp [add_assoc]
   add_comm := by simp [add_comm]
@@ -355,9 +348,6 @@ instance : IntModule α where
 
 theorem hmul_eq_intCast_mul {α} [Ring α] {k : Int} {a : α} : HMul.hMul (α := Int) k a = (k : α) * a := rfl
 
--- Verify that the diamond from `Ring` to `NatModule` via either `Semiring` or `IntModule` is defeq.
-example [Ring R] : (Semiring.instNatModule : NatModule R) = (IntModule.toNatModule R) := rfl
-
 end Ring
 
 namespace CommSemiring
@@ -527,22 +517,20 @@ end Ring
 
 end IsCharP
 
-theorem no_int_zero_divisors {α : Type u} [IntModule α] [NoNatZeroDivisors α] {k : Int} {a : α}
+-- TODO: This should be generalizable to any `IntModule α`, not just `Ring α`.
+theorem no_int_zero_divisors {α : Type u} [Ring α] [NoNatZeroDivisors α] {k : Int} {a : α}
     : k ≠ 0 → k * a = 0 → a = 0 := by
   match k with
   | (k : Nat) =>
     simp [intCast_natCast]
     intro h₁ h₂
     replace h₁ : k ≠ 0 := by intro h; simp [h] at h₁
-    rw [IntModule.hmul_nat] at h₂
-    exact NoNatZeroDivisors.eq_zero_of_mul_eq_zero h₁ h₂
+    exact no_nat_zero_divisors k a h₁ h₂
   | -(k+1 : Nat) =>
-    rw [IntModule.neg_hmul]
+    rw [Int.natCast_add, ← Int.natCast_add, intCast_neg, intCast_natCast]
     intro _ h
-    replace h := congrArg (-·) h
-    dsimp only at h
-    rw [IntModule.neg_neg, IntModule.neg_zero] at h
-    rw [IntModule.hmul_nat] at h
-    exact NoNatZeroDivisors.eq_zero_of_mul_eq_zero (Nat.succ_ne_zero _) h
+    replace h := congrArg (-·) h; simp at h
+    rw [← neg_mul, neg_neg, neg_zero, ← hmul_eq_natCast_mul] at h
+    exact no_nat_zero_divisors (k+1) a (Nat.succ_ne_zero _) h
 
 end Lean.Grind

src/Init/Grind/Ring/Field.lean

@@ -71,19 +71,20 @@ theorem inv_eq_zero_iff {a : α} : a⁻¹ = 0 ↔ a = 0 := by
 theorem zero_eq_inv_iff {a : α} : 0 = a⁻¹ ↔ 0 = a := by
   rw [eq_comm, inv_eq_zero_iff, eq_comm]
 
-instance [IsCharP α 0] : NoNatZeroDivisors α := NoNatZeroDivisors.mk' <| by
-  intro a b h w
-  have := IsCharP.natCast_eq_zero_iff (α := α) 0 a
-  simp only [Nat.mod_zero, h, iff_false] at this
-  if h : b = 0 then
-    exact h
-  else
-    rw [Semiring.ofNat_eq_natCast] at w
-    replace w := congrArg (fun x => x * b⁻¹) w
-    dsimp only [] at w
-    rw [Semiring.hmul_eq_ofNat_mul, Semiring.mul_assoc, Field.mul_inv_cancel h, Semiring.mul_one,
-      Semiring.natCast_zero, Semiring.zero_mul, Semiring.ofNat_eq_natCast] at w
-    contradiction
+instance [IsCharP α 0] : NoNatZeroDivisors α where
+  no_nat_zero_divisors := by
+    intro a b h w
+    have := IsCharP.natCast_eq_zero_iff (α := α) 0 a
+    simp only [Nat.mod_zero, h, iff_false] at this
+    if h : b = 0 then
+      exact h
+    else
+      rw [Semiring.ofNat_eq_natCast] at w
+      replace w := congrArg (fun x => x * b⁻¹) w
+      dsimp only [] at w
+      rw [Semiring.hmul_eq_ofNat_mul, Semiring.mul_assoc, Field.mul_inv_cancel h, Semiring.mul_one,
+        Semiring.natCast_zero, Semiring.zero_mul, Semiring.ofNat_eq_natCast] at w
+      contradiction
 
 end Field
 

src/Init/Grind/Ring/Poly.lean

@@ -28,7 +28,7 @@ inductive Expr where
   | sub  (a b : Expr)
   | mul (a b : Expr)
   | pow (a : Expr) (k : Nat)
-  deriving Inhabited, BEq, Hashable, Repr
+  deriving Inhabited, BEq, Hashable
 
 abbrev Context (α : Type u) := RArray α
 
@@ -553,7 +553,7 @@ theorem Mon.denote_mul {α} [CommRing α] (ctx : Context α) (m₁ m₂ : Mon)
   unfold mul
   generalize hugeFuel = fuel
   fun_induction mul.go
-    <;> simp [denote, denote_concat, one_mul,
+    <;> simp [denote, denote_concat, one_mul, 
       mul_assoc, mul_left_comm, mul_comm, *]
   next h₁ h₂ _ =>
     have := eq_of_blt_false h₁ h₂

src/Init/Grind/Tactics.lean

@@ -66,26 +66,26 @@ Reset all `grind` attributes. This command is intended for testing purposes only
 syntax (name := resetGrindAttrs) "reset_grind_attrs%" : command
 
 namespace Attr
-syntax grindGen    := ppSpace &"gen"
-syntax grindEq     := "=" (grindGen)?
-syntax grindEqBoth := atomic("_" "=" "_") (grindGen)?
-syntax grindEqRhs  := atomic("=" "_") (grindGen)?
-syntax grindEqBwd  := atomic("←" "=") <|> atomic("<-" "=")
-syntax grindBwd    := ("←" <|> "<-") (grindGen)?
-syntax grindFwd    := "→" <|> "->"
-syntax grindRL     := "⇐" <|> "<="
-syntax grindLR     := "⇒" <|> "=>"
-syntax grindUsr    := &"usr"
-syntax grindCases  := &"cases"
-syntax grindCasesEager := atomic(&"cases" &"eager")
-syntax grindIntro  := &"intro"
-syntax grindExt    := &"ext"
+syntax grindGen    := &"gen "
+syntax grindEq     := "= " (grindGen)?
+syntax grindEqBoth := atomic("_" "=" "_ ") (grindGen)?
+syntax grindEqRhs  := atomic("=" "_ ") (grindGen)?
+syntax grindEqBwd  := atomic("←" "= ") <|> atomic("<-" "= ")
+syntax grindBwd    := ("← " <|> "<- ") (grindGen)?
+syntax grindFwd    := "→ " <|> "-> "
+syntax grindRL     := "⇐ " <|> "<= "
+syntax grindLR     := "⇒ " <|> "=> "
+syntax grindUsr    := &"usr "
+syntax grindCases  := &"cases "
+syntax grindCasesEager := atomic(&"cases" &"eager ")
+syntax grindIntro  := &"intro "
+syntax grindExt    := &"ext "
 syntax grindMod :=
     grindEqBoth <|> grindEqRhs <|> grindEq <|> grindEqBwd <|> grindBwd
     <|> grindFwd <|> grindRL <|> grindLR <|> grindUsr <|> grindCasesEager
     <|> grindCases <|> grindIntro <|> grindExt <|> grindGen
-syntax (name := grind) "grind" ppSpace (grindMod)? : attr
-syntax (name := grind?) "grind?" ppSpace (grindMod)? : attr
+syntax (name := grind) "grind" (grindMod)? : attr
+syntax (name := grind?) "grind?" (grindMod)? : attr
 end Attr
 end Lean.Parser
 
@@ -204,7 +204,7 @@ namespace Lean.Parser.Tactic
 -/
 
 syntax grindErase := "-" ident
-syntax grindLemma := (Attr.grindMod ppSpace)? ident
+syntax grindLemma := (Attr.grindMod)? ident
 syntax grindParam := grindErase <|> grindLemma
 
 syntax (name := grind)

src/Init/GrindInstances/Ring/Int.lean

@@ -33,9 +33,13 @@ instance : IsCharP Int 0 := IsCharP.mk' _ _
   (ofNat_eq_zero_iff := fun x => by erw [Int.ofNat_eq_zero]; simp)
 
 instance : NoNatZeroDivisors Int where
-  no_nat_zero_divisors k a b h₁ h₂ := by
-    replace h₁ : (k : Int) ≠ 0 := by simp [h₁]
-    cases Int.mul_eq_mul_left_iff h₁ |>.mp h₂
-    rfl
+  no_nat_zero_divisors k a h₁ h₂ := by
+    cases Int.mul_eq_zero.mp h₂
+    next h =>
+      rw [← Int.natCast_zero] at h
+      have h : (k : Int).toNat = (↑0 : Int).toNat := congrArg Int.toNat h;
+      simp at h
+      contradiction
+    next => assumption
 
 end Lean.Grind

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

@@ -40,8 +40,7 @@ where
   | .var x => return (← getStruct).vars[x]!
   | .add a b => return mkApp2 (← getStruct).addFn (← go a) (← go b)
   | .sub a b => return mkApp2 (← getStruct).subFn (← go a) (← go b)
-  | .natMul k a => return mkApp2 (← getStruct).hmulNatFn (mkNatLit k) (← go a)
-  | .intMul k a => return mkApp2 (← getStruct).hmulFn (mkIntLit k) (← go a)
+  | .mul k a => return mkApp2 (← getStruct).hmulFn (mkIntLit k) (← go a)
   | .neg a => return mkApp (← getStruct).negFn (← go a)
 
 private def mkEq (a b : Expr) : M Expr := do

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

@@ -75,18 +75,18 @@ where
   processHMul (i a b : Expr) : LinearM (Option LinExpr) := do
     if isHMulInst (← getStruct) i then
       let some k ← getIntValue? a | return none
-      return some (.intMul k (← go b))
+      return some (.mul k (← go b))
     else if isHMulNatInst (← getStruct) i then
       let some k ← getNatValue? a | return none
-      return some (.natMul k (← go b))
+      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 (.intMul k (← go b))
+      return some (.mul k (← go b))
     else if isHSMulNatInst (← getStruct) i then
       let some k ← getNatValue? a | return none
-      return some (.natMul k (← go b))
+      return some (.mul k (← go b))
     return none
   go (e : Expr) : LinearM LinExpr := do
     match_expr e with

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

@@ -129,8 +129,7 @@ where
     ensureToHomoFieldDefEq addInst intModuleInst ``Grind.IntModule.toAdd ``instHAdd
     ensureToHomoFieldDefEq subInst intModuleInst ``Grind.IntModule.toSub ``instHSub
     ensureToFieldDefEq negInst intModuleInst ``Grind.IntModule.toNeg
-    ensureToFieldDefEq hmulInst intModuleInst ``Grind.IntModule.hmulInt
-    ensureToFieldDefEq hmulNatInst intModuleInst ``Grind.IntModule.hmulNat
+    ensureToFieldDefEq hmulInst intModuleInst ``Grind.IntModule.toHMul
     let preorderInst? ← getInst? ``Grind.Preorder
     let isOrdInst? ← if let some preorderInst := preorderInst? then
       let isOrderedType := mkApp3 (mkConst ``Grind.IntModule.IsOrdered [u]) type preorderInst intModuleInst
@@ -185,7 +184,7 @@ where
     let getNoNatZeroDivInst? : GoalM (Option Expr) := do
       let hmulNat := mkApp3 (mkConst ``HMul [0, u, u]) Nat.mkType type type
       let .some hmulInst ← trySynthInstance hmulNat | return none
-      let noNatZeroDivType := mkApp2 (mkConst ``Grind.NoNatZeroDivisors [u]) type hmulInst
+      let noNatZeroDivType := mkApp3 (mkConst ``Grind.NoNatZeroDivisors [u]) type zeroInst hmulInst
       return LOption.toOption (← trySynthInstance noNatZeroDivType)
     let noNatDivInst? ← getNoNatZeroDivInst?
     let id := (← get').structs.size

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

@@ -32,8 +32,7 @@ def ofLinExpr (e : Linarith.Expr) : Expr :=
   | .add a b => mkApp2 (mkConst ``Linarith.Expr.add) (ofLinExpr a) (ofLinExpr b)
   | .sub a b => mkApp2 (mkConst ``Linarith.Expr.sub) (ofLinExpr a) (ofLinExpr b)
   | .neg a => mkApp (mkConst ``Linarith.Expr.neg) (ofLinExpr a)
-  | .natMul k a => mkApp2 (mkConst ``Linarith.Expr.natMul) (toExpr k) (ofLinExpr a)
-  | .intMul k a => mkApp2 (mkConst ``Linarith.Expr.intMul) (toExpr k) (ofLinExpr a)
+  | .mul k a => mkApp2 (mkConst ``Linarith.Expr.mul) (toExpr k) (ofLinExpr a)
 
 instance : ToExpr Linarith.Expr where
   toExpr := ofLinExpr

src/Lean/Meta/Tactic/Grind/Arith/Util.lean

@@ -162,9 +162,11 @@ def getIsCharInst? (u : Level) (type : Expr) (semiringInst : Expr) : MetaM (Opti
   pure <| some (charInst, n)
 
 def getNoZeroDivInst? (u : Level) (type : Expr) : MetaM (Option Expr) := do
+  let zeroType := mkApp (mkConst ``Zero [u]) type
+  let .some zeroInst ← trySynthInstance zeroType | return none
   let hmulType := mkApp3 (mkConst ``HMul [0, u, u]) (mkConst ``Nat []) type type
   let .some hmulInst ← trySynthInstance hmulType | return none
-  let noZeroDivType := mkApp2 (mkConst ``Grind.NoNatZeroDivisors [u]) type hmulInst
+  let noZeroDivType := mkApp3 (mkConst ``Grind.NoNatZeroDivisors [u]) type zeroInst hmulInst
   LOption.toOption <$> trySynthInstance noZeroDivType
 
 @[specialize] def split (cs : PArray α) (getCoeff : α → Int) : PArray α × Array (Int × α) := Id.run do

src/Lean/Meta/Tactic/Grind/Attr.lean

@@ -20,28 +20,28 @@ inductive AttrKind where
 /-- Return theorem kind for `stx` of the form `Attr.grindThmMod` -/
 def getAttrKindCore (stx : Syntax) : CoreM AttrKind := do
   match stx with
-  | `(Parser.Attr.grindMod|=) => return .ematch (.eqLhs false)
-  | `(Parser.Attr.grindMod|= gen) => return .ematch (.eqLhs true)
-  | `(Parser.Attr.grindMod|→)
-  | `(Parser.Attr.grindMod|->) => return .ematch .fwd
-  | `(Parser.Attr.grindMod|←)
-  | `(Parser.Attr.grindMod|<-) => return .ematch (.bwd false)
-  | `(Parser.Attr.grindMod|<- gen) => return .ematch (.bwd true)
-  | `(Parser.Attr.grindMod|=_) => return .ematch (.eqRhs false)
-  | `(Parser.Attr.grindMod|=_ gen) => return .ematch (.eqRhs true)
-  | `(Parser.Attr.grindMod|_=_) => return .ematch (.eqBoth false)
-  | `(Parser.Attr.grindMod|_=_ gen) => return .ematch (.eqBoth true)
-  | `(Parser.Attr.grindMod|←=) => return .ematch .eqBwd
-  | `(Parser.Attr.grindMod|⇒)
-  | `(Parser.Attr.grindMod|=>) => return .ematch .leftRight
-  | `(Parser.Attr.grindMod|⇐)
-  | `(Parser.Attr.grindMod|<=) => return .ematch .rightLeft
-  | `(Parser.Attr.grindMod|usr) => return .ematch .user
-  | `(Parser.Attr.grindMod|gen) => return .ematch (.default true)
-  | `(Parser.Attr.grindMod|cases) => return .cases false
-  | `(Parser.Attr.grindMod|cases eager) => return .cases true
-  | `(Parser.Attr.grindMod|intro) => return .intro
-  | `(Parser.Attr.grindMod|ext) => return .ext
+  | `(Parser.Attr.grindMod| =) => return .ematch (.eqLhs false)
+  | `(Parser.Attr.grindMod| = gen) => return .ematch (.eqLhs true)
+  | `(Parser.Attr.grindMod| →)
+  | `(Parser.Attr.grindMod| ->) => return .ematch .fwd
+  | `(Parser.Attr.grindMod| ←)
+  | `(Parser.Attr.grindMod| <-) => return .ematch (.bwd false)
+  | `(Parser.Attr.grindMod| <- gen) => return .ematch (.bwd true)
+  | `(Parser.Attr.grindMod| =_) => return .ematch (.eqRhs false)
+  | `(Parser.Attr.grindMod| =_ gen) => return .ematch (.eqRhs true)
+  | `(Parser.Attr.grindMod| _=_) => return .ematch (.eqBoth false)
+  | `(Parser.Attr.grindMod| _=_ gen) => return .ematch (.eqBoth true)
+  | `(Parser.Attr.grindMod| ←=) => return .ematch .eqBwd
+  | `(Parser.Attr.grindMod| ⇒)
+  | `(Parser.Attr.grindMod| =>) => return .ematch .leftRight
+  | `(Parser.Attr.grindMod| ⇐)
+  | `(Parser.Attr.grindMod| <=) => return .ematch .rightLeft
+  | `(Parser.Attr.grindMod| usr) => return .ematch .user
+  | `(Parser.Attr.grindMod| gen) => return .ematch (.default true)
+  | `(Parser.Attr.grindMod| cases) => return .cases false
+  | `(Parser.Attr.grindMod| cases eager) => return .cases true
+  | `(Parser.Attr.grindMod| intro) => return .intro
+  | `(Parser.Attr.grindMod| ext) => return .ext
   | _ => throwError "unexpected `grind` theorem kind: `{stx}`"
 
 /-- Return theorem kind for `stx` of the form `(Attr.grindMod)?` -/

tests/lakefile.toml

@@ -1,5 +0,0 @@
-name = "tests"
-
-# Allow `module` in tests when opened in the language server.
-# Enabled during actual test runs in the respective test_single.sh.
-moreGlobalServerArgs = ["-Dexperimental.module=true"]

tests/lean/run/1016.lean

@@ -1,5 +1,3 @@
-module
-
 inductive t | one | two
 
 example (h : False) : t.one = t.two := by

tests/lean/run/4716.lean

@@ -1,8 +0,0 @@
-def g (f : Nat → Nat) (n : Nat) : Nat :=
-  inner n
-where
-  @[specialize] inner (n : Nat) : Nat :=
-    if n = 0 then 0 else g f (n - 1)
-
-def x := g (fun _ => 0) 0
-

tests/lean/run/grind_linarith_2.lean

@@ -13,7 +13,7 @@ trace: [grind.debug.proof] Classical.byContradiction fun h =>
       let re_2 := (CommRing.Expr.var 0).add (CommRing.Expr.var 1);
       let rp_1 := CommRing.Poly.num 0;
       let e_1 := Expr.zero;
-      let e_2 := Expr.intMul 0 (Expr.var 0);
+      let e_2 := Expr.mul 0 (Expr.var 0);
       let p_1 := Poly.nil;
       diseq_unsat ctx
         (diseq_norm ctx e_2 e_1 p_1 (Eq.refl true) (CommRing.diseq_norm rctx re_2 re_1 rp_1 (Eq.refl true) h))

tests/lean/run/grind_module_normalization.lean

@@ -10,14 +10,6 @@ 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
-
--- Check the everything still works if we use `•` notation.
-
 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
 

tests/lean/run/grind_pp_attr.lean

@@ -1,59 +0,0 @@
-import Lean.Elab.Command
-
-open Lean Elab Command
-
-def test (stx : Syntax) : CommandElabM Unit := do
-  let fmt : Option Format := ←
-        liftCoreM <| PrettyPrinter.ppCategory `command stx
-  if let some fmt := fmt then
-  let st := fmt.pretty
-  dbg_trace st
-
-
-/--
-info: @[grind =]
-example :=
-  0
--/
-#guard_msgs in
-run_cmd test (← `(@[grind =] example := 0))
-
-/--
-info: @[grind _=_]
-example :=
-  0
--/
-#guard_msgs in
-run_cmd test (← `(@[grind _=_] example := 0))
-
-/--
-info: @[grind =_]
-example :=
-  0
--/
-#guard_msgs in
-run_cmd test (← `(@[grind =_] example := 0))
-
-/--
-info: @[grind →]
-example :=
-  0
--/
-#guard_msgs in
-run_cmd test (← `(@[grind →] example := 0))
-
-/--
-info: @[grind ←]
-example :=
-  0
--/
-#guard_msgs in
-run_cmd test (← `(@[grind ←] example := 0))
-
-/--
-info: @[grind ←=]
-example :=
-  0
--/
-#guard_msgs in
-run_cmd test (← `(@[grind ←=] example := 0))

tests/lean/test_single.sh

@@ -2,5 +2,5 @@
 source ../common.sh
 
 # these tests don't have to succeed
-exec_capture lean -DprintMessageEndPos=true -Dlinter.all=false -Dexperimental.module=true "$f" || true
+exec_capture lean -DprintMessageEndPos=true -Dlinter.all=false -DElab.async=true "$f" || true
 diff_produced