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.

翻译：像 Coq 这样的证明辅助工具越来越受欢迎，帮助数学家完成他们所猜想结果的证明。然而，形式化证明仍然技术性很强，尤其难以重用。在本文中，我们提出一个框架来执行事后的脚本转换。这些转换旨在作为自动化后处理步骤应用，在证明完成后进行。作为示例，我们展示一种转换，该转换接受任意大的证明脚本，并生成等效的单行证明脚本，可以由 Coq 单步执行。其他应用，例如完全展开证明脚本（用于调试目的）、移除所有命名假设等，也可以在该框架内开发。我们将我们的工具应用于各种 Coq 证明脚本，包括来自 GeoCoq 库的一些脚本。