Curry Howard Isomorphism -> (Leibniz Equality * Programming By Refinement)

Abstract：这文章旨意用Coq介绍一下Leibniz Equality，并慢慢引出Curry Howard Isomorphism。

前置知识：Haskell

首先，一些设置：

{-# LANGUAGE MonomorphismRestriction, Rank2Types #-}

module Main (
    main
) where
import Prelude hiding(EQ)

main :: IO ()
main = return ()

会给出一定的Haskell代码以辅助理解Coq。

Set Implicit Arguments.
Set Universe Polymorphism.

第零行开启Coq中的隐式参数。

第一行开启了Universe Polymorphism，详情见Universes，The Coq Proof Assistant，Girard悖论是什么？ - 雾雨魔理沙的回答 - 知乎。不知道这是啥不会影响你的阅读。

当我们认为两个Type相等的时候，我们在说什么？

Monad的创始人（雾，此Monad非彼Monad，不过玄乎程度有过之而不及）Leibniz给出了一个很优雅的解释：当A=B的时候，如果一个命题为真，把里面的任意A替换成B，依然为真。用更formal的话说，

Given any x and y, x = y if and only if, given any predicate P, P(x) if and only if P(y).

-Equality (mathematics)

用代码表示，就是：

Definition EQ (x y: Type) := forall (p: Type -> Type), ((p x -> p y) * (p y -> p x)). (*这是Comment*) (*为了方便阅读，p x y都显式地标出了类型。*)

换成haskell代码，这是：

newtype EQ x y = EQ {unEQ :: forall p. (p x -> p y, p y -> p x)}

你现在也许在困惑：什么叫做‘用代码表示一个命题’？

我们不严谨的定义是：如果一个类型有值，当且仅当一个命题是定理，这个类型表示这个命题。这时候，这个类型的值就表示了这个命题的证明。

相对应的，如果一个命题不是定理，这个命题对应的定理就没有值-换句话说，同构于bottom type，一个没有任何constructor的type。

我们现在看看，我们这段代码‘代不代表’Leibniz给出的Equality（简称Leibniz Equality）。

假设“P(x)当且仅当P(y)”。

现在有两种情况：P(x)，P(y)皆为定理，或皆不是定理。

如果是前者，p x，p y都有值（我们可以构造出p x, p y）。所以，我们可以通过忽略传进来的参数，构造出p x -> p y, p y -> p x。然后，我们可以构造出p x -> p y跟p y -> p x的pair。

如果是后者，p x，p y都同构于bottom type。但是我们可以从bottom type得出一切-如果没明白什么回事，这样想：如果要从有两constructor的sum type返回一个类型A的值，需要进行pattern match，对得出的两个case皆返回A。如果要从有一个constructor的top type返回一个类型A的值，需要进行pattern match，对得出的一个case返回A。如果要从有零个constructor的bottom type返回一个类型A的值，需要进行pattern match，对得出的零个case返回A-而因为只需要对零个case进行操作，什么也不需要做，换句话说我们可以无条件得出A。从另一个角度来想，这是因为我们永远不可能构造出bottom type的值，所以当bottom type作为参数的时候，这个函数永远不可能被调用，自然可以返回随便啥（包括另一个bottom）。

我们现在假设EQ x y有值。

如果如此，当p x有值，换句话说P(x)为真的时候，我们可以通过调用p x -> p y得出p y也有值，换句话说P(y)也为真。反之亦然。顺着这条路想想，我们发现，如果类型x对应命题X，y对应Y，类型x -> y对应X imply Y：给我一个X的证明，我能给你一个Y的证明。相似的，(x * y)对应X and Y：X的证明在左边，Y的证明在右边。x + y则对应或：x有证明，或者y有证明。Bottom Type跟Top Type则分别对应False, True，而x -> bottom则对应not x。这几个都很明显，自己试试看。

所以我们可以认为这个EQ代表了Leibniz Equality。

我们现在试下证明EQ是reflexive，symmetric，transitive的吧。

首先，reflexive的证明：

当我们敲下“EQRefl x: EQ x x.”的时候，由于我们没有给出定义，Coq进入了一个特殊的模式（见右边那奇怪的东西），辅助我们找出证明。这里，—–上面的是我们已知的东西，下面是我们要证明的东西。这只是在说：已知x是一个类型，你需要构造出EQ x x - 我们漏掉没证明的东西。

我们在这个奇怪的mode（叫proof-editing mode）中输入了unfold EQ，命令Coq把EQ展开成定义。于是Coq表示：你需要证明出，对于所有p，(p x -> p x) * (p x -> p x)。

我们做了两件事：我们先用“intros p.”引入p这个假设。

然后我们用“Show Proof.”打印出Coq给我们生成的EQRefl。

引入p后，我们只需要证明p x -> p x跟p x -> p x，只需要两个id就能证出来了。

下面打印的是EQRefl。由于我们还没证明完EQRefl，有一个叫?Goal的东西存在：这代表我们剩下的Goal（或者说，subgoal），为右上角的东西。

这个完成了一半的EQRefl有一个参数，p : Type -> Type，就是上面刚刚引入的p。引入假设，相当于lambda abstraction。

然后，我们用refine直接给出((p x -> p x) * (p x -> p x))。当Coq遇到fun px => _中的_的时候，并不知道如何处理，于是接着想为我们要求给出_的值。用refine，我们可以从Coq中的proof-editing-mode跳到带_的普通mode。

这些各种各样的命令，都旨在对Show Proof产生的partial term发生影响，并且使之更具体，所以这样编程就叫Programming By Refinement。

最后剩下的，很简单-就在假设中，我们用intuition让Coq自动帮我们填入。

最后，用Defined完成这个证明。

相对应的Haskell代码是，

eqRefl :: EQ x x
eqRefl = EQ (id, id)

然后下一个。

我们先想想可以怎么证明EQSym吧。

首先，我们有EQ x y，所以对于出现在任意地方的x，我们可以转成y，也可以y转x。

然后，我们可以生成EQ x x。

所以，我们只需要把EQ x x的第一个x改成y，就可以。

我们把第一个EQ unfold掉，剩下的不动，然后用intros引入所有可以引入的假设。;代表把两个命令串联在一起。

我们指定X的p是(fun h => EQ h x)，换句话说，我们要把第一个EQ x x的x变成y。

Show Proof.中，出现了一个let X0 := X (fun h => EQ h x)，就是specialize后的X。把一个定理变成更特殊的形式，就是定死一个参数。

既然X是个pair，就由两部分构成，我们就可以对之进行case analysis，对于每一个constructor C，假设存在参数x0 x1…，并假设X = x0 x1，由于只有一个case，就会给出这个pair的左右两边。在“普通”Coq中，这是let (e, e0) := X0。case analysis就是pattern matching。

然后，因为e: EQ x x -> EQ y x，所以，我们倒着推理，如果我们需要EQ y x，我们只需要找到EQ x x则可。我们用apply完成这一任务。这是e ?Goal。使用implication就是函数调用。

我们再apply以前证明过的定理，EQRefl，结束证明（你没想错，这也只是函数调用）

newtype EQSwap x y = EQSwap {unEQSwap :: EQ y x}
eqSym :: EQ x y -> EQ y x
eqSym (EQ x) = unEQSwap $ fst x $ EQSwap eqRefl

然后，我们证明EQTrans。具体思路挺简单，我们把EQ x y的y换成z。

我们先unfold并intros。

specialize一次。。。

然后用intuition帮我们做。

eqTrans :: EQ x y -> EQ y z -> EQ x z
eqTrans xy (EQ (yz, _)) = yz xy

Proof Editing Mode的一个好处是，我们可以通过元编程（或者调用已有的命令），使得Coq自动帮我们证明类型，不需要什么都自己来。

然后，Coq自己标准库里面也有一个equality，“=”。我们可以用eq_refl创造x = x，并，给出H: x = y，可以用rewrite H把出现的x变成y。

我们“证明” EQ x y imply x = y。这下，我们直接给出证明，不进入proof editing mode：对于一个x = x，我们改写第二个x。你可以看到，证明只是一个普通的类型的值。

我们最后证明另一边。跟前面一样，我们直接给出定义。但是，跟以前不一样的是，我们用ltac:(LTAC)在定义中让Coq去进入某种意义上的proof editing mode，并且用LTAC证明整个Goal：LTAC用rewrite把EQ x y改写成EQ y y，然后用EQRefl。用ltac:，我们能在普通mode进入proof editing mode（technically不是，不过为了简化问题，可以暂时这样认为），用refine，我们可以在proof editing mode中进入普通mode，两个互相连接，获得了生命的大和谐。

至于Leibniz Equality比Coq默认的好在那？这个可以用在Scala中，在Haskell中不需要GADT支持，Typing Dynamic Typing也是用的这。

PS：EQ的两个参数不一定是Type，但是为了跟Haskell版对应就这么做了。

同时，这些代码比对应的HS代码长很多，因为这是在展示CH同构，而不是用最简单的方法做事。

并且，发现我们只用了左边的转换了吗？其实

forall (p: Type -> Type), ((p x -> p y) * (p y -> p x))

forall (p: Type -> Type), (p x -> p y)

x = y

三者等价。可以自己用纸跟笔试试看，或者在Haskell中证明前两个一样。

最后：这个文章很不严谨，只是引起兴趣作用，Coq/CH同构都没介绍多少，有兴趣的话，最好看看下列的文章。

Future Reading:

Curry Howard Isomorphism:

Propositions as Types

Lectures on The Curry Howard Isomorphism

Coq:

Software Foundations

顺带打个广告，有个Coq的QQ群，372347110

Leibniz Equality:

Leibniz equality can be made injective