HomePage RecentChanges

metamathCalculationalProofs

SHOW PROOF /CALCULATIONAL

An idea that I had some time ago is to output Metamath proofs as 'calculational proofs', i.e., in the format devised by Wim Feijen; this format is explained and used extensively in Dijkstra and Scholten, "Predicate calculus and program semantics", and in Gries and Schneider, "A Logical Approach to Discrete Math". And of course A.J.M. (Nettie) van Gasteren's "On the Shape of Mathematical Arguments" (Springer, Lecture Notes In Computer Science 445).

For some simple examples, see my collection of puzzle solutions that uses this format (http://www.solcon.nl/mklooster/calc/calc-sols.html). (Web references on this proof format: EWD1300 (from page 16 onward) from http://www.cs.utexas.edu/users/EWD/; the work on Structured Calculational Proofs by Jim Grundy, Ralph Back, and Joachim von Wright (http://www.google.com/search?q=%22structured+calculational+proofs%22).)

For now I'll just post a couple of examples that I've worked out by hand. Given enough annotations and/or heuristics, it should be possible to generate this kind of proof automatically from every Metamath proof. I don't think I'll ever have time to program that myself, unfortunately. That's why I'm posting here…

Announcement. I've been able to set apart some time after all. As a first step towards this goal, I've created Hmm, a Haskell module to parse and verify Metamath proof databases; see http://www.solcon.nl/mklooster/repos/hmm/. Later, this code could be used to derive calculational proofs from existing Metamath proofs. --marnix
I like the fact that you decompress proofs. I looked up Haskell. Interesting! May have to check it out. --ocat
Looking at Haskell convinced me: it is time to abandon Java. But I think Python… I want a GUI/user interface that is more approachable than "Swing". BWDIK. --ocat

Comments and feedback (and implementations :-) are welcome! --marnix

I (marnix)'ll add some comments on the why and how.

Why: Personally, I find calculational proofs much more readable than the style on the Metamath site. And they are more complete than the semi-formal proofs usually found in textbooks. And it also brings out the calculational structure that is often present in the Metamath proofs, but which is obfuscated by the many versions of transitivity theorems and 'window rules'. The calculational format brings out the really relevant theorem invocations in a proof, and makes the trivial ones implicit in the format. Think of it as a more essential format than SHOW PROOF /ESSENTIAL. :-)

How: What would the algorithm be to compute proofs in the format of the examples below? It seems fairly simple to me, but perhaps it is difficult to get across here. Generate a calculational proof for the root node of the 'proof tree'. There will be multiple ways to do that usually; use heuristics. In this proof there will be 'holes', one for every subtree of the root of the proof tree. For each of these subtrees, recursively generate a calculational proof. In doing that, let the form of the subproof be guided by the step in the parent proof that contains the 'hole'. After that, if possible, 'lift' the subproof to the parent level, and in that way merge the two.

Now to the examples.

Examples

Apology: all examples use 'Metamath syntax' (more precisely: Norm's set.mm syntax). Personally I think that that is less readable than other ASCII-izations of math that I've seen around, but it should be readable for people who are using Metamath's set.mm.

Russell's Paradox

http://us.metamath.org/mpegif/ru.html.

      { x | x e/ x } e/ V
  <->     "(df-nel) with A := { x | x e/ x } and B := V"
      -. { x | x e/ x } e. V
  <->     "(is-set) with y := x and A := { x | x e/ x }"
      -. E. y y = { x | x e/ x }
  <==     "choose a specific y (nex)"
      -. y = { x | x e/ x}
  <->     "(cleqab) with A := y and ph := x e/ x"
      -. A. x ( x e. y <-> x e/ x )
  <-      "substitute x := y (a4b1) using subproof"
  
        assume x = y
  
            ( x e. y <-> x e/ x )
        <->     "assumption; subproof"
  
                   x e/ x
               <->    "(df-nel) with A := x and B := x"
                   -. x e. x
               <->    "assumption; assumption"
                   -. y e. y
          
            ( y e. y <-> -. y e. y )
  
      -. ( y e. y <-> -. y e. y )
  <->     "logic"
      ( y e. y <-> y e. y )
  <==>    "logic"
      TRUE

Distributive law for cross product over union

http://us.metamath.org/mpegif/xpundi.html

      ( ( A X. B ) u. ( A X. C ) )
  =       "LHS of u.: (df-xp); RHS of u.: (df-xp)"
      ( { <. x, y >. | ( x e. A /\ y e. B ) } u. { <. x, y >. | ( x e. A /\ y e. C ) } )
  =       "(unopab)"
      { <. x, y >. | ( ( x e. A /\ y e. B ) \/ ( x e. A /\ y e. C ) ) }
  =       "in pair comprehension: (andi)"
      { <. x, y >. | ( x e. A /\ ( y e. B \/ y e. C ) ) ) }
  =       "in pair comprehension: RHS of /\: (elun)"
      { <. x, y >. | ( x e. A /\ y e. ( B u. C ) ) }
  =       "(df-xp)"
      ( A X. ( B u. C ) )

This example has some distinctive features:

      ( ( A X. B ) u. ( A X. C ) )
  =       "LHS of u.: (df-xp); RHS of u.: (df-xp)"
      ( { <. x, y >. | ( x e. A /\ y e. B ) } u. { <. x, y >. | ( x e. A /\ y e. C ) } )
  =       "(unopab)"
      { <. x, y >. | ( ( x e. A /\ y e. B ) \/ ( x e. A /\ y e. C ) ) }
  =       "in pair comprehension: subproof"
        
            ( ( x e. A /\ y e. B ) \/ ( x e. A /\ y e. C ) )
        =       "(andi)"
            ( x e. A /\ ( y e. B \/ y e. C ) ) )
        =       "RHS of /\: (elun)"
            ( x e. A /\ y e. ( B u. C ) )
        
      { <. x, y >. | ( x e. A /\ y e. ( B u. C ) ) }
  =       "(df-xp)"
      ( A X. ( B u. C ) )

Omega is a set

http://us.metamath.org/mpegif/omex.html

       TRUE
  <==>    "(zfinf)"
       E. x ( (/) e. x /\ A. y e. x  suc y e. x )
  ->      "in E. x: subproof"
  
         assume (/) e. x
         
              A. y e. x  suc y e. x
         ->      "in A. y: weaken by adding antecedent (ax-1)"
              A. y e. om ( y e. x -> suc y e. x )
         ->      "(peano5) using assumption"
              om (_ x
         
       E. x  om (_ x
  ->      "subset of a set is a set (ssex) using (visset)"
       E. x  om e. V
  <->     "body of E. x contains no x"
       om e. V

Discussion

The Dijkstra reference is interesting and worth reading (esp. for people thinking about parsing math). The reference

http://www.abo.fi/~jwright/schoolmath/papers/tucs65.pdf

found via the google search you suggested is maybe a bit more focused and up-to-date. I'm not sure why you say you like this presentation better; as far as I can tell these "calculational" structured proofs and the "Lamport-style" structured proof "with justifications" seem substantially the same to me, up to minor formatting details. At any rate, this general style of proof does seem like a good one, both for output and input. --jcorneli

Thanks for the feedback, and I agree the report above is a good summary of the proof format. On comparing the presentations: do you really mean mean that you find the above proof the same as the 'structured proof with justifications' on Example of structured proof? When counting the number of symbols, the above calculation has only little longer than the 'coarse outline', and that includes full justification of every step (except for 'basic logic' such as transitivity). The 'structured proof with justifications' is way longer – even a lot longer than the proof as shown on the Metamath site.

And I just realized, why I find all five proofs on that page hard to follow, is because of their tree-like format. I find it difficult to see the 'flow' of the proof. And, for many proofs in textbooks and in Metamath's set.mm, I discovered that they usually have a calculational 'backbone' which is mostly linear. That linear structure is hidden in the formats of these five proofs. Or am I looking in the wrong way, and is this just because of the way I have been trained (training myself) in my mathematical thinking? --marnix

Math is tree-like; IMO you can't avoid that. Whereas the calculational proofs refer to other known theorems for justification of steps, the Lamport-style proof simply adds another level to the outline. If you just read the top level of steps in the outline, you'll see a "linear" proof with references to lower levels. This is essentially the same as what you have here, but your version benefits from being part of a corpus with named theorems. Still, if I expanded the references to named theorems here, your proof would look treelike and long too. --jcorneli

Well, yes, I agree that when drilling down to the lowest level, formal proofs are tree-like. That's true for Metamath, Lamport-style, natural deduction, structured calculational proofs, etc. What I like about the calculational style is that it collects fairly big chuncks of a tree, and shows them as linear calculations. And in many cases (at least for the Metamath proofs that I've tried to tackle), the remaining nesting is limited to just a few levels, if any. For example, the first proof above of

    ( ( A X. B ) u. ( A X. C ) ) = ( A X. ( B u. C ) )

has no nesting at all. So to the reader of this proof, this is not a tree (although it corresponds to a Metamath tree). So it is possible to avoid the tree-like format in the presentation of a proof, or at least minimize the nesting.

This is achieved by leaving out invocations of transitivity theorems (like eqtr4) and 'window rules' (like (biopabi)), and making them implicit in the proof format. Yes, this loses information, but in a different – and to me better – way than the 'coarse outline' of the example does.

I was comparing the calculational proof above to the 'coarse outline', since it seems to work at about the same level of detail, and it is roughly the same size. Now, the 'coarse outline' is not linear, if I understand it correctly: 6 follows from 1 and 5, and 5 follows from 2, 3 and 4. This is a tree, it's just not written like that (and therefore it took me at least a couple of minutes to understand).

Perhaps we're just using the same words with different interpretations. I still feel that there is some qualitative difference between the calculational format and, say, the Lamport style. Not sure exactly what it is, though. This discussion helps; thanks!

By the way, what do you (and others) think about a project to calculationalize Metamath proofs? Would that help people in trying to understand the proofs? Any takers? --marnix

Ah, if the difference is that each step in calculational proofs only follow from the immediately previous step and the "hint", that does seem like a stylistic advantage over other sorts of presentations. It seems clear that any proof can be written in such a style by creating lemmas as needed and referencing them in subsequent hints. I continue to think that these calculational proofs are about the same as the Lamport-style proofs. If you want to know more about what Lamport has to say about proofs, you should check out the reference on the structured proofs page. He may even endorse the "derive each step only from the previous step and the hint" strategy – however, he might not. I don't know enough about metamath to comment on whether or not this is a good way to present or generate proofs. I do tend to think the strategy of presenting proof from the "top level" and allowing people to drill down as they need or desire is a great idea. However, I'm less clear on how to use this strategy for proof generation. You seem to have had some luck with that. I'd need to look at it more to see how well this approach works for me. Then thinking about formalizing it is another story! Even massaging a "known" proof into this format may be computationally tricky. --jcorneli

I enjoyed Lifschitz's On Calculational Proofs <http://www.cs.utexas.edu/users/vl/papers/calc.ps>.