feat: preparation for semirings and noncommutative rings in grind (#8343)

This PR splits `Lean.Grind.CommRing` into 4 typeclasses, for semirings
and noncommutative rings. This does not yet change the behaviour of
`grind`, which expects to find all 4 typeclasses. Later we will make
some generalizations.

Author: kim-em

src/Init/Data/BitVec/Lemmas.lean

@@ -3731,6 +3731,10 @@ theorem mul_add {x y z : BitVec w} :
   rw [Nat.mul_mod, Nat.mod_mod (y.toNat + z.toNat),
     ← Nat.mul_mod, Nat.mul_add]
 
+theorem add_mul {x y z : BitVec w} :
+    (x + y) * z = x * z + y * z := by
+  rw [BitVec.mul_comm, mul_add, BitVec.mul_comm z, BitVec.mul_comm z]
+
 theorem mul_succ {x y : BitVec w} : x * (y + 1#w) = x * y + x := by simp [mul_add]
 theorem succ_mul {x y : BitVec w} : (x + 1#w) * y = x * y + y := by simp [BitVec.mul_comm, BitVec.mul_add]
 

src/Init/Grind/CommRing/Basic.lean

@@ -30,39 +30,51 @@ theorem ofNat_eq_iff_of_lt {x y : Nat} (h₁ : x < p) (h₂ : y < p) :
 
 namespace Lean.Grind
 
-class CommRing (α : Type u) extends Add α, Mul α, Neg α, Sub α, HPow α Nat α where
+class Semiring (α : Type u) extends Add α, Mul α, HPow α Nat α where
   [ofNat : ∀ n, OfNat α n]
   [natCast : NatCast α]
-  [intCast : IntCast α]
   add_assoc : ∀ a b c : α, a + b + c = a + (b + c)
   add_comm : ∀ a b : α, a + b = b + a
   add_zero : ∀ a : α, a + 0 = a
-  neg_add_cancel : ∀ a : α, -a + a = 0
   mul_assoc : ∀ a b c : α, a * b * c = a * (b * c)
-  mul_comm : ∀ a b : α, a * b = b * a
   mul_one : ∀ a : α, a * 1 = a
+  one_mul : ∀ a : α, 1 * a = a
   left_distrib : ∀ a b c : α, a * (b + c) = a * b + a * c
+  right_distrib : ∀ a b c : α, (a + b) * c = a * c + b * c
   zero_mul : ∀ a : α, 0 * a = 0
-  sub_eq_add_neg : ∀ a b : α, a - b = a + -b
+  mul_zero : ∀ a : α, a * 0 = 0
   pow_zero : ∀ a : α, a ^ 0 = 1
   pow_succ : ∀ a : α, ∀ n : Nat, a ^ (n + 1) = (a ^ n) * a
   ofNat_succ : ∀ a : Nat, OfNat.ofNat (α := α) (a + 1) = OfNat.ofNat a + 1 := by intros; rfl
   ofNat_eq_natCast : ∀ n : Nat, OfNat.ofNat (α := α) n = Nat.cast n := by intros; rfl
+
+class Ring (α : Type u) extends Semiring α, Neg α, Sub α where
+  [intCast : IntCast α]
+  neg_add_cancel : ∀ a : α, -a + a = 0
+  sub_eq_add_neg : ∀ a b : α, a - b = a + -b
   intCast_ofNat : ∀ n : Nat, Int.cast (OfNat.ofNat (α := Int) n) = OfNat.ofNat (α := α) n := by intros; rfl
   intCast_neg : ∀ i : Int, Int.cast (R := α) (-i) = -Int.cast i := by intros; rfl
 
+class CommSemiring (α : Type u) extends Semiring α where
+  mul_comm : ∀ a b : α, a * b = b * a
+  one_mul := by intro a; rw [mul_comm, mul_one]
+  mul_zero := by intro a; rw [mul_comm, zero_mul]
+  right_distrib := by intro a b c; rw [mul_comm, left_distrib, mul_comm c, mul_comm c]
+
+class CommRing (α : Type u) extends Ring α, CommSemiring α
+
 -- We reduce the priority of these parent instances,
 -- so that in downstream libraries with their own `CommRing` class,
 -- the path `CommRing -> Add` is found before `CommRing -> Lean.Grind.CommRing -> Add`.
 -- (And similarly for the other parents.)
-attribute [instance 100] CommRing.toAdd CommRing.toMul CommRing.toNeg CommRing.toSub CommRing.toHPow
+attribute [instance 100] Semiring.toAdd Semiring.toMul Semiring.toHPow Ring.toNeg Ring.toSub
 
 -- This is a low-priority instance, to avoid conflicts with existing `OfNat`, `NatCast`, and `IntCast` instances.
-attribute [instance 100] CommRing.ofNat CommRing.natCast CommRing.intCast
+attribute [instance 100] Semiring.ofNat Semiring.natCast Ring.intCast
 
-namespace CommRing
+namespace Semiring
 
-variable {α : Type u} [CommRing α]
+variable {α : Type u} [Semiring α]
 
 theorem natCast_zero : ((0 : Nat) : α) = 0 := (ofNat_eq_natCast 0).symm
 theorem natCast_one : ((1 : Nat) : α) = 1 := (ofNat_eq_natCast 1).symm
@@ -80,24 +92,9 @@ theorem natCast_succ (n : Nat) : ((n + 1 : Nat) : α) = ((n : α) + 1) := by
 theorem zero_add (a : α) : 0 + a = a := by
   rw [add_comm, add_zero]
 
-theorem add_neg_cancel (a : α) : a + -a = 0 := by
-  rw [add_comm, neg_add_cancel]
-
 theorem add_left_comm (a b c : α) : a + (b + c) = b + (a + c) := by
   rw [← add_assoc, ← add_assoc, add_comm a]
 
-theorem one_mul (a : α) : 1 * a = a := by
-  rw [mul_comm, mul_one]
-
-theorem right_distrib (a b c : α) : (a + b) * c = a * c + b * c := by
-  rw [mul_comm, left_distrib, mul_comm c, mul_comm c]
-
-theorem mul_zero (a : α) : a * 0 = 0 := by
-  rw [mul_comm, zero_mul]
-
-theorem mul_left_comm (a b c : α) : a * (b * c) = b * (a * c) := by
-  rw [← mul_assoc, ← mul_assoc, mul_comm a]
-
 theorem ofNat_mul (a b : Nat) : OfNat.ofNat (α := α) (a * b) = OfNat.ofNat a * OfNat.ofNat b := by
   induction b with
   | zero => simp [Nat.mul_zero, mul_zero]
@@ -106,6 +103,22 @@ theorem ofNat_mul (a b : Nat) : OfNat.ofNat (α := α) (a * b) = OfNat.ofNat a *
 theorem natCast_mul (a b : Nat) : ((a * b : Nat) : α) = ((a : α) * (b : α)) := by
   rw [← ofNat_eq_natCast, ofNat_mul, ofNat_eq_natCast, ofNat_eq_natCast]
 
+theorem pow_add (a : α) (k₁ k₂ : Nat) : a ^ (k₁ + k₂) = a^k₁ * a^k₂ := by
+  induction k₂
+  next => simp [pow_zero, mul_one]
+  next k₂ ih => rw [Nat.add_succ, pow_succ, pow_succ, ih, mul_assoc]
+
+end Semiring
+
+namespace Ring
+
+open Semiring
+
+variable {α : Type u} [Ring α]
+
+theorem add_neg_cancel (a : α) : a + -a = 0 := by
+  rw [add_comm, neg_add_cancel]
+
 theorem add_left_inj {a b : α} (c : α) : a + c = b + c ↔ a = b :=
   ⟨fun h => by simpa [add_assoc, add_neg_cancel, add_zero] using (congrArg (· + -c) h),
    fun g => congrArg (· + c) g⟩
@@ -198,11 +211,17 @@ theorem neg_eq_neg_one_mul (a : α) : -a = (-1) * a := by
   rw [← right_distrib, ← intCast_neg_one, ← intCast_one (α := α)]
   simp [← intCast_add, intCast_zero, zero_mul]
 
+theorem neg_eq_mul_neg_one (a : α) : -a = a * (-1) := by
+  rw [← add_left_inj a, neg_add_cancel]
+  conv => rhs; arg 2; rw [← mul_one a]
+  rw [← left_distrib, ← intCast_neg_one, ← intCast_one (α := α)]
+  simp [← intCast_add, intCast_zero, mul_zero]
+
 theorem neg_mul (a b : α) : (-a) * b = -(a * b) := by
   rw [neg_eq_neg_one_mul a, neg_eq_neg_one_mul (a * b), mul_assoc]
 
 theorem mul_neg (a b : α) : a * (-b) = -(a * b) := by
-  rw [mul_comm, neg_mul, mul_comm]
+  rw [neg_eq_mul_neg_one b, neg_eq_mul_neg_one (a * b), mul_assoc]
 
 theorem intCast_nat_mul (x y : Nat) : ((x * y : Int) : α) = ((x : α) * (y : α)) := by
   rw [Int.ofNat_mul_ofNat, intCast_natCast, natCast_mul]
@@ -224,21 +243,27 @@ theorem intCast_pow (x : Int) (k : Nat) : ((x ^ k : Int) : α) = (x : α) ^ k :=
   next => simp [pow_zero, Int.pow_zero, intCast_one]
   next k ih => simp [pow_succ, Int.pow_succ, intCast_mul, *]
 
-theorem pow_add (a : α) (k₁ k₂ : Nat) : a ^ (k₁ + k₂) = a^k₁ * a^k₂ := by
-  induction k₂
-  next => simp [pow_zero, mul_one]
-  next k₂ ih => rw [Nat.add_succ, pow_succ, pow_succ, ih, mul_assoc]
+end Ring
+
+namespace CommSemiring
+
+open Semiring
+
+variable {α : Type u} [CommSemiring α]
+
+theorem mul_left_comm (a b c : α) : a * (b * c) = b * (a * c) := by
+  rw [← mul_assoc, ← mul_assoc, mul_comm a]
 
-end CommRing
+end CommSemiring
 
-open CommRing
+open Semiring Ring CommSemiring CommRing
 
-class IsCharP (α : Type u) [CommRing α] (p : outParam Nat) where
+class IsCharP (α : Type u) [Ring α] (p : outParam Nat) where
   ofNat_eq_zero_iff (p) : ∀ (x : Nat), OfNat.ofNat (α := α) x = 0 ↔ x % p = 0
 
 namespace IsCharP
 
-variable (p)  {α : Type u} [CommRing α] [IsCharP α p]
+variable (p)  {α : Type u} [Ring α] [IsCharP α p]
 
 theorem natCast_eq_zero_iff (x : Nat) : (x : α) = 0 ↔ x % p = 0 := by
   rw [← ofNat_eq_natCast]
@@ -325,12 +350,12 @@ end IsCharP
 /--
 Special case of Mathlib's `NoZeroSMulDivisors Nat α`.
 -/
-class NoNatZeroDivisors (α : Type u) [CommRing α] where
+class NoNatZeroDivisors (α : Type u) [Ring α] where
   no_nat_zero_divisors : ∀ (k : Nat) (a : α), k ≠ 0 → OfNat.ofNat (α := α) k * a = 0 → a = 0
 
 export NoNatZeroDivisors (no_nat_zero_divisors)
 
-theorem no_int_zero_divisors {α : Type u} [CommRing α] [NoNatZeroDivisors α] {k : Int} {a : α}
+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) =>

src/Init/Grind/CommRing/BitVec.lean

@@ -19,8 +19,11 @@ instance : CommRing (BitVec w) where
   mul_assoc := BitVec.mul_assoc
   mul_comm := BitVec.mul_comm
   mul_one := BitVec.mul_one
+  one_mul := BitVec.one_mul
   left_distrib _ _ _ := BitVec.mul_add
+  right_distrib _ _ _ := BitVec.add_mul
   zero_mul _ := BitVec.zero_mul
+  mul_zero _ := BitVec.mul_zero
   sub_eq_add_neg := BitVec.sub_eq_add_neg
   pow_zero _ := BitVec.pow_zero
   pow_succ _ _ := BitVec.pow_succ

src/Init/Grind/CommRing/Int.lean

@@ -19,8 +19,11 @@ instance : CommRing Int where
   mul_assoc := Int.mul_assoc
   mul_comm := Int.mul_comm
   mul_one := Int.mul_one
+  one_mul := Int.one_mul
   left_distrib := Int.mul_add
+  right_distrib := Int.add_mul
   zero_mul := Int.zero_mul
+  mul_zero := Int.mul_zero
   pow_zero _ := rfl
   pow_succ _ _ := rfl
   ofNat_succ _ := rfl

src/Init/Grind/CommRing/Poly.lean

@@ -508,6 +508,8 @@ def NullCert.toPolyC (nc : NullCert) (c : Nat) : Poly :=
 Theorems for justifying the procedure for commutative rings in `grind`.
 -/
 
+open Semiring Ring CommSemiring
+
 theorem denoteInt_eq {α} [CommRing α] (k : Int) : denoteInt (α := α) k = k := by
   simp [denoteInt, cond_eq_if] <;> split
   next h => rw [ofNat_eq_natCast, ← intCast_natCast, ← intCast_neg, ← Int.eq_neg_natAbs_of_nonpos (Int.le_of_lt h)]

src/Init/Grind/CommRing/SInt.lean

@@ -25,8 +25,11 @@ instance : CommRing Int8 where
   mul_assoc := Int8.mul_assoc
   mul_comm := Int8.mul_comm
   mul_one := Int8.mul_one
+  one_mul := Int8.one_mul
   left_distrib _ _ _ := Int8.mul_add
+  right_distrib _ _ _ := Int8.add_mul
   zero_mul _ := Int8.zero_mul
+  mul_zero _ := Int8.mul_zero
   sub_eq_add_neg := Int8.sub_eq_add_neg
   pow_zero := Int8.pow_zero
   pow_succ := Int8.pow_succ
@@ -54,8 +57,11 @@ instance : CommRing Int16 where
   mul_assoc := Int16.mul_assoc
   mul_comm := Int16.mul_comm
   mul_one := Int16.mul_one
+  one_mul := Int16.one_mul
   left_distrib _ _ _ := Int16.mul_add
+  right_distrib _ _ _ := Int16.add_mul
   zero_mul _ := Int16.zero_mul
+  mul_zero _ := Int16.mul_zero
   sub_eq_add_neg := Int16.sub_eq_add_neg
   pow_zero := Int16.pow_zero
   pow_succ := Int16.pow_succ
@@ -82,8 +88,11 @@ instance : CommRing Int32 where
   mul_assoc := Int32.mul_assoc
   mul_comm := Int32.mul_comm
   mul_one := Int32.mul_one
+  one_mul := Int32.one_mul
   left_distrib _ _ _ := Int32.mul_add
+  right_distrib _ _ _ := Int32.add_mul
   zero_mul _ := Int32.zero_mul
+  mul_zero _ := Int32.mul_zero
   sub_eq_add_neg := Int32.sub_eq_add_neg
   pow_zero := Int32.pow_zero
   pow_succ := Int32.pow_succ
@@ -110,8 +119,11 @@ instance : CommRing Int64 where
   mul_assoc := Int64.mul_assoc
   mul_comm := Int64.mul_comm
   mul_one := Int64.mul_one
+  one_mul := Int64.one_mul
   left_distrib _ _ _ := Int64.mul_add
+  right_distrib _ _ _ := Int64.add_mul
   zero_mul _ := Int64.zero_mul
+  mul_zero _ := Int64.mul_zero
   sub_eq_add_neg := Int64.sub_eq_add_neg
   pow_zero := Int64.pow_zero
   pow_succ := Int64.pow_succ
@@ -138,8 +150,11 @@ instance : CommRing ISize where
   mul_assoc := ISize.mul_assoc
   mul_comm := ISize.mul_comm
   mul_one := ISize.mul_one
+  one_mul := ISize.one_mul
   left_distrib _ _ _ := ISize.mul_add
+  right_distrib _ _ _ := ISize.add_mul
   zero_mul _ := ISize.zero_mul
+  mul_zero _ := ISize.mul_zero
   sub_eq_add_neg := ISize.sub_eq_add_neg
   pow_zero := ISize.pow_zero
   pow_succ := ISize.pow_succ

src/Init/Grind/CommRing/UInt.lean

@@ -131,8 +131,11 @@ instance : CommRing UInt8 where
   mul_assoc := UInt8.mul_assoc
   mul_comm := UInt8.mul_comm
   mul_one := UInt8.mul_one
+  one_mul := UInt8.one_mul
   left_distrib _ _ _ := UInt8.mul_add
+  right_distrib _ _ _ := UInt8.add_mul
   zero_mul _ := UInt8.zero_mul
+  mul_zero _ := UInt8.mul_zero
   sub_eq_add_neg := UInt8.sub_eq_add_neg
   pow_zero := UInt8.pow_zero
   pow_succ := UInt8.pow_succ
@@ -153,8 +156,11 @@ instance : CommRing UInt16 where
   mul_assoc := UInt16.mul_assoc
   mul_comm := UInt16.mul_comm
   mul_one := UInt16.mul_one
+  one_mul := UInt16.one_mul
   left_distrib _ _ _ := UInt16.mul_add
+  right_distrib _ _ _ := UInt16.add_mul
   zero_mul _ := UInt16.zero_mul
+  mul_zero _ := UInt16.mul_zero
   sub_eq_add_neg := UInt16.sub_eq_add_neg
   pow_zero := UInt16.pow_zero
   pow_succ := UInt16.pow_succ
@@ -175,8 +181,11 @@ instance : CommRing UInt32 where
   mul_assoc := UInt32.mul_assoc
   mul_comm := UInt32.mul_comm
   mul_one := UInt32.mul_one
+  one_mul := UInt32.one_mul
   left_distrib _ _ _ := UInt32.mul_add
+  right_distrib _ _ _ := UInt32.add_mul
   zero_mul _ := UInt32.zero_mul
+  mul_zero _ := UInt32.mul_zero
   sub_eq_add_neg := UInt32.sub_eq_add_neg
   pow_zero := UInt32.pow_zero
   pow_succ := UInt32.pow_succ
@@ -197,8 +206,11 @@ instance : CommRing UInt64 where
   mul_assoc := UInt64.mul_assoc
   mul_comm := UInt64.mul_comm
   mul_one := UInt64.mul_one
+  one_mul := UInt64.one_mul
   left_distrib _ _ _ := UInt64.mul_add
+  right_distrib _ _ _ := UInt64.add_mul
   zero_mul _ := UInt64.zero_mul
+  mul_zero _ := UInt64.mul_zero
   sub_eq_add_neg := UInt64.sub_eq_add_neg
   pow_zero := UInt64.pow_zero
   pow_succ := UInt64.pow_succ
@@ -219,8 +231,11 @@ instance : CommRing USize where
   mul_assoc := USize.mul_assoc
   mul_comm := USize.mul_comm
   mul_one := USize.mul_one
+  one_mul := USize.one_mul
   left_distrib _ _ _ := USize.mul_add
+  right_distrib _ _ _ := USize.add_mul
   zero_mul _ := USize.zero_mul
+  mul_zero _ := USize.mul_zero
   sub_eq_add_neg := USize.sub_eq_add_neg
   pow_zero := USize.pow_zero
   pow_succ := USize.pow_succ

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

@@ -17,7 +17,7 @@ variable [Monad M] [MonadGetRing M]
 private def denoteNum (k : Int) : M Expr := do
   let ring ← getRing
   let n := mkRawNatLit k.natAbs
-  let ofNatInst := mkApp3 (mkConst ``Grind.CommRing.ofNat [ring.u]) ring.type ring.commRingInst n
+  let ofNatInst := mkApp3 (mkConst ``Grind.Semiring.ofNat [ring.u]) ring.type ring.semiringInst n
   let n := mkApp3 (mkConst ``OfNat.ofNat [ring.u]) ring.type n ofNatInst
   if k < 0 then
     return mkApp ring.negFn n