20.13. 元组🔗

Lean 标准库包含多种类似元组的类型。在实践中，它们有四个方面的差异：

第一投影是类型还是命题
第二投影是类型还是命题
第二投影的类型是否依赖于第一投影的值
整个类型本身是命题还是类型

类型	第一投影	第二投影	依值？	宇宙
`Prod`	`Type u`	`Type v`	❌️	`Type (max u v)`
`And`	`Prop`	`Prop`	❌️	`Prop`
`Sigma`	`Type u`	`Type v`	✔	`Type (max u v)`
`Subtype`	`Type u`	`Prop`	✔	`Type u`
`Exists`	`Type u`	`Prop`	✔	`Prop`

该表中的某些潜在行在库里并不存在：

不存在“第一投影是命题”的依值有序对，因为证明无关性会让它失去意义。
不存在把类型与命题组合起来的非依值有序对，因为这种情况在实践中很少见：把数据与无关的证明放在一起并不常见。

这些差异会带来非常不同的使用场景。 Prod 及其变体 PProd 与 MProd 只是把数据放在一起——它们是积。由于第二投影依值，Sigma 具有和的特征：对于第一投影类型中的每个元素，第二投影都可能对应不同的类型。 Subtype 选出某个类型中满足给定谓词的值。尽管它在语法上像一个有序对，但在实践中它被当作真正的子集。 And 是逻辑联结词，而 Exists 是量词。本章记录的是这些类似元组的有序对，也就是 Prod 与 Sigma。

20.13.1. 有序对🔗

类型 α × β 是 Prod α β 的一种记法，它包含有序对：第一个元素属于 α，第二个元素属于 β。这些有序对写在圆括号中，并以逗号分隔。更大的元组表示为嵌套元组，因此 α × β × γ 等价于 α × (β × γ)，而 (x, y, z) 等价于 (x, (y, z))。

语法积类型

term ::= ...
    | term × term

积 Prod α β 写作 α × β。

语法有序对

term ::= ...
    | ([anonymous]term, term)

结构体

Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)
Prod.{u, v} (α : Type u) (β : Type v) :
  Type (max u v)

产品类型，通常写作α × β。产品类型也称为对或元组类型。这种类型的元素是成对的，其中第一个元素是 α，第二个元素是 β。

产品嵌套在右侧，因此 (x, y, z) : α × β × γ 相当于 (x, (y, z)) : α × (β × γ)。

标识符中的符号约定：

标识符中 × 的建议拼写为 Prod。

构造子

Prod.mk.{u, v}

构造一个有序对。通常写作 (x, y)，而不是 Prod.mk x y。

标识符中的记法约定：

标识符中 (a, b) 的推荐拼写是 mk。

字段

fst : α

有序对的第一个元素。

snd : β

有序对的第二个元素。

还存在变体 α ×' β（它是 PProd α β 的记法）以及 MProd，它们在宇宙层级方面有所不同：与 PSum 类似，PProd 允许 α 或 β 之一是命题，而 MProd 要求二者都是位于同一宇宙层级的类型。一般来说，PProd 主要用于证明自动化和精译器的实现，因为它往往会引发无法解决的宇宙层级合一问题。另一方面，MProd 在某些高级用例中可以简化宇宙层级问题。

语法任意 Sort 的积

term ::= ...
    | term ×' term

积 PProd α β（其中两个参数都可以是命题）写作 α × β。

结构体

PProd.{u, v} (α : Sort u) (β : Sort v) : Sort (max (max 1 u) v)
PProd.{u, v} (α : Sort u) (β : Sort v) :
  Sort (max (max 1 u) v)

一种产品类型，其中类型可以是命题，通常写作α ×' β。

这种类型主要在内部使用，并作为证明自动化的实现细节。它在手写代码中很少有用。

标识符中的符号约定：

标识符中 ×' 的建议拼写为 PProd。

构造子

PProd.mk.{u, v}

字段

fst : α

有序对的第一个元素。

snd : β

有序对的第二个元素。

结构体

MProd.{u} (α β : Type u) : Type u
MProd.{u} (α β : Type u) : Type u

α 和 β 位于同一 Universe 的产品类型。

它被称为 MProd 是因为它是 universe-monomorphic 产品类型。

构造子

MProd.mk.{u}

字段

fst : α

有序对的第一个元素。

snd : β

有序对的第二个元素。

20.13.1.1. 接口参考🔗

作为单纯的有序对，Prod 的主要 API 由模式匹配以及第一、第二投影 Prod.fst 和 Prod.snd 提供。

20.13.1.1.1. 变换🔗

定义

Prod.map.{u₁, u₂, v₁, v₂} {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁}
  {β₂ : Type v₂} (f : α₁ → α₂) (g : β₁ → β₂) : α₁ × β₁ → α₂ × β₂
Prod.map.{u₁, u₂, v₁, v₂} {α₁ : Type u₁}
  {α₂ : Type u₂} {β₁ : Type v₁}
  {β₂ : Type v₂} (f : α₁ → α₂)
  (g : β₁ → β₂) : α₁ × β₁ → α₂ × β₂

通过对两个元素应用函数来转换一对。

示例：

(1, 2).map (· + 1) (· * 3) = (2, 6)
(1, 2).map toString (· * 3) = ("1", 6)

定义

Prod.swap.{u_1, u_2} {α : Type u_1} {β : Type u_2} : α × β → β × α
Prod.swap.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} : α × β → β × α

交换一对中的元素。

示例：

(1, 2).swap = (2, 1)
("orange", -87).swap = (-87, "orange")

20.13.1.1.2. 自然数范围🔗

定义

Prod.allI (i : Nat × Nat)
  (f : (j : Nat) → i.fst ≤ j → j < i.snd → Bool) : Bool
Prod.allI (i : Nat × Nat)
  (f :
    (j : Nat) →
      i.fst ≤ j → j < i.snd → Bool) :
  Bool

检查谓词是否适用于范围内的所有自然数。

具体而言，(start, stop).allI f 返回真，如果 f 对从 start（包含）到 stop（不包含）的所有自然数为真。

示例：

(5, 8).allI (fun j _ _ => j < 10) = (5 < 10) && (6 < 10) && (7 < 10)
(5, 8).allI (fun j _ _ => j % 2 = 0) = false
(6, 7).allI (fun j _ _ => j % 2 = 0) = true

定义

Prod.anyI (i : Nat × Nat)
  (f : (j : Nat) → i.fst ≤ j → j < i.snd → Bool) : Bool
Prod.anyI (i : Nat × Nat)
  (f :
    (j : Nat) →
      i.fst ≤ j → j < i.snd → Bool) :
  Bool

检查谓词是否适用于范围内的任何自然数。

具体而言，(start, stop).allI f 返回真，如果 f 对从 start（包含）到 stop（不包含）的任一自然数为真。

示例：

(5, 8).anyI (fun j _ _ => j == 6) = (5 == 6) || (6 == 6) || (7 == 6)
(5, 8).anyI (fun j _ _ => j % 2 = 0) = true
(6, 6).anyI (fun j _ _ => j % 2 = 0) = false

定义

Prod.foldI.{u} {α : Type u} (i : Nat × Nat)
  (f : (j : Nat) → i.fst ≤ j → j < i.snd → α → α) (init : α) : α
Prod.foldI.{u} {α : Type u}
  (i : Nat × Nat)
  (f :
    (j : Nat) →
      i.fst ≤ j → j < i.snd → α → α)
  (init : α) : α

将初始值与某个范围中的每个自然数按升序组合。

特别是，(start, stop).foldI f init 按升序将 f 应用于从 start（含）到 stop（不含）的所有数字：

示例：

(5, 8).foldI (fun j _ _ xs => xs.push j) #[] = (#[] |>.push 5 |>.push 6 |>.push 7)
(5, 8).foldI (fun j _ _ xs => xs.push j) #[] = #[5, 6, 7]
(5, 8).foldI (fun j _ _ xs => toString j :: xs) [] = ["7", "6", "5"]

20.13.1.1.3. 排序🔗

定义

Prod.lexLt.{u_1, u_2} {α : Type u_1} {β : Type u_2} [LT α] [LT β]
  (s t : α × β) : Prop
Prod.lexLt.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} [LT α] [LT β]
  (s t : α × β) : Prop

产品的字典顺序。

如果两个对的第一个元素是有序的，或者如果它们的第一个元素相等并且它们的第二个元素是有序的，则两个对按字典顺序排序。

20.13.2. 依值有序对🔗

依值有序对 也称为 依值和 或 Σ-类型，是这样一种有序对：第二个项的类型可以依赖于第一个项的值。它与存在量词以及 Subtype 关系密切。不同于存在量化语句，依值有序对位于 Type 宇宙中，是与计算相关的数据。不同于子类型，这里的第二个项也同样是与计算相关的数据。与普通有序对一样，依值有序对也可以嵌套；这种嵌套是右结合的。

语法依值有序对类型

term ::= ...
    | (ident : term) × term

term ::= ...
    | Σ ident ident* (: term)?, term

term ::= ...
    | Σ (ident ident* : term), term

依值有序对类型会绑定一个或多个变量，最终项中可以使用这些变量。若只绑定一个变量，则它的类型就是有序对第一个元素的类型，而最终项则是第二个元素的类型。若绑定多个变量，则类型会按右结合方式嵌套。标识符也可以写成 _。带括号的写法允许多个被绑定变量具有不同类型，而不带括号的写法要求它们都具有相同类型。

嵌套的依值有序对类型

类型

Σ n k : Nat, Fin (n * k)

等价于

Σ n : Nat, Σ k : Nat, Fin (n * k)

以及

(n : Nat) × (k : Nat) × Fin (n * k)

类型

Σ (n k : Nat) (i : Fin (n * k)) , Fin i.val

等价于

Σ (n : Nat), Σ (k : Nat), Σ (i : Fin (n * k)) , Fin i.val

以及

(n : Nat) × (k : Nat) × (i : Fin (n * k)) × Fin i.val

这两种标注风格不能在同一个 «termΣ_,_» : termΣ 类型中混用：

Σ n kunexpected token '('; expected ',' (i : Fin (n * k)) , Fin i.val

<example>:1:5-1:7: unexpected token '('; expected ','

依值有序对通常有两种用法：

它们可用于把某个具体的类型索引与该索引族中的值“打包”在一起，适用于事先不知道索引值的情况。类型 Σ n, Fin n 就是一对值：一个自然数，以及另一个严格小于它的数。这是依值有序对最常见的用法。
第一个元素可以看作一个“标签”，用于在不同类型之间选择第二个项的类型。这类似于和类型中选择某个构造子时，会同时决定该构造子参数的类型。例如，类型
Σ (b : Bool), if b then Unit else α
等价于 Option α；其中 none 对应 ⟨true, ()⟩，而 some x 对应 ⟨false, x⟩。这种用法并不常见，因为通常直接定义一个专用的归纳类型会更容易。

结构体

Sigma.{u, v} {α : Type u} (β : α → Type v) : Type (max u v)
Sigma.{u, v} {α : Type u}
  (β : α → Type v) : Type (max u v)

依赖对，其中第二个元素的类型取决于第一个元素的值。类型 Sigma β 通常写作 Σ a : α, β a 或 (a : α) × β a。

尽管其值是对，但 Sigma 有时也称为“依赖求和类型”，因为它是索引求和的类型级别版本。

构造子

Sigma.mk.{u, v}

构造依值有序对。

在类型未知的上下文中使用此构造子时，通常需要类型标注来确定 β，因为两个值之间所需的关系通常无法自动确定。

字段

fst : α

依值有序对的第一个分量。

snd : β self.fst

依值有序对的第二个分量，其类型依赖于第一个分量。

带数据的依值有序对

类型 Vector 会把一个已知长度与数组关联起来，它可以与该长度本身一起放入依值有序对中。尽管从逻辑上说，这与直接使用 Array 等价，但为了弥补 API 之间的衔接空缺，这种构造有时是必要的。

def getNLinesRev : (n : Nat) → IO (Vector String n)
  | 0 => pure #v[]
  | n + 1 => do
    let xs ← getNLinesRev n
    return xs.push (← (← IO.getStdin).getLine)

def getNLines (n : Nat) : IO (Vector String n) := do
  return (← getNLinesRev n).reverse

partial def getValues : IO (Σ n, Vector String n) := do
  let stdin ← IO.getStdin

  IO.println "How many lines to read?"
  let howMany ← stdin.getLine

  if let some howMany := howMany.trimAscii.copy.toNat? then
    return ⟨howMany, (← getNLines howMany)⟩
  else
    IO.eprintln "Please enter a number."
    getValues

def main : IO Unit := do
  let values ← getValues
  IO.println s!"Got {values.fst} values. They are:"
  for x in values.snd do
    IO.println x.trimAscii

向该程序提供如下标准输入时：

                      stdin4ApplesQuincePlumsRaspberries

输出为：

                      stdoutHow many lines to read?Got 4 values. They are:RaspberriesPlumsQuinceApples

把依值有序对当作和类型

Sigma 可用于实现和类型。第一投影中的 Bool 指示 Sum' 的第二投影值来自哪个类型。

def Sum' (α : Type) (β : Type) : Type :=
  Σ (b : Bool),
    match b with
    | true => α
    | false => β

两个注入构造子都会把一个标签（即 Bool）与指定类型的值配对。为它们加上 match_pattern 标注后，它们既可用于普通项，也可用于模式。

variable {α β : Type}

@[match_pattern]
def Sum'.inl (x : α) : Sum' α β := ⟨true, x⟩

@[match_pattern]
def Sum'.inr (x : β) : Sum' α β := ⟨false, x⟩

def Sum'.swap : Sum' α β → Sum' β α
  | .inl x => .inr x
  | .inr y => .inl y

在线查看 ↪

正如 Prod 有允许命题与类型一并出现的变体 PProd 一样，PSigma 也允许其投影是命题。它与 PProd 有相同的缺点：更容易导致宇宙层级合一失败。不过，在实现自定义证明自动化，或某些罕见的高级用例中，PSigma 可能是必要的。

语法全多态依值有序对类型

term ::= ...
    | Σ' ident ident* (: term)? , term

term ::= ...
    | Σ' (ident ident* : term), term

Σ' 的嵌套规则以及其绑定结构规则，都与 «termΣ_,_» : termΣ 相同。

结构体

PSigma.{u, v} {α : Sort u} (β : α → Sort v) : Sort (max (max 1 u) v)
PSigma.{u, v} {α : Sort u}
  (β : α → Sort v) :
  Sort (max (max 1 u) v)

完全宇宙多态依赖对，其中第二个元素的类型取决于第一个元素的值，并且两种类型都允许是命题。类型 PSigma β 通常写作 Σ' a : α, β a 或 (a : α) ×' β a。

在实践中，这种通用性导致宇宙级约束难以解决，因此 PSigma 很少在手动编写的代码中使用。它通常仅用于构造任意类型对的自动化。

要将值与谓词对其成立的证明配对，请使用 Subtype。要证明存在满足谓词的值，请使用 Exists。由于证明无关，以命题作为其第一个组成部分的依赖对通常没有用处：依赖于特定证明是没有意义的，因为无论如何所有证明都是相等的。

构造子

PSigma.mk.{u, v}

构造完全宇宙多态的依值有序对。

字段

fst : α

依值有序对的第一个分量。

snd : β self.fst

依值有序对的第二个分量，其类型依赖于第一个分量。

20.1.	自然数
20.2.	整数
20.3.	有限自然数
20.4.	定精度整数
20.5.	位向量
20.6.	浮点数
20.7.	字符
20.8.	字符串
20.9.	单元类型
20.10.	空类型
20.11.	布尔值
20.12.	可选值
20.13.	元组
20.14.	和类型
20.15.	链表
20.16.	数组
20.17.	字节数组
20.18.	范围
20.19.	映射与集合
20.20.	子类型
20.21.	惰性计算