One thing I like on theorem proving is that committing to providing a proof of key properties of some artifact, be it a software program or a mathematical definition, creates a pressure to structure the artifact in a way that is amenable to precise reasoning. Hence, artifacts which are equipped with proofs of key properties, are, in my experience, easier to understand then those which are not equipped with such proofs. So, when practicing theorem proving, I am generally happy about the resulting definitions or programs. However, I am not that happy about the structure of the proofs that I produce.

The problem

In my opinion, this is because nothing forces me to structure proofs properly. Unlike the main artifacts, poorly organized proofs do not cause my any significant cognitive discomfort in the short-term. Perhaps only the thought that “when I make this public, I might be viewed as a flaky amateur” is slightly unpleasant, but that has almost no effect due to the percieved time distance of the future event.

This can be also phrased differently. When writing program code, refactoring brings an immediate gain in the form of better understanding of the code. However, I do not get such benefit when refactoring proofs; on the contrary, the immediate consequence of extracting a small argument into a separate lemma is that I lose the context of the bigger proof. In aprticular, when switching between a proof-in-progress of a larger theorem and a proof of newly-extracted lemma, I tend to forget the intended next steps in the WIP proof.

Here is another point, this time specific to Rocq. When I read through the developments of high-profile projects, such as the Stdpp library, I see short proofs written in the SSReflect proof language/framework. One thing I like about these proofs is that the important dependencies are easily visible. One can thus get a higher-level idea of how to proof works (eg., “by induction using Lemma A, B, and C”) without having to dig through some noise.

Why bother?

What benefits would I get from improving the way I write proofs? Should I invest an effort to improving the proofs only to impress people about how short my proofs are? Although I know that impressing people is important and I tend to underestimate the effects of good or bad impressions, to internally motivate me into additional effort, more benefits would be needed.

One benefit of short proofs with the important things visible would be that writing a paper or a blog post about the development could become easier. If I could easily see the high-level arguments for why a property holds, I could easily describe it informally in the writing. This would be a pretty reliable, non-speculative benefit.

Another benefit, potentially powerful but a bit speculative, would be in reuse. I can not tell in advance which small lemmas or proof automation scripts would be reusable later, but when they are reusable, it saves a lot fo time when developing new proofs. Not only I wouldn’t have to spend time repeating an argument, but I would also not have to flush the important content of my working memory related to the proof at hand just to think about how to spell out the details of a boring argument.

Improvement ideas

I could just go through my current development and start refactoring the proofs. However, what I would really want is some mechanism which makes me structure proofs better automatically, in the same way proving properties about code makes me structure the code better automatically. Something that would reduce the friction related to the “I will structure this better now” approach, or something that would make the eventual discomfort caused by poor structure come sooner. One option would be “pair proving” - having a peer who would join me in a proving session, be disgusted by the structure sooner, and perhaps help me regain the lost context after a re-factoring detour. However, such peers are not exactly easy to find; moreover, I have done this before, and while it was really fun, just one hour of pair proving could make me exhausted to the point of being done for the day.

One improvement I already started doing is writing notes whenever I leave a proof unfinished. This reduces the time needed when going back from the supporting lemmas to the main theorem.

Another thing I would like to try is a tool for suggesting names of lemmas. When refactoring on the go, in the middle of another work, thinking about names for some lemmas can be some source of friction. Some lemmas have obvious candidates for their names (f_comm standing for “f is commutative”), and some lemmas relate only a small number of entities (f_g_lt_h standing for “for all x, f of g of x is less than h of x”), other relate a rather larger number of entities - and for these, name suggestions would be helpful.

Maybe I could adopt the ‘red-green-refactor’ cycle commonly applied in test-driven development. This has the problem that it relies solely on self-discipline; however, being targed about refactoring would be helpful.

Lastly, having a personal base library would also be helpful. In many projects, I use the mentioned Stdpp library, and extend it with additional definitions and theorems. It happened to me quite a few times that I wanted to reuse a lemma fron another project of mine, and the easiest thing was to just copy-paste it and modify to the current setting. Perhaps I could use the ‘red-green-refactor’ cycle on a larger scale: that is, instead of “build-publish-abandon”, I could do “build-publish-refactor”. Meaning that after “finishing” a project and writing a paper about it, I should go back to the development and extract the reusable parts to my personal base library. This requires some additional infrastructure work, since I probably do not want to archive projects depending on my personal base library, say, on Zenodo. So I may want to have a way of exporting project with its Rocq dependencies to an archive, or with all dependencies to an OCI/Docker image. Both of which should be fairly easy with Nix.

Conclusion

So, I want to improve my proofs. Perhaps a proof assistant can be more than a reliable devil’s advocate.