10.2. 实例声明🔗

实例声明的语法与定义几乎完全相同。唯一的语法区别在于关键字 Lean.Parser.Command.declaration : commanddef 被替换为 Lean.Parser.Command.declaration : commandinstance，且名称是可选的：

语法实例声明

大多数实例使用 Lean.Parser.Command.declaration : commandwhere 语法来定义各个方法：

instance ::= ...
    | `attrKind` 匹配 `("scoped" <|> "local")?`，用于属性之前，例如 `@[local simp]`。instance ((priority := prio))? `declId` 匹配 `foo` 或 `foo.{u,v}`：一个标识符，后面可以跟一个宇宙名称列表。declId? `declSig` 匹配类型必需的声明签名：先是一列绑定器，随后是 `: type`。declSig where
        structInstField*

然而，类型类本身是归纳类型，因此可以使用任何具有合适类型的表达式来构造实例：

instance ::= ...
    | `attrKind` 匹配 `("scoped" <|> "local")?`，用于属性之前，例如 `@[local simp]`。instance ((priority := prio))? `declId` 匹配 `foo` 或 `foo.{u,v}`：一个标识符，后面可以跟一个宇宙名称列表。declId? `declSig` 匹配类型必需的声明签名：先是一列绑定器，随后是 `: type`。declSig :=
        term终止提示依次为 `termination_by` 和 `decreasing_by`。

实例也可以通过分情况进行定义；然而，除了 Decidable 实例外，这个特性很少被使用：

instance ::= ...
    | `attrKind` 匹配 `("scoped" <|> "local")?`，用于属性之前，例如 `@[local simp]`。instance ((priority := prio))? `declId` 匹配 `foo` 或 `foo.{u,v}`：一个标识符，后面可以跟一个宇宙名称列表。declId? `declSig` 匹配类型必需的声明签名：先是一列绑定器，随后是 `: type`。declSig
        (| term => term)*终止提示依次为 `termination_by` 和 `decreasing_by`。

使用显式项定义的实例通常包含以下两种：要么是包装着方法实现的匿名构造器（Lean.Parser.Term.anonymousCtor : term如果期望类型是只有一个构造器 `c` 的归纳类型，那么*匿名构造器* `⟨e, ...⟩` 等价于 `c e ...`。如果给出的项比 `c` 的参数更多，其余参数会组成新的匿名构造器应用。例如，`⟨a, b, c⟩ : α × (β × γ)` 等价于 `⟨a, ⟨b, c⟩⟩`。⟨...⟩），要么是在定义相等的类型上调用 inferInstanceAs。

实例的精译过程几乎与普通定义的精译相同，除了以下记录的一些注意事项。如果没有提供名称，系统将自动创建一个。可以直接引用这个生成的名称，但用于生成名称的算法过去曾经改变过，将来也可能还会改变。对于将要被直接引用的实例，最好对其进行显式命名。精译之后，新实例会被注册为实例搜索的一个候选者。将 instance 属性添加到一个名称上，可以用来将任何其他已定义的名称标记为候选。

实例名称的生成

执行这些声明后：

structure NatWrapper where
  val : Nat

instance : BEq NatWrapper where
  beq
    | ⟨x⟩, ⟨y⟩ => x == y

名称 instBEqNatWrapper 指代该新实例。

在线查看 ↪

实例定义的变体

给定这个结构体类型：

structure NatWrapper where
  val : Nat

以下所有定义 BEq 实例的方式都是等价的：

instance : BEq NatWrapper where
  beq
    | ⟨x⟩, ⟨y⟩ => x == y

instance : BEq NatWrapper :=
  ⟨fun x y => x.val == y.val⟩

instance : BEq NatWrapper :=
  ⟨fun ⟨x⟩ ⟨y⟩ => x == y⟩

除了向环境中引入了不同的名称外，以下这些也是等价的：

@[instance]
def instBeqNatWrapper : BEq NatWrapper where
  beq
    | ⟨x⟩, ⟨y⟩ => x == y

instance : BEq NatWrapper :=
  ⟨fun x y => x.val == y.val⟩

instance : BEq NatWrapper :=
  ⟨fun ⟨x⟩ ⟨y⟩ => x == y⟩

在线查看 ↪

10.2.1. 递归实例🔗

在结构体定义中使用 Lean.Parser.Command.declaration : commandwhere 语法定义的函数不是递归的。由于实例声明是结构体定义的一种变体，默认情况下，类型类的方法也不是递归的。然而，递归归纳类型的实例是很常见的。为了绕过这个限制，有一个标准的惯用法：在实例之外独立定义一个递归函数，然后在实例定义中引用它。按照惯例，这些递归函数与相应的方法同名，但定义在目标类型的命名空间中。

实例不是递归的

给定如下的 NatTree 定义：

inductive NatTree where
  | leaf
  | branch (left : NatTree) (val : Nat) (right : NatTree)

如下的 BEq 实例会失败：

instance : BEq NatTree where
  beq
    | .leaf, .leaf =>
      true
    | .branch l1 v1 r1, .branch l2 v2 r2 =>
      failed to synthesize instance of type class
  BEq NatTree

Hint: Adding the command `deriving instance BEq for NatTree` may allow Lean to derive the missing instance.l1 == l2 && v1 == v2 && failed to synthesize instance of type class
  BEq NatTree

Hint: Adding the command `deriving instance BEq for NatTree` may allow Lean to derive the missing instance.r1 == r2
    | _, _ =>
      false

在左右的递归调用处都会出现如下报错：

failed to synthesize instance of type class
  BEq NatTree

Hint: Adding the command `deriving instance BEq for NatTree` may allow Lean to derive the missing instance.

给定一个合适的递归函数，例如 NatTree.beq：

def NatTree.beq : NatTree → NatTree → Bool
  | .leaf, .leaf =>
    true
  | .branch l1 v1 r1, .branch l2 v2 r2 =>
    NatTree.beq l1 l2 && v1 == v2 && NatTree.beq r1 r2
  | _, _ =>
    false

就可以分第二步创建这个实例：

instance : BEq NatTree where
  beq := NatTree.beq

或者，等价地，使用匿名构造器语法：

instance : BEq NatTree := ⟨NatTree.beq⟩

在线查看 ↪

此外，实例在其自身的定义期间是不可以用于实例合成的。它们仅在定义完成之后，才会被标记为可供实例合成。对于嵌套归纳类型（其中类型的递归出现是作为其他一些归纳类型的参数），甚至可能需要一个可用的实例才能写出递归函数。绕过这个限制的标准惯用法是：在递归定义的函数中创建一个局部实例（包含对正在定义的函数的引用），从而利用实例合成可使用局部上下文中每一个具有正确类型的绑定这一事实。

嵌套类型的实例

在这个 NatRoseTree 的定义中，正被定义的类型被嵌套在另一个归纳类型构造器（Array）之下：

inductive NatRoseTree where
  | node (val : Nat) (children : Array NatRoseTree)

检查玫瑰树的相等性需要检查数组的相等性。然而，实例在其自身定义期间通常不能用于实例合成，因此以下定义会失败，尽管 NatRoseTree.beq 是一个递归函数并且在其自身定义的作用域内。

def NatRoseTree.beq : (tree1 tree2 : NatRoseTree) → Bool
  | .node val1 children1, .node val2 children2 =>
    val1 == val2 &&
    failed to synthesize instance of type class
  BEq (Array NatRoseTree)

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.children1 == children2

failed to synthesize instance of type class
  BEq (Array NatRoseTree)

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

要解决这个问题，可以通过 let 绑定一个局部的 BEq NatRoseTree 实例：

partial def NatRoseTree.beq : (tree1 tree2 : NatRoseTree) → Bool
  | .node val1 children1, .node val2 children2 =>
    let _ : BEq NatRoseTree := ⟨NatRoseTree.beq⟩
    val1 == val2 &&
    children1 == children2

子节点上使用了数组相等性，可以在实例合成期间找到由 let 绑定的实例。

在线查看 ↪

10.2.2. `class inductive` 的实例🔗

许多实例具有函数类型：任何会递归调用实例搜索的实例本身都是一个函数，具有隐式参数的实例同样如此。虽然大多数实例只是根据它们自己的实例参数投影出方法实现，但类归纳类型的实例通常会对它们的一个或多个参数进行模式匹配，允许实例去选择适当的构造器。这是使用普通的 Lean 函数语法完成的。正如其他实例一样，讨论的这个函数在其自身定义期间是不可用于实例合成的。

和类的实例

因为 DecidableEq α 是 (a b : α) → Decidable (Eq a b) 的缩写，其参数可以直接使用，如此例所示：

inductive ThreeChoices where
  | yes | no | maybe

instance : DecidableEq ThreeChoices
  | .yes,   .yes   =>
    .isTrue rfl
  | .no,    .no    =>
    .isTrue rfl
  | .maybe, .maybe =>
    .isTrue rfl
  | .yes,   .maybe | .yes,   .no
  | .maybe, .yes   | .maybe, .no
  | .no,    .yes   | .no,    .maybe =>
    .isFalse nofun

在线查看 ↪

和类的递归实例

StringList 类型表示字符串的单态列表：

inductive StringList where
  | nil
  | cons (hd : String) (tl : StringList)

在下述定义 DecidableEq 实例的尝试中，精译内部的 termIfThenElse : term`if c then t else e` 是 `ite c t e`（即“如果—那么—否则”）的记法；它根据 `c` 是否为真返回 `t` 或 `e`。显式参数 `c : Prop` 本身没有计算内容；另有一个由实例合成得到的 `[Decidable c]` 参数，真正决定如何把 `c` 求值为真或假。写成 `if h : c then t else e` 时表示依赖式条件 `dite`，此时 `t` 和 `e` 可以使用 `c` 为真或假的事实。标识符中的记法约定：建议将 `if c then t else e` 写作 `ite`，并分别用 `left`、`right` 指代 `t`、`e`。if 时调用的实例合成失败了，因为该实例在其自身的定义期间不能用于实例合成：

instance : DecidableEq StringList
  | .nil, .nil => .isTrue rfl
  | .cons h1 t1, .cons h2 t2 =>
    if h : h1 = h2 then
      failed to synthesize instance of type class
  Decidable (t1 = t2)

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.if h' : t1 = t2 then
        .isTrue (byh1:Stringt1:StringListh2:Stringt2:StringListh:h1 = h2h':t1 = t2⊢ StringList.cons h1 t1 = StringList.cons h2 t2 simp [*]All goals completed! 🐙)
      else
        .isFalse (byh1:Stringt1:StringListh2:Stringt2:StringListh:h1 = h2h':¬t1 = t2⊢ ¬StringList.cons h1 t1 = StringList.cons h2 t2 intro hEqh1:Stringt1:StringListh2:Stringt2:StringListh:h1 = h2h':¬t1 = t2hEq:StringList.cons h1 t1 = StringList.cons h2 t2⊢ False; cases hEqreflh1:Stringt1:StringListh:h1 = h1h':¬t1 = t1⊢ False; trivialAll goals completed! 🐙)
    else
      .isFalse (byh1:Stringt1:StringListh2:Stringt2:StringListh:¬h1 = h2⊢ ¬StringList.cons h1 t1 = StringList.cons h2 t2 intro hEqh1:Stringt1:StringListh2:Stringt2:StringListh:¬h1 = h2hEq:StringList.cons h1 t1 = StringList.cons h2 t2⊢ False; cases hEqreflh1:Stringt1:StringListh:¬h1 = h1⊢ False; trivialAll goals completed! 🐙)
  | .nil, .cons _ _ | .cons _ _, .nil => .isFalse nofun

failed to synthesize instance of type class
  Decidable (t1 = t2)

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

然而，因为它只是一个普通的 Lean 函数，所以它可以递归地引用自身显式提供的名称：

instance instDecidableEqStringList : DecidableEq StringList
  | .nil, .nil => .isTrue rfl
  | .cons h1 t1, .cons h2 t2 =>
    let _ : Decidable (t1 = t2) :=
      instDecidableEqStringList t1 t2
    if h : h1 = h2 then
      if h' : t1 = t2 then
        .isTrue (byh1:Stringt1:StringListh2:Stringt2:StringListx✝:Decidable (t1 = t2) := instDecidableEqStringList t1 t2h:h1 = h2h':t1 = t2⊢ StringList.cons h1 t1 = StringList.cons h2 t2 simp [*]All goals completed! 🐙)
      else
        .isFalse (byh1:Stringt1:StringListh2:Stringt2:StringListx✝:Decidable (t1 = t2) := instDecidableEqStringList t1 t2h:h1 = h2h':¬t1 = t2⊢ ¬StringList.cons h1 t1 = StringList.cons h2 t2 intro hEqh1:Stringt1:StringListh2:Stringt2:StringListx✝:Decidable (t1 = t2) := instDecidableEqStringList t1 t2h:h1 = h2h':¬t1 = t2hEq:StringList.cons h1 t1 = StringList.cons h2 t2⊢ False; cases hEqreflh1:Stringt1:StringListh:h1 = h1x✝:Decidable (t1 = t1) := instDecidableEqStringList t1 t1h':¬t1 = t1⊢ False; trivialAll goals completed! 🐙)
    else
      .isFalse (byh1:Stringt1:StringListh2:Stringt2:StringListx✝:Decidable (t1 = t2) := instDecidableEqStringList t1 t2h:¬h1 = h2⊢ ¬StringList.cons h1 t1 = StringList.cons h2 t2 intro hEqh1:Stringt1:StringListh2:Stringt2:StringListx✝:Decidable (t1 = t2) := instDecidableEqStringList t1 t2h:¬h1 = h2hEq:StringList.cons h1 t1 = StringList.cons h2 t2⊢ False; cases hEqreflh1:Stringt1:StringListh:¬h1 = h1x✝:Decidable (t1 = t1) := instDecidableEqStringList t1 t1⊢ False; trivialAll goals completed! 🐙)
  | .nil, .cons _ _ | .cons _ _, .nil => .isFalse nofun

在线查看 ↪

10.2.3. 实例优先级🔗

可以为实例分配优先级。在实例合成期间，更高优先级的实例会被优先考虑；有关实例合成的详情，请参阅实例合成小节。

语法实例优先级

优先级可以是数字：

prio ::=
    num

如果没有指定优先级，则使用对应于 1000 的默认优先级：

prio ::= ...
    | 默认优先级为 `default = 1000`；未指定优先级时使用它。default

当数字值太细粒度时，有三种命名优先级可用，分别对应于 100、500 和 10000。 prioMid : prio标准“中”优先级为 `mid = 500`；它低于 `default`，高于 `low`。mid 优先级低于 prioDefault : prio默认优先级为 `default = 1000`；未指定优先级时使用它。default。

prio ::= ...
    | 标准“低”优先级为 `low = 100`，用于优先级应低于默认值的项目。low

prio ::= ...
    | 标准“中”优先级为 `mid = 500`；它低于 `default`，高于 `low`。mid

prio ::= ...
    | 标准“高”优先级为 `high = 10000`，用于优先级应高于默认值的项目。high

最后，优先级还可以做加减法，因此 default + 2 也是个有效的优先级，对应于 1002：

prio ::= ...
    | 圆括号用于对优先级表达式进行分组。(prio)

prio ::= ...
    | 优先级的加法。通常仅用于施加偏移，例如 `default + 1`。prio + prio

prio ::= ...
    | 优先级的减法。通常仅用于施加偏移，例如 `default - 1`。prio - prio

10.2.4. 默认实例🔗

default_instance 属性指定了在没有足够的信息来选择实例时，应将其作为后备方案使用。如果没有指定优先级，则使用默认优先级 default。

属性default_instance 属性

attr ::= ...
    | default_instance prio?

默认实例

当缺少其他类型信息时，自然数字面量将通过 OfNat Nat 的默认实例来选择被解释为 Nat 类型。它在 Lean 标准库中被声明，其优先级为 100。给定偶数的如下表示方式，其中偶数由其一半来表示：

structure Even where
  half : Nat

以下实例允许将数字字面量用于较小的 Even 值（对类型类实例搜索深度的限制阻碍了它们被用于任意大的字面量）：

instance ofNatEven0 : OfNat Even 0 where
  ofNat := ⟨0⟩

instance ofNatEvenPlusTwo [OfNat Even n] : OfNat Even (n + 2) where
  ofNat := ⟨(OfNat.ofNat n : Even).half + 1⟩

{ half := 0 }#eval (0 : Even)
{ half := 17 }#eval (34 : Even)
{ half := 127 }#eval (254 : Even)

{ half := 0 }

{ half := 17 }

{ half := 127 }

将它们指定为优先级大于等于 100 的默认实例，会导致在没有类型提示时它们被使用而不是 Nat：

attribute [default_instance 100] ofNatEven0
attribute [default_instance 100] ofNatEvenPlusTwo

{ half := 0 }#eval 0
{ half := 17 }#eval 34

{ half := 0 }

{ half := 17 }

非偶数数字仍使用 OfNat Nat 实例：

5#eval 5

在线查看 ↪

10.2.5. `instance` 属性🔗

instance 属性将一个名称声明为指定优先级的实例。与其他属性一样，instance 可以全局应用，或者局部应用，或者仅当打开了当前命名空间时应用。 Lean.Parser.Command.declaration : commandinstance 声明就是一种会自动应用 instance 属性的定义形式。

属性instance 属性

将其应用的定义声明为一个实例。如果没有提供优先级，则使用默认优先级 default。

attr ::= ...
    | instance prio?

10.2. 实例声明🔗

10.2.1. 递归实例🔗

10.2.2. class inductive 的实例🔗

10.2.3. 实例优先级🔗

10.2.4. 默认实例🔗

10.2.5. instance 属性🔗

10.2.2. `class inductive` 的实例🔗

10.2.5. `instance` 属性🔗