feat: add doc-string to grind algebra typeclasses (#8890)

This PR adds doc-strings to the `Lean.Grind` algebra typeclasses, as
these will appear in the reference manual explaining how to extend
`grind` algebra solvers to new types. Also removes some redundant
fields.

src/Init/Grind/Module/Basic.lean

@@ -14,28 +14,60 @@ namespace Lean.Grind
 class AddRightCancel (M : Type u) [Add M] where
   add_right_cancel : ∀ a b c : M, a + c = b + c → a = b
 
+/--
+A module over the natural numbers, i.e. a type with zero, addition, and scalar multiplication by natural numbers,
+satisfying appropriate compatibilities.
+
+Equivalently, an additive commutative monoid.
+
+Use `IntModule` if the type has negation.
+-/
 class NatModule (M : Type u) extends Zero M, Add M, HMul Nat M M where
+  /-- Zero is the right identity for addition. -/
   add_zero : ∀ a : M, a + 0 = a
+  /-- Addition is commutative. -/
   add_comm : ∀ a b : M, a + b = b + a
+  /-- Addition is associative. -/
   add_assoc : ∀ a b c : M, a + b + c = a + (b + c)
+  /-- Scalar multiplication by zero is zero. -/
   zero_hmul : ∀ a : M, 0 * a = 0
+  /-- Scalar multiplication by one is the identity. -/
   one_hmul : ∀ a : M, 1 * a = a
+  /-- Scalar multiplication is distributive over addition in the natural numbers. -/
   add_hmul : ∀ n m : Nat, ∀ a : M, (n + m) * a = n * a + m * a
+  /-- Scalar multiplication of zero is zero. -/
   hmul_zero : ∀ n : Nat, n * (0 : M) = 0
+  /-- Scalar multiplication is distributive over addition in the module. -/
   hmul_add : ∀ n : Nat, ∀ a b : M, n * (a + b) = n * a + n * b
 
 attribute [instance 100] NatModule.toZero NatModule.toAdd NatModule.toHMul
 
+/--
+A module over the integers, i.e. a type with zero, addition, negation, subtraction, and scalar multiplication by integers,
+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
+  /-- Zero is the right identity for addition. -/
   add_zero : ∀ a : M, a + 0 = a
+  /-- Addition is commutative. -/
   add_comm : ∀ a b : M, a + b = b + a
+  /-- Addition is associative. -/
   add_assoc : ∀ a b c : M, a + b + c = a + (b + c)
+  /-- Scalar multiplication by zero is zero. -/
   zero_hmul : ∀ a : M, (0 : Int) * a = 0
+  /-- Scalar multiplication by one is the identity. -/
   one_hmul : ∀ a : M, (1 : Int) * a = a
+  /-- Scalar multiplication is distributive over addition in the integers. -/
   add_hmul : ∀ n m : Int, ∀ a : M, (n + m) * a = n * a + m * a
+  /-- Scalar multiplication of zero is zero. -/
   hmul_zero : ∀ n : Int, n * (0 : M) = 0
+  /-- Scalar multiplication is distributive over addition in the module. -/
   hmul_add : ∀ n : Int, ∀ a b : M, n * (a + b) = n * a + n * b
+  /-- Negation is the left inverse of addition. -/
   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
 
 namespace NatModule
@@ -155,7 +187,10 @@ theorem mul_hmul (n m : Int) (a : M) : (n * m) * a = n * (m * a) := by
 end IntModule
 
 /--
-Special case of Mathlib's `NoZeroSMulDivisors Nat α`.
+We say a module has no natural number zero divisors if
+`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) [Zero α] [HMul Nat α α] where
   no_nat_zero_divisors : ∀ (k : Nat) (a : α), k ≠ 0 → k * a = 0 → a = 0

src/Init/Grind/Ordered/Module.lean

@@ -12,18 +12,29 @@ import Init.Grind.Ordered.Order
 
 namespace Lean.Grind
 
+/--
+A module over the natural numbers which is also equipped with a preorder is considered an
+ordered module if addition is compatible with the preorder.
+-/
 class NatModule.IsOrdered (M : Type u) [Preorder M] [NatModule M] where
+  /-- `a + c ≤ b + c` iff `a ≤ b`. -/
   add_le_left_iff : ∀ {a b : M} (c : M), a ≤ b ↔ a + c ≤ b + c
-  hmul_lt_hmul_iff : ∀ (k : Nat) {a b : M}, a < b → (k * a < k * b ↔ 0 < k)
-  hmul_le_hmul : ∀ {k : Nat} {a b : M}, a ≤ b → k * a ≤ k * b
 
 -- This class is actually redundant; it is available automatically when we have an
 -- `IntModule` satisfying `NatModule.IsOrdered`.
 -- Replace with a custom constructor?
+/--
+A module over the integers which is also equipped with a preorder is considered an
+ordered module if addition and negation are compatible with the preorder.
+-/
 class IntModule.IsOrdered (M : Type u) [Preorder M] [IntModule M] where
+  /-- `-a ≤ b` iff `-b ≤ a`. -/
   neg_le_iff : ∀ a b : M, -a ≤ b ↔ -b ≤ a
+  /-- `a + c ≤ b + c` iff `a ≤ b`. -/
   add_le_left : ∀ {a b : M}, a ≤ b → (c : M) → a + c ≤ b + c
+  /-- -/
   hmul_pos_iff : ∀ (k : Int) {a : M}, 0 < a → (0 < k * a ↔ 0 < k)
+  /-- -/
   hmul_nonneg : ∀ {k : Int} {a : M}, 0 ≤ k → 0 ≤ a → 0 ≤ k * a
 
 namespace NatModule.IsOrdered
@@ -35,6 +46,13 @@ variable {M : Type u} [Preorder M] [NatModule M] [NatModule.IsOrdered M]
 theorem add_le_right_iff {a b : M} (c : M) : a ≤ b ↔ c + a ≤ c + b := by
   rw [add_comm c a, add_comm c b, add_le_left_iff]
 
+theorem hmul_le_hmul {k : Nat} {a b : M} (h : a ≤ b) : k * a ≤ k * b := by
+  induction k with
+  | zero => simp [zero_hmul, Preorder.le_refl]
+  | succ k ih =>
+    rw [add_hmul, one_hmul, add_hmul, one_hmul]
+    exact Preorder.le_trans ((add_le_left_iff a).mp ih) ((add_le_right_iff (k * b)).mp h)
+
 theorem add_le_left {a b : M} (h : a ≤ b) (c : M) : a + c ≤ b + c :=
   (add_le_left_iff c).mp h
 
@@ -66,6 +84,17 @@ theorem add_lt_left_iff {a b : M} (c : M) : a < b ↔ a + c < b + c := by
 theorem add_lt_right_iff {a b : M} (c : M) : a < b ↔ c + a < c + b := by
   rw [add_comm c a, add_comm c b, add_lt_left_iff]
 
+theorem hmul_lt_hmul_iff (k : Nat) {a b : M} (h : a < b) : k * a < k * b ↔ 0 < k := by
+  induction k with
+  | zero => simp [zero_hmul, Preorder.lt_irrefl]
+  | succ k ih =>
+    rw [add_hmul, one_hmul, add_hmul, one_hmul]
+    simp only [Nat.zero_lt_succ, iff_true]
+    by_cases hk : 0 < k
+    · simp only [hk, iff_true] at ih
+      exact Preorder.lt_trans ((add_lt_left_iff a).mp ih) ((add_lt_right_iff (k * b)).mp h)
+    · simp [Nat.eq_zero_of_not_pos hk, zero_hmul, zero_add, h]
+
 theorem hmul_pos_iff {k : Nat} {a : M} (h : 0 < a) : 0 < k * a ↔ 0 < k:= by
   rw [← hmul_lt_hmul_iff k h, hmul_zero]
 
@@ -239,11 +268,6 @@ theorem add_le_add {a b c d : M} (hab : a ≤ b) (hcd : c ≤ d) : a + c ≤ b +
 
 instance : NatModule.IsOrdered M where
   add_le_left_iff := add_le_left_iff
-  hmul_lt_hmul_iff k {a b} h := by
-    simpa using hmul_lt_hmul_iff k h
-  hmul_le_hmul {k a b} h := by
-    simpa using hmul_le_hmul (Int.natCast_nonneg k) h
-
 
 end IntModule.IsOrdered
 

src/Init/Grind/Ordered/Order.lean

@@ -12,9 +12,12 @@ namespace Lean.Grind
 
 /-- A preorder is a reflexive, transitive relation `≤` with `a < b` defined in the obvious way. -/
 class Preorder (α : Type u) extends LE α, LT α where
+  /-- The less-than-or-equal relation is reflexive. -/
   le_refl : ∀ a : α, a ≤ a
+  /-- The less-than-or-equal relation is transitive. -/
   le_trans : ∀ {a b c : α}, a ≤ b → b ≤ c → a ≤ c
   lt := fun a b => a ≤ b ∧ ¬b ≤ a
+  /-- The less-than relation is determined by the less-than-or-equal relation. -/
   lt_iff_le_not_le : ∀ {a b : α}, a < b ↔ a ≤ b ∧ ¬b ≤ a := by intros; rfl
 
 namespace Preorder
@@ -52,7 +55,9 @@ theorem not_gt_of_lt {a b : α} (h : a < b) : ¬a > b :=
 
 end Preorder
 
+/-- A partial order is a preorder with the additional property that `a ≤ b` and `b ≤ a` implies `a = b`. -/
 class PartialOrder (α : Type u) extends Preorder α where
+  /-- The less-than-or-equal relation is antisymmetric. -/
   le_antisymm : ∀ {a b : α}, a ≤ b → b ≤ a → a = b
 
 namespace PartialOrder
@@ -71,7 +76,9 @@ theorem le_iff_lt_or_eq {a b : α} : a ≤ b ↔ a < b ∨ a = b := by
 
 end PartialOrder
 
+/-- A linear order is a partial order with the additional property that every pair of elements is comparable. -/
 class LinearOrder (α : Type u) extends PartialOrder α where
+  /-- For every two elements `a` and `b`, either `a ≤ b` or `b ≤ a`. -/
   le_total : ∀ a b : α, a ≤ b ∨ b ≤ a
 
 namespace LinearOrder

src/Init/Grind/Ordered/Ring.lean

@@ -11,6 +11,10 @@ import Init.Grind.Ordered.Module
 
 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
   /-- In a strict ordered semiring, we have `0 < 1`. -/
   zero_lt_one : (0 : R) < 1

src/Init/Grind/Ring/Basic.lean

@@ -31,37 +31,86 @@ theorem ofNat_eq_iff_of_lt {x y : Nat} (h₁ : x < p) (h₂ : y < p) :
 
 namespace Lean.Grind
 
+/--
+A semiring, i.e. a type equipped with addition, multiplication, and a map from the natural numbers,
+satisfying appropriate compatibilities.
+
+Use `Ring` instead if the type also has negation,
+`CommSemiring` if the multiplication is commutative,
+or `CommRing` if the type has negation and multiplication is commutative.
+-/
 class Semiring (α : Type u) extends Add α, Mul α, HPow α Nat α where
-  [ofNat : ∀ n, OfNat α n]
+  /--
+  In every semiring there is a canonical map from the natural numbers to the semiring,
+  providing the values of `0` and `1`. Note that this function need not be injective.
+  -/
   [natCast : NatCast α]
+  /--
+  Natural number numerals in the semiring.
+  The field `ofNat_eq_natCast` ensures that these are (propositionally) equal to the values of `natCast`.
+  -/
+  [ofNat : ∀ n, OfNat α n]
+  /-- Addition is associative. -/
   add_assoc : ∀ a b c : α, a + b + c = a + (b + c)
+  /-- Addition is commutative. -/
   add_comm : ∀ a b : α, a + b = b + a
+  /-- Zero is the right identity for addition. -/
   add_zero : ∀ a : α, a + 0 = a
+  /-- Multiplication is associative. -/
   mul_assoc : ∀ a b c : α, a * b * c = a * (b * c)
+  /-- One is the right identity for multiplication. -/
   mul_one : ∀ a : α, a * 1 = a
+  /-- One is the left identity for multiplication. -/
   one_mul : ∀ a : α, 1 * a = a
+  /-- Left distributivity of multiplication over addition. -/
   left_distrib : ∀ a b c : α, a * (b + c) = a * b + a * c
+  /-- Right distributivity of multiplication over addition. -/
   right_distrib : ∀ a b c : α, (a + b) * c = a * c + b * c
+  /-- Zero is right absorbing for multiplication. -/
   zero_mul : ∀ a : α, 0 * a = 0
+  /-- Zero is left absorbing for multiplication. -/
   mul_zero : ∀ a : α, a * 0 = 0
+  /-- The zeroth power of any element is one. -/
   pow_zero : ∀ a : α, a ^ 0 = 1
+  /-- The successor power law for exponentiation. -/
   pow_succ : ∀ a : α, ∀ n : Nat, a ^ (n + 1) = (a ^ n) * a
+  /-- Numerals are consistently defined with respect to addition. -/
   ofNat_succ : ∀ a : Nat, OfNat.ofNat (α := α) (a + 1) = OfNat.ofNat a + 1 := by intros; rfl
+  /-- Numerals are consistently defined with respect to the canonical map from natural numbers. -/
   ofNat_eq_natCast : ∀ n : Nat, OfNat.ofNat (α := α) n = Nat.cast n := by intros; rfl
 
+/--
+A ring, i.e. a type equipped with addition, negation, multiplication, and a map from the integers,
+satisfying appropriate compatibilities.
+
+Use `CommRing` if the multiplication is commutative.
+-/
 class Ring (α : Type u) extends Semiring α, Neg α, Sub α where
+  /-- In every ring there is a canonical map from the integers to the ring. -/
   [intCast : IntCast α]
+  /-- Negation is the left inverse of addition. -/
   neg_add_cancel : ∀ a : α, -a + a = 0
+  /-- Subtraction is addition of the negative. -/
   sub_eq_add_neg : ∀ a b : α, a - b = a + -b
+  /-- The canonical map from the integers is consistent with the canonical map from the natural numbers. -/
   intCast_ofNat : ∀ n : Nat, Int.cast (OfNat.ofNat (α := Int) n) = OfNat.ofNat (α := α) n := by intros; rfl
+  /-- The canonical map from the integers is consistent with negation. -/
   intCast_neg : ∀ i : Int, Int.cast (R := α) (-i) = -Int.cast i := by intros; rfl
 
+/--
+A commutative semiring, i.e. a semiring with commutative multiplication.
+
+Use `CommRing` if the type has negation.
+-/
 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]
 
+/--
+A commutative ring, i.e. a ring with commutative multiplication.
+-/
 class CommRing (α : Type u) extends Ring α, CommSemiring α
 
 -- We reduce the priority of these parent instances,
@@ -313,7 +362,16 @@ end CommSemiring
 
 open Semiring Ring CommSemiring CommRing
 
+/--
+A ring `α` has characteristic `p` if `OfNat.ofNat x = 0` iff `x % p = 0`.
+
+Note that for `p = 0`, we have `x % p = x`, so this says that `OfNat.ofNat` is injective from `Nat` to `α`.
+
+In the case of a semiring, we take the stronger condition that
+`OfNat.ofNat x = OfNat.ofNat y` iff `x % p = y % p`.
+-/
 class IsCharP (α : Type u) [Semiring α] (p : outParam Nat) where
+  /-- Two numerals in a semiring are equal iff they are congruent module `p` in the natural numbers. -/
   ofNat_ext_iff (p) : ∀ {x y : Nat}, OfNat.ofNat (α := α) x = OfNat.ofNat (α := α) y ↔ x % p = y % p
 
 namespace IsCharP