问题描述
Isabelle / HOL证明助理与Coq相比有什么弱点和优势吗？
Does Isabelle/HOL proof assistant have any weaknesses and strengths compared to Coq?
推荐答案
我对Coq最为熟悉，并且对Isabelle / HOL没有太多经验，但我可能会有所帮助。也许其他在Isabelle / HOL方面有丰富经验的人可以帮助改善这一点。
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.
两者Isabelle / HOL和Isabelle / HOL基于功能强大且表达力强的高阶逻辑。但是，这些逻辑在某些功能上有所不同：
Both Coq and Isabelle/HOL are based on powerful, very expressive higher-order logics. These logics, however, differ on a few features:
Coq的逻辑是从属类型理论，称为归纳结构的演算（简称为 CIC ）。 从属类型在这里意味着Coq中的类型可以引用普通值。例如，可以编写类型为
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
此函数的类型表示它需要两个矩阵作为输入，一个维度为 nxm 和另一个维度 mxp ，并返回维度为 nxp 。另一方面，Isabelle / HOL的理论不具有依赖类型。因此，不能编写与上述类型相同的 mult 函数。取而代之的是，必须编写一个对任何类型的矩阵都适用的函数，并在该函数接收正确类型的参数时证明后验的某些属性。换句话说，在研究Isabelle / HOL时，需要将Coq类型中体现的某些属性断言为独立的定理。
The type of this function says that it takes two matrices as inputs, one of dimension n x m and another one of dimension m x p, and returns a matrix of dimension n x p. The theory of Isabelle/HOL, on the other hand, does not possess dependent types; hence, one cannot write a mult function with the same type as the one above. Instead, one would have to write a function that works for any kind of matrix, and prove a posteriori certain properties of this function when it receives arguments of the right kinds. In other words, certain properties that are manifest in Coq types need to be asserted as separate theorems when working on Isabelle/HOL.
虽然从属类型在某些方面很有趣，目前尚不清楚它们在总体上有多有用。我的印象是，有些人觉得它们的使用非常复杂，并且在类型级别上表达某些属性而不是将它们作为单独的定理所带来的好处不值得这种额外的复杂性。就个人而言，在有明确的理由时，我喜欢在少数情况下使用依赖类型。
While dependent types are interesting for some things, it not clear how useful they are in general. My impression is that some feel that they are very complicated to use, and that the benefit of having certain properties expressed at the type level versus having them as separate theorems is not worth this additional complexity. Personally, I like to use dependent types in few cases, when there is a clear reason to do so.
Coq的理论默认缺少许多数学实践中常见的推理原理，例如（即，非构造性推理的能力），可扩展性（例如，能够说产生相等结果的函数本身就是相等的）以及选择公理。另一方面，在Isabelle / HOL中，此类原则是内置的。
Coq's theory by default lacks many reasoning principles that are commonplace in mathematical practice, such as the law of the excluded middle (i.e., the ability to reason non-constructively), extensionality (for instance, being able to say that functions that produce equal results are themselves equal), and the axiom of choice. In Isabelle/HOL, on the other hand, such principles are built-in.
从理论上讲，这并不是什么大问题，因为Coq的逻辑旨在让人们安全地添加这些推理原理作为额外的公理。不过，我的印象是，在Isabelle / HOL上进行这种推理比较容易，因为逻辑是从头开始构建以支持它们的。
In theory, this is not a big problem, because Coq's logic was designed to allow people to safely add these reasoning principles as extra axioms. Nevertheless, I have the impression that it is easier to do this kind of reasoning on Isabelle/HOL, since the logic was built from the ground up to support them.
（您可能想知道为什么将这些基本原理排除在Coq的逻辑之外是什么原因，其动机是哲学上的：在Coq的核心逻辑中，证明可以看作是可执行程序，从而使逻辑具有建设性的味道。例如，证明析取 A \ / B 对应于一个程序，该程序返回一个指示 A中的哪个或 B 是真实的；因此，排除的中间值将对应于一个程序，该程序决定每个数学问题，该问题不存在。 //stackoverflow.com/questions/31554453/why-are-logical-connectives-and-booleans-separate-in-coq/31568076#31568076>此问题对问题进行了进一步讨论。）
(You may wonder what the reason is for leaving such basic principles out of Coq's logic. The motivation is philosophical: in Coq's core logic, proofs can be seen as executable programs, which gives the logic a constructive flavor. The reason for rejecting the excluded middle, for instance, is that the proof of a disjunction A \/ B corresponds to a program that returns a bit indicating which one of A or B is true; thus, the excluded middle would correspond to a program that decided every mathematical question, which cannot exist. This question discusses the issue a bit further.)
Coq和Isabelle / HOL都是交互式定理证明。它们是用于编写定义和证明的语言。计算机会检查这些证明以确保它们没有错误。在这两种系统中，都通过给出解释如何证明事物的命令来写下证明。但是，每个系统上发生这种情况的方式各不相同。
Both Coq and Isabelle/HOL are interactive theorem provers. They are languages for writing definitions and proofs about them; these proofs are checked by a computer to ensure that they have no mistakes. In both systems, one writes down a proof by giving commands that explain how to prove something. The way this happens on each system, however, varies.
总体而言，Isabelle / HOL对按钮式证明自动化具有更成熟的支持。例如，它带有著名的 sledgehammer 策略，该策略调用多个外部自动定理证明者和求解器以尝试证明一个定理。 Coq还提供了许多功能强大的证明自动化程序，例如 omega 或 congruence ，但是它们并不普遍适用，在Isabelle / HOL中用一个命令就能解决的许多定理都需要用Coq进行更明确的证明。
Isabelle/HOL generally speaking has more mature support for "push-button" proof automation. For instance, it comes with the famous sledgehammer tactic, which invokes several external automatic theorem provers and solvers to try to prove a theorem. Coq also comes with many powerful proof automation procedures, such as omega or congruence, but they are not as generally applicable, and many theorems that can be solved with a single command in Isabelle/HOL require more explicit proofs in Coq.
当然，这种便利是有代价的。有人告诉我，在Isabelle / HOL中很难控制一个人的举证，因为该系统会尝试自己做很多事情。证明简单定理时这不是问题，但是当证明自动化不够强大并且您需要告诉定理证明者如何进行更详细的处理时，这便成为问题。
Of course, this convenience comes with a price. I've been told that it is harder to have control over one's proof in Isabelle/HOL because the system tries to do a lot by itself. This is not a problem when proving simple theorems, but it becomes an issue when proof automation is not powerful enough and you need to tell the theorem prover how to proceed in greater detail.
在支持用户定义的证明自动化程序时，情况有所不同。 Coq附带了一种战术语言，用于编写证明（称为Ltac），这是一种独立的编程语言。即使Ltac有一些设计问题，它也允许用户以轻量级的方式对相当复杂的证明自动化程序进行编码。对于繁重的任务，Coq还允许用户使用Coq的实现语言OCaml编写插件。相比之下，在Isabelle / HOL中，没有像Ltac这样的高级自动化语言，并且用户编程自定义证明自动化过程的唯一方法是使用插件。
The situation is a bit different when supporting user-defined, proof-automation procedures. Coq comes with a tactic language for writing proofs, known as Ltac, that is a programming language of its own right. Even though Ltac has some design problems, it does allow users to encode fairly complicated proof automation procedures in a lightweight manner. For heavier tasks, Coq also allows users to write plugins in Coq's implementation language, OCaml. In Isabelle/HOL, in contrast, there is no higher-level automation language like Ltac, and the only way the user can program custom proof automation procedures is with plugins.
这篇关于与Coq相比，Isabelle证明助理的优缺点是什么？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！