Proof Assistant

虽然说是看看 cedille, 不过主要是因为用 cedille 写这篇內容会比较方便了。这篇主要介紹的是 MLTT 70, 又被稱為 Type : Type，只要用 dependent function type 就可以 encode higher order logic。 首先就是 well known 的 dependent function type 对应 universal qualifier。之前的 LdBeth：NuPRL 中的证明–从一到CTT 中提到的 indexed family of intersection type 也对应 universal qualifier ，不过生成的 witness 会不同。在 Cedille 中 indexed intersection 用 $\forall$ ，dependent function 用 $\Pi$ 表示。 Conjunction 可以表为如下，★ ➔ ★ ➔ ★ 是 kind， $\forall P.(A \rightarrow B \rightarrow P)\rightarrow P$ 意为对任意命題 $P$ 在有 $A \rightarrow B \rightarrow P$ 时 $A \wedge B$ 可以证明 $P$ 。...

MetaPRL 的修理告一段落了。在这篇文章里我来介紹一下它用起來大概是什么感觉的。 MetaPRL 不是像 Agda/Lean 那样直接写 proof script 然后 type check，也不是 HOL 那样完全在 repl 里做 interactive 操作，而是一半一半：proposition 先全写在文件里，编译成 rewrite abstract machine 后，link 到 Toplevel 程序，再用 repl 来进行 interactive proof，或者查阅，也可以 print 到 html 或 latex。 MetaPRL 中 proposition, tactic, inference rule 之间没有分別。primitive inference rule 就是不需要证明的 tactic，proposition 就是具有证明的 inference rule。因为用的是类似 sequent calculus 的 language，所以能定义表现力强于其它 proof assistant 里用 lemma 或 tactic 的 metatheorem。这一点原版的 NuPRL 也只是能自定义 inference rule 而不能给出 conservative extension 的证明。比如 显然易见，对形式为 $\Gamma, x:\mathbb{B}, \Delta[x] \vdash C[x]$ 的 goal 应用这个 tactic，就会生成 $\Gamma, \Delta[True] \vdash C[True]$ 和 $\Gamma, \Delta[False] \vdash C[False]$ 两个 goal。在 Agda 里这要用 dependent pattern match, 在 HOL 要用 primitive inference rule compose tactic，而在 MetaPRL 里这只是个能证明的 theorem，而且做为 tactic 没有 HOL tactic 必須要用 primitive inference rule 的 overhead。...

这一篇开头讲一点 constructive real analysis。 Intuitionistic mathematics 中，实数用一个不断提高近似精度的无穷序列(Cauchy Sequence) 定义。 即 $\mathbb{R} =_{\it def} \{q:\mathbb{N}^+\rightarrow \mathbb{Q}\;|\; \forall n,m:\mathbb{N}^+ .|q_n-q_m|\leq n^{-1}+m^{-1} \}$ 这样的无穷的序列就是 free choice sequence 中的一种，表现出来是个 $\mathbb{N}^+ \rightarrow \alpha$ 的 function type。在这里 $\alpha \simeq \mathbb{N}$ ，即和自然数一一对应，众所周知地，有理数滿足这一性质。1 显然地，引入 choice sequence 的概念时，choice sequence 可以分成三种。 一种为 lawlike，即可以用某个 algorithm 表示的。 第二种为 lawless，是完全无序的。 第三种是由前两种 choice sequence 混合得到的，是为 mix。 注意即使是 lawless sequence，也符合 function 的性质，即 $\forall a. f(a) = f(a)$ ，也就是已经生成的数是不会变更了。 尽管 choice sequence 是无限的，但明显地，任何有限的 sequence 同时是无限个 choice sequence 的初始部分。...

本次要用 CTT 来写 Leftpad1，以说明即使不能实际运行 NuPRL 仍是个很好的 programming logic？(因为如下证明我是直接写的，没在 NuPRL 里跑) Takes a padding character, a string, and a total length, returns the string padded to that length with that character. If length is less than the length of the string, does nothing. 问題到手，首先定义的是 string 的 axioms $$\forall x: \mathbb{N}. Str(x) \in Type\\C \in Type\\ \forall x: \mathbb{N}, y: \mathbb{N}_x, a : Str(x). a\ !!\ y \in C\\ \forall x: \mathbb{N}, a : Str(x)....

上一篇 LdBeth：NuPRL 中的证明{x:N|2<x<3}–virtual evidence Constructive proof assistant 有个需求， 千里冰封 你懂吗：dependent type 下的类型推导 (meta variables) 比如 Agda 中 id' : forall (x : Prop) -> x -> x id' _ x = x 的第一个参数是不参与计算的，就可以写成 implicit argument id : forall {x : Prop} -> x -> x id x = x 在用了 implicit argument 以后，id 就是个 polymorphic function。 NuPRL 是如何实现这样的功能的呢。众所周知 universal qualification 是用 dependent function type (Pi type) 实现的。 $\forall x:\mathbb{P}. P(x) == \prod_{x:\mathbb{P}}{P(x)}$...

上一篇 LdBeth：NuPRL 中的证明 (二) – 我从来不写递归的 这篇的主要內容是 Virtual Evidence: A Constructive Semantics for Classical Logics 和 Constructive Reading of Classical Logic 的导读。 也算是第一次展示了下 NuRPL 中的证明，順帯引入 squash type 的概念。 MLTT Agda 中要获得 LEM 得 posutulate （防止你们说 CubicalTT）。众所周知这样 p 出来的 LEM 虽然和 MLTT 相容，但还是沒有 computational meaning 的，这样的 classical logic 是沒有灵魂的。 那 NuPRL 是怎么解決这个的呢？ Recall, refinment type OR subtyping in NuPRL $\{x:A\ |\ P(x) \}$ it is easy to get non dependent form...

图文无关。 上一篇文章 LdBeth：NuPRL 中的证明–从一到CTT 上一篇讲了 CTT 中的一些类型。dependent function, dependent product, dependent record, universe 这些因为和 ITT 的沒什么区別，就默认读者已经会了。CTT 特色的 dependent intersection 和 dependent union 因为应用范围超出了基础，就先不讲了。 General Recursion considered K Also, in some other type systems, general recursion is not expressible, and such structural recursion operations must be built in. 在 Agda 中，众所周知是用写程序來证明的，tc 过了相当于证明过了。然而 NuPRL 因为 undecidable type checking 的性质，除了程序以外，证明还包括了 tc。 比如吧，在 Agda 里要证 $x\leq x!$ ，就要先写 ! (factorial) 的定义，写完了以后，在使用 factorial 的定义之前，还要做两件事: 给它一个能过 tc 的类型声明，并且证明 termination。...

本文假设读者已经装了 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 相等。...