与Coq相比，Isabellecertificate助手的长处和短处是什么？
与Coq相比，Isabelle / HOLcertificate助理是否有缺点和优势？
我大多熟悉Coq，对Isabelle / HOL没有太多的经验，但是我可能会有所帮助。 也许在Isabelle / HOL上有更多经验的人可以帮助改善这一点。
这两个系统之间有两大分歧：基础理论和交互方式 。 我将尝试简要介绍一下每种情况下的主要区别。
理论
Coq和Isabelle / HOL都是基于强大的，非常富有performance力的高阶逻辑。 但是，这些逻辑在几个特征上有所不同：
相关types
Coq的逻辑是一个依赖型理论，被称为归纳结构 （简称CIC ）。 这里的“依赖types”意味着Coq中的types可以指普通的值。 例如，可以用types写一个matrix乘法函数mult
mult : forall (nmp : nat), matrix nm -> matrix mp -> matrix np
这个函数的types表示它需要两个matrix作为input，维度nxm之一和维度nxm另一维度，并返回一个维度为nxp的matrix。 另一方面，Isabelle / HOL理论不具备依赖types; 因此，不能写出与上述types相同的多function函数。 相反，我们必须编写一个适用于任何typesmatrix的函数，并且当它接收到正确types的参数时certificate这个函数的特定属性。 换句话说，当在Isabelle / HOL上工作时，需要在Coqtypes中明确的某些属性作为单独的定理来声明。
虽然依赖types对于某些事情是有趣的，但是它并不清楚它们通常是多么有用。 我的印象是，有些人觉得他们使用起来非常复杂，而且在types层次上expression某些属性的好处，而不是把它们作为单独的定理，这样做并不值得这种额外的复杂性。 就个人而言，当有明确的理由时，我喜欢在less数情况下使用依赖types。
常见的公理
Coq的理论默认缺乏很多在math实践中常见的推理原则，比如被排除的中间的规律 （即非build设性地推理的能力），扩展性（例如，能够说产生相同结果的函数本身是平等的）和select的公理。 另一方面，在Isabelle / HOL，这样的原则是内置的。
从理论上讲，这不是一个大问题，因为Coq的逻辑是为了让人们安全地将这些推理原理作为额外的公理而添加的。 尽pipe如此，我还是觉得在伊莎贝尔/霍尔做这种推理是比较容易的，因为逻辑是从头开始build立起来的。
互动风格
Coq和Isabelle / HOL都是交互式定理certificate 。 他们是编写关于他们的定义和certificate的语言; 这些certificate是由电脑检查，以确保他们没有错误。 在这两个系统中，通过给出解释如何certificate某些事情的命令来logging证据。 然而，在每个系统上发生这种情况的方式各不相同。
一般来说，Isabelle / HOL对“button式”自动化的支持更为成熟。 例如，它带有着名的sledgehammer策略，它引用了几个外部的自动定理certificate器和求解器来试图certificate一个定理。 Coq还带有许多强大的自动化程序，如omega或congruence ，但它们并不普遍适用，许多在Isabelle / HOL中用单一命令可以解决的定理在Coq中需要更明确的certificate。
当然，这个便利是有代价的。 有人告诉我，在Isabelle / HOL中，很难控制自己的证据，因为这个系统本身试图做很多事情。 当certificate简单的定理时，这并不是一个问题，但是当certificate自动化不够强大，并且需要告诉定理certificate者如何更详细地进行时，问题就成了一个问题。
在支持用户定义的校验自动化程序时，情况有点不同。 Coq提供了一种用于编写certificate的策略语言 ，称为Ltac，它是一种自己编程语言。 即使Ltac有一些devise问题，它也允许用户以轻量级的方式编码相当复杂的自动化程序。 对于较重的任务，Coq还允许用户使用Coq的实现语言OCaml编写插件。 在Isabelle / HOL中，相比之下，Ltac没有更高级别的自动化语言，用户可以编程自定义校样自动化程序的唯一方法是使用插件。
由于“Isabelle / HOL”在这个问题上已经过时，所以我会谈谈在Isabelle中使用的HOL逻辑，我认为这是用来与Coq进行比较的最好的逻辑。 我不是types系统和逻辑的专家，但是我认为我在这里说的是正确的，至less大概是这样。 这当然也是品味的问题;而我的回答可能是主观的。
最深刻的区别在于types系统和逻辑。
我认为对于那些熟悉ML家族function语言的人（甚至对知道SML的人更是如此），它的实力是更自然的，它使用务实的方法解决问题，例如使用经典逻辑作为一个基础。 它的types系统接近于Hindley Milner的types，并且默认终止（如果它不被用户修改）。
另一方面，Coq更严格，使用直觉逻辑。 它有一个具有几个命令的专用types系统，并允许types依赖性，这可能是棘手的处理，并可能在某些情况下不终止。 它也允许从Isabelle中直接不可能的certificate（可能相对低效）提取程序。
我将要说明的一个方面，即Isabelle / HOL的“button式”function是Cantor的经典“对angular化”论证的自动化 （回想一下，这表明从自然界到权力集合并没有任何意外，或者更一般地任意设定其功率设定）。
theorem Cantor: "∄f :: 'a ⇒ 'a set. ∀A. ∃x. A = fx" proof assume "∃f :: 'a ⇒ 'a set. ∀A. ∃x. A = fx" then obtain f :: "'a ⇒ 'a set" where *: "∀A. ∃x. A = fx" .. let ?D = "{x. x ∉ fx}" from * obtain a where "?D = fa" by blast moreover have "a ∈ ?D ⟷ a ∉ fa" by blast ultimately show False by blast qed
我刚刚介绍给你的将是Cantor经典论证到Isabelle / HOL的翻译。 毫无疑问，巧妙！ 但是，Isabelle / HOL即使是这样的certificate也可以实现自动化，
theorem "∄f :: 'a ⇒ 'a set. ∀A. ∃x. fx = A" by best theorem "∄f :: 'a ⇒ 'a set. ∀A. ∃x. fx = A" by force
certificate系统能够自动certificateCantor的陈述。 对研究人员来说，一方面这是有帮助的，但是这是一把双刃剑。 我觉得有用的是，像对angular化论证这样复杂的真实陈述可以被信任在Isabelle / HOL的内部得到证实，因为我的定理从此更加复杂。 另一方面，我进一步的研究是由计算机的自动化进程驱动的，我可以越来越less地解释为什么或为什么这个定理是真的。 只有电脑知道为什么，只要我们可以问它！
