Coq and Isabelle/HOL are both “proof assistants” or “interactive theorem provers”. Both systems allows one to model a theorem, and then prove the theorem true. The resulting theorem is then checked, typically by reducing the proof to a program that can be type checked. Type checkers are relatively simple, and so we are confident that these machine checked proofs are correct.
I’ve been reading Software Foundations, which is an introduction to program semantics and verification in which everything is modeled and proved in Coq. Remember doing those dreaded structural induction program semantics proofs by hand? It’s a little bit more satisfying when done in Coq, and sometimes is easier too. More recently, I have been learning Isabelle/HOL. Technically, Isabelle is a proof assistant that allows multiple logics to be built on top of it, including HOL, or High Order Logic.
Unlike Isabelle, Coq only supports High Order Logic natively. Coq has
--> baked in to it.
--> is used to
represent both entailment and logical implication. As a result, it’s
very easy to write down theorems, because there is generally only one
way to write them! Isabelle/HOL, being split up into Isabelle’s
meta-logic and HOL’s logic, is different. Isabelle has a notion of a
/\ and entailment
==> baked in. HOL then
\forall quantifier, and logical implication
course, the two levels are closely related, and it is possible to
switch between them. However, when writing a theorem, it is often not
clear in which level quantification and entailment or implication
should be written.
In my first proofs, I errored on the side of HOL instead of the
metalogic, only to find that some of Isabelle’s utilities only work on
the metalogic level. For instance, there is no quick way to
\forall p q. P p q. There is a syntax,
however, for instantiating
q in the meta-logic quantified
version. The ambiguity between logics is a very inelegant property of
Isabelle/HOL in my opinion.
Isabelle does have some nice features, though. It has a structured proof language called Isar. The idea is to allow Isabelle proofs to look like real, human proofs. (In contrast, non-structural mechanized proofs are just a series of tactics, which do not explain why a theorem is true.) Here’s a simple example:
1 2 3 4 5 6 7 8 9
I bet you can figure out what’s going on, even though you don’t know the syntax.
My last observation about Isabelle/HOL and Coq has to do with their unspoken strategies. Isabelle/HOL seems to be designed to make extensive use of simplification rules. Indeed the tutorial essentially says to prove something, you should write your theorem, try to prove it automatically, and if that fails, add a simplification lemma and repeat! This is nice when it works. However, manipulating rules manually is difficult in my opinion, although that could be because I’m a novice user. Manually manipulating rules in Coq is much easier; the design of tactics just seems to allow me to do what I want more naturally. On the other hand, I’ve been using Coq for longer.
In conclusion, Coq and Isabelle/HOL are both interesting tools, and both can probably accomplish what you want. The differences are subtle, and the best way to get a feel for them is to learn them! I recommend Software Foundations for Coq, and the tutorial for Isabelle/HOL.