10.2. 实例声明🔗

实例声明的语法几乎与定义的语法相同。唯一的语法差异是关键字 Lean.Parser.Command.declaration : commanddef 替换为 Lean.Parser.Command.declaration : commandinstance 并且名称是可选的：

syntaxInstance Declarations

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

instance ::= ...
    | `attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`. instance ((priority := prio))? `declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names declId? `declSig` matches the signature of a declaration with required type: a list of binders and then `: type` declSig where
        structInstField*

但是，类型类是归纳类型，因此可以使用具有适当类型的任何表达式来构造实例：

instance ::= ...
    | `attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`. instance ((priority := prio))? `declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names declId? `declSig` matches the signature of a declaration with required type: a list of binders and then `: type` declSig :=
        termTermination hints are `termination_by` and `decreasing_by`, in that order.

实例也可以通过案例来定义；但是，此功能很少在 Decidable 实例之外使用：

instance ::= ...
    | `attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`. instance ((priority := prio))? `declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names declId? `declSig` matches the signature of a declaration with required type: a list of binders and then `: type` declSig
        (| term => term)*Termination hints are `termination_by` and `decreasing_by`, in that order.

使用显式术语定义的实例通常包含包装方法实现的匿名构造函数 (Lean.Parser.Term.anonymousCtor : termThe *anonymous constructor* `⟨e, ...⟩` is equivalent to `c e ...` if the expected type is an inductive type with a single constructor `c`. If more terms are given than `c` has parameters, the remaining arguments are turned into a new anonymous constructor application. For example, `⟨a, b, c⟩ : α × (β × γ)` is equivalent to `⟨a, ⟨b, c⟩⟩`.⟨...⟩) 或定义等价类型上的 inferInstanceAs 调用。

实例的精化几乎与普通定义的精化相同，但下面记录的注意事项除外。如果未提供名称，则会自动创建一个名称。可以直接引用这个生成的名称，但是用于生成名称的算法过去已经发生变化，并且将来可能会发生变化。最好明确命名将直接引用的实例。在精化之后，新实例被注册为实例搜索的候选者。将属性 instance 添加到名称可用于将任何其他定义的名称标记为候选名称。

Instance Name Generation

遵循这些声明：

structure NatWrapper where
  val : Nat

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

名称 instBEqNatWrapper 指的是新实例。

Live ↪

Variations in Instance Definitions

给定这种结构类型：

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⟩

除了在环境中引入不同的名称之外，以下内容也是等效的：

Definition `instBeqNatWrapper` of class type must be marked with `@[reducible]` or `@[implicit_reducible]`@[instance `instBeqNatWrapper` must be marked with `@[reducible]` or `@[implicit_reducible]`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⟩

Live ↪

10.2.1. 递归实例🔗

Lean.Parser.Command.declaration : commandwhere 结构定义语法中定义的函数不是递归的。因为实例声明是结构定义的一个版本，所以默认情况下类型类方法也不是递归的。然而，递归归纳类型的实例很常见。有一个标准习惯用法可以解决此限制：独立于实例定义递归函数，然后在实例定义中引用它。按照约定，这些递归函数具有相应方法的名称，但在类型的命名空间中定义。

Instances are not recursive

鉴于 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⟩

Live ↪

此外，实例在其自己的定义期间不可用于实例合成。它们在定义后首先被标记为可用于实例合成。嵌套归纳类型（其中类型的递归出现作为某个其他归纳类型的参数）可能需要一个可用的实例，甚至可以编写递归函数。解决此限制的标准习惯用法是在递归定义的函数中创建本地实例，其中包含对正在定义的函数的引用，利用实例合成可以使用本地上下文中具有正确类型的每个绑定这一事实。

Instances for nested types

在 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.

为了解决这个问题，本地 BEq NatRoseTree 实例可能是 let 绑定的：

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

在实例合成期间，对子级使用数组相等来查找 let 绑定实例。

Live ↪

10.2.2. `class inductive` 的实例🔗

许多实例具有函数类型：任何本身递归调用实例搜索的实例都是一个函数，任何具有隐式参数的实例也是如此。虽然大多数实例仅从其自己的实例参数投影方法实现，但类归纳类型的实例通常会对其一个或多个参数进行模式匹配，从而允许实例选择适当的构造函数。这是使用普通的 Lean 函数语法完成的。与其他实例一样，所讨论的函数不可用于其自身定义中的实例综合。

An instance for a sum class

由于 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

Live ↪

A recursive instance for a sum class

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

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

在以下定义 DecidableEq 实例的尝试中，在详细说明内部 termIfThenElse : term`if c then t else e` is notation for `ite c t e`, "if-then-else", which decides to return `t` or `e` depending on whether `c` is true or false. The explicit argument `c : Prop` does not have any actual computational content, but there is an additional `[Decidable c]` argument synthesized by typeclass inference which actually determines how to evaluate `c` to true or false. Write `if h : c then t else e` instead for a "dependent if-then-else" `dite`, which allows `t`/`e` to use the fact that `c` is true/false.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

Live ↪

10.2.3. 实例优先级🔗

实例可以被分配priorities。实例合成时优先选择优先级高的实例；实例综合的详细信息请参见实例综合部分。

syntaxInstance Priorities

优先级可以是数字：

prio ::=
    num

如果未指定优先级，则使用与 1000 对应的默认优先级：

prio ::= ...
    | The default priority `default = 1000`, which is used when no priority is set. default

当数值太细粒度时，可以使用三个命名优先级，分别对应于 100、500 和 10000。 prioMid : prioThe standardized "medium" priority `mid = 500`. This is lower than `default`, and higher than `low`.mid 优先级低于 prioDefault : prioThe default priority `default = 1000`, which is used when no priority is set. default。

prio ::= ...
    | The standardized "low" priority `low = 100`, for things that should be lower than default priority. low

prio ::= ...
    | The standardized "medium" priority `mid = 500`. This is lower than `default`, and higher than `low`.
mid

prio ::= ...
    | The standardized "high" priority `high = 10000`, for things that should be higher than default priority. high

最后，优先级可以进行加减操作，因此default + 2是有效的优先级，对应于1002：

prio ::= ...
    | Parentheses are used for grouping priority expressions. (prio)

prio ::= ...
    | Addition of priorities. This is normally used only for offsetting, e.g. `default + 1`. prio + prio

prio ::= ...
    | Subtraction of priorities. This is normally used only for offsetting, e.g. `default - 1`. prio - prio

10.2.4. 默认实例🔗

default_instance 属性指定实例应在没有足够信息来选择它的情况下用作后备。如果未指定优先级，则使用默认优先级 default。

attributeThe default_instance Attribute

attr ::= ...
    | default_instance prio?

Default Instances

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

Live ↪

10.2.5. 实例属性🔗

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

attributeThe instance Attribute

声明它所应用到的定义是一个实例。如果未提供优先级，则使用默认优先级 default。

attr ::= ...
    | instance prio?

10.2. 实例声明🔗

10.2.1. 递归实例🔗

10.2.2. class inductive 的实例🔗

10.2.3. 实例优先级🔗

10.2.4. 默认实例🔗

10.2.5. 实例属性🔗

10.2.2. `class inductive` 的实例🔗