Coq 证明用法

Question

我是 Coq 的初学者，我很快就学会了这门语言，可以做证明等。

但我不明白我们能用它做什么。 好吧，我们证明了一些定义等。但是我们可以通过哪些方式使用它们呢？ 我看到我们可以提取 Haskell 文件，但我也不明白。

因为我想用语言来证明 CVE 例如。

Answer 1

Coq 的用途之一是验证软件。这意味着写下一个程序并表明它满足您关心的某些规范。规范的定义是开放式的：您可能想要证明 C 程序不会出现缓冲区溢出问题，或者编译器生成的目标代码的行为符合源语言的规范。

Coq 中验证软件有两种主要方法。

内部验证

一种可能性是将程序实现为可以在 Coq 内部执行的函数程序，并证明其属性。该程序可以提取为更传统的编程语言，例如 Haskell 或 OCaml。然后，您可以将此代码链接到提取目标中的其他模块以生成完整的可执行文件。例如，CompCert C 编译器 就采用了这种方法。

具体而言，假设我们要编写一个经过验证的排序算法。下面是 Coq 中插入排序的实现，它使用 数学组件库：

From Coq Require Import Extraction.
From mathcomp Require Import all_ssreflect.

Fixpoint insert n ns :=
  if ns is m :: ns then
    if n <= m then n :: m :: ns
    else m :: insert n ns
  else [:: n].

Lemma sorted_insert n ns : sorted leq ns -> sorted leq (insert n ns).
Proof.
case: ns => //= m ns m_ns; rewrite fun_if /=.
case: ltngtP => // /ltnW m_n.
elim: ns => [|p ns IH] /= in m m_ns m_n *; first by rewrite m_n.
case/andP: m_ns => m_p m_ns; rewrite fun_if /= m_n m_p.
by case: ltngtP => //= /ltnW p_n; rewrite IH.
Qed.

Fixpoint insertion_sort ns :=
  if ns is n :: ns then insert n (insertion_sort ns)
  else [::].

Lemma sorted_insertion_sort ns : sorted leq (insertion_sort ns).
Proof.
by elim: ns => //= n ns IH; rewrite sorted_insert.
Qed.

Extraction "insertion.ml" insertion_sort.

如果编译此文件，您将看到它将生成一个 insertion.ml 文件，其中包含该程序在 OCaml 中的翻译。

外部验证

另一种可能性是对程序的行为给出数学描述并证明该描述是正确的。例如，我们可以使用 Coq 将 C 程序的行为定义为输入和输出之间的数学关系，然后使用此描述来论证特定 C 程序是正确的（即，其输入和输出序列满足某些属性） ）。这个特定的 C 程序可能会从实际的 C 源代码转换为 Coq 可以理解的形式，如 验证软件工具链所做的那样。

这意味着什么？

Coq 证明保证在理想化的程序执行模型中不会出现某些错误。无论您选择哪种验证方法，该模型都比程序实际运行时发生的情况简单得多。例如，我们不会费心对描述运行程序的处理器电路的物理定律进行建模，因为这太复杂了。然而，我们关心的大多数错误都可以用相当简单的模型来描述——例如，我们不需要详细的物理定律来解释为什么在某些执行中会发生缓冲区溢出。这使得 Coq 和相关工具在实践中非常有效地防止错误。