rw not closing refl goal

Stream: general

[Kevin Buzzard]

What's going on here and can I fix it somehow? My lovely calc proof is being interrupted by having to use refl twice after a rewrite.

set_option old_structure_cmd true

namespace lftcm

/-- `monoid M` is the type of monoid structures on a type `M`. -/
class monoid (M : Type) extends has_mul M, has_one M :=
(mul_assoc : ∀ (a b c : M), a * b * c = a * (b * c))
(one_mul : ∀ (a : M), 1 * a = a)
(mul_one : ∀ (a : M), a * 1 = a)

/-- `group G` is the type of group structures on a type `G`. -/
class group (G : Type) extends monoid G, has_inv G :=
(mul_left_inv : ∀ (a : G), a⁻¹ * a = 1)

namespace group

variables {G : Type} [group G]

lemma mul_left_cancel (a b c : G) (Habac : a * b = a * c) : b = c :=
 calc b = 1 * b         : by rw one_mul
    ... = (a⁻¹ * a) * b : by rw mul_left_inv
    ... = a⁻¹ * (a * b) : begin rw mul_assoc, refl, end -- ??
    ... = a⁻¹ * (a * c) : by rw Habac
    ... = (a⁻¹ * a) * c : begin rw mul_assoc, refl, end -- ??
    ... = 1 * c         : by rw mul_left_inv
    ... = c             : by rw one_mul

end group end lftcm

[Kevin Buzzard]

It gets worse:

example (a b : G) : a * a⁻¹ = b :=
begin
  rw ←one_mul b,
  rw ←mul_left_inv a, -- error
  /-
  rewrite tactic failed, did not find instance of the pattern in the target expression
  1
  state:
  G : Type,
  _inst_1 : group G,
  a b : G
  ⊢ a * a⁻¹ = 1 * b
  -/
end

With pp.all on I see that the two 1's are:

1 : (@has_one.one.{0} G (@has_one.mk.{0} G (@lftcm.group.one G _inst_1)))

1 : @has_one.one.{0} G
    (@lftcm.monoid.to_has_one G
       (@lftcm.monoid.mk G (@lftcm.group.mul G _inst_1) (@lftcm.group.one G _inst_1) (@lftcm.group.mul_assoc G _inst_1)
          (@lftcm.group.one_mul G _inst_1)
          (@lftcm.group.mul_one G _inst_1)))

[Chris Hughes]

Here's a fix, but not a satisfactory one

set_option old_structure_cmd true

namespace lftcm

/-- `monoid M` is the type of monoid structures on a type `M`. -/
class monoid (M : Type) extends has_mul M, has_one M :=
(mul_assoc : ∀ (a b c : M), a * b * c = a * (b * c))
(one_mul : ∀ (a : M), 1 * a = a)
(mul_one : ∀ (a : M), a * 1 = a)

lemma one_mul {M : Type} [monoid M] (a : M) : 1 * a = a := monoid.one_mul _

lemma mul_assoc {M : Type} [monoid M] (a b c : M) :
  a * b * c = a * (b * c) := monoid.mul_assoc _ _ _

/-- `group G` is the type of group structures on a type `G`. -/
class group (G : Type) extends monoid G, has_inv G :=
(mul_left_inv : ∀ (a : G), a⁻¹ * a = 1)

namespace group

variables {G : Type} [group G]

lemma mul_left_cancel (a b c : G) (Habac : a * b = a * c) : b = c :=
 calc b = 1 * b         : by rw lftcm.one_mul
    ... = (a⁻¹ * a) * b : by rw mul_left_inv
    ... = a⁻¹ * (a * b) : begin rw lftcm.mul_assoc, end -- ??
    ... = a⁻¹ * (a * c) : by rw Habac
    ... = (a⁻¹ * a) * c : begin rw mul_assoc, refl, end -- ??
    ... = 1 * c         : by rw mul_left_inv
    ... = c             : by rw one_mul

[Kevin Buzzard]

Bhavik pointed out another one: if you don't use old structure command then it's OK -- but then you get other issues because in the group namespace Lean doesn't have a way to choose between _root_.mul_assoc and lftcm.monoid.mul_assoc