What are the strengths and weaknesses of the Isabe

问题:

Does Isabelle/HOL proof assistant have any weaknesses and strengths compared to Coq?

回答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

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.

Basic reasoning principles

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.

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.

(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.)

Style of interaction

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 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.

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.

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.

回答2:

As "Isabelle/HOL" is precised in the question, I will talk about the HOL logic used in Isabelle which I think is the best one to use for a comparison with Coq. I am not an expert in type systems and logics, but I think what I say here is correct, at least approximately. This is also certainly a matter of taste ;-) and my answer may be subjective.

The most profound differences lie in the type systems and the logics.

I would say it strength is to be more natural to someone who knows a functional langage of the ML family (and even more to someone who knows SML) and it uses a pragmatic approach to solve problems as for example the use of a classical logic as a basis. Its type system is close to the Hindley Milner's one and terminating by default (if it is not modified by the user).

On the other hand, Coq is more strict and uses an intuitionistic logic. It has a specialized type system with several orders and allows type dependencies which can be trickier to deal with and may be non-terminating in some circumstances. It also allows one to extract programs from proofs (that may be relatively inefficient) which is not directly possible in Isabelle.

回答3:

One aspect, which I will illustrate, of the "push-button" efficacy of Isabelle/HOL is its automation of the classic "diagonalization" argument by Cantor (recall that this states that there is no surjection from the naturals to its power set, or more generally any set to its power set).

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

What I have just presented to you would be the translation of Cantor's classic argument into Isabelle/HOL. No doubt, ingenious! Isabelle/HOL can automate away the insight from even this proof, however:

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

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

The proof system is able to automatically prove Cantor's statement. For a researcher, on one hand this is helpful, but there is a sense in which this is a double-edged sword. I can find it helpful that true statements as complex as a diagonalization argument can be trusted to be proven internally to the Isabelle/HOL, since my theorems are more sophisticated thereby. On the other hand, the further I go in my research being driven by the automatable progress of the computer, I can explain less and less as to why or for what principle the theorem is true. Only the computer knows why, if only we can ask it!