|
|
|---|
|
|
|
|---|
A verified clause-processor and customized rewriter for large terms that uses existing ACL2 rewrite rules to prove theorems.
RP-Rewriter (rp for 'retain property') is a verified clause processor that can be used to replace ACL2's rewriter for some theorems, and for some cases, can provide time efficiency and convenience when building lemmas. It uses a subset of the heuristics of the ACL2's rewriter but adds two distinctive features: 1. By introducing an invariant, it can retain properties about terms, which we call side-conditions. 2. In the case of alists in the theorems to be rewritten, it can create a corresponding fast-alist in the background. It also has some other improvements pertaining to meta-rules.
It supports a big set of rewrite rules existing in ACL2's world that may have syntaxp. For every other rule-classes, it treats them as rewrire-rules. It also provides a mechanism to run meta functions. The rest of the rule classes are not supported and are discarded by the rewriter. We also do not support rules with bind-free, ACL2::loop-stopper, ACL2::free-variables, force, case-split etc. Note that there is also no ACL2::type-alist or any form of type reasoning.
The rewriter enables users to attach certain properties (i.e., side-conditions) to terms as rewriting takes place. These properties can be used to relieve hypotheses efficiently without backchaining.
If a rewrite rule has hons-acons on its right hand side, rp-rewriter has a built-in mechanism that treats that as a trigger function to create a fast-alist in the background. When another term seems to be trying to read a value from that alist with a known instance of a function such as assoc-equal, the built in meta functions reads the value from the corresponding fast-alist instead of tracing it in the logical term. This may give great timing benefits when dealing with terms with large alists.