What are the strengths and weaknesses of the Isabelle proof assistant compared to Coq?

Asked 10/5, 2015 at 13:44 Answered 14/8, 2017 at 11:31

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

Enlargement answered 10/5, 2015 at 13:44 Comment(0)

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.

Formerly answered 11/5, 2015 at 4:13 Comment(16)

Most of this seems correct to me, but I have two nits to pick: first of all, Isabelle does have matrices, and the type of matrix multiplication is ('a::semiring_1)^'n^'m ⇒ 'a^'p^'n ⇒ 'a^'p^'m. You can, for instance, multiply matrices of type real^2^3 and real^4^2 to get one of type real^4^3. This works because for any positive integer n, there is a built-in type that consists of the numbers from 0 to n-1. – Sungsungari 12/5, 2015 at 6:50

As for a tactic language: Isabelle now has Eisbach (ssrg.nicta.com.au/projects/TS/tactics.pml) – Sungsungari 12/5, 2015 at 6:50

Also, breaking down proofs that are too hard for automation alone can be done quite naturally with structured Isar proofs, in my opinion. – Sungsungari 12/5, 2015 at 6:50

@ManuelEberl thanks a lot for the comments, I'll try to update my answer later to make it more accurate. – Formerly 12/5, 2015 at 14:24

It would help if the answer clarified to what extent Isabelle/HOL and Coq are in fact alternative tools for the same tasks. Right now, the answer implies that the two are interchangeable but that probably wasn't intended. – Fleecy 7/10, 2017 at 5:19

The absence of excluded middle in coq is because it's using intuitionnist logic, excluded middle exists in classical logic; furthermore, it's not an axiom. You might want to edit your answer. – Subclavius 4/4, 2018 at 11:49

@Subclavius Could you clarify what you mean by the excluded middle not being an axiom? – Formerly 4/4, 2018 at 12:17

@ArthurAzevedoDeAmorim It's consequence of $\neg \neg \phi = \phi$. It's consequence of non contradiction axiom in classic logic. – Subclavius 4/4, 2018 at 14:1

@Subclavius Since there are many equivalent formulations of the excluded middle, which one you pick as an axiom and which ones are derived as theorems is largely a matter of taste. Some systems use the principle of non-contradiction as an axiom, as you pointed out, whereas others, including the classical fragment of Coq's standard library and Gentzen's NK calculus, use the excluded middle. Nevertheless, my goal was not to argue about what is an axiom, but to point out that these basic reasoning principles differ in Coq and Isabelle. I'll edit my answer. – Formerly 4/4, 2018 at 15:49

Can the excluded middle be extracted to calls to call-with-current-continuation? – Allhallowmas 27/7, 2018 at 12:51

@Allhallowmas This probably belongs in a separate question. – Formerly 27/7, 2018 at 14:41

I have seen a few instances where Isabelle/HOL is used to prove properties of computer programs, but none for Coq so far. Latest in Formally Verified Software in the Real World: "While generating glue code, CAmkES produces formal proofs in Isabelle/HOL, following a translation validation approach [Pnueli et al., 1998], demonstrating that the generated glue code obeys a high-level specification, and that the generated capDL specification is a correct refinement of the CAmkES description [Fernandez, 2016]." – Flasket 21/10, 2018 at 9:17

The philo of class. and [plato.stanford.edu/entries/logic-intuitionistic/](cons. logic) differ markedly. Same logic symbols but in class, logic you label propositions with true and false - it is assumed every proposition has such a label (everyone forgets about the μ for "meaningless" though). You can prove "by contradiction" assuming 2 labels & consistent systemIn constructive logic, a true proposition means you have a method of positively demonstrating the truth to a questioner. In particular for "exists" statements, you need to generate the element yielding true. – Flasket 21/10, 2018 at 9:33

@David there are many examples of verified software in Coq. Famous ones include the compcert verified c compiler, the vellvm backend for llvm, the certikos operating system, and those using the verified software toolchain from Princeton. – Formerly 21/10, 2018 at 13:51

@ArthurAzevedoDeAmorim Thanks Arthur. I will need to find some time to learn more. – Flasket 21/10, 2018 at 22:28

@ArthurAzevedoDeAmorim May I ask, which would you rather start with? Are there any good tutorials to get you started proving some basic theorems etc.? – Bronchi 27/10, 2018 at 10:41

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!

Chilt answered 14/8, 2017 at 11:31 Comment(4)

Re "Only the computer knows why": there isn't a way to peek at what it figured out? – Cosecant 14/9, 2019 at 21:29

You ask Isabelle to show you the generated proof terms, however, you’ll be overwhelmed by the size and detail. Human-understandable proofs, like the Isar proof of Cantor’s theorem in the above answer, abstract away from details like “what is a set” and “what does ‘∃f’” mean. – Kerril 20/3, 2020 at 8:5

Btw the link seems broken :/ – Bron 22/11, 2022 at 7:57

Unfortunately, the link was not archived by archive.org. – Spatula 27/2 at 2:32

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.

Broadus answered 10/5, 2015 at 22:36 Comment(3)

Could you clarify what you mean by Coq's type system being non-deterministic? – Formerly 11/5, 2015 at 2:57

Oh, sorry, it was late... I meant non terminating, I'll correct this. – Broadus 12/5, 2015 at 11:39

Oh, I see. I think this is a bit delicate, because type-checking Coq programs actually is decidable. What can cause the type-checker to loop are features like type-class inference, but that, strictly speaking, lies outside of the type system. Also, you can always force type-checking to be terminating by manually supplying type-class instances. – Formerly 12/5, 2015 at 14:21

Hot tags

Godot Unity Godot Help Programming Godot 4.X GUI GDScript 3D 2D Physics CSharp Godot 3.X VR XR Projects C++

Theories

Dependent types

Basic reasoning principles

Style of interaction

Recommended topics

Hot tags