error using `by refine {...}; {...}` for an instance

Stream: new members

[Amelia Livingston]

Sorry for the unwieldy mwe. I get an error about metavariables trying to kill every goal with the last 4 lines. I've tried everything I can think of; this compiles if I copy paste this proof into each appropriate structure field. I've tried using @quotient.induction_on and specifying the setoid instances. I've tried reading the pp.all output but didn't manage to deduce anything from it. See #2922 for the real life version.

import ring_theory.localization

variables {R : Type*} [comm_ring R] (M : submonoid R)

instance : comm_monoid (submonoid.localization M) :=
(submonoid.localization.r M).comm_monoid

@[elab_as_eliminator]
protected def lift_on₂ {α : Type*} [monoid α] {β} {c : con α } (q r : c.quotient) (f : α → α → β)
  (h : ∀ a₁ a₂ b₁ b₂, c a₁ b₁ → c a₂ b₂ → f a₁ a₂ = f b₁ b₂) : β := quotient.lift_on₂' q r f h

def submonoid.localization.mk : R → M → submonoid.localization M :=
λ x y, (submonoid.localization.r M).mk' (x, y)

theorem r_of_eq {x y : R × M} (h : y.1 * x.2 = x.1 * y.2) :
  submonoid.localization.r M x y :=
submonoid.localization.r_iff_exists.2 ⟨1, by rw h⟩

instance : has_zero (submonoid.localization M) :=
⟨submonoid.localization.mk M 0 1⟩

instance : has_add (submonoid.localization M) :=
⟨λ z w, lift_on₂ z w
  (λ x y : R × M, submonoid.localization.mk M ((x.2 : R) * y.1 + y.2 * x.1) (x.2 * y.2)) $
λ r1 r2 r3 r4 h1 h2, (con.eq _).2
begin
  rw submonoid.localization.r_eq_r' at h1 h2 ⊢,
  cases h1 with t₅ ht₅,
  cases h2 with t₆ ht₆,
  use t₆ * t₅,
  calc ((r1.2 : R) * r2.1 + r2.2 * r1.1) * (r3.2 * r4.2) * (t₆ * t₅) =
      (r2.1 * r4.2 * t₆) * (r1.2 * r3.2 * t₅) + (r1.1 * r3.2 * t₅) * (r2.2 * r4.2 * t₆) : by ring
      ... = (r3.2 * r4.1 + r4.2 * r3.1) * (r1.2 * r2.2) * (t₆ * t₅) : by rw [ht₆, ht₅]; ring
end⟩

instance : has_neg (submonoid.localization M) :=
⟨λ z, con.lift_on z (λ x : R × M, submonoid.localization.mk M (-x.1) x.2) $
  λ r1 r2 h, (con.eq _).2
begin
  rw submonoid.localization.r_eq_r' at h ⊢,
  cases h with t ht,
  use t,
  rw [neg_mul_eq_neg_mul_symm, neg_mul_eq_neg_mul_symm, ht],
  ring,
end⟩

instance : comm_ring (submonoid.localization M) :=
by refine
{ zero := 0,
  one  := 1,
  add  := (+),
  mul  := (*),
  add_assoc      := λ m n k, quotient.induction_on₃' m n k _,
  zero_add       := λ y, quotient.induction_on' y _,
  add_zero       := λ y, quotient.induction_on' y _,
  neg            := has_neg.neg,
  add_left_neg   := λ y, quotient.induction_on' y _,
  add_comm       := λ y z, quotient.induction_on₂' z y _,
  left_distrib   := λ m n k, quotient.induction_on₃' m n k _,
  right_distrib  := λ m n k, quotient.induction_on₃' m n k _,
   ..submonoid.localization.comm_monoid M };
  {  intros,
     refine quotient.sound (r_of_eq M _),
     simp only [prod.snd_mul, prod.fst_mul, submonoid.coe_mul],
     ring }

[Chris Hughes]

If you set_option pp.all true and #print comm_ring.zero_add, you can see the type of comm_ring.zero_add. It has add_semigroup.mk in the type, and then uses comm_ring.mul_assoc, so the type of comm_ring.zero_add actually depends on comm_ring.mul_assoc, which contains a metavariable since you didn't finish proving it yet.

[Chris Hughes]

That's not a solution.

[Mario Carneiro]

Here is a workaround:

private meta def tac := `[{
  intros,
  refine quotient.sound' (r_of_eq M _),
  simp only [prod.snd_mul, prod.fst_mul, submonoid.coe_mul],
  ring }]

instance : comm_ring (submonoid.localization M) :=
{ zero := 0,
  one  := 1,
  add  := (+),
  mul  := (*),
  add_assoc      := λ m n k, quotient.induction_on₃' m n k (by tac),
  zero_add       := λ y, quotient.induction_on' y (by tac),
  add_zero       := λ y, quotient.induction_on' y (by tac),
  neg            := has_neg.neg,
  add_left_neg   := λ y, quotient.induction_on' y (by tac),
  add_comm       := λ y z, quotient.induction_on₂' z y (by tac),
  left_distrib   := λ m n k, quotient.induction_on₃' m n k (by tac),
  right_distrib  := λ m n k, quotient.induction_on₃' m n k (by tac),
   ..submonoid.localization.comm_monoid M }

[Mario Carneiro]

it is times like this when I wish that interactive blocks had lambdas

[Amelia Livingston]

thank you!!