Coq证明用法

Question

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

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

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

Answer 1

Coq 的用途之一是验证软件。这意味着写下一个程序并证明它满足您关心的某些规范。什么算作规范是相当开放的:您可能想证明 C 程序不会遭受缓冲区溢出，或者编译器生成的目标代码的行为符合源语言的规范。

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

内部验证

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

为了具体起见，假设我们要编写一个经过验证的排序算法。这是 Coq 中插入排序的一个实现，它使用 Mathematical Components library :

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 可以理解的形式，如 the Verified Software Toolchain 所做的那样。 .

这是什么意思？

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