A tale of four theorem provers, or: A (reasonably) opinionated comparison of Isabelle/HOL, Lean, HOL4, and Agda
28 points by blueberrywren
28 points by blueberrywren
I've only ever learnt Agda, and I feel like I should learn another popular proof assistant, but I can never understand the proofs that are made in other proof assistants. I suppose the point is not to understand but to trust that the compiler has checked it? The fact that Agda has barely any tactics means that at the end of the proof, you're left with a very readable program.
For example, the proof that 2 is prime from the post:
theorem prime_two : prime 2 := by
simp
intros k x
simp [divides] at x
have ⟨q,hq⟩ := x
(cases q <;> cases k <;> grind)
versus
two-prime : Prime 2
two-prime .gt1 = s≤s (s≤s z≤n)
two-prime .div zero (divides (suc q) eq) rewrite *-comm q 0 = ⊥-elim (1+n≢0 eq)
two-prime .div (suc zero) (divides (suc q) eq) = inj₁ refl
two-prime .div (2+ zero) (divides (suc q) eq) = inj₂ refl
I can understand the Agda proof by looking up what the requirements of the field gt1 and div are, then I can understand what the available arguments represent and what we're supposed to return as the return value of the function. But in the Lean proof, I have no clue what it's doing; what's the first simp for, what's grind actually doing? I can't translate the proof into mathematical terms, which I personally find annoying.
Yet another manifestation that the optimal shape to write the code, to read it, and to modify it are three different shapes.
When one is writing the proof, there is a side display with a list of goals, so one can see what simp actually did. The written list of just the tactics to apply does not have this affordance. Ideally, some kind of exporting the goal lists after each step would get the norm… but obviously we are not there.
Yeah, this is an example of what you might call “proof language paradigms” which I am sure has been written about somewhere although I don’t know of it. But basically with the proof languages we’ve developed so far there’s a tradeoff between how easy a proof is to write and how easy a proof is to read. The more declarative your proof is the more it looks like a real informal proof that you can read & follow, but also it seems much more difficult to understand why the prover is getting stuck while you are writing the proof.
TLA+ has a proof sub-language that is the most extreme example of declarative proofs I am aware of; you don’t get very much help when figuring out why discharging an obligation failed. However, the proofs are quite readable (as long as you collapse some of the longer nested child proofs). The TLA+ proof language has no support for tactics whatsoever.
Contrast this with Lean where proofs comprise a series of operations that directly manipulate the current assumption & goal states, often in an automated way using tactics. It is very easy to see why a proof obligation cannot be discharged while writing it, but it is impossible to read the proof without stepping through it in a Lean development environment.
I think at least part of the power of using tactics is being able to inspect proof state at any given point. Various tools even make this possible for HTML-rendered versions of these proofs (they names elude me, but I'm sure they're not hard to find). So maybe you don't REALLY need to be able to evaluate proof steps in your head; you need more so to follow the general shape of the proof. Which, I think the lean version shows pretty well.
I do find myself wondering where Rocq (being also fairly constructive and automatable) sits here, though I presume it’d rank similarly to Lean based on my vague failed attempts to learn Lean from a Rocq user perspective over the years.
I’ve never quite got a good handle on what Lean does better than Rocq, and any cases of the opposite.
I think 99% of people that learn theorem provers learn to use perhaps one new one per decade, so comparisons are hard to come by. It’s a big investment!