doc-string

This PR refactors the `NoNatZeroDivisors` to make sure it will work
with the new `Semiring` support.

src/Init/Grind/Module/Basic.lean

@@ -48,7 +48,11 @@ satisfying appropriate compatibilities.
 
 Equivalently, an additive commutative group.
 -/
-class IntModule (M : Type u) extends Zero M, Add M, Neg M, Sub M, HMul Int M M where
+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]
   /-- Zero is the right identity for addition. -/
   add_zero : ∀ a : M, a + 0 = a
   /-- Addition is commutative. -/
@@ -69,6 +73,8 @@ class IntModule (M : Type u) extends Zero M, Add M, Neg M, Sub M, HMul Int M M w
   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
 
@@ -83,27 +89,33 @@ 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.toHMul
+attribute [instance 100] IntModule.toZero IntModule.toAdd IntModule.toNeg IntModule.toSub
+  IntModule.hmulNat IntModule.hmulInt
 
 instance toNatModule (M : Type u) [i : IntModule M] : NatModule M :=
   { i with
-    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]
+    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] }
 
 instance (priority := 100) (M : Type u) [IntModule M] : SMul Nat M where
-  smul a x := (a : Int) * x
+  smul a x := a * 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]
 
@@ -171,6 +183,9 @@ 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
@@ -195,6 +210,23 @@ class NoNatZeroDivisors (α : Type u) [HMul Nat α α] where
 
 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 hmul_zero one_hmul
+attribute [local simp] add_zero zero_add zero_hmul nat_zero_hmul hmul_zero one_hmul
 
 inductive Expr where
   | zero
@@ -28,8 +28,9 @@ inductive Expr where
   | add  (a b : Expr)
   | sub  (a b : Expr)
   | neg  (a : Expr)
-  | mul  (k : Int) (a : Expr)
-  deriving Inhabited, BEq
+  | natMul  (k : Nat) (a : Expr)
+  | intMul  (k : Int) (a : Expr)
+  deriving Inhabited, BEq, Repr
 
 abbrev Context (α : Type u) := RArray α
 
@@ -41,13 +42,14 @@ 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
-  | .mul k a  => k * denote ctx a
+  | .natMul k a  => k * denote ctx a
+  | .intMul k a  => k * denote ctx a
   | .neg a    => -denote ctx a
 
 inductive Poly where
   | nil
   | add (k : Int) (v : Var) (p : Poly)
-  deriving BEq
+  deriving BEq, Repr
 
 def Poly.denote {α} [IntModule α] (ctx : Context α) (p : Poly) : α :=
   match p with
@@ -144,7 +146,8 @@ where
     | .var v    => (.add coeff v ·)
     | .add a b  => go coeff a ∘ go coeff b
     | .sub a b  => go coeff a ∘ go (-coeff) b
-    | .mul k a  => bif k == 0 then id else go (Int.mul coeff k) a
+    | .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
     | .neg a    => go (-coeff) a
 
 /-- Converts the given expression into a polynomial, and then normalizes it. -/
@@ -215,6 +218,8 @@ 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]
 
@@ -469,17 +474,10 @@ theorem eq_neg {α} [IntModule α] (ctx : Context α) (p₁ p₂ : Poly)
 def eq_coeff_cert (p₁ p₂ : Poly) (k : Nat) :=
   k != 0 && p₁ == p₂.mul k
 
-theorem no_nat_zero_divisors' [IntModule α] [NoNatZeroDivisors α] (k : Nat) (a : α)
-    : k ≠ 0 → k * a = 0 → a = 0 := by
-  intro h₁ h₂
-  have : k * a = (↑k : Int) * (0 : α) → a = 0 := no_nat_zero_divisors k a 0 h₁
-  rw [IntModule.hmul_zero] at this
-  exact this h₂
-
 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 [*]
-  exact no_nat_zero_divisors' k (p₂.denote ctx) h
+  simp [eq_coeff_cert]; intro h _; subst p₁; simp [*, hmul_nat]
+  exact NoNatZeroDivisors.eq_zero_of_mul_eq_zero h
 
 def coeff_cert (p₁ p₂ : Poly) (k : Nat) :=
   k > 0 && p₁ == p₂.mul k
@@ -523,8 +521,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]
-    exact this
-  have := no_nat_zero_divisors' (k₁.natAbs) (p₂.denote ctx) hne this
+    simpa [hmul_nat] using this
+  have := NoNatZeroDivisors.eq_zero_of_mul_eq_zero hne this
   contradiction
 
 def eq_diseq_subst1_cert (k : Int) (p₁ p₂ p₃ : Poly) : Bool :=

src/Init/Grind/Ordered/Module.lean

@@ -146,8 +146,7 @@ instance : IntModule.IsOrdered M where
     match k with
     | (k + 1 : Nat) => by
       intro h
-      have := hmul_lt_hmul_iff (k := k + 1) h
-      simpa [NatModule.hmul_zero] using hmul_lt_hmul_iff (k := k + 1) h
+      simpa [hmul_zero, ← hmul_nat] 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
@@ -158,11 +157,11 @@ instance : IntModule.IsOrdered M where
       simp
       intro h'
       rw [NatModule.IsOrdered.neg_le_iff, neg_zero]
-      simpa [NatModule.hmul_zero] using hmul_le_hmul (k := k + 1) (Preorder.le_of_lt h)
+      simpa [hmul_zero, ← hmul_nat] 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 using NatModule.IsOrdered.hmul_nonneg
+      simpa [hmul_nat] 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 IntModule.IsOrdered R where
+class Ring.IsOrdered (R : Type u) [Ring R] [Preorder R] extends NatModule.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 := IntModule.IsOrdered.add_lt_left h (-1)
+  have := NatModule.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 := IntModule.IsOrdered.add_le_left ih 1
+    replace ih := NatModule.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,6 +125,9 @@ 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 α]
@@ -334,7 +337,11 @@ 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
-  hMul a x := a * x
+  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]
   add_zero := by simp [add_zero]
   add_assoc := by simp [add_assoc]
   add_comm := by simp [add_comm]
@@ -348,6 +355,9 @@ 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
@@ -517,23 +527,22 @@ end Ring
 
 end IsCharP
 
--- TODO: This should be generalizable to any `IntModule α`, not just `Ring α`.
-theorem no_int_zero_divisors {α : Type u} [Ring α] [NoNatZeroDivisors α] {k : Int} {a : α}
+theorem no_int_zero_divisors {α : Type u} [IntModule α] [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₁
-    replace h₂ : k * a = k * 0 := by simp [mul_zero, h₂]
-    exact no_nat_zero_divisors k a 0 h₁ h₂
+    rw [IntModule.hmul_nat] at h₂
+    exact NoNatZeroDivisors.eq_zero_of_mul_eq_zero h₁ h₂
   | -(k+1 : Nat) =>
-    rw [Int.natCast_add, ← Int.natCast_add, intCast_neg, intCast_natCast]
+    rw [IntModule.neg_hmul]
     intro _ h
-    replace h := congrArg (-·) h; simp at h
-    rw [← neg_mul, neg_neg, neg_zero, ← hmul_eq_natCast_mul] at h
-    replace h : (k + 1 : Nat) * a = (k + 1 : Nat) * 0 := by
-      simp [mul_zero]; exact h
-    exact no_nat_zero_divisors (k+1) a 0 (Nat.succ_ne_zero _) 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
 
 end Lean.Grind

src/Init/Grind/Ring/Field.lean

@@ -71,24 +71,19 @@ 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]
 
-attribute [local instance] Semiring.natCast
-
-instance [IsCharP α 0] : NoNatZeroDivisors α where
-  no_nat_zero_divisors := by
-    intro k a b h₁ h₂
-    replace h₂ : (↑k) * a = (↑k : α) * b := h₂
-    have := IsCharP.natCast_eq_zero_iff (α := α) 0 k
-    simp only [Nat.mod_zero, h₁, iff_false] at this
-    replace h₂ := congrArg (· - k * b) h₂;
-    simp [Ring.sub_self] at h₂
-    rw [Ring.sub_eq_add_neg, CommRing.mul_comm _  b, ←Ring.neg_mul,
-        CommRing.mul_comm (-b), ←Semiring.left_distrib,
-        ← Ring.sub_eq_add_neg] at h₂
-    replace h₂ := congrArg (fun x => x * (↑k:α)⁻¹) h₂
-    simp [Semiring.zero_mul] at h₂
-    rw [Semiring.mul_assoc, CommRing.mul_comm (a - b), ← Semiring.mul_assoc,
-        Field.mul_inv_cancel this, Semiring.one_mul] at h₂
-    exact Ring.sub_eq_zero_iff.mp h₂
+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
 
 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
+  deriving Inhabited, BEq, Hashable, Repr
 
 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/Lean/Meta/Tactic/Grind/Arith/Linear/DenoteExpr.lean

@@ -40,7 +40,8 @@ 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)
-  | .mul k a => return mkApp2 (← getStruct).hmulFn (mkIntLit k) (← go a)
+  | .natMul k a => return mkApp2 (← getStruct).hmulNatFn (mkNatLit k) (← go a)
+  | .intMul 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 (.mul k (← go b))
+      return some (.intMul k (← go b))
     else if isHMulNatInst (← getStruct) i then
       let some k ← getNatValue? a | return none
-      return some (.mul k (← go b))
+      return some (.natMul 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))
+      return some (.intMul k (← go b))
     else if isHSMulNatInst (← getStruct) i then
       let some k ← getNatValue? a | return none
-      return some (.mul k (← go b))
+      return some (.natMul 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,7 +129,8 @@ 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.toHMul
+    ensureToFieldDefEq hmulInst intModuleInst ``Grind.IntModule.hmulInt
+    ensureToFieldDefEq hmulNatInst intModuleInst ``Grind.IntModule.hmulNat
     let preorderInst? ← getInst? ``Grind.Preorder
     let isOrdInst? ← if let some preorderInst := preorderInst? then
       let isOrderedType := mkApp3 (mkConst ``Grind.IntModule.IsOrdered [u]) type preorderInst intModuleInst

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

@@ -32,7 +32,8 @@ 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)
-  | .mul k a => mkApp2 (mkConst ``Linarith.Expr.mul) (toExpr k) (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)
 
 instance : ToExpr Linarith.Expr where
   toExpr := ofLinExpr

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.mul 0 (Expr.var 0);
+      let e_2 := Expr.intMul 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,6 +10,14 @@ 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