Notation version theorem only compiled with extra theorems

Stream: new members

[Shanghe Chen]

Hi when reading MIL§6 (continue Failed to write a*b on Group₁ but new topic for clearner context) I setup the class Group₂ as the tutorial

namespace Ex3
class Group₂ (α : Type u) where
  mul : α → α → α
  one : α
  inv : α → α
  mul_assoc : ∀ x y z : α, mul (mul x y) z = mul x (mul y z)
  mul_left_one : ∀ x : α, mul one x = x
  mul_left_inv : ∀ x : α, mul (inv x) x = one

instance hasMulGroup₂ {α : Type u} [Group₂ α] : Mul α := ⟨Group₂.mul⟩
instance hasOneGroup₂ {α : Type u} [Group₂ α] : One α := ⟨Group₂.one⟩
instance hasInvGroup₂ {α : Type u} [Group₂ α] : Inv α := ⟨Group₂.inv⟩
namespace Group₂

theorem self_mul_self_eq_self_imply_one [Group₂ α]: ∀ x : α,  mul x x = x → x = one := by
    intro x h
    have h₁: mul (inv x) (mul x x) = one := by
      simp only [h, mul_left_inv]
    have h₂: mul (inv x) (mul x x) = x := by
      simp only [←mul_assoc, mul_left_inv, mul_left_one]
    rw [h₂] at h₁
    exact h₁

theorem mul_left_inv' [Group₂ α]: ∀ x : α, x⁻¹ * x = 1 := mul_left_inv
theorem mul_left_one' [Group₂ α]: ∀ x : α, 1 * x = x := mul_left_one
theorem mul_assoc' [Group₂ α]: ∀ x y z : α, (x * y) * z = x * (y * z) := mul_assoc

-- It succeeds only with the three theorems aobve rather than the three axioms in `Group₂`
theorem self_mul_self_eq_self_imply_one' [Group₂ α]: ∀ x : α, x * x = x → x = 1 := by
    intro x h
    have h₁: x⁻¹ * (x * x) = 1 := by
      simp only [h, mul_left_inv']
    have h₂: x⁻¹ * (x * x) = x := by
      simp only [←mul_assoc', mul_left_inv', mul_left_one']
    rw [h₂] at h₁
    exact h₁

end Group₂
end Ex3

[Shanghe Chen]

I found that I must supply extra theorems stated with notations like mul_left_inv' to prove theorem that uses these notations. Is this by design that when we introduce notations, we must duplicate the original theorems/axioms with a notatoned version? Or is it any option to control this behavior? I found that self_mul_self_eq_self_imply_one' failed if I use mul_left_inv rather than mul_left_inv' in the proof.

[Kevin Buzzard]

Unfortunately what you're seeing above is a common idiom in mathlib. One way around it in this case (which is also the way it's done in mathlib) is to make Group2 extend Mul, One etc, then you can use the notation in the axioms and don't have to do this

[Kevin Buzzard]

This is teaching you the difference between definitonal and syntactic equality. In practice mathlib has a chosen syntactic preference for saying any basic mathematical idea (so for example in group theory it's a * b rather than mul a b) and all the lemmas are written using this so-called normal form (other than the simp lemmas of the from non_normal form = normal form)

[Shanghe Chen]

Yeah I am getting some information about equality from xena too:smiling_face: