coq - Isabelle 证明助手与 Coq 相比有哪些优点和缺点？

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 (即，非 build 性推理的能力)、外延性(例如，能够说产生相等结果的函数本身是相等的)和选择公理。另一方面，在 Isabelle/HOL 中，这些原则是内置的。

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

(你可能想知道为什么把这些基本原则排除在 Coq 的逻辑之外。动机是哲学的:在 Coq 的核心逻辑中，证明可以被视为可执行程序，这给逻辑带来了 build 性的味道。拒绝排除的原因例如，中间是析取的证明 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 这样的更高级别的自动化语言，用户编写自定义证明自动化程序的唯一方法是使用插件。