Towards Automatic Transformations of Coq Proof Scripts

Autor:	Magaud, Nicolas
Rok vydání:	2024
Předmět:	Computer Science - Logic in Computer Science Computer Science - Symbolic Computation Computer Science - Software Engineering
Zdroj:	EPTCS 398, 2024, pp. 4-10
Druh dokumentu:	Working Paper
DOI:	10.4204/EPTCS.398.4
Popis:	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. Comment: In Proceedings ADG 2023, arXiv:2401.10725
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/2401.11897 Zobrazit plný text záznamu View this record from Arxiv