Zulip Chat Archive

As I go through Kevin Buzzard's (amazing!) formalising-mathematics-2022 repo, I notice that there are a lot of boilerplate proofs that I keep repeating. For an egregious example, my proofs that $\mathbb{Z}$ is an abelian group is almost exactly the same as my proof that it is a commutative ring. I just copy-pasted basically the same block of code. It seems like there should be a better way of doing this. Is there?

instance add_comm_group : add_comm_group myint :=
{ add := (+),
  add_assoc := begin
    rintros a' b' c',
    apply quotient.induction_on₃ a' b' c',
    rintros ⟨a,b⟩ ⟨c,d⟩ ⟨e,f⟩,
    simp,
    ring,
  end,
  zero := 0,
  zero_add := begin
    intros a',
    apply quotient.induction_on a',
    rintros ⟨a,b⟩,
    simp,
    ring,
  end,
  add_zero := begin
    intros a',
    apply quotient.induction_on a',
    rintros ⟨a,b⟩,
    simp,
    ring,
  end,
  neg := has_neg.neg,
  add_left_neg := begin
    intros a',
    apply quotient.induction_on a',
    rintros ⟨a,b⟩,
    simp,
    ring,
  end,
  add_comm := begin
    rintros a' b',
    apply quotient.induction_on₂ a' b',
    rintros ⟨a,b⟩ ⟨c,d⟩,
    simp,
    ring,
  end }

and

instance : comm_ring myint :=
{ add := (+),
  zero := 0,
  mul := (*),
  mul_assoc := begin
    rintros a' b' c',
    apply quotient.induction_on₃ a' b' c',
    rintros ⟨a,b⟩ ⟨c,d⟩ ⟨e,f⟩,
    simp,
    ring,
  end,
  one := 1,
  one_mul := begin
    intros a',
    apply quotient.induction_on a',
    rintros ⟨a,b⟩,
    simp,
    ring,
  end,
  mul_one := begin
    intros a',
    apply quotient.induction_on a',
    rintros ⟨a,b⟩,
    simp,
    ring,
  end,
  left_distrib := begin
    rintros a' b' c',
    apply quotient.induction_on₃ a' b' c',
    rintros ⟨a,b⟩ ⟨c,d⟩ ⟨e,f⟩,
    simp,
    ring,
  end,
  right_distrib := begin
    rintros a' b' c',
    apply quotient.induction_on₃ a' b' c',
    rintros ⟨a,b⟩ ⟨c,d⟩ ⟨e,f⟩,
    simp,
    ring,
  end,
  mul_comm := begin
    rintros a' b',
    apply quotient.induction_on₂ a' b',
    rintros ⟨a,b⟩ ⟨c,d⟩,
    simp,
    ring,
  end,
  ..myint.add_comm_group }