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?
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 }