Lean 语言参考

20.14. 总和类型🔗

Sum types 表示两种类型之间的选择：和的元素是其他类型之一的元素，并与它来自哪种类型的指示配对。 求和也称为不相交联合、可区分联合或标记联合。 sum 的构造函数也称为 injections；从数学上讲，它们可以被视为从每个被加数到总和的单射函数。

sum 类型有两种类型：

  • Sum 是所有 Type 宇宙 上的 多态，并且绝不是 命题。

  • PSum 允许加数是命题或类型。与 Or 不同，两个命题的 PSum 仍然是一个类型，非命题代码可以检查使用哪个注入来构造给定值。

手动编写的 Lean 代码几乎总是仅使用 Sum，而 PSum 则用作证明自动化实现的一部分。 这是因为它施加了 宇宙层级 统一无法解决的有问题的约束。 特别是，该类型位于宇宙 Sort (max 1 u v) 中，这可能会导致 宇宙层级 统一出现问题，因为方程 max 1 u v = ?u + 1 在级别算术中无解。 PSum 通常仅用于构造任意类型之和的自动化。

🔗inductive type
Sum.{u, v} (α : Type u) (β : Type v) : Type (max u v)
Sum.{u, v} (α : Type u) (β : Type v) :
  Type (max u v)

The disjoint union of types α and β, ordinarily written α ⊕ β.

An element of α ⊕ β is either an a : α wrapped in Sum.inl or a b : β wrapped in Sum.inr. α ⊕ β is not equivalent to the set-theoretic union of α and β because its values include an indication of which of the two types was chosen. The union of a singleton set with itself contains one element, while Unit ⊕ Unit contains distinct values inl () and inr ().

Constructors

Sum.inl.{u, v} {α : Type u} {β : Type v} (val : α) : α ⊕ β

Left injection into the sum type α ⊕ β.

Sum.inr.{u, v} {α : Type u} {β : Type v} (val : β) : α ⊕ β

Right injection into the sum type α ⊕ β.

🔗inductive type
PSum.{u, v} (α : Sort u) (β : Sort v) : Sort (max (max 1 u) v)
PSum.{u, v} (α : Sort u) (β : Sort v) :
  Sort (max (max 1 u) v)

The disjoint union of arbitrary sorts α β, or α ⊕' β.

It differs from α ⊕ β in that it allows α and β to have arbitrary sorts Sort u and Sort v, instead of restricting them to Type u and Type v. This means that it can be used in situations where one side is a proposition, like True ⊕' Nat. However, the resulting universe level constraints are often more difficult to solve than those that result from Sum.

Constructors

PSum.inl.{u, v} {α : Sort u} {β : Sort v} (val : α) : α ⊕' β

Left injection into the sum type α ⊕' β.

PSum.inr.{u, v} {α : Sort u} {β : Sort v} (val : β) : α ⊕' β

Right injection into the sum type α ⊕' β.

20.14.1. 句法🔗

名称 Sum 和 PSum 很少明确写入。 大多数代码使用相应的中缀运算符。

syntaxSum Types
term ::= ...
    | The disjoint union of types `α` and `β`, ordinarily written `α ⊕ β`.

An element of `α ⊕ β` is either an `a : α` wrapped in `Sum.inl` or a `b : β` wrapped in `Sum.inr`.
`α ⊕ β` is not equivalent to the set-theoretic union of `α` and `β` because its values include an
indication of which of the two types was chosen. The union of a singleton set with itself contains
one element, while `Unit ⊕ Unit` contains distinct values `inl ()` and `inr ()`.
term ⊕ term

α ⊕ β 是 Sum α β 的表示法。

syntaxPotentially-Propositional Sum Types
term ::= ...
    | The disjoint union of arbitrary sorts `α` `β`, or `α ⊕' β`.

It differs from `α ⊕ β` in that it allows `α` and `β` to have arbitrary sorts `Sort u` and `Sort v`,
instead of restricting them to `Type u` and `Type v`. This means that it can be used in situations
where one side is a proposition, like `True ⊕' Nat`. However, the resulting universe level
constraints are often more difficult to solve than those that result from `Sum`.
term ⊕' term

α ⊕' β 是 PSum α β 的表示法。

20.14.2. API 参考🔗

Sum 类型主要用于 模式匹配，而不是来自 API 的显式函数调用。 因此，它们的主要 API 是构造函数 inl 和 inr。

20.14.2.1. 案例区分🔗

🔗def
Sum.isLeft.{u_1, u_2} {α : Type u_1} {β : Type u_2} : α ⊕ β → Bool
Sum.isLeft.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} : α ⊕ β → Bool

Checks whether a sum is the left injection inl.

🔗def
Sum.isRight.{u_1, u_2} {α : Type u_1} {β : Type u_2} : α ⊕ β → Bool
Sum.isRight.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} : α ⊕ β → Bool

Checks whether a sum is the right injection inr.

20.14.2.2. 提取值🔗

🔗def
Sum.elim.{u_1, u_2, u_3} {α : Type u_1} {β : Type u_2} {γ : Sort u_3}
  (f : α → γ) (g : β → γ) : α ⊕ β → γ
Sum.elim.{u_1, u_2, u_3} {α : Type u_1}
  {β : Type u_2} {γ : Sort u_3}
  (f : α → γ) (g : β → γ) : α ⊕ β → γ

Case analysis for sums that applies the appropriate function f or g after checking which constructor is present.

🔗def
Sum.getLeft.{u_1, u_2} {α : Type u_1} {β : Type u_2} (ab : α ⊕ β) :
  ab.isLeft = true → α
Sum.getLeft.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} (ab : α ⊕ β) :
  ab.isLeft = true → α

Retrieves the contents from a sum known to be inl.

🔗def
Sum.getLeft?.{u_1, u_2} {α : Type u_1} {β : Type u_2} : α ⊕ β → Option α
Sum.getLeft?.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} : α ⊕ β → Option α

Checks whether a sum is the left injection inl and, if so, retrieves its contents.

🔗def
Sum.getRight.{u_1, u_2} {α : Type u_1} {β : Type u_2} (ab : α ⊕ β) :
  ab.isRight = true → β
Sum.getRight.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} (ab : α ⊕ β) :
  ab.isRight = true → β

Retrieves the contents from a sum known to be inr.

🔗def
Sum.getRight?.{u_1, u_2} {α : Type u_1} {β : Type u_2} :
  α ⊕ β → Option β
Sum.getRight?.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} : α ⊕ β → Option β

Checks whether a sum is the right injection inr and, if so, retrieves its contents.

20.14.2.3. 转换🔗

🔗def
Sum.map.{u_1, u_2, u_3, u_4} {α : Type u_1} {α' : Type u_2}
  {β : Type u_3} {β' : Type u_4} (f : α → α') (g : β → β') :
  α ⊕ β → α' ⊕ β'
Sum.map.{u_1, u_2, u_3, u_4}
  {α : Type u_1} {α' : Type u_2}
  {β : Type u_3} {β' : Type u_4}
  (f : α → α') (g : β → β') :
  α ⊕ β → α' ⊕ β'

Transforms a sum according to functions on each type.

This function maps α ⊕ β to α' ⊕ β', sending α to α' and β to β'.

🔗def
Sum.swap.{u_1, u_2} {α : Type u_1} {β : Type u_2} : α ⊕ β → β ⊕ α
Sum.swap.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} : α ⊕ β → β ⊕ α

Swaps the factors of a sum type.

The constructor Sum.inl is replaced with Sum.inr, and vice versa.

20.14.2.4. 有人居住🔗

Sum 和 PSum 的 Inhabited 定义未注册为实例。 这是因为有两种不同的方法来构造默认值（通过 inl 或 inr），并且实例综合可能会导致任一选择。 结果可能是两个相同书写的术语的精化不同并且不 定义等价。

两种类型都有 Nonempty 实例，对于 证明无关性，选择 inl 或 inr 并不重要。 这足以启用 partial 功能。 对于需要 Inhabited 实例的情况（例如使用 panic! 的程序），可以通过使用 Lean.Parser.Term.have : term`have` is used to declare local hypotheses and opaque local definitions. It has the same syntax as `let`, and it is equivalent to `let +nondep`, creating a *nondependent* let expression. have 或 Lean.Parser.Term.let : term`let` is used to declare a local definition. Example: ``` let x := 1 let y := x + 1 x + y ``` Since functions are first class citizens in Lean, you can use `let` to declare local functions too. ``` let double := fun x => 2*x double (double 3) ``` For recursive definitions, you should use `let rec`. You can also perform pattern matching using `let`. For example, assume `p` has type `Nat × Nat`, then you can write ``` let (x, y) := p x + y ``` The *anaphoric let* `let := v` defines a variable called `this`. let 将实例添加到本地上下文来显式使用该实例。

Inhabited Sum Types

在 Lean 的逻辑中，Lean.Parser.Term.panic : term`panic! msg` formally evaluates to `@Inhabited.default α` if the expected type `α` implements `Inhabited`. At runtime, `msg` and the file position are printed to stderr unless the C function `lean_set_panic_messages(false)` has been executed before. If the C function `lean_set_exit_on_panic(true)` has been executed before, the process is then aborted. panic! 相当于其类型的 Inhabited 实例中指定的默认值。 这意味着该类型必须具有这样的实例 - Nonempty 实例与选择公理相结合将使程序不可计算。

产品有正确的实例：

example : Nat × String := panic! "Can't find it"

默认情况下，总和不会：

example : Nat ⊕ String := failed to synthesize instance of type class Inhabited (Nat ⊕ String) Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.panic! "Can't find it" 
failed to synthesize instance of type class
  Inhabited (Nat ⊕ String)

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

可以使用 Lean.Parser.Term.have : term`have` is used to declare local hypotheses and opaque local definitions. It has the same syntax as `let`, and it is equivalent to `let +nondep`, creating a *nondependent* let expression. have 使所需实例可用于实例合成：

example : Nat ⊕ String := have : Inhabited (Nat ⊕ String) := Sum.inhabitedLeft panic! "Can't find it"
Live ↪
🔗def
Sum.inhabitedLeft.{u, v} {α : Type u} {β : Type v} [Inhabited α] :
  Inhabited (α ⊕ β)
Sum.inhabitedLeft.{u, v} {α : Type u}
  {β : Type v} [Inhabited α] :
  Inhabited (α ⊕ β)

If the left type in a sum is inhabited then the sum is inhabited.

This is not an instance to avoid non-canonical instances when both the left and right types are inhabited.

🔗def
Sum.inhabitedRight.{u, v} {α : Type u} {β : Type v} [Inhabited β] :
  Inhabited (α ⊕ β)
Sum.inhabitedRight.{u, v} {α : Type u}
  {β : Type v} [Inhabited β] :
  Inhabited (α ⊕ β)

If the right type in a sum is inhabited then the sum is inhabited.

This is not an instance to avoid non-canonical instances when both the left and right types are inhabited.

🔗def
PSum.inhabitedLeft.{u_1, u_2} {α : Sort u_1} {β : Sort u_2}
  [Inhabited α] : Inhabited (α ⊕' β)
PSum.inhabitedLeft.{u_1, u_2}
  {α : Sort u_1} {β : Sort u_2}
  [Inhabited α] : Inhabited (α ⊕' β)

If the left type in a sum is inhabited then the sum is inhabited.

This is not an instance to avoid non-canonical instances when both the left and right types are inhabited.

🔗def
PSum.inhabitedRight.{u_1, u_2} {α : Sort u_1} {β : Sort u_2}
  [Inhabited β] : Inhabited (α ⊕' β)
PSum.inhabitedRight.{u_1, u_2}
  {α : Sort u_1} {β : Sort u_2}
  [Inhabited β] : Inhabited (α ⊕' β)

If the right type in a sum is inhabited then the sum is inhabited.

This is not an instance to avoid non-canonical instances when both the left and right types are inhabited.