Group notation

Stream: new members

[Martin Epstein]

Hello all. My next Lean project is to do a little group theory. Following along with Mathematics In Lean I got the convenient notation for multiplication, one, and inverses to work for my custom mygroup class. But the rewrite tactic doesn't seem to have gotten the memo.
"""
Tactic rewrite failed: Did not find an occurrence of the pattern
mul (inv a) a
in the target expression
mul (mul a⁻¹⁻¹ a⁻¹) a = mul a⁻¹⁻¹ (mul a⁻¹ a)
"""
How can I get the rewrite tactic to identify expressions like mul a⁻¹ a and mul (inv a) a?

Here is the whole file so far:

import Mathlib.Tactic

class mygroup (α : Type*) where
  mul : α → α → α
  one : α
  inv : α → α
  assoc : ∀ a b c, mul (mul a b) c = mul a (mul b c)
  one_mul : ∀ a, mul one a = a
  inv_mul : ∀ a, mul (inv a) a = one

instance {α : Type*} [mygroup α] : Mul α :=
  ⟨mygroup.mul⟩

instance {α : Type*} [mygroup α] : One α :=
  ⟨mygroup.one⟩

instance {α : Type*} [mygroup α] : Inv α :=
  ⟨mygroup.inv⟩

namespace mygroup

lemma inv_inv_mul_one (α : Type*) [mygroup α] (a : α) :
    a = (a⁻¹)⁻¹ * 1 := by
  have h1 := assoc (a⁻¹)⁻¹ a⁻¹ a
  have h2 := inv_mul a
  rw [h2] at h1
  sorry

end mygroup

The error is at h2 in the line rw [h2] at h1. The infoview shows:

α : Type u_1
inst✝ : mygroup α
a : α
h1 : mul (mul a⁻¹⁻¹ a⁻¹) a = mul a⁻¹⁻¹ (mul a⁻¹ a)
h2 : mul (inv a) a = one
⊢ a = a⁻¹⁻¹ * 1

[Riccardo Brasca]

It's a little technical to explain, but basically don't state you assumptions using mul, only use *.

[Riccardo Brasca]

You have to define mygroup extending Mul

[Riccardo Brasca]

(deleted)

[Riccardo Brasca]

The following works

import Mathlib.Tactic

class mygroup (α : Type*) extends Mul α, One α, Inv α where
  assoc : ∀ (a b c : α), (a * b) * c = a * (b * c)
  one_mul : ∀ (a : α), 1 * a = a
  inv_mul : ∀ (a : α), a⁻¹ * a = 1

namespace mygroup

lemma inv_inv_mul_one (α : Type*) [mygroup α] (a : α) :
    a = (a⁻¹)⁻¹ * 1 := by
  have h1 := assoc (a⁻¹)⁻¹ a⁻¹ a
  have h2 := inv_mul a
  rw [h2] at h1
  sorry

end mygroup

[Riccardo Brasca]

You can also write

change mul (mul a⁻¹⁻¹ a⁻¹) a = mul a⁻¹⁻¹ (mul (inv a) a) at h1

before rw [h2] at h1, but you are going to suffer a lot. If you do as I suggested you never see mul, inv, one and everything is as it is on paper

[Martin Epstein]

Perfect, thanks!

[Michael Rothgang]

Riccardo Brasca said:

It's a little technical to explain, but basically don't state you assumptions using mul, only use *.

Thanks, TIL! Do you have a link to the technical explanation/the key term to search for?

[Riccardo Brasca]

It's the fact that rw wants syntactic equality, definitional equality is not enough. This is surely explained several times zulip but you're right, it would be good to have a nicely written reference.

[Snir Broshi]

Riccardo Brasca said:

it would be good to have a nicely written reference.

This exists in Xena project handbook and Xena project blog, and MIL mentions it in passing:

Contrary to some other tactics, rw operates on the syntactic level, it won’t unfold definitions or apply reductions for you (it has a variant called erw that tries a little harder in this direction, but not much harder).