用了一段时间Agda的感想

2019/08 13

最近闲下来的时候其实一直有在玩Agda。其实之前也知道Agda，但是由于Coq的相关资料更多，而且那时候我在Windows平台上无法安装Agda（old-times库的问题），于是拖到近来PLFA这本书的中文翻译动工才开始跟着看。

我的第一感觉就是，Agda真的很好入门。Agda的语法和Haskell几乎完全一致，而且由于Agda支持Unicode，于是代码中可以使用大量的数学符号，可以很简单的将一个命题翻译为Agda代码。和Coq相比，虽然Gallina也支持使用Unicode字符作为identifier，但是Coq并没有广泛使用。

在证明方面，Agda和Coq有本质的不同。虽然都以有类型λ演算为理论基础（Agda是UTT，Coq是归纳构造演算），但是表现在证明上，两者就有很大的不同了。在Agda中，命题的证明就是给出一个类型的一个项。可以说，在Agda中证明一个命题能充分体现Curry-Horwad同构的实质。进一步的说，Agda根本没有强调“证明”，而你的每一次证明，其实都是C-H同构的体现。而Coq却完全相反。Coq使用了不同的Tactics来辅助证明。在Coq中进行证明的过程更加类似于一般的数学证明。以下是证明皮尔士定律与排中律等价的Agda、Coq程序片段。

open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Relation.Nullary using (¬_)
open import Data.Empty using (⊥; ⊥-elim)

em : Set₁
em = ∀ {A : Set} → A ⊎ ¬ A

peirce : Set₁
peirce = ∀ {P Q : Set}
  → ((P → Q) → P)
  → P

peirce→em : peirce → em
peirce→em h = h λ x → inj₂ λ a → x (inj₁ a)

em→peirce : em → peirce
em→peirce h {P} x with h {P}
... | inj₁ p = p
... | inj₂ ¬p = x (λ p → ⊥-elim (¬p p))

Definition pierce := forall (p q : Prop), ((p -> q) -> p) -> p.

Definition em := forall p, p \/ ~ p.

Theorem pierce_equiv_em: pierce <-> em.
Proof.
  unfold pierce, em.
  firstorder.
  apply H with (q := ~(p \/ ~p)).
  firstorder.
  destruct (H p).
  assumption.
  tauto.
Qed.

Agda的证明并没有用Function.Equality的_⇔_，因为我个人觉得那个东西非常复杂。

证明过程中，Agda实际上是在辅助使用者获得某类型的项。而针对这个目标，Agda提供了比如Case和Refine之类的工具来根据类型生成目标代码，这一点是十分方便的。但是缺点也显而易见，就是证明过程并不按照一般的证明顺序进行的，毕竟只是项的构造。虽然有≡-Reasoning将证明过程展示为竖式，但是表达能力有限。另外，Agda的证明代码也需要一定理解才能获得大致的证明思路。

相比之下，Coq的证明过程更加近似于人工证明。Coq的证明中自然而然的带入的证明的“顺序”，所以在一定程度上，阅读Coq的代码更容易得到证明的大致思路。而且由于Tactics的应用是有序的，所以结合相关证明信息的说明，Coq代码的证明过程可以得到非常直观的展现。而且，Coq区分了Definition、Thereom、Lemma、Example、Proof等等，为阅读提供了很大的便利。当然，这种证明形式隐藏了C-H同构。对于更深层次的证明，需要学习更多内容才可以。

最后是关于ide。Agda与Coq都提供了Emacs的插件以便编写程序。此外，Agda还有Atom与Vscode（不完善）等现代编辑器的插件。Coq有官方的CoqIde，还有比如ProofAssistant也可以使用Coq。