refactor: remove numeric (#177)

This removes the `Numeric` parent for `Semiring` which was used for both coercions and numerals, and replaces it by a low-priority instance for `OfNat` on `Semiring`.  The coercion from Nat to R is removed.

Numerals are now implemented using `Nat.cast`.  As Sebastian has noted, to avoid diamonds for *numerals* it suffices that `Nat.cast n` and `(n : R)` are definitionally equal for every `n : Nat`.  It is not necessary that `(Nat.cast ∙)` and `(∙ : R)` are definitionally equal as functions (and after this PR they are not, for most rings).  Similarly, `Nat.cast` is carefully defined so that both `0 = 0` and `1 = 1` are true definitionally in any ring.

The setup still has a couple of downsides:
1. `OfNat.ofNat` must never be applied to anything except concrete natural numbers (or we get diamonds).
2. `(123456 : R)` is a massive performance issue when executing in the VM. :-/  (Which is not entirely true, in reality it fails quickly due to a stack overflow.)

We do not register `Nat.cast` as a coercion because of the performance issues.

Author: gebner

Mathlib/Algebra/Group/Defs.lean

@@ -175,11 +175,10 @@ end AddMonoid_lemmas
 
 -/
 
-class AddCommMonoid (A : Type u) extends AddMonoid A where
-  add_comm (a b : A) : a + b = b + a
-
-instance (A : Type u) [AddCommMonoid A] : AddCommSemigroup A where
-  __ := ‹AddCommMonoid A›
+class AddCommMonoid (A : Type u) extends AddMonoid A, AddCommSemigroup A where
+  -- TODO: doesn't work
+  zero_add a := (by rw [add_comm, add_zero])
+  add_zero a := (by rw [add_comm, zero_add])
 
 /-
 
@@ -199,6 +198,8 @@ class SubNegMonoid (A : Type u) extends AddMonoid A, Neg A, Sub A where
   gsmul_succ' (n : ℕ) (a : A) : gsmul (Int.ofNat n.succ) a = a + gsmul (Int.ofNat n) a
   gsmul_neg' (n : ℕ) (a : A) : gsmul (Int.negSucc n) a = -(gsmul ↑(n.succ) a)
 
+export SubNegMonoid (sub_eq_add_neg)
+
 /-
 
 ### Additive groups
@@ -243,6 +244,9 @@ instance (A : Type u) [AddGroup A] : IsAddLeftCancel A where
   add_left_cancel a b c h := by
   rw [← neg_add_cancel_left a b, h, neg_add_cancel_left]
 
+lemma eq_of_sub_eq_zero' (h : a - b = 0) : a = b :=
+  add_right_cancel <| show a + (-b) = b + (-b) by rw [← sub_eq_add_neg, h, add_neg_self]
+
 end AddGroup_lemmas
 
 class AddCommGroup (A : Type u) extends AddGroup A where

Mathlib/Algebra/Ring/Basic.lean

@@ -2,44 +2,45 @@ import Mathlib.Init.Data.Int.Basic
 import Mathlib.Algebra.GroupWithZero.Defs
 import Mathlib.Algebra.Group.Basic
 import Mathlib.Tactic.Spread
-/-
-
-# Semirings and rings
+import Mathlib.Util.WhatsNew
 
--/
+@[reducible, inline]
+protected def Nat.cast [Add α] [Zero α] [One α] : Nat → α
+  | 0 => 0
+  | 1 => 1
+  | n + 1 => Nat.cast n + 1
 
-class Numeric (α : Type u) where
-  ofNat : Nat → α
+@[simp] lemma Nat.cast_zero [Add α] [Zero α] [One α] : Nat.cast 0 = (0 : α) := rfl
+@[simp] lemma Nat.cast_one [Add α] [Zero α] [One α] : Nat.cast 1 = (1 : α) := rfl
+lemma Nat.cast_succ_succ [Add α] [Zero α] [One α] : Nat.cast (n+2) = ((n + 1).cast + 1 : α) := rfl
 
-instance Numeric.OfNat [Numeric α] : OfNat α n := ⟨Numeric.ofNat n⟩
-instance [Numeric α] : CoeTail ℕ α := ⟨Numeric.ofNat⟩
+@[simp]
+lemma Nat.cast_Nat : ∀ {n : Nat}, n.cast = n
+  | 0 => rfl
+  | 1 => rfl
+  | n + 2 => by simp [Nat.cast, cast_Nat]; rfl
 
-theorem ofNat_eq_ofNat (α) (n : ℕ) [Numeric α] : Numeric.ofNat (α := α) n = OfNat.ofNat n := rfl
+@[simp]
+lemma Nat.cast_Int : ∀ {n : Nat}, n.cast = (n : Int)
+  | 0 => rfl
+  | 1 => rfl
+  | n + 2 => by simp [Nat.cast, cast_Int]; rfl
 
-class Semiring (R : Type u) extends Semigroup R, AddCommSemigroup R, Numeric R where
-  add_zero (a : R) : a + 0 = a
-  zero_add (a : R) : 0 + a = a
-  nsmul : ℕ → R → R := nsmul_rec
-  nsmul_zero' : ∀ x, nsmul 0 x = 0 -- fill in with tactic once we can do this
-  nsmul_succ' : ∀ (n : ℕ) x, nsmul n.succ x = x + nsmul n x -- fill in with tactic
+class HasNumerals (α : Type u) extends Add α, Zero α, One α
 
-  zero_mul (a : R) : 0 * a = 0
-  mul_zero (a : R) : a * 0 = 0
+instance (priority := low) [HasNumerals α] : OfNat α n where
+  ofNat := n.cast
 
-  -- Monoid R
-  one_mul (a : R) : 1 * a = a
-  mul_one (a : R) : a * 1 = a
-  npow : ℕ → R → R := npow_rec
-  npow_zero' : ∀ x, npow 0 x = 1 -- fill in with tactic once we can do this
-  npow_succ' : ∀ (n : ℕ) x, npow n.succ x = x * npow n x -- fill in with tactic
+/-
+# Semirings and rings
+-/
 
+class Semiring (R : Type u) extends AddCommMonoid R, MonoidWithZero R, HasNumerals R where
   mul_add (a b c : R) : a * (b + c) = a * b + a * c
   add_mul (a b c : R) : (a + b) * c = a * c + b * c
-  ofNat_succ (a : Nat) : ofNat (a + 1) = ofNat a + 1
 
 section Semiring
 variable {R} [Semiring R]
-open Numeric
 
 instance : MonoidWithZero R where
   __ := ‹Semiring R›
@@ -51,31 +52,35 @@ theorem mul_add (a b c : R) : a * (b + c) = a * b + a * c := Semiring.mul_add a
 
 theorem add_mul (a b c : R) : (a + b) * c = a * c + b * c := Semiring.add_mul a b c
 
-@[simp] lemma ofNat_zero : (ofNat 0 : R) = 0 := rfl
-@[simp] lemma ofNat_one : (ofNat 1 : R) = 1 := rfl
+lemma Nat.cast_succ {R} [Semiring R] {n : ℕ} : Nat.cast (n + 1) = (Nat.cast n + 1 : R) := by
+  cases n <;> simp [Nat.cast_succ_succ]
 
-@[simp] lemma ofNat_add : ∀ {a b}, (ofNat (a + b) : R) = ofNat a + ofNat b
-  | a, 0 => (add_zero _).symm
-  | a, b + 1 => trans (Semiring.ofNat_succ _)
-    (by simp [Semiring.ofNat_succ, ofNat_add (b := b), add_assoc])
+lemma Nat.cast_succ' {R} [Semiring R] {n : ℕ} : Nat.cast n.succ = (Nat.cast n + 1 : R) :=
+  Nat.cast_succ
 
-@[simp] lemma ofNat_mul : ∀ {a b}, (ofNat (a * b) : R) = ofNat a * ofNat b
-  | a, 0 => by simp
-  | a, b + 1 => by simp [Nat.mul_succ, mul_add,
-    (show ofNat (a * b) = ofNat a * ofNat b from ofNat_mul)]
+lemma Nat.cast_add {R} [Semiring R] {m n : ℕ} : (m + n).cast = (m.cast + n.cast : R) := by
+  induction n generalizing m
+  case zero => simp
+  case succ n ih =>
+    show Nat.cast ((m + n) + 1) = _ + Nat.cast (n + 1)
+    simp [Nat.cast_succ, ih, add_assoc]
 
-@[simp] theorem ofNat_pow (a n : ℕ) : Numeric.ofNat (a^n) = (Numeric.ofNat a : R)^n := by
-  induction n with
-  | zero =>
-    rw [pow_zero, Nat.pow_zero]
-    exact rfl
-  | succ n ih =>
-    rw [pow_succ, Nat.pow_succ, ofNat_mul, ih]
+lemma Nat.cast_mul {R} [Semiring R] {m n : ℕ} : (m * n).cast = (m.cast * n.cast : R) := by
+  induction n generalizing m <;> simp_all [mul_succ, cast_add, cast_succ', mul_add]
+
+lemma Nat.pow_succ' {m n : Nat} : m ^ n.succ = m * m ^ n := by
+  rw [Nat.pow_succ, Nat.mul_comm]
+
+lemma Nat.cast_pow {R} [Semiring R] {m n : ℕ} : (m ^ n).cast = (m.cast ^ n : R) := by
+  induction n generalizing m <;>
+    simp_all [cast_mul, cast_add, cast_succ', Nat.pow_succ', _root_.pow_succ', pow_zero]
 
 end Semiring
 
 class CommSemiring (R : Type u) extends Semiring R where
   mul_comm (a b : R) : a * b = b * a
+  -- TODO: doesn't work
+  add_mul a b c := (by rw [mul_comm, mul_add, mul_comm c, mul_comm c])
 
 instance (R : Type u) [CommSemiring R] : CommMonoid R where
   __ := ‹CommSemiring R›
@@ -92,6 +97,11 @@ class Ring (R : Type u) extends Semiring R, Neg R, Sub R where
 
 instance {R} [Ring R] : AddCommGroup R := { ‹Ring R› with }
 
+theorem neg_mul_eq_neg_mul {R} [Ring R] (a b : R) : -(a * b) = (-a) * b :=
+  Eq.symm <| eq_of_sub_eq_zero' <| by
+    rw [sub_eq_add_neg, neg_neg (a * b) /- TODO: why is arg necessary? -/]
+    rw [← add_mul, neg_add_self a /- TODO: why is arg necessary? -/, zero_mul]
+
 class CommRing (R : Type u) extends Ring R where
   mul_comm (a b : R) : a * b = b * a
 
@@ -103,15 +113,10 @@ instance (R : Type u) [CommRing R] : CommSemiring R where
 
 namespace Nat
 
-instance : Numeric Nat := ⟨id⟩
-
-@[simp] theorem ofNat_eq_Nat (n : Nat) : Numeric.ofNat n = n := rfl
-
 instance : CommSemiring ℕ where
   mul_comm := Nat.mul_comm
   mul_add := Nat.left_distrib
   add_mul := Nat.right_distrib
-  ofNat_succ := fun _ => rfl
   mul_one := Nat.mul_one
   one_mul := Nat.one_mul
   npow (n x) := x ^ n
@@ -132,15 +137,12 @@ end Nat
 
 namespace Int
 
-instance : Numeric ℤ := ⟨Int.ofNat⟩
-
 instance : CommRing ℤ where
   zero_mul := Int.zero_mul
   mul_zero := Int.mul_zero
   mul_comm := Int.mul_comm
   mul_add := Int.distrib_left
   add_mul := Int.distrib_right
-  ofNat_succ := fun _ => rfl
   mul_one := Int.mul_one
   one_mul := Int.one_mul
   npow (n x) := HPow.hPow x n