Community experiences writing Lamport's structured proofs

Question

About two years ago, I came across this paper by Lamport

http://research.microsoft.com/en-us/um/people/lamport/pubs/lamport-how-to-write.pdf

on writing proofs hierarchically. It changed how I wrote all of my proofs for about six months and identified the gaps in my understanding and knowledge extremely well. These days, I won't use it for simpler proofs, but I find it indispensable when I want to thoroughly understand long and complex ones.

I think this is potentially a wonderful pedagogical tool, in that all steps and assumptions are organized and easily referred to, and is also useful for self-checking. Some discussion on the blog evaluating Deolalikar's claimed proof of $P\neq NP$, to give one example, Professor Tao's apposite remarks on the need for precision, (August 15, 2010, 3:05 PM - I hope he doesn't mind my quoting him)

One thing this illustrates is the importance of setting out precise definitions. I feel that if Deolalikar had written down a precise definition of what it meant for a solution space to be polylog parameterisable, the difficulties would have been found a lot sooner, and in particular probably by Deolalikar himself, well before he finished the preprint to share with others.

reminded me of Lamport's essay. Lamport comments on something similar from his own experience:

The style was first applied to proofs of ordinary theorems in a paper I wrote with Martín Abadi. He had already written conventional proofs—proofs that were good enough to convince us and, presumably, the referees. Rewriting the proofs in a structured style, we discovered that almost every one had serious mistakes, though the theorems were correct. Any hope that incorrect proofs might not lead to incorrect theorems was destroyed in our next collaboration. Time and again, we would make a conjecture and write a proof sketch on the blackboard—a sketch that could easily have been turned into a convincing conventional proof—only to discover, by trying to write a structured proof, that the conjecture was false. Since then, I have never believed a result without a careful, structured proof. My skepticism has helped avoid numerous errors.

Has anyone had experience with this style of writing proofs?

Answer 1

From a proof-theoretic point of view, Lamport essentially suggests is writing proofs in natural deduction style, along with a system of conventions to structure proofs by the relevant level of detail. (It would be very interesting to study how to formalize this kind of convention -- it's something common in mathematical practice missing from proof theory.)

I have written proofs in this style, and once taught it to students. I find that this system -- or indeed any variant of natural deduction -- is extremely valuable for teaching proof to students, because it associates to each logical connective the exact mathematical language needed to use it and to construct it. This is particularly helpful when you are teaching students how to manipulate quantifiers, and how to use the axiom of induction.

When doing proofs myself, I find that this kind of structured proof works fantastically well, except when working with quotients -- i.e., modulo an equivalence relation. The reason for this is that the natural deduction rules for quotient types are rather awkward. Introducing elements of a set modulo an equivalence relation is quite natural:

$$ \frac{\Gamma \vdash e \in A \qquad R \;\mathrm{equivalence\;relation}} {\Gamma \vdash [e]_R \in A/R} $$

That is, we just need to produce an element of $A$, and then say we're talking about the equivalence class of which it is a member.

But using this fact is rather painful:

$$ \frac{\Gamma \vdash e \in A/R \qquad \Gamma, x\in A \vdash t \in B \qquad \Gamma \vdash \forall y,z:A, (y,z) \in R.\;t[y/x] = t[z/x]}{\Gamma \vdash \mbox{choose}\;[x]_R\;\mbox{from}\;e\;\mbox{in}\;t \in B} $$

This rule says that if you know that

• $e$ is an element of $A/R$, and
• $t$ is some element of $B$ with a free variable $x$ in set $A$, and
• if you can show that for any $x$ and $y$ in $R$, that $t(y) = t(z)$ (ie, $t$ doesn't distinguish between elements of the same equivalence class)

Then you can form an element of $B$ by picking an element of the equivalence class and substituting it for $x$. (This works because $t$ doesn't care about the specific choice of representative.)

What makes this rule so ungainly is the equality premise -- it requires proving something about the whole subderivation which uses the member of the quotient set. It's so painful that I tend to avoid structured proofs when working with quotients, even though this is when I need them the most (since it's so easy to forget to work mod the equivalence relation in one little corner of the proof).

I would pay money for a better elimination rule for quotients, and I'm not sure I mean this as a figure of speech, either.