Generating Mutually Inductive Theorems from Concise Descriptions

TL;DR

This paper introduces defret-mutual-generate, a utility that automates the generation of theorems for large mutually recursive function cliques in ACL2, significantly simplifying proof maintenance and readability.

Contribution

The paper presents a new utility that automates common proof patterns for large mutually recursive function cliques, improving proof efficiency and maintainability.

Findings

Reduced theorem form size by an order of magnitude for a 49-function clique

Significantly decreased manual editing when definitions change

Enhanced proof readability and automation in ACL2 environments

Abstract

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.