Best way to define ring instance?

Stream: mathlib4

[Alix Trieu]

I'm trying to define the following ring instance, but I don't see a way without proving all the intermediate instances from the bottom up, is there an better way? I thought about maybe showing it's isomorphic to a known ring, but I haven't found any suitable candidate.

variable {k: Type u} [Field k]

def PMod (q: k[X]): Type u :=
  { poly: k[X] // poly = poly % q}

noncomputable instance instRing {q: k[X]} (Hq: q.degree > 0): Ring (PMod q) :=
  by sorry

Full MWE:

import Mathlib.Algebra.Polynomial.Basic
import Mathlib.Algebra.Polynomial.FieldDivision

namespace Polynomial

universe u

variable {k: Type u} [Field k]

def PMod (q: k[X]): Type u :=
  { poly: k[X] // poly = poly % q}

namespace PMod

variable {q: k[X]} (Hq: q.degree > 0)

@[simp]
noncomputable def zero: PMod q :=
  ⟨0, by simp⟩

@[simp]
noncomputable instance instZero: Zero (PMod q) :=
  Zero.mk PMod.zero

@[simp]
noncomputable def one: PMod q :=
  ⟨1, by symm
         rw [mod_eq_self_iff (by intro Heq; rw [Heq, degree_zero] at Hq; simp at Hq)]
         rw [show degree 1 = 0 by simp]; exact Hq ⟩

@[simp]
noncomputable instance instOne: One (PMod q) :=
  One.mk (PMod.one Hq)

@[simp]
noncomputable def add (a b: PMod q): PMod q :=
  ⟨(a.1 + b.1) % q, by symm
                       rw [mod_eq_self_iff (by intro Heq; rw [Heq, degree_zero] at Hq; simp at Hq)]
                       have Hlt := natDegree_mod_lt (q:=q) (a.1 + b.1) (by rw [natDegree]; simp; aesop)
                       apply degree_lt_degree Hlt⟩

@[simp]
noncomputable instance instAdd: Add (PMod q) :=
  Add.mk (PMod.add Hq)

@[simp]
noncomputable def mul (a b: PMod q): PMod q :=
  ⟨(a.1 * b.1) % q, by symm
                       rw [mod_eq_self_iff (by intro Heq; rw [Heq, degree_zero] at Hq; simp at Hq)]
                       have Hlt := natDegree_mod_lt (q:=q) (a.1 * b.1) (by rw [natDegree]; simp; aesop)
                       apply degree_lt_degree Hlt⟩

@[simp]
noncomputable instance instMul: Mul (PMod q) :=
  Mul.mk (PMod.mul Hq)

@[simp]
noncomputable def neg (a: PMod q): PMod q :=
  ⟨- a.1, by nth_rw 1 [a.2]; rw [mod_def, mod_def, neg_modByMonic]⟩

@[simp]
noncomputable instance instNeg: Neg (PMod q) :=
  Neg.mk PMod.neg

noncomputable instance instRing: Ring (PMod q) :=
  by sorry

end PMod

end Polynomial

[Kenny Lau]

import Mathlib

variable {k: Type*} [Field k]

open Polynomial

abbrev PMod (q: k[X]) :=
  k[X] ⧸ Ideal.span {q}

noncomputable example {q: k[X]} : Ring (PMod q) := inferInstance

[Kenny Lau]

Thinking about it in terms of % is the "constructivist's pitfall" I suppose

[Kenny Lau]

if you "really want" the % for computation reasons, still use this, and then define a set bijection (≃) between the two sets, and then transport the ring structure over

[Alix Trieu]

Thanks! I will try that

[Kenny Lau]

(or maybe never transport the ring structure over. it feels like a bad idea to mix proofs with computation)