Resolving a "diamond inheritance" class in lean

Question

I have a pretty basic construction of loops in mind for lean. I construct a class for magmata, a class for quasigroups (cancellative magmata), and a class for unital magmata. From there a loop is just something that is both a quasigroup and a unital magma.

In Haskell this would look like

class Magma a where
  add :: a -> a -> a

class Magma a => Unital a where
  unit :: a

class Magma a => Quasigroup a where
  left_div :: a -> a -> a
  right_div :: a -> a -> a

class (Quasigroup a, Unital a) => Loop a

So I try to translate that to lean:

universe u

class magma (α : Type u) :=
  ( add : α → α → α )

class unital (α : Type u) extends magma α :=
  ( unit : α )
  ( left_id : ∀ a : α, add unit a = a )
  ( right_id : ∀ a : α, add a unit = a )

class quasigroup (α : Type u) extends magma α :=
  ( left_div : α → α → α )
  ( right_div : α → α → α )
  ( left_cancel : ∀ a b : α, add a (left_div a b) = b )
  ( right_cancel : ∀ a b : α, add (right_div b a) a = b )

class loop (α : Type u) extends quasigroup α, unital α

But lean complains that:

invalid 'structure' header, field 'to_magma' from 'unital' has already been declared

Which is pretty cryptic, but if we play around with things, it becomes apparent that this is some sort of problem resembling diamond inheritance. It doesn't like that we have made two paths from loop to magma.

How can I tell lean that these are the same magmata and resolve this issue?

user_7690601 · Answer

On Lean 3.35.1, you have several possible solutions. For Haskell-like record merging, there is old_structure_cmd:

universe u

class magma (α : Type u) :=
(add : α → α → α)

class unital (α : Type u) extends magma α :=
(unit : α)
(left_id : ∀ a : α, add unit a = a)
(right_id : ∀ a : α, add a unit = a)

class quasigroup (α : Type u) extends magma α :=
(left_div : α → α → α)
(right_div : α → α → α)
(left_cancel : ∀ a b : α, add a (left_div a b) = b)
(right_cancel : ∀ a b : α, add (right_div b a) a = b)

set_option old_structure_cmd true

class loop (α : Type u) extends quasigroup α, unital α.

That will work as you expect. However, the downside of old_structure_cmd is that the structures are all "flattened" and grow in size. The "new" way is to have a main "trunk" of structure, and create offshoot inheritance:

universe u

class magma (α : Type u) :=
(add : α → α → α)

class unital (α : Type u) extends magma α :=
(unit : α)
(left_id : ∀ a : α, add unit a = a)
(right_id : ∀ a : α, add a unit = a)

class quasigroup (α : Type u) extends magma α :=
(left_div : α → α → α)
(right_div : α → α → α)
(left_cancel : ∀ a b : α, add a (left_div a b) = b)
(right_cancel : ∀ a b : α, add (right_div b a) a = b)

class loop (α : Type u) extends quasigroup α :=
(unit : α)
(left_id : ∀ a : α, add unit a = a)
(right_id : ∀ a : α, add a unit = a)

instance loop.to_unital {α : Type u} [h : loop α] : unital α :=
{ ..h }

Resolving a "diamond inheritance" class in lean

1 Answers