NuPRL 中的证明--从一到CTT
本文假设读者已经装了 NuPRL5 的 VM/要到了帳號并照著 http://nuprl.org/html/02cucs-NuprlManual-02overview.pdf 做基操。 这是向略懂 dependent type 的人的 NuPRL 教程，介紹这一最神/传奇的定理证明器。你不需要会 Haskell，但是至少要能理解 untyped lambda calculus，最好会点 OCaml/SML，最理想是 LCF ML，因为这是 NuPRL 的 Tactic 语言，而且它沒正式的 language report。Lisp 麻，会用 Emacs 程度就可以了，在 NuPRL 里几本用不上。 这文章只能向有 Agda/Coq/HOL/PVS/Metamath 经验的介绍下 NuPRL 了，因为完全 normie 的话像我一样出见 NuPRL 怕是不太可能有过了。 Equality in CTT 我们先来看 equivalence。不好意思让你们失望了，NuPRL 里沒有 ADT。所以 NuPRL 的 $a = b \in T$ 是个 primitive，如果 a 和 b 不等就是个空集，相等则有唯一成员 $*$ ，相当于 unit type。 值得一提的是，在 Agda 用的 ITT 中，一个 value 只能和自己相等，但在 CTT，因为有 quotient type 的概念，你还可以定义一个类型使两个不同的 value 相等。...