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 support for \forall and --> 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 universal quantifier /\ and entailment ==> baked in. HOL then models the \forall quantifier, and logical implication -->. Of 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 instantiate p and q in \forall p q. P p q. There is a syntax, however, for instantiating p and 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

  case (Assert bexp)
  assume eq: "bval p st = bval q st"
  show ?case
    proof -
      have "bval (fse (Assert bexp) p) st = bval (And p bexp) st" by simp
      also from eq have "... = bval (And q bexp) st" by (rule and_equiv)
      also have "... = bval (fse (Assert bexp) q) st" by simp
      finally show "?thesis" .
    qed

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.