Any advice for advoiding type class ambiguities?

Stream: new members

[Robert Culling]

Kia ora :)

I am trying to recreate some of the algebra hierarchy. I have the following code leading up to the definition of an elementary theorem in Group theory.

-- Magma are types with a single binary operation.
class Magma (α : Type) where
  bop : α → α → α

infixl: 70 " * " => Magma.bop

open Magma

-- Semirgroups are a Magma whose binary operation is associative.
class Semigroup (G : Type) extends Magma G where
  bop_assoc : ∀ x y z : G, (x * y) * z = x * (y * z)

open Semigroup

-- Monoids are Semigroups with an identity.
class Monoid (G : Type) extends Semigroup G where
  id : G
  id_bop : ∀ x : G, id * x = x

open Monoid

-- Groups are Monoids with inverses.
class Group (G : Type) extends Monoid G where
  inv : G → G
  inv_bop : ∀ x : G, (inv x) * x = id

postfix: 100 " ⁻¹ " => Group.inv

open Group

theorem bop_cancel_left (G : Type) (t : Group G) :
  ∀ a x y : G, a * x = a * y → x = y :=
    by
      intro a x y
      intro h
      calc x
      _ = id * x        := by rw [←id_bop]
      _ = (a⁻¹ * a) * x := by rw [←inv_bop]
      _ = a⁻¹ * (a * x) := by rw [bop_assoc]
      _ = a⁻¹ * (a * y) := by rw [h]
      _ = (a⁻¹ * a) * y := by rw [←bop_assoc]
      _ = id * y        := by rw [inv_bop]
      _ = y             := by rw [id_bop]

Lean is unhappy with the first line in the calculation. There is a red line underneath id * x and it explains that it doesn't know how to make sense of id. I changed the name of the identity, and I introduced parentheses. But the ambiguity remains.

Does any one have any advice on how to set up the hierarchy in such a way as to avoid the ambiguities? Thank you!

[Kyle Miller]

The other ambiguity is that there's already a *. It'd be best if you didn't override the notation and instead made an HMul instance, but if you set a high priority you can override * completely.

I'm not sure if there's anything you can do for id but rename it, so it doesn't conflict with the identity function. I suppose you could do notation "id" => Monoid.id to make it be syntax.

-- Magma are types with a single binary operation.
class Magma (α : Type) where
  bop : α → α → α

infixl:70 (priority := high)" * " => Magma.bop

open Magma

-- Semirgroups are a Magma whose binary operation is associative.
class Semigroup (G : Type) extends Magma G where
  bop_assoc : ∀ x y z : G, (x * y) * z = x * (y * z)

open Semigroup

-- Monoids are Semigroups with an identity.
class Monoid (G : Type) extends Semigroup G where
  id' : G
  id_bop : ∀ x : G, id' * x = x

open Monoid

-- Groups are Monoids with inverses.
class Group (G : Type) extends Monoid G where
  inv : G → G
  inv_bop : ∀ x : G, (inv x) * x = id'

postfix:100 (priority := high) " ⁻¹ " => Group.inv

open Group

theorem bop_cancel_left (G : Type) (t : Group G) :
  ∀ a x y : G, a * x = a * y → x = y :=
    by
      intro a x y
      intro h
      calc x
      _ = id' * x        := by rw [id_bop]
      _ = (a⁻¹ * a) * x := by rw [←inv_bop]
      _ = a⁻¹ * (a * x) := by rw [bop_assoc]
      _ = a⁻¹ * (a * y) := by rw [h]
      _ = (a⁻¹ * a) * y := by rw [←bop_assoc]
      _ = id' * y        := by rw [inv_bop]
      _ = y             := by rw [id_bop]

[Robert Culling]

@Kyle Miller thank you :) Renaming id and renaming the multiplication symbol fixed the errors!

Is it possible to make Magma.bop an instance of HMul?

[N Gelwan]

Given an instance of Magma α you can obtain an instance of HMul α α α:

instance [Magma α] : HMul α α α where
  hMul := Magma.bop