long elaboration time

Stream: general

[Kenny Lau]

import group_theory.free_abelian_group

universes u v

def free_ring (α : Type u) : Type u :=
free_abelian_group $ list α

namespace free_ring

variables (α : Type u)

instance : add_comm_group (free_ring α) :=
{ .. free_abelian_group.add_comm_group (list α) }

instance : ring (free_ring α) :=
{ mul := λ x, free_abelian_group.lift $ λ L2, free_abelian_group.lift (λ L1, free_abelian_group.of $ L1 ++ L2) x,
  one := free_abelian_group.of [],
  mul_assoc := λ x y z, begin
    unfold has_mul.mul,
    refine free_abelian_group.induction_on z rfl _ _ _,
    { intros L3, rw [free_abelian_group.lift.of, free_abelian_group.lift.of],
      refine free_abelian_group.induction_on y rfl _ _ _,
      { intros L2, iterate 3 { rw free_abelian_group.lift.of },
        refine free_abelian_group.induction_on x rfl _ _ _,
        { intros L1, iterate 3 { rw free_abelian_group.lift.of }, rw list.append_assoc },
        { intros L1 ih, iterate 3 { rw free_abelian_group.lift.neg }, rw ih },
        { intros x1 x2 ih1 ih2, iterate 3 { rw free_abelian_group.lift.add }, rw [ih1, ih2] } },
      { intros L2 ih, iterate 4 { rw free_abelian_group.lift.neg }, rw ih },
      { intros y1 y2 ih1 ih2, iterate 4 { rw free_abelian_group.lift.add }, rw [ih1, ih2] } },
    { intros L3 ih, iterate 3 { rw free_abelian_group.lift.neg }, rw ih },
    { intros z1 z2 ih1 ih2, iterate 2 { rw free_abelian_group.lift.add }, rw [ih1, ih2],
      exact (free_abelian_group.lift.add _ _ _).symm }
  end,
  .. free_ring.add_comm_group α }

end free_ring

[Kenny Lau]

@Mario Carneiro Could you help me debug the long elaboration time?

[Kenny Lau]

Isolating a semigroup instance seems to speed things up