Coq 证明助手（The Rocq Prover）简明教程

对大多数人来说 Coq 是一个很陌生的东西，Coq 官网对他的定义为：

Coq 是一个形式化证明管理系统。它提供了一种用于编写数学定义、可执行算法和定理的形式化语言，以及一个用于半交互式开发机器校验证明的环境。 — Coq 官网

短短的一句中文，可能会让大家一头雾水，简而言之：我们把需要证明的定理（引理、推论等等）以及定理涉及的定义编写为Coq，并为其编写一个 证明思路，Coq 会自动为你完成证明，如果我们给的证明思路不对，Coq 也会帮我检查出来，但是他并不能帮我们修正错误。 这就是 Coq 的使命，同时其半交互性也可以用debug 方式逐步检查我们的 证明思路。

本教程将与大家一起学习这种神奇而新奇的技术。

持续但缓慢更新中