最近闲下来的时候其实一直有在玩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程序片段。
代码语言：javascript复制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。
CoqIde
agda-mode in Atom
agda-mode in Emacs
相比之下，CoqIde编写代码的体验较好。三个分栏窗体提供的信息充足且格式完整。不过agda-mode的编写体验也是挺好的，尤其是关于Hole的处理，个人感觉在一定程度上替代了Tactics的作用。而且通过类似latex方式，Unicode字符的输入也不是特别复杂。
综上，如果是数学的证明，我大概会选择Coq。如果是用来实现论文里的Type System，我会更青睐于使用Agda。
