deriving Group from PresentedGroup

Stream: new members

[Alex Brodbelt]

I am following the example from MIL and #new members > Group presentation hom injective but I am not sure why I cannot derive the Group instance in the following

import Mathlib

inductive Symbols
 | x
 | y

open FreeGroup Symbols PresentedGroup

/-
The set of relations for the group presentation ⟨x, y | x^n = y^2, y * x * y⁻¹ = x⁻¹ ⟩
-/
def Relations (n : ℕ) : Set (FreeGroup (Symbols)) :=
  {.of x ^ n * (.of y)⁻¹ * (.of y)⁻¹ } ∪
  {.of y * .of x * (.of y)⁻¹ * .of x }

variable (n : ℕ)

def myGroup :=
  PresentedGroup <| Relations n deriving Group

[Aaron Liu]

There is no deriving handler for group.

[Aaron Liu]

Maybe something like this?

import Mathlib

inductive Symbols
 | x
 | y

open FreeGroup Symbols PresentedGroup

/-
The set of relations for the group presentation ⟨x, y | x^n = y^2, y * x * y⁻¹ = x⁻¹ ⟩
-/
def Relations (n : ℕ) : Set (FreeGroup (Symbols)) :=
  {.of x ^ n * (.of y)⁻¹ * (.of y)⁻¹ } ∪
  {.of y * .of x * (.of y)⁻¹ * .of x }

variable (n : ℕ)

abbrev myGroup := PresentedGroup <| Relations n

#synth Group (myGroup _)

[Alex Brodbelt]

Hmm maybe MIL is a bit misleading?
image.png

In the chapter https://leanprover-community.github.io/mathematics_in_lean/C08_Groups_and_Rings.html

[Alex Brodbelt]

thank you @Aaron Liu !

[Aaron Liu]

Alex Brodbelt said:

Hmm maybe MIL is a bit misleading?
image.png

In the chapter https://leanprover-community.github.io/mathematics_in_lean/C08_Groups_and_Rings.html

This is definitely wrong

[Alex Brodbelt]

Hmm #synth Group (myGroup _) does not work for me... Maybe I need to update my dependencies.

[Kevin Buzzard]

Even with the abbrev change?

[Alex Brodbelt]

I will take this a sign that I should go to sleep - thanks Kevin, it now works. I don't get why it works but I'll trust Lean's magic.

[Kevin Buzzard]

Lean does not do magic. Typeclass inference can see through abbrev s (because they're reducible) but not defs (because they're irreducible).

import Mathlib

def X := ℕ
abbrev Y := ℕ

example : X := 0 -- fails
example : Y := 0 -- works