- Published on
依赖类型与定理证明
- Authors
- Name
- Mu Xian Ming
- 什么是依赖类型
- 准备工作
- Pie 语言简介
- 函数
- Atom
- Nat
- 柯里化
- 依赖于类型的类型：List
- 依赖于值的类型：Vec
- 更强大的归纳式 eliminator
- List 和 Vec 的归纳式 eliminator
- 定理证明
- 全称量词
- 存在量词
- 结尾
什么是依赖类型
传统的静态类型语言对类型和值有明确的区分，对于类型信息可以出现在哪也有严格的限制。而在支持依赖类型（dependent type）的语言里，类型和值之间的界限变得模糊，类型可以像值一样被计算（即所谓的 first-class 类型 1），同时值也可以出现在类型信息里，“依赖”两个字指的就是类型可以依赖于值。因此类型和值之间不再是单向的而变成了双向的描述关系。支持依赖类型的好处一是类型系统变得更加强大，可以检测并阻止更多的错误类型，让程序更可靠；二是依赖类型可以让计算机像运行传统的程序一样来运行数学证明 2，从而在逻辑上保证程序关键属性的成立。
为了对依赖类型有一个直观的感受，举一个假想的例子。假如 Java 中加入了对依赖类型的支持，那么以 Java 的数组类型为例，可以让它包含更多的信息，比如数组的长度：
String[3] threeNames = {"张三", "赵四", "成吉思汗"}; // 虚构的语法
这么做的好处是，所有围绕于数组类型的方法现在都可以在类型信息中包含更具体的对行为的描述。比如合并两个数组的函数concat的签名可以写成：
String[n + m] concat(String[n] start, String[m] end) {...} // 虚构的语法
这里通过类型就可以知道concat返回的数组的长度是两个参数数组长度的和。这样不仅程序变得更易读，所有可以借由数组长度反映出来的程序错误都能在运行前被检测出来（后面会有实例说明）。再举一个 first-class 类型的例子，下面是用 Idris 写的一个程序片段，Idris 是一个支持依赖类型、和 Haskell 非常接近的语言。
StringOrInt : Bool -> Type
StringOrInt x = case x of
True => Int
False => String
getStringOrInt : (x : Bool) -> StringOrInt x
getStringOrInt x = case x of
True => 42
False => "Fourty two"
valToString : (x : Bool) -> StringOrInt x -> String
valToString x val = case x of
True => cast val
False => val
这段程序的第 1、6、11 行分别声明了三个函数StringOrInt、getStringOrInt和valToString的类型。StringOrInt接受一个布尔类型的参数，返回值的类型是Type（也就是类型的类型，因为类型也是一种值），当参数是True，返回Int类型，参数为False时，返回String类型。而在getStringOrInt的类型声明中可以看到它的返回值类型是StringOrInt x，也就是说返回值类型依赖于参数x的值：当x的值为True时，返回值类型是StringOrInt True的值，也就是Int；当x是False是，返回值类型就变成了String。函数StringOrInt和getStringOrInt体现了依赖类型的两个特性：
- 类型可以由函数动态地计算出来。
- 类型声明中可以包括变量或者复杂的表达式，如
StringOrInt x，最后实际的类型取决于所依赖的值。
最后一个函数valToString的类型和getStringOrInt的类似，区别只在于它的第二个参数类型（而不是返回值类型）依赖于参数x的值。如果x是True，参数val的类型就是Int，又因为返回值类型是String，所以需要用cast函数做一个类型转换；若x等于False，参数val的类型和返回值类型一致，就可以直接返回。
有了一个直观的感受后，为了更详细准确地阐释依赖类型以及基于依赖类型的定理证明，本文会围绕一个叫做 Pie 的语言进行下去。Pie 是为了 Friedman 和 Christiansen 的《The Little Typer》这本书而被开发出来的包含依赖类型所有核心功能的一个小巧简洁（完整的参考手册只有不到 3000 字）的语言。
准备工作
Pie 是一个用 Racket 开发的语言，所以它的开发环境也是基于 DrRacket。具体的安装步骤很简单，可以参照官方网站上的指示。这里说几个让开发环境更易用的设置。一是 DrRacket 安装成功后可以在 View 菜单设置一下 layout 和 toolbar：
下图是设置之后的界面布局。左右两个编辑区域分别是定义和交互区，工具栏在最右侧垂直排列。在定义区输入变量、函数定义等程序的主体部分后，点击工具栏的绿色箭头（或者按快捷键 ⌘-R 或 Ctrl-R）来运行，这时右侧的交互区就变成一个基于当前程序的 REPL 环境。
再有就是可以打开 DrRacket 的 Preferences 界面（⌘-, 或 Ctrl-,），将 Background expansion 设置成 "with gold highlighting"：
这样就可以更容易地定位到程序中有问题的部分：
Pie 语言简介
Pie 的语法类似于 Lisp 的各种方言（Scheme，Racket 和 Clojure 等），也就意味着程序中括号的数量会比较可观。在 Pie 语言里，每个变量或函数在定义前都必须声明类型：
(claim age
Nat)
(define age
18)
这里是先声明变量age的类型为自然数Nat，再把它的值定义为18。Pie 的几个基础类型分别是，
- 自然数
Nat。表示所有大于等于 0 的整数。 - 原子
Atom。相当于 Lisp 中的 symbol 类型，或者也可以粗略的近似于大部分语言里的字符串。Atom的值由单撇号和一个或多个字母或连字符组成，例如'abc，'---和'Atom。 - 函数
(-> Type-1 Type-2 ... Type-n)。这里最后的Type-n是函数的返回值类型，其他的Type-1 Type-2 ...是参数类型。 - 全集
U。因为在 Pie 里所有的类型可以像值一样被计算和传递，所以它们本身也需要一个类型，这个类型就是U。U是除自身外所有类型的类型。
还有一些复合类型会在后面用到的时候再作详细解释。Pie 的每个类型都有对应的 constructor 和 eliminator。前者用来构造该类型的值；后者的用处是运用该类型的值所包含的信息来得到所需要的新值，如果把某种类型的值看作一个罐头的话，那它对应的 eliminator 就像一个起子，而且不同构造的罐头需要用到不一样的起子。
函数
函数的 constructor 拥有如下结构：
(lambda (x1 x2 ...)
e1 e2 ...)
x1 x2 ...是函数的参数，e1 e2 ...是作为函数体的一个或多个表达式，函数体的最后一个表达式的值同时也是函数的返回值。另外lambda关键字也可以用希腊字母λ来代替 3，让程序看起来更简洁。下面是一个完整的函数定义示例：
(claim echo
(-> Atom
Atom))
(define echo
(λ (any-atom)
any-atom))
这里先是声名这个函数的类型：接受一个Atom类型的值作为参数，然后返回一个Atom类型的值。接着就是函数echo的具体定义：无论传入什么Atom都原样返回。对于函数来说 eliminator 只有一个，那就是对函数的调用，只能借由这唯一的途径来使用定义好的函数。函数的调用语法是，(函数名或匿名函数 参数1 参数2 ...)：
> (echo '你好)
(the Atom '你好)
以>开头的一行表示这是在交互区输入的内容，下面紧跟着的是这行运行后得到的值。'你好前面的the Atom是对这个值的类型注解。对于在交互区输入的表达式，Pie 都会以 (the 类型 值) 的形式来显示它的值：
> 18
(the Nat 18)
Atom
对于Atom来说所有符合规则的值都是一个 constructor，而且Atom没有对应的 eliminator，因为每个值本身就是它的意义所在。
Nat
自然数Nat的 constructor 是zero和add1。zero顾名思义得到的是最小自然数零，而add1接受一个自然数n作为参数，得到一个比n大1的自然数。所以自然数 1、2、3 可以分别表示成(add1 zero)、(add1 (add1 zero))、(add1 (add1 (add1 zero)))。如果用归纳法来定义Nat的话，可以写作：
Nat ::= zero
Nat ::= (add1 Nat)
用这种方式定义出来的自然数又叫做皮亚诺数（Peano number）。当然这种表示方式写起来有些繁琐，所以 Pie 也提供了更便捷的语法：可以直接把自然数写作数字，例如zero和0、(add1 (add1 zero))和2都是等价的。对于自然数， Pie 提供了多个可供使用的 eliminator。具体使用哪个取决于要解决的问题。比如定义一个类型为(-> Nat Nat)的函数pred，规定它对于自然数0返回0，对于其他自然数返回比自身小一的数：
(claim pred
(-> Nat
Nat))
(define pred
(λ (n)
(which-Nat n
0
(λ (n-1)
n-1))))
在上述函数pred中，which-Nat的target是pred的参数n，base是0，step是函数(λ (n-1) n-1)。所以当n等于0时，which-Nat返回base的值，0；当n大于0或者说n等于(add1 n-1)时，which-Nat返回的就是(step n-1)的值，即参数n-1本身。
> (pred 10086)
(the Nat 10085)
> (pred 0)
(the Nat 0)
如果熟悉所谓的函数式语言，可以看出来which-Nat其实就是这些语言里的 pattern matching（虽然并不完全等同，后边会说到区别）。如果用 Idris 实现pred的话，会是这个样子：
pred : Nat -> Nat
pred Z = Z
pred (S k) = k
在 Idris 里，Z和S分别是Nat类型的两个 constructor，等同于 Pie 里的zero和add1。后两行的两个 pattern matching 的分支也对应于which-Nat的base和step。前面说到的which-Nat和 pattern matching 的区别指的是，在常规的 pattern matching 中可以对函数递归调用，而 Pie 并不允许用户定义的函数对自身的递归调用，这个限制的目的是为了保证所有的函数都是 total 的。举实现自然数加法运算的函数为例，在支持递归调用的语言比如 Idris 中可以这样实现（递归在最后一行）：
plus : Nat -> Nat -> Nat
plus Z m = m
plus (S k) m = S (plus k m)
如果 Pie 允许函数的递归调用，完全可以用which-Nat实现同样的逻辑：
(claim +
(-> Nat Nat
Nat))
(define +
(λ (n m)
(which-Nat n
m
(λ (n-1)
(add1 (+ n-1 m)))))) ; 错误: Unknown variable +
用rec-Nat来实现+函数同样可以把n作为target，n等于0时base的值应该为m，因为(+ 0 m)等于m：
(claim +
(-> Nat Nat
Nat))
(define +
(λ (n m)
(rec-Nat n
m
TODO)))
因为还没有决定step如何实现，可以在它的位置上暂时写上TODO。在 Pie 里可以用TODO替代程序中尚未实现的部分，Pie 还可以提示每个TODO应该是什么类型。如果运行上面的程序片段，会得到和TODO相关的信息：
n : Nat
m : Nat
------------
(→ Nat Nat
Nat)
横线上面的n和m是当前TODO所在的 scope 里所有的变量类型，下面是它本身的类型。从rec-Nat的定义可以知道TODO代表的step函数接受的第一个参数是比n小一的自然数（因为n是target），可以取名为n-1；另一个参数是把n-1作为新的target时递归调用rec-Nat的结果，其实也就是n-1与m的和，所以可以取名n-1+m：
(define +
(λ (n m)
(rec-Nat n
m
(λ (n-1 n-1+m)
TODO))))
此时TODO的类型变为了：
n : Nat
m : Nat
n-1 : Nat
n-1+m : Nat
-------------
Nat
从这个类型描述可以知道step函数体必须是一个值类型为Nat的表达式，这个表达式的值也是最终的结果，n与m的和。现在我们已经有了n-1与m的和，想得到n加m的话当然就是把n-1+m参数加一：
(define +
(λ (n m)
(rec-Nat n
m
(λ (n-1 n-1+m)
(add1 n-1+m)))))
这样就得到了完整的+函数的定义。为了加深对rec-Nat的理解，我们可以模拟一下解释器对(+ 2 1)的求值过程。当解释器遇到表达式(+ 2 1)时，首先会判断这是一个函数调用，所以第一步把函数名替换成实际的函数定义：
((λ (n m)
(rec-Nat n
m
(λ (n-1 n-1+m)
(add1 n-1+m))))
2 1)
然后将函数体中的n和m分别替换成2和1：
(rec-Nat 2
1
(λ (n-1 n-1+m)
(add1 n-1+m)))
因为target等于非零自然数2，也就是(add1 1)，所以rec-Nat的值就等于对step函数调用后的值（将step的函数体(add1 n-1+m)中的n-1+m替换成对rec-Nat的递归调用）：
(add1
(rec-Nat 1
1
(λ (n-1 n-1+m)
(add1 n-1+m))))
这时内层的rec-Nat的target参数等于(add1 zero)仍然不为零，所以继续将rec-Nat表达式替换成调用step所得到的值：
(add1
(add1
(rec-Nat 0
1
(λ (n-1 n-1+m)
(add1 n-1+m)))))
现在最里层的rec-Nat的target等于0，所以它的值就等于base的值1:
(add1
(add1
1))
这样就得到了最后的结果3。
柯里化
虽然前面介绍函数时说函数是可以接受多个参数的（(lambda (x1 x2 ...) e1 e2 ...)），但其实本质上 Pie 的函数只接受一个参数。之所以可以定义出接受多个参数的函数，是因为 Pie 的解释器会对函数作一个叫做 柯里化（currying） 的处理。比如这四个函数：
;; 接受两个 Atom 参数，返回值类型为 Atom
;; 声明类型和函数定义的形式一致
(claim currying-test1
(-> Atom Atom
Atom))
(define currying-test1
(λ (a b)
b))
;; 声明类型同上
;; 声明类型和函数定义的形式不一致
(claim currying-test2
(-> Atom Atom
Atom))
(define currying-test2
(λ (a)
(λ (b)
b)))
;; 接受一个 Atom 参数，返回一个类型为 (-> Atom Atom) 的函数
;; 声明类型和函数定义的形式不一致
(claim currying-test3
(-> Atom
(-> Atom
Atom)))
(define currying-test3
(λ (a b)
b))
;; 声明类型同上
;; 声明类型和函数定义的形式一致
(claim currying-test4
(-> Atom
(-> Atom
Atom)))
(define currying-test4
(λ (a)
(λ (b)
b)))
这几个函数无论是否有声明类型上的差异，还是声明和定义形式是否一致，在 Pie 的解释器看来都是完全相同的：
> currying-test1
(the (→ Atom Atom
Atom)
(λ (a b)
b))
> currying-test2
(the (→ Atom Atom
Atom)
(λ (a b)
b))
> currying-test3
(the (→ Atom Atom
Atom)
(λ (a b)
b))
> currying-test4
(the (→ Atom Atom
Atom)
(λ (a b)
b))
知道了这一点我们就可以运用所谓的 partial application 从已有的函数生成出其他“固定”了某些参数的值的新函数。比如可以从前述的加法函数+得到把参数加一的新函数：
(claim plus-one
(-> Nat
Nat))
(define plus-one
(+ 1))
> (plus-one 2)
(the Nat 3)
用了比较长的篇幅来介绍 Pie 的几个基础类型，接下来可以说一说 Pie 语言里的几种依赖类型了。
依赖于类型的类型：List
如果熟悉 Java 的泛型（generics）或者 ML 的多态（polymorphism）的话，应该会很容易理解 Pie 的 List 类型。在 Pie 中，若E是一个类型则(List E)是一个 List 类型，代表一类元素类型都是E的 List。(List Nat)、(List (-> Nat Atom))和(List (List Atom))都是 List 类型，但是(List 1)和(List '你好)不是合法的类型。
List 有两个 constructor：nil和:: 4。nil构造一个空 List；::接受两个参数e、es，如果e和es的类型分别为E和(List E)，则(:: e es)构造的是类型为(List E)比es多一个元素e的 List。List 类型可以用归纳法描述如下：
(List E) ::= nil
(List E) ::= (:: E (List E))
可以看出来 List 的 constructor 和Nat的很相似：nil对应于zero，::对应于add1。下面是构造一个(List Atom)的示例：
(claim philosophers
(List Atom))
(define philosophers
(:: 'Descartes
(:: 'Hume
(:: 'Kant nil))))
(claim length
(-> (List E) ; 错误: Not a type
Nat))
解释器会在第二行提示“Not a type”的错误，因为在它看来E没有被声明过是一个未知的变量，所以(List E)也就不是一个合法的类型。所以我们需要一个新表达式用来在类型声明中引入变量，这个表达式叫作Pi（在程序中也可以用希腊字母Π5 代替）。length的新的类型声明如下：
(claim length
(Π ((E U))
(-> (List E)
Nat)))
Pi表达式的第一个列表里可以写多个类型变量(Π ((x X) (y Y) ...) ...)，其中x、y是变量名，X和Y是变量的类型。length的类型声明里只需要一个变量E，因为E是 List 里元素的类型，所以E的类型是U。如果类比 Java 的泛型，
<E> int length(List<E> lst) {...}
可能会觉得Pi表达式也只是实现了类似的功能，但其实Pi可以做的更多。开头介绍的箭头型的函数类型只是Pi表达式的一个简写形式，所以Pi本质上声明的是一个函数，意味着列表里可以放入任何类型的变量。比如
(claim fun1
(-> Atom Nat
Atom))
也可以写成
(claim fun1
(Π ((a Atom)
(n Nat))
Atom))
只不过这里变量a和n没有在后面的类型声明里用到，所以写作箭头型的就足够。下面是用了Pi表达式后，完整的length定义：
(claim length
(Π ((E U))
(-> (List E)
Nat)))
(define length
(λ (E lst)
(rec-List lst
0
(λ (e es length-es)
(add1 length-es)))))
Π和箭头表达式组合在一起声明了一个接受两个参数返回一个Nat的函数，定义中对应的两个参数一个是类型为U的参数E，另一个是类型为(List E)的参数lst。函数体中只用到了第二个参数lst，把它作为target传给rec-List表达式。当lst为nil时长度为0；若lst可以表示为(:: e es)形式的非空 List，则step函数的第三个参数是表达式(rec-List es 0 step)的值，因为这个值其实就是es的长度，所以起名叫length-es。又因为es比lst少一个元素e，所以lst长度等于es的长度加一，即(add1 length-es)。
有了length就可以得到任意 List 的长度了：
> (length Atom philosophers)
(the Nat 3)
> (length Nat
(:: 1 (:: 2 (:: 3 (:: 4 nil)))))
(the Nat 4)
类似的也可以通过rec-List定义合并 List 的函数append：
(claim append
(Π ((E U))
(-> (List E)
(List E)
(List E))))
(define append
(λ (E)
(λ (start end)
(rec-List start
end
(λ (e es append-es)
(:: e append-es))))))
(claim existentialists
(List Atom))
(define existentialists
(:: 'Kierkegaard
(:: 'Sartre
(:: 'Camus nil))))
> (append Atom philosophers existentialists)
(the (List Atom)
(:: 'Descartes
(:: 'Hume
(:: 'Kant
(:: 'Kierkegaard
(:: 'Sartre
(:: 'Camus nil)))))))
假设我们没能正确地实现append，比如错误地定义了step：
(claim append-wrong
(Π ((E U))
(-> (List E)
(List E)
(List E))))
(define append-wrong
(λ (E)
(λ (start end)
(rec-List start
end
(λ (e es append-es)
append-es))))) ;; 错误地忽略了 e
解释器仍然会接受这个函数定义，因为从类型系统的角度来看append-wrong仍然是“正确”的，它确实返回了类型是(List E)的值，即使这个值不是我们所预期的：
> (append-wrong Atom philosophers existentialists)
(the (List Atom)
(:: 'Kierkegaard
(:: 'Sartre
(:: 'Camus nil))))
如果想让解释器帮助我们判断程序是否正确，只能通过某种形式的“测试”来实现：
(check-same Nat
(length Atom
(append-wrong Atom philosophers existentialists))
(+ (length Atom philosophers)
(length Atom existentialists)))
下面要介绍的这个新类型可以说是有长度属性的 List，和这个新类型相关的函数都可以借助参数和返回值的类型来自动实现类似于上面程序片段中的对于长度属性的检查。
依赖于值的类型：Vec
文章开头假想的那个 Java 的有长度属性的数组类型其实就是对 Vec 类型的模仿。Vec 类型写作(Vec E len)，其中E和 List 类型中的一样，是一个类型为U的值，代表所有元素的类型；而len是一个Nat类型的值，代表 Vec 的长度。所以开头的three-names可以声明为：
(claim three-names
(Vec Atom 3))
Vec 的 constructor 和 List 的非常相似，分别是vecnil和vec::，对应于 List 的nil和::。这样three-names可以定义为：
(define three-names
(vec:: '张三
(vec:: '赵四
(vec:: '成吉思汗 vecnill))))
在深入讨论 Vec 类型前需要再介绍另一个Nat类型的 eliminator，因为它与 Vec 类型有着非常密切的关系。仍然是通过一个例子来说明，假设定义一个函数repeat，它可以重复count次某个任意类型E的值e，返回的结果是一个长度为count、元素类型E且所有元素都是e的 Vec。这个函数声明如下：
(claim repeat
(Π ((E U)
(count Nat))
(-> E
(Vec E count))))
因为类型E和次数count在后面的类型声明中都会用到，所以被放在了Π表达式的参数列表里。表达式(-> E (Vec E count))指的是一个接受一个类型为E的值作为参数，返回一个(Vec E count)的函数。假设我们用已有的rec-Nat来实现的话，大概会这样写：
;; 一次失败的尝试😢
(define repeat
(λ (E count)
(λ (e)
(rec-Nat count
vecnil
(λ (c-1 repeat-c-1)
(vec:: e repeat-c-1))))))
但是问题是rec-Nat要求base、step以及整个rec-Nat表达式的值的类型必须一致，在上述定义中，repeat的声明类型即整个rec-Nat表达式的类型是(Vec E count)；base是类型为(Vec E 0)的vecnil；而step每次递归调用所返回的类型都不一样，在target从1到count变化的过程中，返回值也从(Vec E 1)变到(Vec E count)。所以解释器不会接受这个函数定义。
更强大的归纳式 eliminator
(Π ((n Nat))
(-> (motive n)
(motive (add1 n))))
它接受两个类型分别为Nat和(motive n)的参数，返回一个类型为(motive (add1 n))的值。step的第一个参数是比当前target小一的自然数n，第二个是把n作为新的target递归调用ind-Nat——(ind-Nat n motive base step)——后得到的值。因为(add1 n)等于当前的target，所以step的返回值类型(motive (add1 n))和整个ind-Nat表达式值的类型(motive target)也是相同的。现在可以着手用ind-Nat来实现repeat函数了。首先将count参数作为target传递给ind-Nat：
(claim repeat
(Π ((E U)
(count Nat))
(-> E
(Vec E count))))
(define repeat
(λ (E count)
(λ (e)
(ind-Nat count ; count 作为 target
TODO
TODO
TODO))))
接下来确定比较简单的base的值，当count为0时，repeat应该返回一个长度为0的(Vec E 0)，这样的 Vec 只有一个，就是vecnil：
(define repeat
(λ (E count)
(λ (e)
(ind-Nat count
TODO
vecnil ; 类型为 (Vec E 0) 的 vecnil 作为 base
TODO))))
又因为base的类型其实是由motive函数决定的，即(motive 0)。所以从base的类型可以反推出motive应该是一个接受一个自然数k作为参数，返回类型(Vec E k)的函数。这里需要注意motive返回的是类型(Vec E k)，而不是类型为(Vec E k)的值，换句话说motive返回的是类型为U的值(Vec E k)。
(define repeat
(λ (E count)
(λ (e)
(ind-Nat count
(λ (k) ; motive 函数
(Vec E k)) ; 返回的是类型
vecnil
TODO))))
有了motive之后，就可以知道step的类型了：
(Π ((c-1 Nat)) ; c-1 代表比 count 小一的自然数
(-> (Vec E c-1) ; 即 (motive c-1)
(Vec E (add1 c-1)))) ; 即 (motive (add1 c-1))
根据类型就可以确定step的函数定义中需要接受两个参数：
(define repeat
(λ (E count)
(λ (e)
(ind-Nat count
(λ (k)
(Vec E k))
vecnil
(λ (c-1 repeat-c-1)
TODO)))))
repeat-c-1参数代表的是把count减一后得到的自然数c-1作为新的target去递归调用ind-Nat所得到的类型为(Vec E c-1)的值。这个值比repeat要返回的(Vec E (add1 c-1))长度少一，又因为返回的 Vec 的所有元素都是e（repeat的参数之一），所以只要把e放到repeat-c-1里就得到了最终的结果：
(define repeat
(λ (E count)
(λ (e)
(ind-Nat count
(λ (k)
(Vec E k))
vecnil
(λ (c-1 repeat-c-1)
(vec:: e repeat-c-1))))))
所以当一个处理 Vec 类型的函数通过了类型系统检查的时候，我们就会对它的正确性有更多的信心。
通过repeat这个例子也可以看出来ind-Nat的用法和思路与rec-Nat非常接近，区别只在于rec-Nat中的base、step的第二个参数以及step的返回值的类型都是一样的，这个类型也是整个rec-Nat表达式值的类型；而对于ind-Nat来说，这三者的类型可能相同也可能不同，具体是什么类型取决于motive函数分别作用于zero、比target小一的自然数以及target本身时所得到的类型。从这一点也可以看出rec-Nat其实是更通用的ind-Nat的一个特例，所以可以用ind-Nat来实现rec-Nat：
(claim my-rec-Nat
(Π ((E U))
(-> Nat ; target 的类型
E ; base 的类型
(-> Nat ; step 的第一个参数的类型
E ; step 的第二个参数的类型
E) ; step 的返回值类型
E))) ; my-rec-Nat 的返回值类型
(define my-rec-Nat
(λ (E)
(λ (target base step)
(ind-Nat target
(λ (k) E) ; 这里的 motive 决定了 base、step 的参数
base ; 和返回值类型都是 E
step))))
归纳式 eliminator 之所以被这样称呼是因为它们包含了和数学中归纳式证明相类似的想法。如果要证明一个关于自然数的定理，首先证明 x = 0 的情况成立，然后假设 x = n - 1 时定理成立，如果可以从这个假设推出 x = n 时定理也成立，那么就可以肯定这个定理在自然数范围内都成立。同样的，如果我们告诉ind-Nat当target等于zero时表达式的值，以及当target等于(add1 n)时，如何从n所对应的结果得到(add1 n)所对应的结果，那么ind-Nat就可以得到所有自然数范围内的参数所对应的表达式的值，只不过首先需要通过motive参数指出任意一个Nat所对应的类型。Pie 语言中所有以 ind- 开头的 eliminator 都包含同样的思想，区别只在于target和step参数的类型。接下来再分别看一下 List 和 Vec 的归纳式 eliminator。
List 和 Vec 的归纳式 eliminator
(claim list->vec
(Π ((E U)
(lst (List E)))
(Vec E (length E lst))))
首先list->vec需要一个(List E)类型的参数，所以在这个参数之前要有一个类型为U的变量E，另外返回值类型中也会用到 List 类型的参数，这样就把lst参数也作为类型变量放到Π表达式的括号内。返回值类型中包含的表达式(length E lst)是用来表达转换前后长度相同的语义，这里的length是上文中实现的计算 List 长度的函数。下面是函数list->vec的实现：
(define list->vec
(λ (E lst)
(ind-List lst
(λ (xs) ; motive 返回与 List 类型的参数 xs
(Vec E (length E xs))) ; 长度相同的 Vec 类型
vecnil ; base 的类型为 (motive nil)，即 (Vec E 0)，只能是 vecnil
(λ (e es list->vec-es) ; list->vec-es 是参数 es 被转换后的结果
(vec:: e list->vec-es)))))
和使用ind-Nat时运用的归纳式思想一样，在使用ind-List的时候需要，
- 通过
motive定义如何从(List E)得到所需的类型，这里motive的参数xs对应一个元素类型为E，长度与xs相等的 Vec； - 通过
base参数指出当target等于nil时整个ind-List表达式的值，nil的长度为0，所以对应的 Vec 就是vecnil； - 通过
step函数告诉解释器，当target等于(:: e es)时如何从es对应的结果，也就是es所转换成为的list->vec-es，来得到(:: e es)所要转换成为的那个 Vec，可以很容易的知道就是(vec:: e list->vec-es)。
这样最终得到的就是一个可以把任意 List 转换成等价的 Vec 的函数。
> (list->vec Atom philosophers)
(the (Vec Atom 3)
(vec:: 'Descartes
(vec:: 'Hume
(vec:: 'Kant vecnil))))
在前面repeat的例子里展示过，Vec 类型使得类型系统可以在程序运行前就检测出导致长度不一致的一类错误。但是仍然有可能写出长度和类型都正确而实际值却不是所预期的错误程序。比如下面这个只是重复第一个元素的错误版list->vec：
(claim list->vec-wrong
(Π ((E U)
(lst (List E)))
(Vec E (length E lst))))
(define list->vec-wrong
(λ (E lst)
(ind-List lst
(λ (xs)
(Vec E (length E xs)))
vecnil
(λ (e es list->vec-es)
(repeat E (length E (:: e es)) e)))))
> (list->vec-wrong Atom philosophers)
(the (Vec Atom 3)
(vec:: 'Descartes
(vec:: 'Descartes
(vec:: 'Descartes vecnil))))
类型系统没能检测出这个错误，程序运行的结果也不是预期的。那么怎样才能检测出这类错误呢？一个可行的办法是，我们可以写出list->vec的“逆运算”vec->list，继而就可以让这俩个函数互相检验对方的正确性。vec->list的声明部分写作：
(claim vec->list
(Π ((E U)
(l Nat))
(-> (Vec E l)
(List E))))
(claim vec->list
(Π ((E U)
(l Nat))
(-> (Vec E l)
(List E))))
(define vec->list
(λ (E l)
(λ (vec)
(ind-Vec l vec
(λ (k xs)
(List E))
nil
(λ (l-1 e es vec->list-es)
(:: e vec->list-es))))))
有了vec->list之后要解决的问题是，如何用程序表达出“连续两次调用list->vec和vec->list仍然得到原先的 List”这个意思。我们现在知道的最接近这个需求的工具是check-same。比如下面检查的是对(List Atom)类型的philosophers接连应用list->vec和vec-list之后，内容不变：
(check-same (List Atom)
philosophers
(vec->list Atom 3
(list->vec Atom philosophers)))
不过这也只能验证对于philosophers来说，list->vec和vec-list两个函数是正确的。这个测试并不能保证这两个函数对于任何 List 或 Vec 都是正确的。这其实也是大多数语言中的单元测试所处的窘境，它们只能检验出某些错误的“存在”但是却没办法保证这类错误在任何情况下都“不存在”。有的测试工具也提供了一些方法来应对这个局限性，比如 ScalaTest 所提供的基于属性的测试方法，指的是用一个函数来表达测试对象应该包含的目标属性，然后结合内置的 generator 来模拟对测试对象在整个作用域内的测试。下面就是对一个分数实现类Fraction在整个作用域（所有可能的被除数、除数对）内的一个测试：
class Fraction(n: Int, d: Int) {
require(d != 0)
require(d != Integer.MIN_VALUE)
require(n != Integer.MIN_VALUE)
val numer = if (d < 0) -1 * n else n
val denom = d.abs
override def toString = numer + " / " + denom
}
forAll { (n: Int, d: Int) =>
whenever (d != 0 && d != Integer.MIN_VALUE
&& n != Integer.MIN_VALUE) {
val f = new Fraction(n, d)
if (n < 0 && d < 0 || n > 0 && d > 0)
f.numer should be > 0
else if (n != 0)
f.numer should be < 0
else
f.numer should be === 0
f.denom should be > 0
}
}
不过这里用到的forAll并不是真的对所有可能的n、d组合来生成测试（不然测试程序会无限期的运行下去），只是尽可能多得生成一些范围内有代表性的实例。虽然这类工具能让测试更可靠，但是它们仍然没有带给开发者对程序正确性的绝对信心。本文开头提到过，像 Pie 之类的支持依赖类型的语言提供了一个在逻辑上证明程序某些属性成立与否的途径，有了它我们可以让程序变得更可靠了。
定理证明
为了说明这个证明的方法，需要从 Pie 语言里表达相等关系的类型说起。在 Pie 语言里，表示x等于y的类型写作(= T x y)，其中T是x和y的类型。例如(= Nat (+ 1 1) 2)表示表达式(+ 1 1)和2的值相等。所以=类型也是一个依赖于值的类型。
构造一个=类型的值时用到的 constructor 是same。如果表达式e的类型是E，那么(same e)就是类型为(= E e e)的值。前例中的(= Nat (+ 1 1) 2)类型的值可以写作(same 2)，因为解释器对(+ 1 1)的求值结果也是2。那么(= Nat 3 4)是不是一个合法的类型呢？答案是是的，但是我们没办法构造一个该类型的值：
在定义中放入(same 4)也会得到类似的错误提示。如果套用传统编程语言对类型的定位来理解=类型的话，可能会觉得它有些怪异，因为=类型并不像前面的Nat或Vec类型，它看起来不像是一类值的集合。所以不如换一个角度来看待=类型，可以把它看作一个陈述或命题。这样就可以把(= Nat (+ 1 1) 2)读作“(+ 1 1)和2是两个相等的自然数”。这时=类型的值就变成它所代表的那个命题的一个证明。那么为什么(same 2)是(= Nat (+ 1 1) 2)的一个证明呢？这是因为我们举证出了一个值2，它既等于(+ 1 1)也等于2。同理，不存在(= Nat 3 4)类型的值也是因为我们没法找到一个可以证明3等于4的证据。像这种通过举证来证明的方法在数学中被叫作构造式证明（Constructive Proof）6。
全称量词
有了这个看待类型的全新角度后，其实我们可以把任意类型都看作一个命题。比如Atom就是一个命题，而任何一个Atom类型的值都是它的证明，只不过这个命题的证明对我们来说没有多大的用处。而让我们感兴趣的是把Π表达式与=类型结合所得到的一类命题。因为=是依赖类型，所以可以放在Π表达式里，此时Π可以被看作是全称量词，整个表达式就变成了一个全称命题。比如下面这个声明：
(claim 1+=add1
(Π ((n Nat))
(= Nat (+ 1 n) (add1 n))))
可以把1+=add1的类型读作，“对于任意一个自然数n，(+ 1 n)与(add1 n)的值是两个相等的自然数”。这样声明的变量1+=add1代表的就是对命题的陈述。那么要如何证明这种全称命题？其实证明的过程也就是实现由Π表达式声明的函数的过程。
(define 1+=add1
(λ (n)
TODO))
这里TODO代表的是=类型的返回值，因为=类型的 constructor 只有same，所以TODO是一个same表达式，现在的问题是应该在same里放入什么样的既等于(+ 1 n)又等于(add1 n)的表达式。回忆一下+函数的定义：
(define +
(λ (n m)
(rec-Nat n
m
(λ (n-1 n-1+m)
(add1 n-1+m)))))
可以看出来(+ 1 n)经过一次递归调用rec-Nat后可以简化成(add1 n)，所以应该用(same (add1 n))来替换TODO。其实如果看一下解释器输出的TODO类型提示，已经可以知道same里应该放入(add1 n)：
c8.pie:28.4: TODO:
n : Nat
-------------
(= Nat
(add1 n)
(add1 n))
这样1+=add1的定义，或者说对1+=add1这个命题的证明最后就是这个样子：
(claim 1+=add1
(Π ((n Nat))
(= Nat (+ 1 n) (add1 n))))
(define 1+=add1
(λ (n)
(same (add1 n))))
那么应该怎样来证明这个调换了1和n的位置后所得到的命题呢？前面曾经提过归纳式 eliminator（ind-Nat、ind-List 等）的用法和数学上的归纳式证明非常相似，而对于命题+1=add1我们就要真的用ind-Nat来进行归纳式证明了。对于所有的ind-eliminator 的使用第一步基本都是要写出 motive 函数，这里因为最终要得到是(= Nat (+ n 1) (add1 n))类型的值，如果把n作为ind-Nat的 target 的话，那我们需要的 motive 函数显然就是(λ (k) (= Nat (+ k 1) (add1 k)))，这样 base 的类型就是 motive 的参数k等于0时的返回值，(= Nat (+ 0 1) (add1 0))，简化得到(= Nat 1 1)，所以 base 的值就是(same 1)。包含了 motive 和 base 的定义如下：
(claim +1=add1
(Π ((n Nat))
(= Nat (+ n 1) (add1 n))))
(define +1=add1
(λ (n)
(ind-Nat n
(λ (k)
(= Nat (+ k 1) (add1 k)))
(same 1)
TODO)))
接下来需要写出 step 函数的定义。回忆一下ind-Nat中 step 的类型是：
(Π ((n-1 Nat))
(-> (motive n-1)
(motive (add1 n-1))))
其中的n-1是比 target 小一的数，把motive替换成写好的定义后得到的 step 的类型就是：
(Π ((n-1 Nat))
(-> (= Nat (+ n-1 1) (add1 n-1))
(= Nat (+ (add1 n-1) 1) (add1 (add1 n-1)))))
如果从求值的角度来看，step 的类型是说接受两个类型为Nat和=的参数得到另一个=类型的的值。不过我们还可以继续从定理证明的角度来解释这个类型，这时可以把->类型看作是一个“如果...那么...”的陈述句。这样整个类型就可以读作，“对于任意自然数n-1，如果(+ n-1 1)等于(add1 n-1)，那么(+ (add1 n-1) 1)也等于(add1 (add1 n-1))”，这其实就是数学上的归纳证明，所以对 step 函数的实现也是在完成归纳证明的第二步：从假设推导出要证明的结论。
另外要说的一点是返回值类型中的(+ (add1 n-1) 1)这一部分其实还可以进一步简化：根据+函数的定义可以把add1拿到最外层，变成(add1 (+ n-1 1))。为了更容易得实现 step，我们把它作为一个独立的函数来定义（返回值类型变成前述简化后的形式）：
(claim step-+1=add1
(Π ((n-1 Nat))
(-> (= Nat (+ n-1 1) (add1 n-1))
(= Nat (add1 (+ n-1 1)) (add1 (add1 n-1))))))
(define step-+1=add1
(λ (n-1 +1=add1-n-1)
TODO))
接下来要解决的问题就是，怎样从类型为(= Nat (+ n-1 1) (add1 n-1))的+1=add1-n-1推导出(= Nat (add1 (+ n-1 1)) (add1 (add1 n-1)))这个命题。观察一下可以发现这两个=类型或者说命题的唯一区别是后边两个相等的表达式分别比前面的两个多了一个add1。所以这相当于在证明如果(= Nat x y)那么(= Nat (add1 x) (add1 y))，从直觉来判断这一定是成立的，如果两个自然数相等，那么各自加一后仍然相等。但是要如何在 Pie 语言里表达这样的等价关系？这里我们要用到的是=类型的其中一个 eliminator，cong，它是 congruent（一致）的缩写。
用cong来实现step-+1=add1的话，我们就可以把(= Nat (+ n-1 1) (add1 n-1))类型的+1=add1-n-1作为 target，再把一个给任意自然数加一的函数当作cong的第二个参数，这样最后cong的返回值就是我们想要的(= Nat (add1 (+ n-1 1)) (add1 (add1 n-1)))这个命题的证明：
(claim step-+1=add1
(Π ((n-1 Nat))
(-> (= Nat (+ n-1 1) (add1 n-1))
(= Nat (add1 (+ n-1 1)) (add1 (add1 n-1))))))
(define step-+1=add1
(λ (n-1 +1=add1-n-1)
(cong +1=add1-n-1 (+ 1))))
请注意这里我们用到了 Pie 的函数 currying 的特性，(+ 1)就是一个把任意自然数加一的函数。这样我们就完成了对命题的证明：
(claim +1=add1
(Π ((n Nat))
(= Nat (+ n 1) (add1 n))))
(define +1=add1
(λ (n)
(ind-Nat n
(λ (k)
(= Nat (+ k 1) (add1 k)))
(same 1)
step-+1=add1)))
可以看到，在 Pie 语言里对命题的证明就是一个实现类型定义的过程，只要写出了类型系统可以接受的实现，也就完成了对命题的证明。解释器对证明的解释是一个静态的过程，我们并不需要去“运行”写好的定义。
有了这些了解后，我们可以着手解决上节结尾处留下来的关于vec->list和list->vec的正确性证明了。这个命题可以陈述为，“对于任意一个 List，连续应用函数list->vec和vec->list后得到的结果和它本身相等”。和这个命题等价的类型声明是：
(claim list->vec->list=
(Π ((E U)
(lst (List E)))
(= (List E)
lst
(vec->list E
(length E lst)
(list->vec E lst)))))
前面证明+1=add1的时候，因为是关于自然数的定理，所以用的是ind-Nat。现在要证明的是一个关于 List 的命题，自然会选择ind-List作为入手点。因为lst参数应该作为 target，这样只需要把返回值类型中的lst都替换成 motive 函数的参数xs就可以得到 motive 的定义：
(λ (xs)
(= (List E)
xs
(vec->list E
(length E xs)
(list->vec E xs))))
继而可以知道 base 的类型，即(motive nil)的值是：
(= (List E)
nil
(vec->list E
(length E nil)
(list->vec E nil)))
这个表达式可以简化成(= (List E) nil nil)。所以应该用(same nil)作为 base 的值。有了 motive 和 base 之后list->vec->list=的定义如下：
(claim list->vec->list=
(Π ((E U)
(lst (List E)))
(= (List E)
lst
(vec->list E
(length E lst)
(list->vec E lst)))))
(define list->vec->list=
(λ (E lst)
(ind-List lst
(λ (xs)
(= (List E)
xs
(vec->list E
(length E xs)
(list->vec E xs))))
(same nil)
TODO)))
接下来需要确定 step 函数的类型及定义。ind-List的 step 参数类型是：
(Π ((e E)
(es (List E)))
(-> (motive es)
(motive (:: e es))))
把motive替换成我们写好的定义后得到的类型是：
(Π ((e E)
(es (List E)))
(-> (= (List E)
es
(vec->list E
(length E es)
(list->vec E es)))
(= (List E)
(:: e es)
(vec->list E
(length E (:: e es))
(list->vec E (:: e es))))))
这个类型乍看起来比较复杂，直接证明的话可能会觉得无从下手。我们可以试着简化一下最后的返回值类型。根据length函数的定义，可以知道(length E (:: e es))其实等于(add1 (length E es))；同样的，(list->vec E (:: e es))表达式也可以简化成(vec:: e (list->vec E es))。这样转换后的返回值类型就变成了：
(= (List E)
(:: e es)
(vec->list E
(add1 (length E es))
(vec:: e (list->vec E es))))
最后再根据vec->list的定义，把这个类型进一步简化成：
(= (List E)
(:: e es)
(:: e
(vec->list E
(length E es)
(list->vec E es))))
把这个结果带回 step 的类型中，就得到了简化后的 step 类型：
(Π ((e E)
(es (List E)))
(-> (= (List E)
es
(vec->list E
(length E es)
(list->vec E es)))
(= (List E)
(:: e es)
(:: e
(vec->list E
(length E es)
(list->vec E es))))))
现在从假设（->的参数）到结论（->的返回值）的途径变得更明显了：分别把元素e加到假设中的es和(vec-list ...)表达式的前面。所以仍然可以借助cong来写出 step 的定义：
(λ (e es =-es)
(cong =-es
(λ (xs) (:: e xs))))
所以我们需要用the表达式来加入一个类型提示：
(λ (e es =-es)
(cong =-es
(the (-> (List E) (List E))
(λ (xs) (:: e xs)))))
这样我们就写出了完整的对于list->vec->list=命题的证明：
(claim list->vec->list=
(Π ((E U)
(es (List E)))
(= (List E)
es
(vec->list E
(length E es)
(list->vec E es)))))
(define list->vec->list=
(λ (E lst)
(ind-List lst
(λ (xs)
(= (List E)
xs
(vec->list E
(length E xs)
(list->vec E xs))))
(same nil)
(λ (e es =-es)
(cong =-es
(the (-> (List E) (List E))
(λ (xs) (:: e xs))))))))
类型系统不再接受这个证明了，虽然错误消息比较抽象，但至少能看出来如果函数定义错误的话，类型系统就会拒绝我们对定理的证明。
存在量词
上节说了如果把类型看作定理的话，Π就相当于全称量词。那么谓词逻辑中的存在量词在 Pie 的类型中是如何表达的呢。先介绍一个新的类型Pair。从名字就可以看出来，一个Pair类型的值由两个值组成，这两个值的类型可以相同也可以不同。Pair类型可以写作(Pair A D)，其中A是第一个元素的类型，D则是第二个的类型。构造一个Pair用到的 constructor 是cons:
(claim a-pair
(Pair Nat Atom))
(define a-pair
(cons 5 'men))
另外Pair有两个 eliminator，car和cdr，可以分别用来得到第一个和第二个元素：
> a-pair
(the (Pair Nat Atom)
(cons 5 'men))
> (car a-pair)
(the Nat 5)
> (cdr a-pair)
(the Atom 'men)
就像Π表达式是->类型的一个更一般的表现形式一样，Pair也有一个更通用的类型表达式Sigma，也可以简写成希腊字母Σ7。Σ类型表达式的用法是(Σ ((x A1) (y A2) ...) D)，其中x和y是两个变量，可以出现在类型D中。当Σ和=类型一起使用时，我们就可以把Σ看作是存在量词。例如这个类型：
(Σ ((name Atom))
(= Atom name 'Jack))
可以把它读作，“存在一个Atom类型的值name，它的值等于'Jack”。这个命题的证明也很简单，和'Jack相等的Atom值也只有'Jack：
(cons 'Jack (same 'Jack))
里面的same是用来构造=类型的值，cons是用来构造Σ表达式所声明的Pair类型的值，这个值也是这个存在命题的证明。
有了存在量词Σ，我们可以用它来表达更多有意思的命题了，比如可以用定理来表示某个自然数是否是偶数。回想一下数学书上对偶数的定义：能被 2 整除的数叫做偶数。如果直接套用这个定义的话我们首先需要实现一个针对自然数的除法函数，不过也可以换个思路，能被 2 整除也意味着这个自然数等于另一个数与 2 的乘积，如果把乘法换成加法的话，就是另一个数与自身的和。所以这个偶数命题可以表达为，“如果自然数 n 是偶数，那么存在另一个数 m 使得 n 等于 m + m”。这样“0 是偶数”就可以用类型写成：
(Σ ((m Nat))
(= Nat 0 (+ m m)))
我们可以进一步把类型中的0抽象成一个函数参数，来得到一个生成“某个自然数是偶数”这个定理的函数：
(claim Even
(-> Nat U))
(define Even
(λ (n)
(Σ ((half Nat))
(= Nat n (+ half half)))))
因为Even接受一个自然数类型的参数n，返回一个关于n的定理（n是偶数），而定理即类型，所以Even也是一个生成类型的函数，这就需要在声明中把返回值类型写作U，而在函数定义中才返回一个Σ表达式。现在就可以把“0 是偶数”这个命题声明为：
(claim zero-is-even
(Even 0))
证明zero-is-even这个命题就是去构造一个(Σ ((half Nat)) (= Nat 0 (+ half half)))类型的值。因为0的一半还是0，所以它的证明是：
(claim zero-is-even
(Even 0))
(define zero-is-even
(cons 0 (same 0)))
同理，“10 是偶数”这个命题的证明可以写作：
(claim ten-is-even
(Even 10))
(define ten-is-even
(cons 5 (same 10)))
我们还知道把任意一个偶数加 2 得到的仍然是偶数，那么如何证明这个定理呢？先写出它的类型声明：
(claim +two-even
(Π ((n Nat))
(-> (Even n)
(Even (+ 2 n)))))
要证明这个命题，就得想办法从(Even n)类型也就是(Σ ((half Nat)) (= Nat n (+ half half)))类型的值得到(Even (+ 2 n))类型即(Σ ((new-half Nat)) (= Nat (+ 2 n) (+ new-half new-half)))类型的值。这两个类型里的half和new-half是有一定关联性的，想一下会发现new-half其实等于(add1 half)，因为偶数加 2 后的一半比原来的一半大一。所以返回值的cdr部分的等式可以进一步写成(= Nat (+ 2 n) (+ (add1 half) (add1 half)))。下面是证明的开头部分：
(define +two-even
(λ (n)
(λ (even-n) ; (Σ ((half Nat)) (= Nat n (+ half half)))
(cons (add1 (car even-n)) ; (car even-n) 就是 (Even n) 中的 half
TODO)))) ; (= Nat (+ 2 n) (+ (add1 half) (add1 half)))
如果对比一下(cdr even-n)的类型(= Nat n (+ half half))和TODO的类型(= Nat (+ 2 n) (+ (add1 half) (add1 half))，会发现其实后者其实就是把前者的两个加数分别加 2 后得到的（两个(add1 half)相加相当于把(+ half half)整个加 2）。这样看起我们可以用cong从(cdr even-n)来得到期望的类型的值：
(define +two-even
(λ (n)
(λ (even-n)
(cons (add1 (car even-n))
(cong (cdr even-n) (+ 2)))))) ; 错误：类型不匹配
(claim lift-right-add1
(Π ((n Nat)
(m Nat))
(= Nat (add1 (+ n m)) (+ n (add1 m)))))
这里=类型的 from 部分的add1在+的外面，to 部分的add1则在第二个加数的前面，如果 from 和 to 相等也就意味着第二个加数前的add1是可以提到+函数外层的。这是个关于自然数的命题，可以用ind-Nat来证明：
(define lift-right-add1
(λ (n m)
(ind-Nat n
(λ (k)
(= Nat (add1 (+ k m)) (+ k (add1 m))))
(same (add1 m))
(λ (n-1 lra-n-1) ; (= Nat (add1 (+ n-1 m)) (+ n-1 (add1 m)))
TODO)))) ; (= Nat (add1 (+ (add1 n-1) m)) (+ (add1 n-1) (add1 m)))
这里为了让证明更简单，选择把第一个参数n作为 target。注释中分别写出了lra-n-1和TODO的类型，TODO的类型可以通过把两个n-1前面的add1都提到最外层进一步简化成(= Nat (add1 (add1 (+ n-1 m))) (add1 (+ n-1 (add1 m))))，这样我们就又可以用cong来证明了：
(define lift-right-add1
(λ (n m)
(ind-Nat n
(λ (k)
(= Nat (add1 (+ k m)) (+ k (add1 m))))
(same (add1 m))
(λ (n-1 lra-n-1) ; (= Nat (add1 (+ n-1 m)) (+ n-1 (add1 m)))
(cong lra-n-1 (+ 1)))))) ; (= Nat (add1 (add1 (+ n-1 m))) (add1 (+ n-1 (add1 m))))
最后当把蓝色的部分传递给 motive 后，得到的就是我们要证明的命题（箭头 4 所指），而replace表达式的返回值就是这个命题的证明。从逻辑上来理解replace可能会更容易一些，它表达的想法其实就是，如果我们有两个等价的命题，target 的 from 和 to，如果能给出 from -> U（(motive from)）这个命题的证明（replace的 base），那么就可以得到 to -> U（(motive to)）这个命题的证明。现在我们有了+two-even的证明的最后一块拼图了：
(claim +two-even
(Π ((n Nat))
(-> (Even n)
(Even (+ 2 n)))))
(define +two-even
(λ (n)
(λ (even-n) ; (Σ ((half Nat)) (= Nat n (+ half half)))
(cons (add1 (car even-n))
(replace (lift-right-add1
(add1 (car even-n))
(car even-n))
(λ (k)
(= Nat (+ 2 n) k))
(cong (cdr even-n) (+ 2)))))))
这段程序里的(car even-n)是(Even n)类型中的half，(cdr even-n)是(Even n)中的等式。而(lift-right-add1 (add1 (car even-n)) (car even-n))其实就是把中间定理lift-right-add1里的n和m分别换成(add1 (car even-n))和(car even-n)。
费尽辛苦终于得到了命题+two-even的证明，不过这份“辛苦”也许并不是很必要 😅。 像前面提到的，这个证明的困难根源于+函数的第二个参数如果是(add1 ...)的形式，这个add1是没法拿到+外面的。那么如果我们换一种方式定义Even，使得+不再出现，是不是+two-even也会变得更加容易证明呢？比如我们可以定义一个函数double：
(claim double
(-> Nat Nat))
(define double
(λ (n)
(rec-Nat n
0
(λ (n-1 double-n-1)
(+ 2 double-n-1)))))
这个定义递归地遍历参数n中的每个add1，然后将其替换成两个add1，所以最终结果就是一个二倍于参数n的自然数。接下来用double来定义一个新的Even-with-double：
(claim Even-with-double
(-> Nat U))
(define Even-with-double
(λ (n)
(Σ ((half Nat))
(= Nat n (double half)))))
Even-with-double表达的想法和Even是一致的，区别只在于前者用的double实现，而后者用的是+。现在对基于Even-with-double的命题+two-even的证明就变得简单了多：
(claim +two-even-with-double
(Π ((n Nat))
(-> (Even-with-double n)
(Even-with-double (+ 2 n)))))
(define +two-even-with-double
(λ (n)
(λ (even-n)
(cons (add1 (car even-n))
(cong (cdr even-n) (+ 2))))))
可以看到这次不再需要用到replace，因为根据定义，(double (add1 half))可以直接变为(add1 (add1 (double half)))，这样表达式(cong (cdr even-n) (+ 2))的类型也就和期望的返回值类型一致了。所以可以看出来，不同的命题表达形式会影响到证明的难易程度。一般来说，选择能让参数“更快”得缩减到最简形式的函数来定义命题的话，会使证明更简单。
结尾
到这里本文对 Pie 语言中的定理证明的介绍已经完结，这篇文章也接近尾声了。其实最开始只是想写一篇《The Little Typer》的读后感，结果慢慢地发展（啰嗦）到了这么长。如果读过本文升起了一丝对依赖类型或定理证明的兴趣，强烈推荐继续读一下《The Little Typer》这本书，它远比本文有趣的多，而且还有很多有意思的概念这里限于篇幅也没办法一一介绍。如果想了解依赖类型的一些更“实际”的应用场景，可以看一下本文开头所提的 Idris 语言，以及该语言作者的书《Type-Driven Development with Idris》。另外，如果想从更理论的方向掌握定理证明的话，这本在线的教科书《Software Foundations》，以及配套的编程语言 Coq 会是个不错的选择。
