与 Coq 相比，Isabelle 证明助手的优缺点是什么？

Question

Isabelle/HOL 证明助手与 Coq 相比有什么弱点和优势吗？

Answer 1

我对 Coq 很熟悉，对 Isabelle/HOL 没有太多经验，但我或许能提供一点帮助。也许其他对 Isabelle/HOL 有更多经验的人可以帮助改进这一点。

两个系统之间存在两大分歧点：基础理论和交互方式。我将尝试简要概述每种情况下的主要区别。

理论

Coq 和 Isabelle/HOL 都基于强大且极具表现力的高阶逻辑。然而，这些逻辑在一些特点上有所不同：

依赖类型

Coq 的逻辑是一种依赖类型理论，称为归纳构造演算（简称​​CIC）。这里的“依赖类型”是指 Coq 中的类型可以引用普通值。例如，可以编写一个矩阵乘法函数mult，类型为

mult : forall (n m p : nat), matrix n m -> matrix m p -> matrix n p

这个函数的类型说它需要两个矩阵作为输入，一个维度为n x m，另一个维度为m x p，并返回一个维度为n x p的矩阵。另一方面，Isabelle/HOL 的理论不具有依赖类型；因此，不能编写与上述相同类型的mult 函数。相反，必须编写一个适用于任何类型矩阵的函数，并在接收到正确类型的参数时证明该函数的某些属性后验。换句话说，在处理 Isabelle/HOL 时，需要将 Coq 类型中表现出来的某些属性声明为单独的定理。

虽然依赖类型在某些方面很有趣，但它们通常有多大用处尚不清楚。我的印象是，有些人觉得它们使用起来非常复杂，并且在类型级别表达某些属性而不是将它们作为单独的定理的好处不值得这种额外的复杂性。就个人而言，我喜欢在少数情况下使用依赖类型，但有明确的理由这样做。

基本推理原理

默认情况下，Coq 的理论缺乏许多数学实践中常见的推理原则，例如 the law of the excluded middle（即非建设性推理的能力）、可扩展性（例如，能够说产生相同结果的函数）本身是平等的）和选择公理。另一方面，在 Isabelle/HOL 中，这些原则是内置的。

理论上，这不是什么大问题，因为 Coq 的逻辑旨在让人们安全地将这些推理原则添加为额外的公理。尽管如此，我的印象是在 Isabelle/HOL 上进行这种推理更容易，因为逻辑是从头开始构建来支持它们的。

（你可能想知道为什么将这些基本原则排除在 Coq 逻辑之外。动机是哲学上的：在 Coq 的核心逻辑中，证明可以被视为可执行程序，这使逻辑具有建设性的味道。例如，拒绝排中是指析取的证明A \/ B 对应于一个程序，该程序返回一个位，指示A 或B 中的哪一个为真；因此，排中将对应于一个程序这决定了每一个不可能存在的数学问题。This question 进一步讨论了这个问题。）

交互方式

Coq 和 Isabelle/HOL 都是交互式定理证明者。它们是用于编写关于它们的定义和证明的语言；这些证明由计算机检查以确保它们没有错误。在这两个系统中，一个人通过给出解释如何证明某事的命令来写下证明。但是，每个系统上发生这种情况的方式各不相同。

Isabelle/HOL 一般而言对“按钮式”自动校样有更成熟的支持。例如，它带有著名的sledgehammer 策略，它调用几个外部自动定理证明器和求解器来尝试证明一个定理。 Coq 还附带了许多强大的证明自动化程序，例如omega 或congruence，但它们并不普遍适用，并且在 Isabelle/HOL 中可以通过单个命令解决的许多定理需要在 Coq 中进行更明确的证明。

当然，这种便利是有代价的。有人告诉我，在 Isabelle/HOL 中很难控制自己的证明，因为系统试图自己做很多事情。这在证明简单的定理时不是问题，但是当证明自动化不够强大并且您需要告诉定理证明者如何更详细地进行时，它就会成为问题。

当支持用户定义的证明自动化程序时，情况会有所不同。 Coq 附带了一种用于编写证明的策略语言，称为 Ltac，它本身就是一种编程语言。尽管 Ltac 存在一些设计问题，但它确实允许用户以轻量级的方式对相当复杂的证明自动化程序进行编码。对于较重的任务，Coq 还允许用户使用 Coq 的实现语言 OCaml 编写插件。相比之下，在 Isabelle/HOL 中，没有像 Ltac 这样的高级自动化语言，用户编写自定义证明自动化程序的唯一方法是使用插件。

Answer 2

我将说明 Isabelle/HOL 的“按钮”功效的一个方面是其 automation Cantor 的经典“对角化”论点（回想一下，这表明没有来自自然到它的幂集，或者更一般地any集到它的幂集）。

theorem Cantor: "∄f :: 'a ⇒ 'a set. ∀A. ∃x. A = f x"
proof
  assume "∃f :: 'a ⇒ 'a set. ∀A. ∃x. A = f x"
  then obtain f :: "'a ⇒ 'a set" where *: "∀A. ∃x. A = f x" ..
  let ?D = "{x. x ∉ f x}"
  from * obtain a where "?D = f a" by blast
  moreover have "a ∈ ?D ⟷ a ∉ f a" by blast
  ultimately show False by blast
qed

我刚刚向您展示的是将康托尔的经典论点翻译成 Isabelle/HOL。毫无疑问，巧妙！ Isabelle/HOL 甚至可以自动消除来自这个证明的洞察力，但是：

theorem "∄f :: 'a ⇒ 'a set. ∀A. ∃x. f x = A"
  by best

theorem "∄f :: 'a ⇒ 'a set. ∀A. ∃x. f x = A"
  by force

证明系统能够自动证明康托尔的陈述。对于研究人员来说，一方面这是有帮助的，但在某种意义上这是一把双刃剑。我发现像对角化参数这样复杂的真实陈述可以被信任在 Isabelle/HOL 内部得到证明是有帮助的，因为我的定理因此更加复杂。另一方面，随着计算机自动化进步的推动，我在研究中走得越远，我就越不能解释为什么这个定理是正确的，或者因为什么原理是正确的。只有电脑知道为什么，如果我们能问它！

Answer 3

由于“Isabelle/HOL”在问题中是精确的，我将讨论 Isabelle 中使用的 HOL 逻辑，我认为这是与 Coq 进行比较的最佳逻辑。我不是类型系统和逻辑方面的专家，但我认为我在这里所说的是正确的，至少大致上是正确的。这当然也是一个品味问题；-) 我的回答可能是主观的。

最深刻的区别在于类型系统和逻辑。

我想说，对于了解 ML 家族的功能语言的人来说，它的优势是更自然（对于了解 SML 的人来说更是如此），并且它使用务实的方法来解决问题，例如使用经典逻辑为基础。它的类型系统接近于 Hindley Milner 的类型系统并且默认终止（如果它没有被用户修改）。

另一方面，Coq 更严格并且使用直觉逻辑。它有一个专门的类型系统，有几个命令，并允许类型依赖，这可能更难以处理，并且在某些情况下可能是非终止的。它还允许人们从证明中提取程序（这可能相对低效），这在 Isabelle 中是无法直接实现的。