## Stream: new members

### Topic: boilerplate code

#### Vasily Ilin (Apr 05 2022 at 22:22):

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 := (+),
rintros a' b' c',
apply quotient.induction_on₃ a' b' c',
rintros ⟨a,b⟩ ⟨c,d⟩ ⟨e,f⟩,
simp,
ring,
end,
zero := 0,
intros a',
apply quotient.induction_on a',
rintros ⟨a,b⟩,
simp,
ring,
end,
intros a',
apply quotient.induction_on a',
rintros ⟨a,b⟩,
simp,
ring,
end,
neg := has_neg.neg,
intros a',
apply quotient.induction_on a',
rintros ⟨a,b⟩,
simp,
ring,
end,
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,


#### Mario Carneiro (Apr 05 2022 at 22:29):

you should take a look at the proof that the complexes are a ring

#### Mario Carneiro (Apr 05 2022 at 22:29):

it has a very similar structure: apply ext , simp, ring and repeat 16 times or so

#### Mario Carneiro (Apr 05 2022 at 22:30):

this kind of proof compresses very well using tactic combinators like ; which say "run this tactic on all subgoals"

#### Mario Carneiro (Apr 05 2022 at 22:30):

src#complex.comm_ring

#### Kevin Buzzard (Apr 05 2022 at 23:11):

How do I compress these proofs though? I have to apply quotient.induction_on_{x} for varying values of x.

#### Eric Wieser (Apr 06 2022 at 03:48):

repeat { intro x, apply quotient.induction_on x }?

#### Kevin Buzzard (Apr 06 2022 at 17:01):

I think this might produce different goals?

Last updated: Dec 20 2023 at 11:08 UTC