# Community experiences writing Lamport's structured proofs

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?

• Lamport's article says that there is a mistake in Kelley's proof of Schroeder-Bernstein. But he doesn't say what the mistake is (maybe he does that to reinforce his point that mistakes are hard to find, but nevertheless I wish he did explicitly identify the error). Does anyone know whether this mistake has been found and acknowledged by others? Aug 16, 2010 at 8:58
• @Pete I looked at it 5 years ago and had trouble spotting the error. But when I went to formalized Kelley's proof in Coq I found an error. It was something about neglecting the possibility of an element x being its own ancestor. Aug 16, 2010 at 20:02
• @Pete. Elaborating on @Russell. Using the notation from Kelley (books.google.co.in/… ) p. 28, I think his claim that "f maps A_E onto B_O" is not correct since x might already belong to the set of ancestors of x. For eg. if f is onto and g=f^{-1} then each element x in A has exactly two ancestors {x,f(x)} and each element in y also has exactly two ancestors {y,g(y)} Aug 19, 2010 at 11:10
• Feb 4, 2016 at 11:28
• Related: there is a question on Math SE about identifying the mistake in Kelley's proof — Lamport claims there is an error in Kelley's proof of the Schroeder-Bernstein theorem. What is it?
– user82537
Sep 16, 2020 at 11:42

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.

• @Neel: A linguistic comment. In writing math (i) we strive for clarity of meaning above all else and (ii) we have a truly international audience, I think it is a good idea to try to use words and terminology which are maximally transparent. Ideally, someone encountering a term for the first time can reasonably guess its meaning. As a corollary, I think we should try to avoid "tricky" words which mean the opposite of what someone might guess. In this case, you say utterly invaluable, and, though your usage is utterly correct, I can imagine many readers here misinterpreting it. Aug 16, 2010 at 8:54
• It might be worth mentioning that Lamport's approach more closely follows Jaskowski-style natural deduction rather than the Gentzen and Prawitz style of natural deduction that most people are taught in courses on proof theory, lambda calculus, etc. They represent essentially the same abstract structure but the practical difference in usability is very great. Aug 16, 2010 at 12:35
• If anyone is interested in the background of my remark, a quick overview (with an attractively typeset demonstration of Jaskowski-style proof boxes) can be found in the History section, page 44, of Restall's Proof Theory and Philosophy: consequently.org/papers/ptp.pdf Aug 16, 2010 at 17:36
• Anthony: By subderivation he means the part of the proof that refers to the representative of the equivalence class. For example, say you're working with the rationals represented as pairs of natural numbers p/q. The whole part of the proof that manipulates some p/q must be invariant under multiplying p and q by a nonzero integer. Anyway, I'm not sure I agree with Neel that this is any less of a problem in non-structural proofs; it's just that dealing with these issues formally is a little painful. When possible, one could alleviate part of the pain by working with normal forms. Aug 17, 2010 at 7:57
• Quotients are a godforsaken mess; it's not just undergrads that are struggling with them. They aren't easy to use in Coq either, unless one essentially constructs them by hand (i.e., instead of equivalence classes one uses objects defined explicitly, with explicit projection and lift maps). Feb 4, 2016 at 11:30