如何解决Lean中定义loop类时的菱形继承报错问题

问题根源 #

该报错由菱形继承导致的字段重复冲突引起：quasigroup和unital都继承自magma，Lean默认会为两个父类分别生成独立的to_magma字段，导致loop结构中出现两个同名的magma实例声明，无法通过编译。

解决方案1：启用旧结构命令（最简便） #

在代码开头添加set_option old_structure_cmd true即可，该选项会让Lean沿用旧版结构继承逻辑，允许多个父类共享同一祖先结构的字段，不会重复生成to_magma字段。修改后的完整代码如下：

set_option old_structure_cmd true
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 α

解决方案2：显式绑定magma实例（无需修改全局选项） #

如果不想启用全局的旧结构命令，可以显式指定unital使用的magma实例来自已经继承的quasigroup，避免重复声明，写法如下：

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 )

-- 显式指定unital的magma实例来自quasigroup导出的实例
class loop (α : Type u) extends quasigroup α, @unital α (quasigroup.to_magma α)

两种方案都可以正常编译，实现同时具备quasigroup和unital性质的loop结构。

内容的提问来源于stack exchange，提问作者Wheat Wizard