Ring is determined by Semiring

Stream: mathlib4

[Raghuram]

What's the easiest way to show that two Rings whose underlying Semirings are Eq are themselves Eq?

I eventually got fed up of wrestling with all the typeclass instances flying around, and brute-forced everything, but I really hope there's a better way than this.

import Mathlib.Algebra.Ring.Basic

lemma Ring.semiring_ext {R : Type*} : {inst₁ inst₂ : Ring R} →
  inst₁.toSemiring = inst₂.toSemiring → inst₁ = inst₂
/- Anything less than this makes it difficult to access
instance-implicit fields of the constructor. -/
| @Ring.mk .(R) sr ⟨neg₁⟩ ⟨sub₁⟩ sub_eq_neg₁ zsmul₁ zsmul₁_zero zsmul₁_succ zsmul₁_negSucc neg_add_left₁ ⟨intCast₁⟩ intCast₁_ofNat intCast₁_negSucc,
  @Ring.mk .(R) .(sr) ⟨neg₂⟩ ⟨sub₂⟩ sub_eq_neg₂ zsmul₂ zsmul₂_zero zsmul₂_succ zsmul₂_negSucc neg_add_left₂ ⟨intCast₂⟩ intCast₂_ofNat intCast₂_negSucc,
  rfl => by

  /- Eliminate all accursed typeclass (neg, sub, most coe) wrappers,
  so that e.g. `rw [neg_eq_nat]` actually works. -/
  change ∀ a b, sub₁ a b = a + neg₁ b at sub_eq_neg₁
  change ∀ a b, sub₂ a b = a + neg₂ b at sub_eq_neg₂
  change ∀ a, zsmul₁ (.ofNat 0) a = 0 at zsmul₁_zero
  change ∀ a, zsmul₂ (.ofNat 0) a = 0 at zsmul₂_zero
  -- change ∀ (n : ℕ) a, zsmul₁ (.ofNat n.succ) a = a + zsmul₁ (.ofNat n) a at zsmul₁_succ
  -- change ∀ (n : ℕ) a, zsmul₂ (.ofNat n.succ) a = a + zsmul₂ (.ofNat n) a at zsmul₂_succ
  change ∀ n a, zsmul₁ (.negSucc n) a = neg₁ (zsmul₁ (.ofNat n.succ) a) at zsmul₁_negSucc
  change ∀ n a, zsmul₂ (.negSucc n) a = neg₂ (zsmul₂ (.ofNat n.succ) a) at zsmul₂_negSucc
  change ∀ n, intCast₁ (.ofNat n) = ↑n at intCast₁_ofNat
  change ∀ n, intCast₂ (.ofNat n) = ↑n at intCast₂_ofNat
  change ∀ n, intCast₁ (.negSucc n) = neg₁ ↑(n + 1) at intCast₁_negSucc
  change ∀ n, intCast₂ (.negSucc n) = neg₂ ↑(n + 1) at intCast₂_negSucc

  -- Lemma used in every case
  have neg_eq x : neg₁ x = neg₂ x := by
    apply neg_unique (x := x) <;> try rewrite [add_comm]
    · exact neg_add_left₁ x
    · exact neg_add_left₂ x

  -- Prove equality for each field of `Ring` separately.
  congr <;> funext
  · apply neg_eq
  · rw [sub_eq_neg₁, sub_eq_neg₂, neg_eq]
  · have zsmul_eq_nat (n : ℕ) a : zsmul₁ (.ofNat n) a = zsmul₂ (.ofNat n) a := by
      induction n
      case zero => rw [zsmul₁_zero, zsmul₂_zero]
      case succ n h => rw [zsmul₁_succ, zsmul₂_succ, h]
    rename_i n _; cases n
    case ofNat => apply zsmul_eq_nat
    case negSucc => rw [zsmul₁_negSucc, zsmul₂_negSucc,
                        zsmul_eq_nat, neg_eq]
  · rename_i n; cases n
    case ofNat => rw [intCast₁_ofNat, intCast₂_ofNat]
    case negSucc => rw [intCast₁_negSucc, intCast₂_negSucc, neg_eq]

[Riccardo Brasca]

We already have docs#Monoid.ext, so we should have Ring.ext, then it should be obvious

[Eric Wieser]

Probably you should prove Semiring.ext first

[Jireh Loreaux]

Yeah, we should just start a new file with all of these.

[Raghuram]

Riccardo Brasca said:

We already have docs#Monoid.ext, so we should have Ring.ext, then it should be obvious

Ah, now I'm realising that I couldn't find any lemma like Monoid.ext because I had used very minimal imports. :face_palm:

[Jireh Loreaux]

But indeed, I think Ring.ext and friends are missing.

[Raghuram]

True. It doesn't sound too difficult to implement either.

[Jireh Loreaux]

@Raghuram if you implement this, (a) please PR it and (b) use the file containing docs#Monoid.ext as a guide and/or use those results.

[Raghuram]

Would a file proving the "obvious" ext lemma (instances are equal if a minimal set of operations are equal on all arguments) for all the typeclasses in Mathlib.Algebra.Ring.Defsone by one (as done in Mathlib.Algebra.Group.Ext be appropriate?

[Jireh Loreaux]

Yes, definitely.

[Riccardo Brasca]

Yeah, I mean, we want all the various results. Proving them in order should be relatively easy.

[Raghuram]

Jireh Loreaux said:

Raghuram if you implement this, (a) please PR it and (b) use the file containing docs#Monoid.ext as a guide and/or use those results.

I'm interested; that being said, this will be my first time contributing to Mathlib.
The procedure is to 1) ask for write access 2) clone and start writing 3) make a PR, right?

[Riccardo Brasca]

Yes, what is your github username?

[Riccardo Brasca]

Sorry, you shouldn't clone

[Raghuram]

Riccardo Brasca said:

Sorry, you shouldn't clone

Clone locally, I meant.

[Riccardo Brasca]

You can have a look here

[Raghuram]

Riccardo Brasca said:

Yes, what is your github username?

raghuram-13.

[Riccardo Brasca]

You should have an invitation

[Raghuram]

Created and pushed new branch raghuram-13/ext-for-rings (no commits yet).

[Raghuram]

I find myself needing (or at least, it would be convenient to have) ext lemmas for Add and Mul.
Is there an appropriate file to put such lemmas?

[Jireh Loreaux]

You mean because of HMul? or why exactly?

[Jireh Loreaux]

I guess I'm not sure why you can't just use congr.

[Raghuram]

Jireh Loreaux said:

I guess I'm not sure why you can't just use congr.

I have this code:

@[ext] theorem NonUnitalNonAssocSemiring.ext ⦃inst₁ inst₂ : NonUnitalNonAssocSemiring R⦄
    (h_add : ∀ a b, a +[R, inst₁] b = a +[R, inst₂] b)
    (h_mul : ∀ a b, a *[R, inst₁] b = a *[R, inst₂] b) :
    inst₁ = inst₂ := by
  -- Extract `AddMonoid` instance and `mul` function
  rcases inst₁ with ⟨⟩
  rcases inst₂ with ⟨⟩
  congr <;> (ext; apply_assumption)

The congr generates two cases, to show that the underlying AddMonoids are equal and that the underlying Muls are equal.
The former already has ext lemmas so it's easy to deal with.
The same will work for the latter after applying congr, except that for congr to have an effect I have to destructure the Muls, and to do that I have to rename_i them.

That can be done, but it seemed like it would be cleaner to have an ext for Mul, which seems like the same kind of lemma as these - if the operations are the same, the typeclass instances are the same.

[Raghuram]

Actually, I just realised that I can use the rcases to do the destructuring by changing ⟨⟩ to @⟨_, ⟨⟩⟩. So IG it's not needed yet.

[Raghuram]

PR'd.