Generating Mutually Inductive Theorems from Concise Descriptions

Sol Swords
(Centaur Technology, Inc.)

We describe defret-mutual-generate, a utility for proving ACL2 theorems about large mutually recursive cliques of functions. This builds on previous tools such as defret-mutual and make-flag, which automate parts of the process but still require a theorem body to be written out for each function in the clique. For large cliques, this tends to mean that certain common hypotheses and conclusions are repeated many times, making proofs difficult to read, write, and maintain. This utility automates several of the most common patterns that occur in these forms, such as including hypotheses based on formal names or types. Its input language is rich enough to support forms that have some common parts and some unique parts per function. One application of defret-mutual-generate has been to support proofs about the FGL rewriter, which consists of a mutually recursive clique of 49 functions. The use of this utility reduced the size of the forms that express theorems about this clique by an order of magnitude. It also greatly has reduced the need to edit theorem forms when changing definitions in the clique, even when adding or removing functions.

In Grant Passmore and Ruben Gamboa: Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2020), Worldwide, Planet Earth, May 28-29, 2020, Electronic Proceedings in Theoretical Computer Science 327, pp. 95–107.
Published: 29th September 2020.

ArXived at: http://dx.doi.org/10.4204/EPTCS.327.10 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org