chore: remove provable fields from Grind.Nat/IntModule

src/Init/Grind/Module/Basic.lean

@@ -51,14 +51,8 @@ class NatModule (M : Type u) extends AddCommMonoid M where
   [nsmul : HMul Nat M M]
   /-- Scalar multiplication by zero is zero. -/
   zero_nsmul : ∀ a : M, 0 * a = 0
-  /-- Scalar multiplication by one is the identity. -/
-  one_nsmul : ∀ a : M, 1 * a = a
-  /-- Scalar multiplication is distributive over addition in the natural numbers. -/
-  add_nsmul : ∀ n m : Nat, ∀ a : M, (n + m) * a = n * a + m * a
-  /-- Scalar multiplication of zero is zero. -/
-  nsmul_zero : ∀ n : Nat, n * (0 : M) = 0
-  /-- Scalar multiplication is distributive over addition in the module. -/
-  nsmul_add : ∀ n : Nat, ∀ a b : M, n * (a + b) = n * a + n * b
+  /-- Scalar multiplication by a successor. -/
+  add_one_nsmul : ∀ n : Nat, ∀ a : M, (n + 1) * a = n * a + a
 
 attribute [instance 100] NatModule.toAddCommMonoid NatModule.nsmul
 
@@ -79,22 +73,22 @@ class IntModule (M : Type u) extends AddCommGroup M where
   one_zsmul : ∀ a : M, (1 : Int) * a = a
   /-- Scalar multiplication is distributive over addition in the integers. -/
   add_zsmul : ∀ n m : Int, ∀ a : M, (n + m) * a = n * a + m * a
-  /-- Scalar multiplication of zero is zero. -/
-  zsmul_zero : ∀ n : Int, n * (0 : M) = 0
-  /-- Scalar multiplication by integers is distributive over addition in the module. -/
-  zsmul_add : ∀ n : Int, ∀ a b : M, n * (a + b) = n * a + n * b
   /-- Scalar multiplication by natural numbers is consistent with scalar multiplication by integers. -/
   zsmul_natCast_eq_nsmul : ∀ n : Nat, ∀ a : M, (n : Int) * a = n * a
 
 attribute [instance 100] IntModule.toAddCommGroup IntModule.zsmul
 
-instance (priority := 100) IntModule.toNatModule [I : IntModule M] : NatModule M :=
+namespace IntModule
+
+variable {M : Type u} [IntModule M]
+
+instance (priority := 100) toNatModule [I : IntModule M] : NatModule M :=
   { I with
     zero_nsmul a := by rw [← zsmul_natCast_eq_nsmul, Int.natCast_zero, zero_zsmul]
-    one_nsmul a := by rw [← zsmul_natCast_eq_nsmul, Int.natCast_one, one_zsmul]
-    add_nsmul n m a := by rw [← zsmul_natCast_eq_nsmul, Int.natCast_add, add_zsmul, zsmul_natCast_eq_nsmul, zsmul_natCast_eq_nsmul]
-    nsmul_zero n := by rw [← zsmul_natCast_eq_nsmul, zsmul_zero]
-    nsmul_add n a b := by rw [← zsmul_natCast_eq_nsmul, zsmul_add, zsmul_natCast_eq_nsmul, zsmul_natCast_eq_nsmul] }
+    add_one_nsmul n a := by rw [← zsmul_natCast_eq_nsmul, Int.natCast_add_one, add_zsmul,
+      zsmul_natCast_eq_nsmul, one_zsmul] }
+
+end IntModule
 
 namespace AddCommMonoid
 
@@ -173,6 +167,25 @@ namespace NatModule
 
 variable {M : Type u} [NatModule M]
 
+theorem one_nsmul (a : M) : 1 * a = a := by
+  rw [← Nat.zero_add 1, add_one_nsmul, zero_nsmul, AddCommMonoid.zero_add]
+
+theorem add_nsmul (n m : Nat) (a : M) : (n + m) * a = n * a + m * a := by
+  induction m with
+  | zero => rw [Nat.add_zero, zero_nsmul, AddCommMonoid.add_zero]
+  | succ m ih => rw [add_one_nsmul, ← Nat.add_assoc, add_one_nsmul, ih, AddCommMonoid.add_assoc]
+
+theorem nsmul_zero (n : Nat) : n * (0 : M) = 0 := by
+  induction n with
+  | zero => rw [zero_nsmul]
+  | succ n ih => rw [add_one_nsmul, ih, AddCommMonoid.zero_add]
+
+theorem nsmul_add (n : Nat) (a b : M) : n * (a + b) = n * a + n * b := by
+  induction n with
+  | zero => rw [zero_nsmul, zero_nsmul, zero_nsmul, AddCommMonoid.zero_add]
+  | succ n ih => rw [add_one_nsmul, add_one_nsmul, add_one_nsmul, ih, AddCommMonoid.add_assoc,
+      AddCommMonoid.add_left_comm (n * b), AddCommMonoid.add_assoc]
+
 theorem mul_nsmul (n m : Nat) (a : M) : (n * m) * a = n * (m * a) := by
   induction n with
   | zero => simp [zero_nsmul]
@@ -197,6 +210,17 @@ theorem neg_zsmul (n : Int) (a : M) : (-n) * a = - (n * a) := by
   apply (add_left_inj (n * a)).mp
   rw [← add_zsmul, Int.add_left_neg, zero_zsmul, neg_add_cancel]
 
+theorem zsmul_zero (n : Int) : n * (0 : M) = 0 := by
+  match n with
+  | (n : Nat) => rw [zsmul_natCast_eq_nsmul, NatModule.nsmul_zero]
+  | -(n + 1 : Nat) => rw [neg_zsmul, zsmul_natCast_eq_nsmul, NatModule.nsmul_zero, neg_zero]
+
+theorem zsmul_add (n : Int) (a b : M) : n * (a + b) = n * a + n * b := by
+  match n with
+  | (n : Nat) => rw [zsmul_natCast_eq_nsmul, NatModule.nsmul_add, zsmul_natCast_eq_nsmul, zsmul_natCast_eq_nsmul]
+  | -(n + 1 : Nat) => rw [neg_zsmul, zsmul_natCast_eq_nsmul, NatModule.nsmul_add,
+      neg_zsmul, zsmul_natCast_eq_nsmul, neg_zsmul, zsmul_natCast_eq_nsmul, neg_add]
+
 theorem zsmul_neg (n : Int) (a : M) : n * (-a) = - (n * a) := by
   apply (add_left_inj (n * a)).mp
   rw [← zsmul_add, neg_add_cancel, neg_add_cancel, zsmul_zero]

src/Init/Grind/Module/Envelope.lean

@@ -158,20 +158,6 @@ theorem zero_zsmul (a : Q α) : zsmul 0 a = zero := by
   induction a using Quot.ind
   next a => cases a; simp
 
-theorem zsmul_zero (a : Int) : zsmul a (zero : Q α) = zero := by
-  simp
-
-theorem zsmul_add (a : Int) (b c : Q α) : zsmul a (add b c) = add (zsmul a b) (zsmul a c) := by
-  induction b using Q.ind
-  induction c using Q.ind
-  next b c =>
-  cases b; cases c; simp
-  split <;>
-  · apply Quot.sound
-    refine ⟨0, ?_⟩
-    simp
-    ac_rfl
-
 theorem add_zsmul (a b : Int) (c : Q α) : zsmul (a + b) c = add (zsmul a c) (zsmul b c) := by
   induction c using Q.ind
   next c =>
@@ -228,7 +214,7 @@ def ofNatModule : IntModule (Q α) := {
   add, sub, neg,
   add_comm, add_assoc, add_zero,
   neg_add_cancel, sub_eq_add_neg,
-  one_zsmul, zero_zsmul, zsmul_zero, zsmul_add, add_zsmul,
+  one_zsmul, zero_zsmul, add_zsmul,
   zsmul_natCast_eq_nsmul
 }
 

src/Init/Grind/Ring/Basic.lean

@@ -157,10 +157,8 @@ theorem ofNat_add (a b : Nat) : OfNat.ofNat (α := α) (a + b) = OfNat.ofNat a +
 instance toNatModule [I : Semiring α] : NatModule α :=
   { I with
     zero_nsmul a := by rw [nsmul_eq_natCast_mul, ← ofNat_eq_natCast, zero_mul]
-    one_nsmul a := by rw [nsmul_eq_natCast_mul, ← ofNat_eq_natCast, one_mul]
-    add_nsmul n m a := by rw [nsmul_eq_natCast_mul, ← ofNat_eq_natCast, ofNat_add, right_distrib, ofNat_eq_natCast, ofNat_eq_natCast, ← nsmul_eq_natCast_mul, ← nsmul_eq_natCast_mul]
-    nsmul_zero n := by rw [nsmul_eq_natCast_mul, mul_zero]
-    nsmul_add n a b := by rw [nsmul_eq_natCast_mul, ← ofNat_eq_natCast, left_distrib, ofNat_eq_natCast, ← nsmul_eq_natCast_mul, ← nsmul_eq_natCast_mul] }
+    add_one_nsmul n a := by rw [nsmul_eq_natCast_mul, ← ofNat_eq_natCast, ofNat_add, right_distrib,
+      ofNat_eq_natCast, ← nsmul_eq_natCast_mul, ofNat_eq_natCast, natCast_one, one_mul] }
 
 theorem natCast_add (a b : Nat) : ((a + b : Nat) : α) = ((a : α) + (b : α)) := by
   rw [← ofNat_eq_natCast, ← ofNat_eq_natCast, ofNat_add, ofNat_eq_natCast, ofNat_eq_natCast]
@@ -295,10 +293,7 @@ instance toIntModule [I : Ring α] : IntModule α :=
   { I, Semiring.toNatModule (α := α) with
     zero_zsmul a := by rw [← Int.natCast_zero, zsmul_natCast_eq_nsmul, zero_nsmul]
     one_zsmul a := by rw [← Int.natCast_one, zsmul_natCast_eq_nsmul, one_nsmul]
-    add_zsmul n m a := by rw [zsmul_eq_intCast_mul, intCast_add, right_distrib, zsmul_eq_intCast_mul, zsmul_eq_intCast_mul]
-    zsmul_zero n := by rw [zsmul_eq_intCast_mul, mul_zero]
-    zsmul_add n a b := by
-      rw [zsmul_eq_intCast_mul, left_distrib, zsmul_eq_intCast_mul, zsmul_eq_intCast_mul] }
+    add_zsmul n m a := by rw [zsmul_eq_intCast_mul, intCast_add, right_distrib, zsmul_eq_intCast_mul, zsmul_eq_intCast_mul] }
 
 private theorem intCast_mul_aux (x y : Nat) : ((x * y : Int) : α) = ((x : α) * (y : α)) := by
   rw [Int.ofNat_mul_ofNat, intCast_natCast, natCast_mul]