Coq.tex

\section{Coq入门}

\subsection{简述}
Coq是一个基于Calculus of Constructions的扩展的Proof Assistant，除此之外还加入了下列扩展：

1: 加入了Definition

2：加入了Inductive，CoInductive data type

3: 为了一致性，加入了Universe。也就是说，Type : Type在Coq中不成立，成立的是Type 0 : Type 1, Type 1 : Type 2, ... (有兴趣的读者可以试试看在Coq中开启-type-in-type使得Type : Type后证明矛盾)

\subsection{证明原理}
根据Curry-Howard同态，每个Coq命题都是一个类型，命题的证明就是符合该类型的表达式。用户证明命题就是通过证明策略来逐步构造表达式。比如命题"forall P Q R:Prop, (P->Q)->(Q->R)->(P->R)"的证明就是表达式"fun (H:P->Q)(H’:Q->R)(p:P) => H’ (H p)".\\

Trusted Computing Base
Reason of formal verification

Proof by refinement.
Step by step, interactive, dialog like

Proof automation, De Brujin Criteria
tauto, first order, meaning of formal verification, why tactic is OK

LCF approach
Help user. "Dialog like" property

\subsection{例子}

\subsection{Coq的ML扩展}
Coq提供了扩展机制，方便开发者使用Coq的开发语言OCaml为Coq书写证明插件。

\begin{itemize}
    \item \emph{Software Foundations} by Benjamin C. Pierce et al.
          \href{https://www.cis.upenn.edu/~bcpierce/sf/current/index.html}{HTML version}\\
          练习很多，适合 Coq 初学者自学和作为教材使用。前半部分是 Coq 本身和形式化证明本身的一些东西，后半部分更多和程序验证相关。
    \item \emph{Programs and Proofs - Mechanizing Mathematics with Dependent Types} by Ilya Sergey.
          \href{http://ilyasergey.net/pnp}{Homepage}\\
          本书亮点是对 ssreflect 用法有一定介绍。同样有练习，但是相对较少。
    \item \emph{CoqArt} by
          \href{https://www.labri.fr/perso/casteran/CoqArt/}\\ Yves Bertot \& Pierre Castéran
          非常详尽地介绍了Coq的理论与使用，并且在主页上有课后习题答案，答案也随着Coq版本更新。
    \item \emph{Certified Programming with Dependent Types} by Adam Chlipala.
          \href{http://adam.chlipala.net/cpdt/}{Homepage}\\
          老司机必备。介绍了一些Coq的高级玩法，比如CoInductive的应用、使用Ltac来自动化证明等。
\end{itemize}