Lean 标准库包含各种类似元组的类型。 在实践中，它们有四个方面的不同：
第一个投影是类型还是命题
第二个投影是类型还是命题
第二个投影的类型是否取决于第一个投影的值
类型作为一个整体是命题还是类型
Type | 第一个投影 | 第二次投影 | 依赖？ | 宇宙 |
|---|---|---|---|---|
|
| ❌️ |
| |
|
| ❌️ |
| |
|
| ✔ |
| |
|
| ✔ |
| |
|
| ✔ |
|
该表中的一些潜在行在库中不存在：
不存在依赖对，其中第一个投影是命题，因为 证明无关性 使这变得毫无意义。
不存在将类型与命题组合在一起的非依赖对，因为这种情况在实践中很少见：将数据与不相关证明进行分组并不常见。
这些差异导致了非常不同的用例。
Prod 及其变体 PProd 和 MProd 只是将数据组合在一起 - 它们是产品。
因为它的第二个投影是相关的，所以 Sigma 具有求和的特征：对于第一个投影类型的每个元素，第二个投影中可能有不同的类型。
Subtype 选择满足谓词的类型的值。
尽管它在语法上类似于一对，但实际上它被视为实际的子集。
And 是逻辑连接词，Exists 是量词。
本章记录了类似元组的对，即 Prod 和 Sigma。
类型 α × β 是 Prod α β 的 符号，包含有序对，其中第一项是 α，第二项是 β。
这些对写在括号中，并用逗号分隔。
较大的元组表示为嵌套元组，因此 α × β × γ 相当于 α × (β × γ)，(x, y, z) 相当于 (x, (y, z))。
term ::= ...
| The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.
Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.
Conventions for notations in identifiers:
* The recommended spelling of `×` in identifiers is `Prod`.
产品 Prod α β 写作 α × β。
term ::= ...
| Tuple notation; `()` is short for `Unit.unit`, `(a, b, c)` for `Prod.mk a (Prod.mk b c)`, etc.
Conventions for notations in identifiers:
* The recommended spelling of `(a, b)` in identifiers is `mk`.
The product type, usually written α × β. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an α and the second element is a
β.
Products nest to the right, so (x, y, z) : α × β × γ is equivalent to (x, (y, z)) : α × (β × γ).
Conventions for notations in identifiers:
The recommended spelling of × in identifiers is Prod.
Prod.mk.{u, v}
Constructs a pair. This is usually written (x, y) instead of Prod.mk x y.
Conventions for notations in identifiers:
The recommended spelling of (a, b) in identifiers is mk.
fst : α
The first element of a pair.
snd : β
The second element of a pair.
还有 α ×' β（PProd α β 的表示法）和 MProd 的变体，它们在 universe 级别方面有所不同：与 PSum 一样，PProd 允许 α 或β 是一个命题，而 MProd 要求两者的类型相同 宇宙层级。
一般来说，PProd主要用于证明自动化和精化器的实现，因为它容易产生无法解决的宇宙层级统一问题。
另一方面，MProd 可以简化某些高级用例中的 宇宙层级 问题。
term ::= ...
| A product type in which the types may be propositions, usually written `α ×' β`.
This type is primarily used internally and as an implementation detail of proof automation. It is
rarely useful in hand-written code.
Conventions for notations in identifiers:
* The recommended spelling of `×'` in identifiers is `PProd`.
乘积 PProd α β（其中两种类型都可以是命题）写作 α × β。
A product type in which the types may be propositions, usually written α ×' β.
This type is primarily used internally and as an implementation detail of proof automation. It is rarely useful in hand-written code.
Conventions for notations in identifiers:
The recommended spelling of ×' in identifiers is PProd.
PProd.mk.{u, v}
fst : α
The first element of a pair.
snd : β
The second element of a pair.
仅作为一对，Prod 的主 API 由模式匹配以及第一和第二投影 Prod.fst 和 Prod.snd 提供。
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 : β₁ → β₂) : α₁ × β₁ → α₂ × β₂
Checks whether a predicate holds for all natural numbers in a range.
In particular, (start, stop).allI f returns true if f is true for all natural numbers from
start (inclusive) to stop (exclusive).
Examples:
Checks whether a predicate holds for any natural number in a range.
In particular, (start, stop).allI f returns true if f is true for any natural number from
start (inclusive) to stop (exclusive).
Examples:
Combines an initial value with each natural number from a range, in increasing order.
In particular, (start, stop).foldI f init applies fon all the numbers
from start (inclusive) to stop (exclusive) in increasing order:
Examples:
Lexicographical order for products.
Two pairs are lexicographically ordered if their first elements are ordered or if their first elements are equal and their second elements are ordered.
Dependentpairs，也称为 dependent sums 或 Σ-types， 是其中第二项的类型可能取决于第一项的value的对。
它们与存在量词 和 Subtype 密切相关。
与存在量化的陈述不同，依赖对位于 Type 宇宙中，并且是计算相关的数据。
与子类型不同，第二项也是计算相关的数据。
与普通对一样，依赖对可以嵌套；这种嵌套是右结合的。
term ::= ...
| (`binderIdent` matches an `ident` or a `_`. It is used for identifiers in binding
position, where `_` means that the value should be left unnamed and inaccessible.
term ::= ... | Σident`binderIdent` matches an `ident` or a `_`. It is used for identifiers in binding position, where `_` means that the value should be left unnamed and inaccessible.ident* (: term)?, term`binderIdent` matches an `ident` or a `_`. It is used for identifiers in binding position, where `_` means that the value should be left unnamed and inaccessible.
term ::= ... | Σ (ident`binderIdent` matches an `ident` or a `_`. It is used for identifiers in binding position, where `_` means that the value should be left unnamed and inaccessible.ident* : term), term`binderIdent` matches an `ident` or a `_`. It is used for identifiers in binding position, where `_` means that the value should be left unnamed and inaccessible.
依赖对类型绑定一个或多个变量，这些变量位于最后一项的范围内。
如果有一个变量，那么它的类型是对中第一个元素的类型，最后一项是对中第二个元素的类型。
如果有多个变量，则类型以右关联方式嵌套。
标识符也可以是_。
使用括号时，多个绑定变量可以具有不同的类型，而不带括号的变量则要求所有变量具有相同的类型。
类型
Σ 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 ki : Fin (n * k)) , Fin i.val依赖对通常以以下两种方式之一使用：
它们可用于将具体类型索引与索引族的值“打包”在一起，在事先未知索引值时使用。
Σ n, Fin n 类型是一对自然数和一些其他严格较小的数字。
这是使用依赖对的最常见方法。
Dependent pairs, in which the second element's type depends on the value of the first element. The
type Sigma β is typically written Σ a : α, β a or (a : α) × β a.
Although its values are pairs, Sigma is sometimes known as the dependent sum type, since it is
the type level version of an indexed summation.
Sigma.mk.{u, v}
Constructs a dependent pair.
Using this constructor in a context in which the type is not known usually requires a type
ascription to determine β. This is because the desired relationship between the two values can't
generally be determined automatically.
fst : α
The first component of a dependent pair.
snd : β self.fst
The second component of a dependent pair. Its type depends on the first component.
将已知长度与数组关联的类型 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 可用于实现求和类型。
Sum' 第一个投影中的 Bool 指示第二个投影是从哪种类型绘制的。
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`binderIdent` matches an `ident` or a `_`. It is used for identifiers in binding position, where `_` means that the value should be left unnamed and inaccessible.ident* (: term)? , term`binderIdent` matches an `ident` or a `_`. It is used for identifiers in binding position, where `_` means that the value should be left unnamed and inaccessible.
term ::= ... | Σ' (ident`binderIdent` matches an `ident` or a `_`. It is used for identifiers in binding position, where `_` means that the value should be left unnamed and inaccessible.ident* : term), term`binderIdent` matches an `ident` or a `_`. It is used for identifiers in binding position, where `_` means that the value should be left unnamed and inaccessible.
嵌套 Σ' 的规则以及管理其绑定结构的规则与 «termΣ_,_» : termΣ 的规则相同。
Fully universe-polymorphic dependent pairs, in which the second element's type depends on the value
of the first element and both types are allowed to be propositions. The type PSigma β is typically
written Σ' a : α, β a or (a : α) ×' β a.
In practice, this generality leads to universe level constraints that are difficult to solve, so
PSigma is rarely used in manually-written code. It is usually only used in automation that
constructs pairs of arbitrary types.
To pair a value with a proof that a predicate holds for it, use Subtype. To demonstrate that a
value exists that satisfies a predicate, use Exists. A dependent pair with a proposition as its
first component is not typically useful due to proof irrelevance: there's no point in depending on a
specific proof because all proofs are equal anyway.
PSigma.mk.{u, v}
Constructs a fully universe-polymorphic dependent pair.
fst : α
The first component of a dependent pair.
snd : β self.fst
The second component of a dependent pair. Its type depends on the first component.