## Stream: general

### Topic: rw not closing refl goal

#### Kevin Buzzard (Jul 11 2020 at 21:48):

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 (Jul 11 2020 at 21:56):

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 (Jul 11 2020 at 22:01):

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 (Jul 11 2020 at 22:10):

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

Last updated: May 11 2021 at 00:31 UTC