# Meta-extract: Using Existing Facts in Meta-reasoning

## TL;DR

This paper discusses an extension to ACL2 that allows correctness proofs of simplifiers to assume the soundness of certain proof tools and facts, enhancing meta-reasoning capabilities.

## Contribution

It introduces a new capability in ACL2 for assuming the correctness of proof tools and facts during simplifier correctness proofs, with illustrative examples.

## Key findings

- Enhanced meta-reasoning in ACL2 with assumed proof tool correctness
- Demonstrated utility through practical examples
- Improved flexibility in simplifying proofs

## Abstract

ACL2 has long supported user-defined simplifiers, so-called metafunctions and clause processors, which are installed when corresponding rules of class :meta or :clause-processor are proved. Historically, such simplifiers could access the logical world at execution time and could call certain built-in proof tools, but one could not assume the soundness of the proof tools or the truth of any facts extracted from the world or context when proving a simplifier correct. Starting with ACL2 Version 6.0, released in December 2012, an additional capability was added which allows the correctness proofs of simplifiers to assume the correctness of some such proof tools and extracted facts. In this paper we explain this capability and give examples that demonstrate its utility.