Ring proving natural number arithmetic unexpectedly

Stream: general

[Brandon Harad]

I am currently constructing the integers (Z) as a quotient of pairs of naturals, and I constructed an instance of CommRing for it, as well as an OfNat instance. Now, the ring tactic proves that (1 : Z) + 1 = 2, but I see no reason that it should be able to do so. At no point did I prove that my OfNat instance worked with arithmetic. Why can ring prove this? #mwe below.

import Mathlib

def R : (ℕ × ℕ) → (ℕ × ℕ) → Prop
  | (a, b), (c, d) => a+d = c+b

instance setoid : Setoid (ℕ × ℕ) := ⟨R, sorry⟩
def Z := Quotient setoid
instance instOfNat : OfNat Z n := ⟨⟦(n, 0)⟧⟩
instance instCommRing : CommRing Z := sorry

example : (1 : Z) + 1 = 2 := by
  ring

[Kim Morrison]

It is baked into the definition of CommRing that casts of natural numbers are equal to the "natural numbers in the ring".

[Kim Morrison]

You should try actually constructing the CommRing instance, and you'll see what you're hiding behind that sorry!

[Brandon Harad]

Ah, I see what I've done. I was using CommRing.ofMinimalAxioms rather than the full constructor, and it must have been overruling my OfNat instance. Thank you!