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

Question

与Coq相比，Isabelle/HOL证明助手是否有任何优缺点？

- elysefaulkner

Answer 1

"I am mostly familiar with Coq, and do not have much experience with Isabelle/HOL, but I might be able to help a little bit. Perhaps others with more experience on Isabelle/HOL can help improve this."

"There are two big points of divergence between the two systems: the underlying theories and the style of interaction. I'll try to give a brief overview of the main differences in each case."

"Theories"

"Both Coq and Isabelle/HOL are based on powerful, very expressive higher-order logics. These logics, however, differ on a few features:"

"Dependent types"

"Coq's logic is a dependent type theory, known as the calculus of inductive constructions (CIC for short). "Dependent type" here means that types in Coq can refer to ordinary values. For instance, one can write a matrix multiplication function 'mult' with type."

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

这个函数的类型表明它接受两个矩阵作为输入，一个维度为n × m，另一个维度为m × p，并返回一个维度为n × p的矩阵。然而，Isabelle/HOL理论并没有依赖类型，因此不能编写与上述类型相同的mult函数。相反，需要编写适用于任何类型的矩阵的函数，并在其接收到正确类型的参数时事后证明该函数具有某些特定属性。换句话说，在Coq类型中体现的某些属性需要在使用Isabelle/HOL时作为单独的定理进行断言。

虽然依赖类型对于某些事情很有趣，但它们一般来说并不清楚有多么有用。我的印象是，有些人觉得它们非常复杂，将某些属性表达为类型级别的好处与将它们作为单独的定理不值得这种额外复杂性。就我个人而言，我喜欢在少数情况下使用依赖类型，当存在明确的理由时。

基本推理原则

Coq的理论默认缺乏许多在数学实践中常见的推理原则，例如排中律（即非构造性推理的能力），外延性（例如，能够说产生相等结果的函数本身是相等的）和选择公理。另一方面，在Isabelle/HOL中，这些原则是内置的。

从理论上讲，这不是一个大问题，因为Coq的逻辑被设计成允许人们安全地将这些推理原则作为额外的公理添加进去。然而，我有这样的印象，即在Isabelle/HOL上进行这种推理更容易，因为该逻辑是从头开始构建来支持它们的。

（您可能会想知道为什么Coq的逻辑中缺少这些基本原则。其动机是哲学性的：在Coq的核心逻辑中，证明可以被视为可执行程序，这赋予了逻辑一种建设性的风格。例如，拒绝排中律的原因是，析取A \/ B的证明对应于返回一个比特位来指示A或B中哪个为真的程序；因此，排中律将对应于决定每个数学问题的程序，而这是不存在的。 这个问题进一步讨论了这个问题。）

交互方式

Coq和Isabelle/HOL都是交互式定理证明器。它们是编写定义及其证明的语言；这些证明通过计算机检查以确保没有错误。在两个系统中，我们通过给出解释如何证明某些东西的命令来书写证明。然而，这在每个系统中发生的方式是不同的。

Isabelle/HOL通常具有更成熟的“按钮式”证明自动化支持。例如，它带有著名的策略，该策略调用多个外部自动定理证明器和求解器来尝试证明定理。Coq也提供了许多强大的证明自动化程序，如或，但它们不太适用于一般情况，在Isabelle/HOL中可以通过单个命令解决的许多定理在Coq中需要更明确的证明。

当然，这种便利是有代价的。我被告知，在Isabelle/HOL中控制自己的证明更加困难，因为系统试图自行完成很多工作。这并不是证明简单定理时的问题，但当证明自动化不够强大且需要更详细地告诉定理证明器如何进行时，这就成为一个问题了。

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

- Arthur Azevedo De Amorim

---

我认为大部分内容是正确的，但我有两个小问题要提出：首先，Isabelle确实拥有矩阵，并且矩阵乘法的类型为 ('a::semiring_1)^'n^'m ⇒ 'a^'p^'n ⇒ 'a^'p^'m。例如，您可以将类型为 real^2^3 和 real^4^2 的矩阵相乘，得到类型为 real^4^3 的矩阵。这是因为对于任何正整数 n，都有一个内置类型，由从0到n-1的数字组成。 - Manuel Eberl

针对一种策略语言：Isabelle现在拥有Eisbach (ssrg.nicta.com.au/projects/TS/tactics.pml)。 - Manuel Eberl

在我看来，使用结构化的 Isar 证明，可以相当自然地分解那些对于仅靠自动化来说太难以处理的证明。 - Manuel Eberl

@Soleil，由于排中律有许多等价的表述方式，选择哪一种作为公理，哪些作为定理是在很大程度上取决于个人口味。一些系统使用非矛盾原则作为公理，就像你指出的那样，而其他系统如 Coq 标准库的古典片段和 Gentzen 的 NK 演算则使用排中律。然而，我的目标不是争论什么是公理，而是指出这些基本推理原则在 Coq 和 Isabelle 中存在差异。我将编辑我的回答。 - Arthur Azevedo De Amorim

@David，Coq中有许多经过验证的软件示例。其中著名的包括compcert经过验证的c编译器、vellvm用于llvm的后端、certikos操作系统以及使用Princeton的验证软件工具链的软件。 - Arthur Azevedo De Amorim

Answer 2

我将说明Isabelle/HOL“按钮式”功效的一个方面，即其对Cantor经典“对角线法”论证的自动化(回想一下，这个论证表明从自然数到其幂集（或者更普遍地说，从任何集合到其幂集）不存在满射)。

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

我所呈现的内容是 Cantor 经典论证在 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内部被证明是可信的有益，因为我的定理更加复杂。另一方面，随着计算机自动化进展驱动我在研究中走得越来越远，我就越解释不清为什么或者基于什么原则定理是真实的。只有计算机知道为什么，如果我们能问它！

- user48801

---

“只有计算机知道原因”，那么没有一种方法可以窥视它所找出的结果吗？ - Max Heiber

你要求伊莎贝尔展示生成的证明术语，但是你可能会被其规模和细节所震撼。与人类可理解的证明相比，如上面回答中 Cantor 定理的 Isar 证明，它们会抽象掉诸如“什么是集合”和“∃f是什么意思”的细节。请注意不要改变原文意思。 - Søren Debois

顺便说一下，链接好像坏了 :/ - ch271828n

Answer 3

由于问题中明确提到了“Isabelle / HOL”，因此我将讨论在Isabelle中使用的HOL逻辑，我认为这是用于与Coq进行比较的最佳逻辑。虽然我不是类型系统和逻辑方面的专家，但我认为我在这里所说的至少是大致正确的。这也肯定是一种品味;-)，我的答案可能是主观的。

最深刻的差异在于类型系统和逻辑。

我认为它的优势在于对ML家族的功能语言（甚至对SML有更多了解的人）更加自然，并采用实用主义方法来解决问题，例如使用经典逻辑作为基础。它的类型系统接近于Hindley Milner的类型系统，并且默认情况下终止（除非用户修改它）。

另一方面，Coq更加严格并使用直觉逻辑。它具有具有几个顺序的专门类型系统，并允许类型依赖性，这可能更加棘手，并且在某些情况下可能不会终止。它还允许从证明中提取程序（可能相对低效），这在Isabelle中无法直接完成。

- Mathieu

---

你能澄清一下，Coq的类型系统非确定性是什么意思吗？ - Arthur Azevedo De Amorim

哦，抱歉，我晚了……我的意思是非终止的，我会更正的。 - Mathieu

我明白了。我认为这有点微妙，因为对 Coq 程序进行类型检查实际上是可判定的。导致类型检查器循环的原因可能是诸如类型类推断之类的特性，但严格来说，这在类型系统外。此外，您始终可以通过手动提供类型类实例来强制类型检查终止。 - Arthur Azevedo De Amorim