翻译-Type Theory of Lean

$\rm\LaTeX\textrm{ 定义在此。} %\let\ph=\phantom %\let\hph=\hphantom %\let\vph=\vphantom %\let\mrel=\mathrel %\let\mbin=\mathbin %\let\mop=\mathop %\let\mclap=\mathclap %\let\mllap=\mathllap %\let\mrlap=\mathrlap \def\prstt#1{{\tt (}#1{\tt )}} % 圆括号 \tt \def\prsrm#1{{\rm (}#1{\rm )}} % 圆括号 \rm \def\brkrm#1{{\rm [}#1{\rm ]}} % 方括号 \rm \def\brkrmdbl#1{{\rm [\![}#1{\rm ]\!]}} % 方括号双 \rm \def\pla#1{\vphantom{fg()}{#1}} % 打印，限制行高 smash % 在思考要不要弄一个语法范畴专门表示字面量，比如数字 \newcommand{\teridn}[1][x]{% % 非终结符：标识符 \bbox[lightgray]{\idn[{#1}]}% }% \newcommand{\terlvl}[1][l]{% % 层级表达式：非终结符 \bbox[pink]{\lvl[\mathscr{#1}]}% }% \newcommand{\terexp}[1][e]{% % 表达式：非终结符 \bbox[lightblue]{\exp[{#1}]}% }% \newcommand{\terctx}[1][\Gamma]{% % 语境：非终结符 \bbox[lightgreen]{\ctx[{#1}]}% }% \newcommand{\idn}[1][x]{% % 标识符 \bbox[border: 1px solid gray]{\pla{\mathit{#1}}}% }% \newcommand{\lvl}[1][l]{% % 层级表达式 \bbox[border: 1px solid red]{\pla{\mathscr{#1}}}% }% \newcommand{\exp}[1][e]{% % 表达式 \bbox[border: 1px solid blue]{\pla{#1}}% }% \newcommand{\ctx}[1][\Gamma]{% % 语境 \bbox[border: 1px solid green]{\pla{#1}}% }% \newcommand{\prd}[1]{% % 谓词 \bbox[border: 1px solid limegreen]{\pla{#1}}% }% \newcommand{\jdg}[1]{% % 判断 \bbox[border: 1px solid]{\pla{#1}}% }% \newcommand{\lvlvar}[1][u]{% % 层级表达式：宇宙变量 \lvl[{\idn[{#1}]}]% }% \newcommand{\lvlconst}[1][0]{% % 层级表达式：数字常量 \lvl[{\mathrm{#1}}]% }% \newcommand{\lvlsucc}[2][\prsrm]{% % 层级表达式：后继 \lvl[#1{\mathit{S}{#2}}]% }% \newcommand{\lvlmax}[3][\prsrm]{% % 层级表达式：最大值 \lvl[#1{\textrm{max}\prsrm{{#2}{\rm {},{}}{#3}}}]% }% \newcommand{\lvlimax}[3][\prsrm]{% % 层级表达式：最大值（非直谓） \lvl[#1{\textrm{imax}\prsrm{{#2}{\rm {},{}}{#3}}}]% }% \newcommand{\lvlsubst}[4][\prsrm]{% % 层级表达式：替换 \lvl[#1{{#2}{\rm[}{#3}{\rm {}/{}}{#4}{\rm ]}}]% }% \newcommand{\lvlbin}[4][\prsrm]{% % 层级表达式：二元运算 \lvl[#1{\rm{#3}\mathbin{#2}\text{\(#4\)}}]% }% \newcommand{\expvar}[1][x]{% % 表达式：表达式变量 \exp[{\idn[{#1}]}]% }% \newcommand{\expuni}[2][]{% % 表达式：宇宙 \exp[#1{\textsf{U}_{\pla{#2}}}]% }% \newcommand{\exptrmelm}[3][\prstt]{% % 表达式：函数项的消去 \exp[#1{{#2}\texttt{~}{#3}}]% }% \newcommand{\bndtyp}[3][\prstt]{% % 表达式：函数项的变量绑定器 \prd{#1{{#2}\mathrel{\texttt{:}}{#3}}}% }% \newcommand{\bndtypidx}[3][\prstt]{% % 表达式：函数项的变量绑定器（带指标） \prd{#1{{#2}\mathrel{\texttt{::}}{#3}}}% }% \newcommand{\exptrmcst}[4][\prstt]{% % 表达式：函数项的构造 \exp[#1{\lambda\bndtyp{#2}{#3}\texttt{.\,}{#4}}]% }% \newcommand{\exptypcst}[4][\prstt]{% % 表达式：函数类型构造 \exp[#1{\forall\bndtyp{#2}{#3}\texttt{.\,}{#4}}]% }% \newcommand{\exptrmidxcst}[4][\prstt]{% % 表达式：函数项的构造（带指标） \exp[#1{\lambda\bndtypidx{#2}{#3}\texttt{.\,}{#4}}]% }% \newcommand{\exptypidxcst}[4][\prstt]{% % 表达式：函数类型构造（带指标） \exp[#1{\forall\bndtypidx{#2}{#3}\texttt{.\,}{#4}}]% }% \newcommand{\expsubst}[4][\prstt]{% % 表达式：替换 \exp[#1{{#2}{\rm[}{#3}{\rm {}/{}}{#4}{\rm ]}}]% }% \newcommand{\explet}[5][\prstt]{% % 表达式：let 绑定 \exp[#1{% \texttt{let }% \bndtyp[]{#2}{#3}% \mathrel{\mathtt{:={}}}% {#4}\texttt{ in }{#5}}% ]}% \newcommand{\expdef}[2][c]{% % 表达式：def 常量 \exp[{\idn[{#1}]}_{#2}]% }% \newcommand{\expdeftyp}[2][c]{% % 表达式：def 常量的类型 \exp[\tau_{#2}\prsrm{\idn[{#1}]}] }% \newcommand{\expdefval}[2][c]{% % 表达式：def 常量的值 \exp[{\it v}_{#2}\prsrm{\idn[{#1}]}] }% \newcommand{\ctxempty}{% % 语境：空 \ctx[\cdot]% }% \newcommand{\ctxmany}[2]{% % 语境：多个 \ctx[{{#1}{\rm {},{}}{#2}}]% }% \newcommand{\prdtyp}[3][\prsrm]{% % 谓词：元素居留于类型 \prd{#1{{#2}\mathrel{\textrm{:}}{#3}}}% }% \newcommand{\prdtypidx}[3][\prsrm]{% % 谓词：元素居留于类型 \prd{#1{{#2}\mathrel{\textrm{::}}{#3}}}% }% \newcommand{\prdeql}[3][\prsrm]{% % 谓词：等价 \prd{#1{{#2}\equiv{#3}}}% }% \newcommand{\prdeqltyp}[4][\prsrm]{% % 谓词：等价，带类型 %\prd{#1{{#2}\equiv{#3}\mathrel{\textrm{:}}{#4}}}% \prdtyp[#1]{\prdeql[]{#2}{#3}}{#4} }% \newcommand{\prdeqlalg}[3][\prsrm]{% % 谓词：等价，带算法 \prd{#1{{#2}\Leftrightarrow{#3}}}% }% \newcommand{\prdtypok}[2][\prsrm]{% % 谓词：类型正确 \prd{#1{{#2}~\mathsf{type}}}% }% \newcommand{\prdctxok}[2][\prsrm]{% % 谓词：语境正确 \prd{#1{{#2}~\mathsf{ok}}}% }% \newcommand{\jdgeqllvl}[3][\prsrm]{% % 判断：层级相等 \jdg{#1{{#2}\equiv{#3}}}% }% \newcommand{\jdgbinlvl}[4][\prsrm]{% % 判断：层级关系 \jdg{#1{{#3}#2{#4}}}% }% \newcommand{\jdgrdc}[3][\prsrm]{% % 判断：归约 \jdg{#1{{#2}\rightsquigarrow{#3}}}% }% \newcommand{\jdgrdchd}[3][\prsrm]{% % 判断：头部归约 \jdg{#1{{#2}\mathbin{\rightsquigarrow^*}{#3}}}% }% \newcommand{\lst}[1]{% % 列表 \pla{\smash{\bar{#1}}} }% $

参考文献：^{123456789101112131415161718192021222324}

摘要 Abstract

本文旨在介绍一种依赖类型理论，其具有以下特征： 支持归纳类型 Inductive Type， 拥有一系列层级化的宇宙 Hierarchical Universe ——包括一个 由命题构成的非直谓性 Impredicative 的宇宙；具有 证明无关性 Proof Irelevance、 子单例消去性 Subsingleton Elimination，内置 与命题外延性 Propositional Extensionality、商类型 Quotient Type 有关的公理，以及 选择公理 Axiom of Choice。 该理论是 Lean 定理证明助手的公理框架。 公理系统的完整细节在本文中将被详细介绍， 这包含了如 let 名称绑定器和常量声明 这样的类型系统的“可选”特性。 我们会将该理论化简为一个具有有限数目公理的片段， 这是利用一组固定的归纳类型（$W$-类型外加其他几个）完成的， 以便对该公理框架进行研究。

该类型理论的元理论（我们称作 $\textrm{Lean}$）将被分析。我们还特意 证明了定义等价性的类型唯一性 Unique Typing，并利用这一点 构造了预期的集合论模型，并从中 推导出 Lean 相对于 $\textrm{ZFC}$ ${}+{}$ $\{\textrm{存在 $n$ 个不可达基数} \mid n < \omega\}$ （一个相对较弱的大基数假设）的一致性。 由于 Lean 支持具有 $n$ 个不可达基数的 $\textrm{ZFC}$ 模型，因此这是坠好的。

我们也会展示一些负面结果以揭示该理论一些不尽如人意的地方。特别地， 类型检查是不可判定的，而 由 Lean 定理证明助手所实现的类型检查是一个 可判定的、非传递性的、对类型判断的欠近似 Underapproximation。 非传递性也会导致主语归约 Subject Reduction 性质缺失，并且 归约关系不满足 Church-Rosser 性质，因此 归约到规范形式 Normal Form 并不能为定义等价性产生一个判定程序；然而， 修改后的归约关系允许我们在牺牲保证终止性 Guaranteed Termination 的情况下 恢复 Church-Rosser 性质，从而证明类型唯一性 Unique Typing 成立。

1. 简介 Introduction

1.1. 编程语言中的类型理论 Type Theory in Programming Languages

类型在数理逻辑中的历史可以追溯到 Frege 的 Begriffsschrift¹⁰： 该书建立了一种符号系统，表达能力相当于是带有等式的二阶逻辑。 Betrand Russel 在 Frege 的系统中发现了一个悖论： 谓词 $P(A) := \neg A(A)$ 会导致矛盾（或者用集合论的记号来说： 集合 $S = \{x \mid x \in x\}$ 无法构成一个集合）。作为回应， Ernst Zermelo 通过对集合施加“大小限制”来解决矛盾，从而促成了 Zermelo 集合论的诞生； 并且后者最终发展成为 Zermelo-Fraenkel 集合论（$\textrm{ZFC}$）。该理论已 成为现代数学公理化的黄金标准， 提供了一个无类型但具有分层结构的数学概念宇宙视图。

Russell 本人对 Russell 悖论的回应则有所不同： 与其对语言本身施加分层， 不如将以“类型不良的 Ill-Typed”为理由将形如 $A(A)$ 或 $x \in x$ 这样的表达式拒绝。 这种推理方式声称 $A$ 并不是一个可以对与自身类型相同的对象进行谓词判断的对象， 因此从表面上 Prima Facie 看这种写法是形式不良 Ill-Formed 的。这种想法在 Principia Mathematica²⁴ 和 Quine 的 New Foundations²¹ 中得到了发展， 但与之关连最密切的应用还是 Church 对简单类型 $\lambda$-演算⁵的研究（1940）。

编程语言在某种程度上独立地重新发现了类型的概念¹⁶。 早期的编程语言并没有明确的类型概念： Lisp 使用了一种与无类型 $\lambda$-演算密切相关的求值模型； FORTRAN（1956）有表达式的“模式”，要么是定点数，要么是浮点数； Algol 60（1960）发展出了表达式和变量的类型（ 整数 Integer、 实数 Real、 布尔值 Boolean），而 Wirth 和 Hoare 在 1966 年提出的 Algol W 则发展了一种能生成类型的语法，囊括了 记录类型 Record Type 和 带类型的引用。

逻辑和编程传统最终通过 Curry-Howard 对应¹¹明确地联系在了一起；该对应关系观察到了 相继式演算中的逻辑推导与 简单类型 $\lambda$-演算中的 $\lambda$ 项 之间的联系（在同样的对应关系中 Howard 还讨论了对一阶逻辑的扩展，其中 取值取决于“数字变量”的 $\lambda$-项 $(\lambda x.~F^\beta)^{\forall x~\beta}$ 有别于 带类型的 $\lambda$-项 $(\lambda x^\alpha. F^\beta)^{\alpha \supset \beta}$）。 但依赖类型理论真正成形始于 Per Martin-Löf¹⁴， 他为 Brouwer 的直觉主义类型理论奠定了基础， 这是简单类型 $\lambda$-演算与依赖类型的一个延伸。

Martin-Löf 描述了构造性类型理论该如何在编程语言中使用：

如果是在如类型理论这样为构造性数学而生的形式语言中进行编程， 那么除去那些严重依赖排中律 Law of Excluded Middle 的部分， 整套纯数学的概念框架都可以被拿来使用； 然而直至今日，人们设计出的最优秀的高级程序设计语言 作为数学语言都是完全不合格的（当然也没人敢声称它们能做到这一点）。 事实上，我并不认为对于逻辑上日趋完善的高级程序设计语言的探索 会止步于任何东西，除了那些能够充分表达（构造性）数学的语言以外。¹⁵

英文原文

By choosing to program in a formal language for constructive mathematics, like the theory of types, one gets access to the whole conceptual apparatus of pure mathematics, neglecting those parts that depend critically on the law of excluded middle, whereas even the best high level programming languages so far designed are wholly inadequate as mathematical languages (and, of course, nobody has claimed them to be so). In fact, I do not think that the search for logically ever more satisfactory high level programming languages can stop short of anything but a language in which (constructive) mathematics can be adequately expressed. [15]

---

这个梦想最终被 Coquand 和 Huet 实现：他们 引入了构造演算 Calculus of Constructions，$\textrm{CoC}$⁶，并 将其实现为交互式定理证明助手 Coq⁴。 通过补充对归纳类型⁸的支持，该类型理论最终演变为了 归纳构造演算 Calculus of Inductive Constructions，$\textrm{CIC}$¹⁹。

Lean⁷ 同样也是一个基于 $\textrm{CIC}$ 的定理证明助手， 但是与前者相比有一些微妙但重要的差别。本文的目标便是演示 所有这些差别将会导致的综合后果。 虽然 $\textrm{CIC}$ 本身已经被充分研究过了^{1 2 3}， 但是大多数论文研究的都是 Coq 已实现的实际公理系统下的子系统， 这些子系统可能会被称作是 $\textrm{CIC}^+$，因为在这些年它被扩展了许多功能。 尽管在文中我们不会分析 $\textrm{CIC}^+$， 但是我们将会分析 Lean 的 $\textrm{CIC}$ 内的所有扩展， 如此我们对一致性 Consistency 的证明 便可被直接应用于完整的 Lean 内核（参见章节 2.8 以 了解在尝试将此分析拓展到 $\textrm{CIC}^+$ 时可能出现的问题）。

1.2. 类型理论对应的集合理论 Set Theoretic Models of Type Theory

对于 Martin-Löf 类型理论而言存在着一个相对明显的集合理论模型：当中 类型被解释为集合，而 该类型下的项会被解释为相应集合的元素。 从本质上说，这相当于是将 形如 $A \to B$ 的“函数类型”视作是 由 $\textrm{ZFC}$ 编码的函数（有序对构成的集合）所组成的实际集合。 由于大部分类型理论的直觉和术语都是从这个语境中继承而来的，因此从标准数学的角度来看， 我们有理由期望这种解释作为一个模型来说是行得通的；反过来看， 我们也可以将该模型作为一种指导，以判断类型理论规则的各种变体是否合理。

在此模型中，收容命题的最容易的方式便是拥有一个只有两个元素的宇宙 $\textrm{Prop} =\{0, 1\}$：当中的两个元素都是命题，一个是 $0 = \varnothing$，另一个是 $1 = \{\bullet\}$——其中 $\bullet$ 表示“真命题的平凡证明”。 如此该模型便具有证明无关性 Proof-Irrelevant， 意味着一个命题的多个证明在模型中都会被一视同仁。 这对于某些形式上具有证明无关性的类型理论（也称作 公理 $\textrm{K}$ 或者是 等价证明的唯一性 Uniqueness of Identity Proofs（UIP） ）来说是非常好的， 但却与同伦类型理论 Homotopy Type Theory（HoTT）²²相矛盾，因为 泛等公理 Univalence Axiom 与 UIP 是不一致的（ 由于 Definitional UIP 是 Lean 当中的一个公理， 因此 HoTT 的模型在这里不会被进一步探讨）。

这个模型同样也适用于命题宇宙的非直谓性 Impredicativity；也就是说， 类型理论允许命题对“大的宇宙”中的元素进行量化。 对于习惯于集合论的数学家们而言， 这似乎并不构成一个问题，但是非直谓性 在公理上是相当强的，并且在 $\textrm{ZFC}$ 的视角下 这意味着拥有“完整幂集”。 对于直谓性 Predicative 类型理论——比如 Agda¹⁸ 所使用的公理系统， 非直谓性 Impredicative 模型仍然适用，但在某种意义上是“过度设计 Overkill”。 我们更青睐那些建立于项的部分等价关系 Partial Equivalence Relations 之上的模型， 以避免大基数。

$\textrm{CIC}$ 的宇宙在函数类型和归纳类型下是封闭的； 若是翻译为集合论语言，则意味着它们是 Grothendieck 宇宙。 如果我们只考虑累积层级 $V_\lambda$ 的各个层次， 那么这相当于是要求 $\lambda$ 是一个不可达基数。 由于 Lean 拥有无限数目的宇宙，那么这也就意味着 在 $\textrm{ZFC}$ 宇宙（从中我们将会构建出一个模型）中 将会拥有 $\omega$ 个不可达基数，而这正是我们所需要的主要大基数公理。 不难看出这个假设（或者是某个具有类似一致性强度的东西）是必要的，因为 一旦有了一个适当定义的归纳类型， 我们就可以在第一层以上的每个宇宙中构造出一个 $\textrm{ZFC}$ 模型，并且 我们还可以在更大的模型中定义特定的不可达基数，如此 我们便可以获得具有 $n$ 个不可达基数的 $\textrm{ZFC}$ 模型。

在 “Sets in Types, Types in Sets” 一文²³中，Werner 证明了 $\textrm{ZFC}_\omega$ 和 $\textrm{CIC}_\omega$ 的一致性是彼此等价的 Equiconsistency，这是通过证明 $\textrm{ZFC}_{n} \vdash \textrm{Con}(\textrm{CIC}_{n+1})$ 和 $\textrm{CIC}_{n+2} \vdash \textrm{Con}(\textrm{ZFC}_n)$ 来完成的；其中 $\textrm{ZFC}_{n}$ 是具有 $n$ 个不可达基数的 $\textrm{ZFC}$， $\textrm{CIC}_{n}$ 是具有 $n$ 个宇宙的 $\textrm{CIC}$，而 $\textrm{ZFC}_\omega$ / $\textrm{CIC}_\omega$ 则是 将所有满足 $n < \omega$ 的 $\textrm{ZFC}_n$ / $\textrm{CIC}_n$ 全部并在一起后得到的结果。 Werner 在（Coq 的）$\textrm{CIC}$ 中构造集合论模型的工作已被照搬到 Lean 中，只做了少量修改； 因此根据同样的原因我们也可以声称 $\textrm{Lean}_{n+2} \vdash \textrm{Con}(\textrm{ZFC}_n)$。

当前的工作则是建立了反向方向 $\textrm{ZFC}_{n+1} \vdash \textrm{Con}(\textrm{Lean}_{n+1})$，因此 $\textrm{Lean}_\omega$（或者直接称作是 $\textrm{Lean}$）、 $\textrm{ZFC}_\omega$、$\textrm{CIC}_\omega$ 的一致性都是彼此等价的 Equiconsistent。 我们不会尝试精确地处理宇宙界限，但是 如果我们想要得到类似 Werner 的结果 $\textrm{ZFC}_n \vdash \textrm{Con}(\textrm{CIC}_{n+1})$， 那么我们将不得不在 $\textrm{ZFC}$ 中引入一个全局选择公理（即 在宇宙 $V$ 上存在一个真类选择函数）以解释 Lean 的选择公理。

在某种程度上本文可视作是对 Werner 的工作的进一步展开， 只不过研究背景从 Coq 切换为了 Lean 而已。然而， 我们认为 $\textrm{CIC}$ 和 $\textrm{Lean}$ 中的归纳类型 会比它们在简单示例中的行为更为复杂，因此 我们希望确保能够正确地建模整个语言，包括所有那些 会以不寻常方式相互作用的边界情况特性。 事实上，正如我们将要看到的， 具有子单例消去性的归纳类型 Subsingleton Eliminating Inductive Types 与 Definitional Proof Irrelevance 相结合会破坏 Lean 类型系统的可判定性 Decidability，进而 导致若干理想性质无法成立。考虑到这一点，以及 Coq 历史上曾因 归纳类型声明或 模式匹配 中的某些特殊特性 而导致的类型可靠性 Soundness 方面的漏洞⁹，我们认为 完整地写明 Lean 类型系统的公理基础是有必要的，并将 以此作为出发点开展研究。见章节 2 以了解规范。

在 “The not so simple proof irrelevant model of CC” 一文¹⁷中， Miquel 和 Werner 详细描述了 在诸如本文所描述的 具有证明无关性的模型中 会出现的一个问题。简而言之， 如果不知道一个表达式或类型所处的宇宙，那么 翻译命题宇宙上的 Pi 类型将会比 翻译其他宇宙上的 Pi 类型更难， 因为我们必须确保 $U_0 = \{\varnothing, \{\bullet\}\}$ 可以作为命题的布尔宇宙。 这个问题在这里也会出现，而克服它的关键步骤是类型唯一性 Unique Typing。 尽管这在文献¹⁷中所讨论的 Pure Type System（PTS）的语境下大多都是轻松的， 但是对于 Lean 而言这是个非常棘手的语法相关的证明，具体证明请见章节 4。 虽然它受到了 Tait–Martin-Löf 对 Church–Rosser 定理的证明²⁰的启发， 但是 Definitional Proof Irrelevance 依然带来了许多新的麻烦，并且 相对于我们已有的知识而言，这个证明是原创的。

在文献¹中，为了使具有的证明无关性的命题宇宙以及其他宇宙都能够被统一处理， Barras 使用了一个简单且巧妙的技巧——即使用 Aczel 编码函数的方式，也就是 $f := \{(x, y) \mid x \in \textrm{dom}(f)\wedge y \in f(x)\}$； 这种编码会具有如下性质： 如果我们将 $\bullet$ 解释为空集。 那么就会有 $(x \in A \mapsto \bullet) = \bullet$。这一简单的性质意味着 我们无需在构造中确定类型和元素的种类 Sort，因此 我们可以在可靠性 Soundness 证明中避免依赖类型唯一性 Unique Typing。也就是说， 如果我们的目标只是证明可靠性 Soundness， 那么我们可以直接跳过章节 4； 但是这仍然是一个非常有用的性质。一旦将其证明， 我们就可以使用更直接的 $\textrm{ZFC}$ 编码来表示函数。

本文的其余部分组织如下： 章节 2 详细 介绍了 Lean 的类型系统的形式符号。 章节 3 研究了类型系统的基本元理论，特别是 展示了类型系统不可判定性 Decidability 缺失所导致的负面结果。 章节 4 证明了类型系统的类型唯一性 Unique Typing（也 囊括了不可判定 Undecidable 的部分）。 章节 5 展示了所有归纳类型都可以被归约为一组有限的基底——由 8 个特定的基本归纳类型组成。 章节 6 介绍了可靠性 Soundness 定理，该定理 以前面提到的 $\textrm{W}$ 作为基础详细 构造了的集合论模型。

2. 公理 The Axioms

2.1. 类型 Typing

表达式的语法由以下语法给出：

其中 $\lvl[{\teridn[u]}]$ 表示一个宇宙变量， $\exp[{\teridn[x]}]$ 表示一个表达式变量。 类型判断由以下规则定义：

判断：$\jdg{\ctx \vdash \prdtyp[]\exp{\exp[\alpha]}}$

• 规则：弱化

  $\begin{prooftree} \AXC{\(\jdg{\ctx \vdash \prdtyp[]{\exp[\alpha]}{\expuni\lvl}}\)} \AXC{\(\jdg{\ctx \vdash \prdtyp[]\exp{\exp[\beta]}}\)} \RL{\(\prsrm{\href{#规则-弱化}{\text{弱化}}}\)} \BIC{\(\jdg{% \ctxmany\ctx{\prdtyp[]{\expvar}{\exp[\alpha]}} \vdash \prdtyp[]\exp{\exp[\beta]}% }\)} \end{prooftree}$

• 规则：公理

  $\begin{prooftree} \AXC{\(\jdg{\ctx \vdash \prdtyp[]{\exp[\alpha]}{\expuni\lvl}}\)} \RL{\((\href{#规则-公理}{\text{公理}})\)} \UIC{\(\jdg{% \ctxmany\ctx{\prdtyp[]{\expvar}{\exp[\alpha]}} \vdash \prdtyp[]{\expvar}{\exp[\alpha]} }\)} \end{prooftree}$

• 规则：宇宙类型构造

  $\begin{prooftree} \AXC{\(\jdg{}\)} \RL{\(\prsrm{\href{#规则-宇宙类型构造}{\text{$\mathsf{U}$ 引入}}}\)} \UIC{\(\jdg{ \vdash \prdtyp[]{\expuni\lvl}{\expuni{\lvlsucc[]\lvl}} }\)} \end{prooftree}$

• 规则：函数项的应用

  $\begin{prooftree} \AXC{\(\jdg{\ctx \vdash \prdtyp[]{\exp[e_1]}{\exptypcst[]\expvar{\exp[\alpha]}{\exp[\beta]}}}\)} \AXC{\(\jdg{\ctx \vdash \prdtyp[]{\exp[e_2]}{\exp[\alpha]}}\)} \RL{\(\prsrm{\href{#规则-函数项的应用}{\text{\(\to\) 消去}}}\)} \BIC{\(\jdg{\ctx \vdash \prdtyp[] {\exptrmelm[]{\exp[e_1]}{\exp[e_2]}} {\expsubst[]{\exp[\beta]}{\exp[e_2]}\expvar} }\)} \end{prooftree}$

• 规则：函数项的构造

  $\begin{prooftree} \AXC{\(\jdg{ \ctxmany\ctx{\prdtyp[]{\expvar}{\exp[\alpha]}} \vdash \prdtyp[]\exp{\exp[\beta]} }\)} \RL{\(\prsrm{\href{#规则-函数项的构造}{\text{\(\to\) 引入}}}\)} \UIC{\(\jdg{ \ctx \vdash \prdtyp[] {\exptrmcst[]\expvar{\exp[\alpha]}\exp} {\exptypcst[]\expvar{\exp[\alpha]}{\exp[\beta]}} }\)} \end{prooftree}$

• 规则：函数类型构造

  $\begin{prooftree} \AXC{\(\jdg{ \ctx \vdash \prdtyp[]{\exp[\alpha]}{\expuni{\lvl[l_1]}} }\)} \AXC{\(\jdg{ \ctxmany\ctx{\prdtyp[]\expvar{\exp[\alpha]}}\vdash \prdtyp[]{\exp[\beta]}{\expuni{\lvl[l_2]}} }\)} \RL{\(\prsrm{\href{#规则-函数类型构造}{\text{\(\forall\) 引入}}}\)} \BIC{\(\jdg{ \ctx \vdash \prdtyp[] {\exptypcst[]\expvar{\exp[\alpha]}{\exp[\beta]}} {\expuni[]{\lvlimax[]{\lvl[l_1]}{\lvl[l_2]}}} }\)} \end{prooftree}$

• 规则：理想等式应用

  $\begin{prooftree} \AXC{\(\jdg{\ctx \vdash \prdtyp[]\exp{\exp[\alpha]}}\)} \AXC{\(\jdg{\ctx \vdash \prdeql[]{\exp[\alpha]}{\exp[\beta]}}\)} \RL{\(\prsrm{\href{#规则-理想等式应用}{\text{\(\equiv\) 消去}}}\)} \BIC{\(\jdg{\ctx \vdash \prdtyp[]\exp{\exp[\beta]}}\)} \end{prooftree}$

每个常量都拥有一个宇宙变量列表 $\lst\lvlvar$。 当中的宇宙变量可能会出现在常量的类型中， 它们会被替换为给定的宇宙层级表达式 $\expsubst[]{\expdeftyp{\lst\lvlvar}}{\lst\lvl}{\lst\lvlvar}$。

方便起见，我们也会定义以下简单的判断：

判断：$\jdg{\ctx \vdash \prdtypok[]{\exp[\alpha]}}$

• 规则：00-规则-08

  $\begin{prooftree} \AXC{\(\jdg{\ctx \vdash \prdtyp[]{\exp[\alpha]}{\expuni\lvl}}\)} \RL{\(\prsrm{\href{#00-规则-08}{\text{00-规则-08}}}\)} \UIC{\(\jdg{\ctx \vdash \prdtypok[]{\exp[\alpha]}}\)} \end{prooftree}$

判断：$\jdg{\ctx[]\vdash \prdctxok[]\ctx}$

• 规则：00-规则-09

  $\begin{prooftree} \AXC{\(\jdg{}\)} \RL{\(\prsrm{\href{#00-规则-09}{\text{00-规则-09}}}\)} \UIC{\(\jdg{\ctx[]\vdash \prdctxok[]\ctxempty}\)} \end{prooftree}$

• 规则：00-规则-10

  $\begin{prooftree} \AXC{\(\jdg{\ctx \vdash \prdtypok[]{\exp[\alpha]}}\)} \RL{\(\prsrm{\href{#00-规则-10}{\text{00-规则-10}}}\)} \UIC{\(\jdg{\vdash \prdctxok[]{\ctxmany\ctx{\prdtyp[]\expvar{\exp[\alpha]}}} }\)} \end{prooftree}$

2.2. 定义等价性 Definitional Equality

我们将会区分两种定义等价性：一种是 “理想的”定义等价性，记作 $\prdeql[]{\exp[\alpha]}{\exp[\beta]}$；另一种是 “算法的”定义等价性，记作 $\prdeqlalg[]{\exp[\alpha]}{\exp[\beta]}$。 后者可以推导出 $\prdeql[]{\exp[\alpha]}{\exp[\beta]}$，并且是 Lean 实际上所检查的内容。

判断：$\jdg{\ctx \vdash \prdeql[]\exp{\exp[e']}}$

• 规则：理想等价关系具有自反性

  $\begin{prooftree} \AXC{\(\jdg{\ctx \vdash \prdtyp[]\exp{\exp[\alpha]}}\)} \RL{\(\prsrm{\href{#规则-理想等价关系具有自反性}{\text{\(\equiv\) 自反}}}\)} \UIC{\(\jdg{\ctx \vdash \prdeql[]\exp\exp}\)} \end{prooftree}$

• 规则：理想等价关系具有对称性

  $\begin{prooftree} \AXC{\(\jdg{\ctx \vdash \prdeql[]\exp{\exp[e']}}\)} \RL{\(\prsrm{\href{#规则-理想等价关系具有对称性}{\text{\(\equiv\) 对称}}}\)} \UIC{\(\jdg{\ctx \vdash \prdeql[]{\exp[e']}\exp}\)} \end{prooftree}$

• 规则：理想等价关系具有传递性

  $\begin{prooftree} \AXC{\(\jdg{\ctx \vdash \prdeql[]{\exp[e_1]}{\exp[e_2]}}\)} \AXC{\(\jdg{\ctx \vdash \prdeql[]{\exp[e_2]}{\exp[e_3]}}\)} \RL{\(\prsrm{\href{#规则-理想等价关系具有传递性}{\text{\(\equiv\) 传递}}}\)} \BIC{\(\jdg{\ctx \vdash \prdeql[]{\exp[e_1]}{\exp[e_3]}}\)} \end{prooftree}$

• 规则：理想等价关系具有合同性（关于宇宙类型构造）

  $\begin{prooftree} \AXC{\(\jdgeqllvl[]\lvl{\lvl[l']}\)} \RL{\(\prsrm{\href{#规则-理想等价关系具有合同性（关于宇宙类型构造）}{\text{\(\equiv\) 合同（\(\mathsf{U}\) 引入）}}}\)} \UIC{\(\jdg{\ctx[] \vdash \prdeql[]{\expuni\lvl}{\expuni{\lvl[l']}}}\)} \end{prooftree}$

• 规则：理想等价关系具有合同性（关于函数项的应用）

  $\begin{prooftree} \AXC{\(\jdg{\ctx \vdash \prdeqltyp[] {\exp[e_1]}{\exp[e_1']} {\exptypcst[]\expvar{\exp[\alpha]}{\exp[\beta]}} }\)} \AXC{\(\jdg{\ctx \vdash \prdeqltyp[]{\exp[e_2]}{\exp[e_2']}{\exp[\alpha]}}\)} \RL{\(\prsrm{\href{#规则-理想等价关系具有合同性（关于函数项的应用）}{\text{\(\equiv\) 合同（\(\to\) 消去）}}}\)} \BIC{\(\jdg{\ctx \vdash \prdeql[]{\exptrmelm[]{\exp[e_1]}{\exp[e_2]}}{\exptrmelm[]{\exp[e_1']}{\exp[e_2']}}}\)} \end{prooftree}$

• 规则：理想等价关系具有合同性（关于函数项的构造）

  $\begin{prooftree} \AXC{\(\jdg{\ctx \vdash \prdeql[]{\exp[\alpha]}{\exp[\alpha']}}\)} \AXC{\(\jdg{\ctxmany\ctx{\prdtyp[]\expvar{\exp[\alpha]}} \vdash \prdeql[]{\exp}{\exp[e']}}\)} \RL{\(\prsrm{\href{#规则-理想等价关系具有合同性（关于函数项的构造）}{\text{\(\equiv\) 合同（\(\to\) 引入）}}}\)} \BIC{\(\jdg{\ctx \vdash \prdeql[]{\exptrmcst[]\expvar{\exp[\alpha]}\exp}{\exptrmcst[]\expvar{\exp[\alpha']}{\exp[e']}}}\)} \end{prooftree}$

• 规则：理想等价关系具有合同性（关于函数类型构造）

  $\begin{prooftree} \AXC{\(\jdg{\ctx \vdash \prdeql[]{\exp[\alpha]}{\exp[\alpha']}}\)} \AXC{\(\jdg{\ctxmany\ctx{\prdtyp[]\expvar{\exp[\alpha]}} \vdash \prdeql[]{\exp[\beta]}{\exp[\beta']}}\)} \RL{\(\prsrm{\href{#规则-理想等价关系具有合同性（关于函数类型构造）}{\text{\(\equiv\) 合同（\(\forall\) 引入）}}}\)} \BIC{\(\jdg{\ctx \vdash \prdeql[]{\exptypcst[]\expvar{\exp[\alpha]}{\exp[\beta]}}{\exptypcst[]\expvar{\exp[\alpha']}{\exp[\beta']}}}\)} \end{prooftree}$

• 规则：$\beta$ 归约

  $\begin{prooftree} \AXC{\(\jdg{\ctxmany\ctx{\prdtyp[]\expvar{\exp[\alpha]}} \vdash \prdtyp[]\exp{\exp[\beta]}}\)} \AXC{\(\jdg{\ctx \vdash \prdtyp[]{\exp[e']}{\exp[\alpha]}}\)} \RL{\(\prsrm{\href{#规则-Beta归约}{\text{\(\beta\) 归约}}}\)} \BIC{\(\jdg{\ctx \vdash \prdeql[]{\exptrmelm[]{\exptrmcst\expvar{\exp[\alpha]}\exp}{\exp[e']}}{\expsubst[]\exp{\exp[e']}\expvar}}\)} \end{prooftree}$

• 规则：$\eta$ 归约

  $\begin{prooftree} \AXC{\(\jdg{\ctx \vdash \prdtyp[]\exp{\exptypcst[]{\expvar[y]}{\exp[\alpha]}{\exp[\beta]}}}\)} \RL{\(\prsrm{\href{#规则-Eta归约}{\text{\(\eta\) 归约}}}\)} \UIC{\(\jdg{\ctx \vdash \prdtyp[]{\exptrmcst[]\expvar{\exp[\alpha]}{\exptrmelm[]\exp\expvar}}\exp}\)} \end{prooftree}$

• 规则：理想等价关系描述命题宇宙的证明无关性

  $\begin{prooftree} \AXC{\(\jdg{\ctx \vdash \prdtyp[]{\exp[p]}{\exp[\mathbb{P}]}}\)} \AXC{\(\jdg{\ctx \vdash \prdtyp[]{\exp[h]}{\exp[p]}}\)} \AXC{\(\jdg{\ctx \vdash \prdtyp[]{\exp[h']}{\exp[p]}}\)} \RL{\(\prsrm{\href{#规则-理想等价关系描述命题宇宙的证明无关性}{\text{\(\equiv\) \(\mathbb{P}\) 证明无关}}}\)} \TIC{\(\jdg{\ctx \vdash \prdeql[]{\exp[h]}{\exp[h']}}\)} \end{prooftree}$

记号 $\jdg{\ctx \vdash \prdeqltyp[]\exp{\exp[e']}{\exp[\alpha]}}$ 在应用规则中用于表示 $\jdg{\ctx \vdash \prdeql[]\exp{\exp[e']}}$ ${}\wedge{}$ $\jdg{\ctx \vdash \prdtyp[]\exp{\exp[\alpha]}}$ ${}\wedge{}$ $\jdg{\ctx \vdash \prdtyp[]{\exp[e']}{\exp[\alpha]}}$ 的缩写。 最后一条推理规则被称作是证明无关性 Proof Irrelevance：它指出 同一个命题（即 $\exp[\mathbb{P}] := \expuni\lvlconst$ 中的类型）的 任何两个证明始终都是等价的。 层级的等价性是通过一个算法不等式判断 $\jdgbinlvl[]\leq\lvl{\lvlbin[]+{\lvl[l']} n}$ 来定义的，其中 $n \in \mathbb{Z}$（若 $n = 0$ 则简记为 $\jdgbinlvl[]\leq\lvl{\lvl[l']}$）：

判断：$\jdgeqllvl[]\lvl{\lvl[l']}$

• 规则：00-规则-21

  $\begin{prooftree} \AXC{\(\jdgbinlvl[]\leq\lvl{\lvl[l']}\)} \AXC{\(\jdgbinlvl[]\leq{\lvl[l']}\lvl\)} \RL{\(\prsrm{\href{#00-规则-21}{\text{00-规则-21}}}\)} \BIC{\(\jdgeqllvl[]\lvl{\lvl[l']}\)} \end{prooftree}$

判断：$\jdg{\lvl \leq \lvlbin[]+\lvl n}$

• 规则：00-规则-22

  $\begin{prooftree} \AXC{\(\jdg{n \geq 0}\)} \RL{\(\prsrm{\href{#00-规则-22}{\text{00-规则-22}}}\)} \UIC{\(\jdgbinlvl[]\leq\lvlconst{\lvlbin[]+\lvl n}\)} \end{prooftree}$

• 规则：00-规则-23

  $\begin{prooftree} \AXC{\(\jdg{n \geq 0}\)} \RL{\(\prsrm{\href{#00-规则-23}{\text{00-规则-23}}}\)} \UIC{\(\jdgbinlvl[]\leq\lvl{\lvlbin[]+\lvl n}\)} \end{prooftree}$

• 规则：00-规则-24

  $\begin{prooftree} \AXC{\(\jdgbinlvl[]\leq\lvl{\lvlbin[]+{\lvl[l']}{(n - 1)}}\)} \RL{\(\prsrm{\href{#00-规则-24}{\text{00-规则-24}}}\)} \UIC{\(\jdgbinlvl[]\leq{\lvlsucc[]\lvl}{\lvlbin[]+{\lvl[l']}n}\)} \end{prooftree}$

• 规则：00-规则-25

  $\begin{prooftree} \AXC{\(\jdgbinlvl[]\leq\lvl{\lvlbin[]+{\lvl[l']}{(n + 1)}}\)} \RL{\(\prsrm{\href{#00-规则-25}{\text{00-规则-25}}}\)} \UIC{\(\jdgbinlvl[]\leq\lvl{\lvlbin[]+{\lvlsucc[]{\lvl[l']}}n}\)} \end{prooftree}$

• 规则：00-规则-26

  $\begin{prooftree} \AXC{\(\jdgbinlvl[]\leq\lvl{\lvlbin[]+{\lvl[l_1]}n}\)} \RL{\(\prsrm{\href{#00-规则-26}{\text{00-规则-26}}}\)} \UIC{\(\jdgbinlvl[]\leq\lvl{\lvlbin[]+{\lvlmax[]{\lvl[l_1]}{\lvl[l_2]}}n}\)} \end{prooftree}$

• 规则：00-规则-27

  $\begin{prooftree} \AXC{\(\jdgbinlvl[]\leq\lvl{\lvlbin[]+{\lvl[l_2]}n}\)} \RL{\(\prsrm{\href{#00-规则-27}{\text{00-规则-27}}}\)} \UIC{\(\jdgbinlvl[]\leq\lvl{\lvlbin[]+{\lvlmax[]{\lvl[l_1]}{\lvl[l_2]}}n}\)} \end{prooftree}$

• 规则：00-规则-28

  $\begin{prooftree} \AXC{\(\jdgbinlvl[]\leq{\lvl[l_1]}{\lvlbin[]+\lvl n}\)} \AXC{\(\jdgbinlvl[]\leq{\lvl[l_2]}{\lvlbin[]+\lvl n}\)} \RL{\(\prsrm{\href{#00-规则-28}{\text{00-规则-28}}}\)} \BIC{\(\jdgbinlvl[]\leq{\lvlimax[]{\lvl[l_1]}{\lvl[l_2]}}{\lvlbin[]+\lvl n}\)} \end{prooftree}$

• 规则：00-规则-29

  $\begin{prooftree} \AXC{\(\jdgbinlvl[]\leq\lvlconst{\lvlbin[]+\lvl n}\)} \RL{\(\prsrm{\href{#00-规则-29}{\text{00-规则-29}}}\)} \UIC{\(\jdgbinlvl[]\leq{\lvlimax[]{\lvl[l_1]}\lvlconst}{\lvlbin[]+\lvl n}\)} \end{prooftree}$

• 规则：00-规则-30

  $\begin{prooftree} \AXC{\(\jdgbinlvl[]\leq{\lvlmax[]{\lvl[l_1]}{\lvlsucc[]{\lvl[l_2]}}}{\lvlbin[]+\lvl n}\)} \RL{\(\prsrm{\href{#00-规则-30}{\text{00-规则-30}}}\)} \UIC{\(\jdgbinlvl[]\leq{\lvlimax[]{\lvl[l_1]}{\lvlsucc[]{\lvl[l_2]}}}{\lvlbin[]+\lvl n}\)} \end{prooftree}$

• 规则：00-规则-31

  $\begin{prooftree} \AXC{\(\jdgbinlvl[]\leq{\lvlmax[] {\lvlimax[]{\lvl[l_1]}{\lvl[l_3]}} {\lvlimax[]{\lvl[l_2]}{\lvl[l_3]}}} {\lvlbin[]+\lvl n}\)} \RL{\(\prsrm{\href{#00-规则-31}{\text{00-规则-31}}}\)} \UIC{\(\jdgbinlvl[]\leq{\lvlimax[] {\lvl[l_1]} {\lvlimax[]{\lvl[l_2]}{\lvl[l_3]}}} {\lvlbin[]+\lvl n}\)} \end{prooftree}$

• 规则：00-规则-32

  $\begin{prooftree} \AXC{\(\jdgbinlvl[]\leq{\lvlmax[] {\lvlimax[]{\lvl[l_1]}{\lvl[l_2]}} {\lvlimax[]{\lvl[l_1]}{\lvl[l_3]}}} {\lvlbin[]+\lvl n}\)} \RL{\(\prsrm{\href{#00-规则-32}{\text{00-规则-32}}}\)} \UIC{\(\jdgbinlvl[]\leq{\lvlimax[] {\lvl[l_1]} {\lvlimax[]{\lvl[l_2]}{\lvl[l_3]}}} {\lvlbin[]+\lvl n}\)} \end{prooftree}$

• 规则：00-规则-33

  $\begin{prooftree} \AXC{\(\jdgbinlvl[]\leq\lvl{\lvlbin[]+{\lvlmax[] {\lvlimax[]{\lvl[l_1]}{\lvl[l_3]}} {\lvlimax[]{\lvl[l_2]}{\lvl[l_3]}}}n}\)} \RL{\(\prsrm{\href{#00-规则-33}{\text{00-规则-33}}}\)} \UIC{\(\jdgbinlvl[]\leq\lvl{\lvlbin[]+{\lvlimax[] {\lvl[l_1]} {\lvlimax[]{\lvl[l_2]}{\lvl[l_3]}}}n}\)} \end{prooftree}$

• 规则：00-规则-34

  $\begin{prooftree} \AXC{\(\jdgbinlvl[]\leq\lvl{\lvlbin[]+{\lvlmax[] {\lvlimax[]{\lvl[l_1]}{\lvl[l_2]}} {\lvlimax[]{\lvl[l_1]}{\lvl[l_3]}}}n}\)} \RL{\(\prsrm{\href{#00-规则-34}{\text{00-规则-34}}}\)} \UIC{\(\jdgbinlvl[]\leq\lvl{\lvlbin[]+{\lvlimax[] {\lvl[l_1]} {\lvlimax[]{\lvl[l_2]}{\lvl[l_3]}}}n}\)} \end{prooftree}$

• 规则：00-规则-35

  $\begin{prooftree} \AXC{\( \jdgbinlvl[]\leq{\lvlsubst[]\lvl\lvlconst\lvlvar} {\lvlbin[]+{\lvlsubst[]{\lvl[l']}\lvlconst\lvlvar}n} \)} \AXC{\( \jdgbinlvl[]\leq{\lvlsubst[]\lvl{\lvlsucc[]{\lvlvar}}{\lvlvar}} {\lvlbin[]+{\lvlsubst[]{\lvl[l']}{\lvlsucc[]{\lvlvar}}{\lvlvar}}n}\)} \RL{\(\prsrm{\href{#00-规则-35}{\text{00-规则-35}}}\)} \BIC{\(\jdgbinlvl[]\leq\lvl{\lvlbin[]+{\lvl[l']}n}\)} \end{prooftree}$

尽管上述定义看起来非常复杂， 但是用其语义来理解会更轻松： 层级的取值范围是 $\mathbb{N}$，且有 $\lvl[\brkrmdbl\lvlconst] = \lvlconst$，$\lvl[\brkrmdbl{\lvlsucc[]\lvl}]$${}={}$$\lvlbin[]+{\lvl[\brkrmdbl\lvl]}1$，$\lvl[\brkrmdbl{\lvlmax[]{\lvl[l_1]}{\lvl[l_2]}}]$${}={}$$\lvlmax[]{\lvl[\brkrmdbl{\lvl[l_1]}]}{\lvl[\brkrmdbl{\lvl[l_2]}]}$，$\lvl[\brkrmdbl{\lvlimax[]{\lvl[l_1]}{\lvl[l_2]}}]= \lvlimax[]{\lvl[\brkrmdbl{\lvl[l_1]}]}{\lvl[\brkrmdbl{\lvl[l_2]}]}$ ——其中 $\textrm{imax}(m,n)$ 是一个函数，满足 $\textrm{imax}(m,0)=0$ 并且有 $\textrm{imax}(m,n+1)$${}={}$$\textrm{max}(m,n+1)$； 如此一来，只要对所有那些将数值代入层级 $\lvl$ 和 $\lvl[l']$ 中的变量的替换 $v$ 都有 $\lvl[\brkrmdbl{\lvl}_v] \leq \lvlbin[]+{\lvl[\brkrmdbl{\lvl[l']}_v]}n$ 成立， 那么层级不等式 $\jdgbinlvl[]\leq\lvl{\lvlbin[]+\lvl n}$ 就会成立。 我们将在章节 6 中详细讨论这一点。

2.3. 归约 Reduction

“算法的”定义等价性关系是通过 针对项的归约操作来定义的：

判断：$\jdg{\ctx \vdash \prdeqlalg[]\exp{\exp[e']}}$

• 规则：算法等价关系具有自反性

  $\begin{prooftree} \AXC{\(\jdg{}\)} \RL{\(\prsrm{\href{#规则-算法等价关系具有自反性}{\text{\(\Leftrightarrow\) 自反}}}\)} \UIC{\(\jdg{\ctx \vdash \prdeqlalg[]\exp\exp}\)} \end{prooftree}$

• 规则：算法等价关系具有对称性

  $\begin{prooftree} \AXC{\(\jdg{\ctx \vdash \prdeqlalg[]\exp{\exp[e']}}\)} \RL{\(\prsrm{\href{#规则-算法等价关系具有对称性}{\text{\(\Leftrightarrow\) 对称}}}\)} \UIC{\(\jdg{\ctx \vdash \prdeqlalg[]{\exp[e']}\exp}\)} \end{prooftree}$

• 规则：算法等价关系具有“传递性”

  $\begin{prooftree} \AXC{\(\jdgrdc[]\exp{\exp[k]}\)} \AXC{\(\jdg{\ctx \vdash \prdeqlalg[]{\exp[k]}{\exp[e']} }\)} \RL{\(\prsrm{\href{#规则-算法等价关系具有“传递性”}{\text{\(\Leftrightarrow\) “传递”}}}\)} \BIC{\(\jdg{\ctx \vdash \prdeqlalg[]{\exp}{\exp[e']}}\)} \end{prooftree}$

• 规则：算法等价关系具有合同性（关于宇宙类型）

  $\begin{prooftree} \AXC{\(\jdgeqllvl[]\lvl{\lvl[l']}\)} \RL{\(\prsrm{\href{#规则-算法等价关系具有合同性（关于宇宙类型）}{\text{\(\Leftrightarrow\) 合同（\(\mathsf{U}\) 引入）}}}\)} \UIC{\(\jdg{\ctx \vdash \prdeqlalg[]{\expuni\lvl}{\expuni{\lvl[l']}}}\)} \end{prooftree}$

• 规则：算法等价关系具有合同性（关于函数项的应用）

  $\begin{prooftree} \AXC{\(\jdg{\ctx \vdash \prdeqlalg[]{\exp[e_1]}{\exp[e_1']}}\)} \AXC{\(\jdg{\ctx \vdash \prdeqlalg[]{\exp[e_2]}{\exp[e_2']}}\)} \RL{\(\prsrm{\href{#规则-算法等价关系具有合同性（关于函数项的应用）}{\text{\(\Leftrightarrow\) 合同（\(\to\) 消去）}}}\)} \BIC{\(\jdg{\ctx \vdash \prdeqlalg[] {\exptrmelm[]{\exp[e_1]}{\exp[e_2]}} {\exptrmelm[]{\exp[e_1']}{\exp[e_2']}} }\)} \end{prooftree}$

• 规则：算法等价关系具有合同性（关于函数项的构造）

  $\begin{prooftree} \AXC{\(\jdg{\ctx \vdash \prdeqlalg[]{\exp[\alpha]}{\exp[\alpha']} }\)} \AXC{\(\jdg{ \ctxmany\ctx{\prdtyp[]\expvar{\exp[\alpha]}} \vdash \prdeqlalg[]\exp{\exp[e']} }\)} \RL{\(\prsrm{\href{#规则-算法等价关系具有合同性（关于函数项的构造）}{\text{\(\Leftrightarrow\) 合同（\(\to\) 引入）}}}\)} \BIC{\(\jdg{\ctx \vdash \prdeqlalg[] {\exptrmcst[]\expvar{\exp[\alpha]}\exp} {\exptrmcst[]\expvar{\exp[\alpha']}{\exp[e']}} }\)} \end{prooftree}$

• 规则：算法等价关系具有合同性（关于函数类型构造）

  $\begin{prooftree} \AXC{\(\jdg{\ctx \vdash \prdeqlalg[]{\exp[\alpha]}{\exp[\alpha']} }\)} \AXC{\(\jdg{ \ctxmany\ctx{\prdtyp[]\expvar{\exp[\alpha]}} \vdash \prdeqlalg[]\exp{\exp[e']} }\)} \RL{\(\prsrm{\href{#规则-算法等价关系具有合同性（关于函数类型构造）}{\text{\(\Leftrightarrow\) 合同（\(\forall\) 引入）}}}\)} \BIC{\(\jdg{\ctx \vdash \prdeqlalg[] {\exptypcst[]\expvar{\exp[\alpha]}\exp} {\exptypcst[]\expvar{\exp[\alpha']}{\exp[e']}} }\)} \end{prooftree}$

• 规则：函数类型具有外延性

  $\begin{prooftree} \AXC{\(\jdg{\ctx \vdash \prdtyp[]\exp{\exptypcst[]\expvar{\exp[\alpha]}{\exp[\beta]}} }\)} \AXC{\(\jdg{ \ctxmany\ctx{\prdtyp[]\expvar{\exp[\alpha]}} \vdash \prdeqlalg[] {\exptrmelm[]\exp\expvar} {\exptrmelm[]{\exp[e']}\expvar} }\)} \RL{\(\prsrm{\href{#规则-函数类型具有外延性}{\text{\(\to\) 外延}}}\)} \BIC{\(\jdg{\ctx\vdash \prdeqlalg[]\exp{\exp[e']}}\)} \end{prooftree}$

• 规则：算法等价关系描述命题宇宙的证明无关性

  $\begin{prooftree} \AXC{\(\jdg{\ctx \vdash \prdtyp[]{\exp[p]}{\exp[\mathbb{P}]}}\)} \AXC{\(\jdg{\ctx \vdash \prdtyp[]{\exp[h]}{\exp[p]}}\)} \AXC{\(\jdg{\ctx \vdash \prdtyp[]{\exp[h']}{\exp[p']}}\)} \AXC{\(\jdg{\ctx \vdash \prdeqlalg[]{\exp[p]}{\exp[p']}}\)} \RL{\(\prsrm{\href{#规则-算法等价关系描述命题宇宙的证明无关性}{\text{\(\Leftrightarrow\) \(\mathbb{P}\) 证明无关}}}\)} \QuaternaryInfC{\( \jdg{\ctx \vdash \prdeqlalg[]{\exp[h]}{\exp[h']}} \)} \end{prooftree}$

注意到对于这个判断传递性规则是缺失的。除去 $\beta$ 规则， 大部分合同性 Congruence 规则都延续了下来，并且这些规则构成了定义等价关系的所有“简单”情况。 $\eta$ 规则被一个 外延性原理 所取代（这是合理的，因为 如果 $\prdtyp[]{\exptrmelm[]\exp\expvar}{\exptrmelm[]{\exp[e']}\expvar}$， 那么 $\prdeql[] {\exptrmcst[]\expvar{\exp[\alpha]}{\exptrmelm[]\exp\expvar}} {\exptrmcst[]\expvar{\exp[\alpha']}{\exptrmelm[]{\exp[e']}\expvar}}$， 所以根据 $\eta$ 规则可以 得出 $\prdtyp[]\exp{\exp[e']}$）。 当其他规则无法继续时，我们会使用 头部归约关系 $\jdgrdchd[]\exp{\exp[k]}$ 来应用 $\beta$ 规则以及 $\delta$、 $\iota$、 $\zeta$ 规则， 后面三个规则将在它们自己对应的章节中讨论。

判断：$\jdgrdc[]\exp{\exp[e']}$

• 规则：00-规则-45

  $\begin{prooftree} \AXC{\(\jdgrdc[]{\exp[e_1]}{\exp[e_1']}\)} \RL{\(\prsrm{\href{#00-规则-45}{\text{00-规则-45}}}\)} \UIC{\(\jdgrdc[] {\exptrmelm[]{\exp[e_1]}{\exp[e_2]}} {\exptrmelm[]{\exp[e_1']}{\exp[e_2]}}\)} \end{prooftree}$

• 规则：00-规则-46

  $\begin{prooftree} \AXC{\(\jdg{}\)} \RL{\(\prsrm{\href{#00-规则-46}{\text{00-规则-46}}}\)} \UIC{\(\jdgrdc[] {\exptrmelm[]{\exptrmcst\expvar{\exp[\alpha]}\exp}{\exp[e']}} {\expsubst[]\exp{\exp[e']}\expvar} \)} \end{prooftree}$

尽管在后续引入新的构造时 我们还会往这个列表里添加更多规则， 但是这其实已经足够描述 Lean 的基础依赖类型理论了。

2.4. $\texttt{let}$ 绑定器（$\zeta$ 归约） $\texttt{let}$ Binders ($\zeta$ Reduction)

我们对该语言的首个（并且也是最简单的一个）扩展 便是提供对 $\texttt{let}$ 绑定器的支持。我们规定： 表达式 $\explet[]\expvar{\exp[\alpha]}{\exp[e']}\exp$ 等价于 $\expsubst[]\exp{\exp[e']}\expvar$ （断言该等式成立的规则被称为 $\zeta$ 归约）。 该表达式与 $\exptrmelm[]{\exptrmcst\expvar{\exp[\alpha]}\exp}{\exp[e']}$ 的不同之处在于： 后者要求 $\exptrmcst[]\expvar{\exp[\alpha]}\exp$ 必须是类型良好的，而 在前者中我们可以在对 $\exp$ 的主体进行类型检查时使用定义等价 $\prdeql[]\expvar{\exp[e']}$。 你或许会想利用这样的定义等价来扩展语境；但是 Lean 采取了更简单的方法， 并在必要时对这些绑定器进行 $\zeta$ 展开以进行检查。

将 $\texttt{let}$ 绑定器添加到语言中意味着 在前面各节的语法和规则中添加以下内容：

判断：$\jdg{\ctx \vdash \prdtyp[]\exp{\exp[\alpha]}}$

• 规则：$\texttt{let}$ 项的构造

  $\begin{prooftree} \AXC{\(\jdg{\ctx \vdash \prdtyp[]{\exp[e']}{\exp[\alpha]}}\)} \AXC{\(\jdg{\ctx \vdash \prdtyp[]{\expsubst[]\exp{\exp[e']}\expvar}{\exp[\beta]}}\)} \RL{\(\prsrm{\href{#规则-Let项的构造}{\text{{\tt let} 引入}}}\)} \BIC{\(\jdg{\ctx \vdash \prdtyp[]{\explet[]\expvar{\exp[\alpha]}{\exp[e']}\exp}{\exp[\beta]}}\)} \end{prooftree}$

判断：$\jdg{\ctx \vdash \prdeql[]\exp{\exp[e']}}$

• 规则：$\zeta$ 归约

  $\begin{prooftree} \AXC{\(\jdg{\ctx \vdash \prdtyp[]{\exp[e']}{\exp[\alpha]}}\)} \AXC{\(\jdg{\ctx \vdash \prdtyp[]{\expsubst[]\exp{\exp[e']}\expvar}{\exp[\beta]}}\)} \RL{\(\prsrm{\href{#规则-Zeta归约}{\text{\(\zeta\) 归约}}}\)} \BIC{\(\jdg{\ctx \vdash \prdeql[]{\explet[]\expvar{\exp[\alpha]}{\exp[e']}\exp}{\expsubst[]\exp{\exp[e']}\expvar}}\)} \end{prooftree}$

判断：$\jdgrdc[]\exp{\exp[e']}$

• 规则：00-规则-49

  $\begin{prooftree} \AXC{\(\jdg{}\)} \RL{\(\prsrm{\href{#00-规则-49}{\text{00-规则-49}}}\)} \UIC{\(\jdgrdc[] {\explet[]\expvar{\exp[\alpha]}{\exp[e']}\exp} {\expsubst[]\exp{\exp[e']}\expvar} \)} \end{prooftree}$

注意 $\texttt{let}$ 没有任何合同性 Congruence 规则。 我们只需在需要检查它的任何内容时展开它即可。 可以很明显地看出这是一个保守的 Conservative 扩展，因为我们可以用 $\expsubst[]\exp{\exp[e']}\expvar$ 去替换 $\explet[]\expvar{\exp[\alpha]}{\exp[e']}\exp$，并且 在弱头规范形式 Weak Head Normal Form（WHNF）的推导中移除任何 $\zeta$ 归约步骤以恢复原始系统。

2.5. 常量声明 Definitions

Lean 里面有两种类型的常量： 一种是带有定义的常量， 一种是原始常量。 尽管两者都形如 $\expdef{\lst\lvlvar}$ —— 其中 $\idn[c]$ 表示一个新名称， $\lst\lvlvar$ 表示一个宇宙变量列表； 但是关于带有定义的常量还存在一个 与其相关的归约步骤，也就是 $\delta$ 归约。

为了使原始常量的声明 $\texttt{constant }~\bndtyp[]{\expdef{\lst\lvlvar}}{\exp[\alpha]}$ 可被接纳， 我们要求 $\jdg{\ctx[] \vdash \prdtyp[]{\exp[\alpha]}{\expuni\lvl}}$， 其中 $\exp[\alpha]$ 和 $\lvl$ 中的宇宙变量都位于 $\lst\lvlvar$ 中。类似地， 带有定义的常量可以通过子句 $\texttt{def}~\bndtyp[]{\expdef{\lst\lvlvar}}{\exp[\alpha]}\mathrel{\texttt{:={}}}\exp$ 来指定； 需要注意的是该子句只有在 $\jdg{\exp[]\vdash \prdtyp[]\exp{\exp[\alpha]}}$ 且 $\exp$ 和 $\exp[\alpha]$ 中的宇宙变量都位于 $\lst\lvlvar$ 中时 才是可接纳的。 另外规定 $\expdeftyp{\lst\lvl} = \expsubst[]{\exp[\alpha]}{\lst\lvl}{\lst\lvlvar}$ 表示替换掉宇宙变量后的常量的类型， $\expdefval{\lst\lvl} = \expsubst[]\exp{\lst\lvl}{\lst\lvlvar}$ 表示替换掉宇宙变量后的常量的值。 我们现在向系统中添加以下规则：

判断：$\jdg{\ctx \vdash \prdtyp[]\exp{\exp[\alpha]}}$

• 规则：常量声明

  $\begin{prooftree} \AXC{\(\jdg{}\)} \RL{\(\prsrm{\href{#规则-常量声明}{\text{常量声明}}}\)} \UIC{\(\jdg{\ctx[]\vdash \prdtyp[]{\expdef{\lst\lvlvar}}{\expdeftyp{\lst\lvlvar}}}\)} \end{prooftree}$

判断：$\jdg{\ctx \vdash \prdeql[]\exp{\exp[e']}}$

• 规则：00-规则-51

  $\begin{prooftree} \AXC{\(\jdgeqllvl[]\lvl{\lvl[l_1']}\)} \AXC{\(\ldots\)} \AXC{\(\jdgeqllvl[]{\lvl[l_n]}{\lvl[l_n']}\)} \RL{\(\prsrm{\href{#00-规则-51}{\text{00-规则-51}}}\)} \TIC{\(\jdg{\ctx[]\vdash \prdeql[]{\expdef{\lst\lvl}}{\expdef{\lst{\lvl[l']}}}}\)} \end{prooftree}$

判断：$\jdg{\ctx \vdash \prdeqlalg[]\exp{\exp[e']}}$

• 规则：00-规则-52

  $\begin{prooftree} \AXC{\(\jdgeqllvl[]\lvl{\lvl[l_1']}\)} \AXC{\(\ldots\)} \AXC{\(\jdgeqllvl[]{\lvl[l_n]}{\lvl[l_n']}\)} \RL{\(\prsrm{\href{#00-规则-52}{\text{00-规则-52}}}\)} \TIC{\(\jdg{\ctx \vdash \prdeqlalg[]{\expdef{\lst\lvl}}{\expdef{\lst{\lvl[l']}}}}\)} \end{prooftree}$

此外我们还为常量声明添加了额外的规则：

判断：$\jdg{\ctx \vdash \prdeql[]\exp{\exp[e']}}$

• 规则：$\delta$ 归约

  $\begin{prooftree} \AXC{\(\jdg{}\)} \RL{\(\prsrm{\href{#规则-Delta归约}{\text{\(\delta\) 归约}}}\)} \UIC{\(\jdg{\ctx[] \vdash \prdeql[]{\expdef{\lst\lvl}}{\expdefval{\lst\lvl}} }\)} \end{prooftree}$

判断：$\jdgrdc[]\exp{\exp[e']}$

• 规则：00-规则-54

  $\begin{prooftree} \AXC{\(\jdg{}\)} \RL{\(\prsrm{\href{#00-规则-54}{\text{00-规则-54}}}\)} \UIC{\(\jdgrdc[]{\expdef{\lst\lvl}}{\expdefval{\lst\lvl}}\)} \end{prooftree}$

同样也可以很明显地看出：带定义常量的声明也是一个保守的 Conservative 扩展，因为我们可以 用 $\expdefval{\lst\lvl}$ 把 $\expdef{\lst\lvl}$ 替换掉并 移除任何与 $\delta$ 归约有关的步骤以 获得一个完全不借助定义的类型推导过程。 当然啦，这个论证并不适用于 $\textsf{constant}$，因为它们不附带任何归约规则； 可见这不过是对系统的一个公理性 Axiomatic 扩展而已。 我们后续会在探讨各种不同的 一致 Consistent 且保守 Conservative 的常量声明扩展， 它们会在带定义常量的声明因技术原因无法满足需求时派上用场。

2.6. 归纳类型 Inductive Types

归纳类型是我们目前遇到过的所有 Lean 公理系统特性中最复杂的一个，并且 由于它们的记号复杂性 Notational Complexity，要证明它们的性质也十分棘手。我们将 定义一个用于声明归纳类型的语法，并 给出一系列判断以说明它们是可被接纳的。

This is the type of an inductive specification, which is a list of introduction forms with name $c$ and type $e$. We will write $(c : \alpha)$ for the single constructor form $(c : \alpha) + 0$, and abbreviate the whole sequence as $\sum_i(c_i : \alpha_i)$.

Let the notation $\prdtypidx{\expvar[x]}{\exp[\alpha]}$, called a “telescope”, denote a dependent sequence of binders $\prdtyp[]{\expvar[x_1]}{\exp[\alpha_1]}$, $\prdtyp[]{\expvar[x_2]}{\exp[\alpha_2]}$, $\ldots$, $\prdtyp[]{\expvar[x_n]}{\exp[\alpha_n]}$. This will be used in contexts, on the left ($\jdg{\ctxmany\ctx{\prdtypidx[]\expvar{\exp[\alpha]}} \vdash \prdtyp[]\exp{\exp[\beta]}}$) as well as on the right ($\jdg{\ctx \vdash \prdtypidx[]\expvar{\exp[\alpha]}}$); this latter expression means that $\jdg{\ctx \vdash \prdtyp[]{\expvar[x_1]}{\exp[\alpha_1]}}$, and $\jdg{\ctxmany\ctx {\prdtyp[]{\expvar[x_1]}{\exp[\alpha_1]}}\vdash \prdtyp[]{\expvar[x_2]}{\exp[\alpha_2]}}$, and so on up to $\jdg{\ctxmany{\ctxmany{\ctxmany\ctx {\prdtyp[]{\expvar[x_1]}{\exp[\alpha_1]}}}\ldots} {\prdtyp[]{\expvar[x_{n-1}]}{\exp[\alpha_{n-1}]}} \vdash \prdtyp[]{\expvar[x_n]}{\exp[\alpha_n]}}$. It will also be used to abbreviate sequences of $\lambda$ and $\forall$ as in $\exptrmidxcst[]\expvar{\exp[\alpha]}{\exp[\beta]}$${}={}$$ \exptrmcst[]{\expvar[x_1]}{\exp[\alpha_1]}{ \exptrmcst[]{\expvar[x_2]}{\exp[\alpha_2]}{\ldots \texttt{.} \exptrmcst[]{\expvar[x_n]}{\exp[\alpha_n]}{\exp[\beta]}}}$. If $\prdtypidx[]\exp{\exp[\alpha]}$ and $\prdtyp[]{\expvar[f]}{\exptypidxcst[]\expvar{\exp[\alpha]}{\exp[\beta]}}$, then $\prdtyp[]{\exptrmelm[]{\expvar[f]}\exp}{\expsubst[]{\exp[\beta]}\exp{\expvar}}$ denotes the sequence of applications $\exptrmelm[]{ \exptrmelm[]{ \exptrmelm[]{\expvar[f]}{\exp[e_1]}}\ldots}{\exp[e_n]}$.

A specification $K$ is typechecked in a context of a variable $\prdtyp[]{\expvar[t]}{\exp[F]}$ where $\exp[F] = \exptypidxcst[]\expvar{\exp[\alpha]}{\expuni\lvl}$ is a family of sorts (so $\expvar[t]$ is a family of types). The result will be the recursive type $\mu t : F. K$ which roughly satisfies the equivalence $\mu t : F . K \simeq K[\mu t: F.K/t]$.

参考文献 References