Towards Automatic Transformations of Coq Proof Scripts
Nicolas Magaud
TL;DR
The paper addresses the challenge of maintaining and reusing Coq proofs by introducing a framework for a posteriori post-processing transformations of proof scripts. It presents an OCaml-based tool, leveraging SerAPI, that converts large multi-step proofs into concise single-step scripts, demonstrated on examples including a distributivity proof and larger libraries. The approach is validated through transformations of Cantor.v and GeoCoq, and is extended to refactoring proofs generated by automated provers in projective incidence geometry. The work suggests substantial benefits for proof maintenance and portability, with future plans to broaden transformations, support additional tactic languages, and explore reciprocal and debugging-oriented transformations.
Abstract
Proof assistants like Coq are increasingly popular to help mathematicians carry out proofs of the results they conjecture. However, formal proofs remain highly technical and are especially difficult to reuse. In this paper, we present a framework to carry out a posteriori script transformations. These transformations are meant to be applied as an automated post-processing step, once the proof has been completed. As an example, we present a transformation which takes an arbitrary large proof script and produces an equivalent single-line proof script, which can be executed by Coq in one single step. Other applications, such as fully expanding a proof script (for debugging purposes), removing all named hypotheses, etc. could be developed within this framework. We apply our tool to various Coq proof scripts, including some from the GeoCoq library.