Problems with stuck typeclass instance (Group-related)

Stream: lean4

[Hannah Santos]

I've been trying to prove some theorems with Groups, but I ended up with this error that I have no idea how to fix. It's on the end of the code block, when I'm trying to prove that inv id = id, in other words.

------------------------------------------------
-- Useful Theorems :
------------------------------------------------

theorem determinist_fun {α β : Type u} :
  ∀ (f : α → β) (a a' : α), a = a' → f a = f a' :=
by
  intro f a a' h
  rw [h]

------------------------------------------------
-- Group Definition :
------------------------------------------------

class Group (G : Type u) where
  op : G → G → G
  e : G
  inv : G → G
  Op_Ass : ∀ (a b c : G), op (op a b) c = op a (op b c)
  Id_Op : ∀ (a : G), op e a = a
  Op_Id : ∀ (a : G), op a e = a
  Op_Inv_L : ∀ (a : G), op (inv a) a = e
  Op_Inv_R : ∀ (a : G), op a (inv a) = e

open Group

infixl:65   " ⋆ " => op
postfix:max "⁻¹"  => inv

------------------------------------------------
-- Group Theorems:
------------------------------------------------

theorem Op_Can_R [Group G] :
  ∀ (a b c : G), a ⋆ c = b ⋆ c → a = b :=
by
  intro a b c h
  have h1 :  a ⋆ c ⋆ c⁻¹ = b ⋆ c ⋆ c⁻¹ := by
    exact determinist_fun (· ⋆ c⁻¹) (a ⋆ c) (b ⋆ c) h
  rw [Op_Ass, Op_Inv_R, Op_Ass, Op_Inv_R, Op_Id, Op_Id] at h1
  exact h1

theorem Op_Can_L [Group G] :
  ∀ (a b c : G), c ⋆ a = c ⋆ b → a = b :=
by
  intro a b c h
  have h1 :  c⁻¹ ⋆ (c ⋆ a) = c⁻¹ ⋆ (c ⋆ b) := by
    exact determinist_fun (c⁻¹ ⋆ ·) (c ⋆ a) (c ⋆ b) h
  rw [← Op_Ass, Op_Inv_L, ← Op_Ass, Op_Inv_L, Id_Op, Id_Op] at h1
  exact h1

theorem Pass [Group G] :
  ∀ (a b : G), a = b → a ⋆ b⁻¹ = e :=
by
  intro a b h
  have h1 :  a ⋆ b⁻¹ = b ⋆ b⁻¹ := by
    exact determinist_fun (· ⋆ b⁻¹) a b h
  rw [Op_Inv_R] at h1
  exact h1

theorem Back [Group G] :
  ∀ (a b : G), a ⋆ b⁻¹ = e → a = b :=
by
  intro a b h
  have h1 :  a ⋆ b⁻¹ ⋆ b = e ⋆ b := by
    exact determinist_fun (· ⋆ b) (a ⋆ b⁻¹) e h
  rw [Id_Op, Op_Ass, Op_Inv_L, Op_Id] at h1
  exact h1

theorem Op_Exists_Res_R [Group G] :
  ∀ (a b : G), ∃ (x : G), a ⋆ x = b :=
by
  intro a b
  refine ⟨(a⁻¹ ⋆ b), ?_⟩
  rw [← Op_Ass, Op_Inv_R, Id_Op]

theorem Op_Exists_Res_L [Group G] :
  ∀ (a b : G), ∃ (x : G), x ⋆ a = b :=
by
  intro a b
  refine ⟨(b ⋆ a⁻¹), ?_⟩
  rw [Op_Ass, Op_Inv_L, Op_Id]

theorem Op_Only_Res_R [Group G] :
  ∀ (a u u' : G), a ⋆ u = b ∧ a ⋆ u' = b → u = u' :=
by
  intro a u u' h
  have h1 : a ⋆ u = a ⋆ u' := by
    rw [h.1, h.2]
  exact Op_Can_L u u' a h1

theorem Op_Only_Res_L [Group G] :
  ∀ (a u u' : G), u ⋆ a = b ∧ u' ⋆ a = b → u = u' :=
by
  intro a u u' h
  have h1 : u ⋆ a = u' ⋆ a := by
    rw [h.1, h.2]
  exact Op_Can_R u u' a h1

theorem Cheap_Id_L [Group G] :
  ∀ (a u : G), u ⋆ a = a → u = e :=
by
  intro a u h
  exact Op_Only_Res_L a u e ⟨h, Id_Op a⟩

theorem Cheap_Id_R [Group G] :
  ∀ (u a : G), a ⋆ u = a → u = e :=
by
  intro u a h
  exact Op_Only_Res_R a u e ⟨h, Op_Id a⟩

theorem Cheap_Inv_L [Group G] :
  ∀ (a u : G), u ⋆ a = e → u = a⁻¹ :=
by
  intro a u h
  exact Op_Only_Res_L a u a⁻¹ ⟨h, Op_Inv_L a⟩

theorem Cheap_Inv_R [Group G] :
  ∀ (a u : G), a ⋆ u = e → u = a⁻¹ :=
by
  intro a u h
  exact Op_Only_Res_R a u a⁻¹ ⟨h, Op_Inv_R a⟩

theorem Inv_Cheap_R [Group G] :
  ∀ (a u : G), a⁻¹ ⋆ u = e → u = a :=
by
  intro a u h
  exact Op_Only_Res_R a⁻¹ u a ⟨h, Op_Inv_L a⟩


theorem Inv_Inv [Group G] :
  ∀ (a : G), (a⁻¹)⁻¹ = a :=
by
  intro a
  suffices h : a⁻¹ ⋆ (a⁻¹)⁻¹ = e from Inv_Cheap_R a (a⁻¹)⁻¹ h
  rw [Op_Inv_R]

theorem Inv_Id [Group G] :
  e⁻¹ = e :=
by
  suffices h : ∀ (x : G), x ⋆ e⁻¹ = x from Cheap_Id_R e⁻¹ h

/-
Group.lean:145:9
Expected type
G : Type ?u.16886
inst✝ : Group G
⊢ {G : Type ?u.16893} → [self : Group G] → G
Messages (1)
 Group.lean:145:8
  typeclass instance problem is stuck, it is often due to metavariables
    Group ?m.16910
All Messages (1)
-/

[Marcus Rossel]

Lean doesn't know what the type of e is supposed to be. If you explicitly annotate its type, it works:

theorem Inv_Id [Group G] : e⁻¹ = (e : G) := ...

[Patrick Massot]

Yes, there is no way Lean can guess the type of e in this statement.

[Hannah Santos]

But why does that happen? Wasn't it supposed to be infer it by the type of =?

[Hannah Santos]

Or by the Goup.e in itself?

[Marcus Rossel]

Perhaps this is more clear in the following example:

example [Group G] [Group G'] : e⁻¹ = e := ...

In this case, which type should Lean choose for e?

[Damiano Testa]

Also, lean complains about the second e, but you can ascript the first e and also that is good enough.

[Hannah Santos]

Thank you, guys.

[Richard Osborn]

Side note: Your determinist_fun is basically just docs#congrArg.

[Hannah Santos]

I have tried getting mathlib, but even with the tutorial I just couldn't, no idea why.

[Hannah Santos]

Also, I don't mind, since I use Lean for this specific reason anyway, to write proofs and study.

[Eric Wieser]

congrArg is not part of mathlib, it's part of Lean itself

[Eric Wieser]

(you can tell because the top of the page that links to says Init. instead of Mathlib.)

[Marcus Rossel]

(Also, if you do want to use Mathlib, people here could probably walk you through the setup in no time.)