Rough Diamond: An Extension of Equivalence-based Rewriting

ABSTRACT. Previous work by the authors generalized conditional rewriting from the use of equalities to the use of arbitrary equivalence relations. This (classic) {\em equivalence-based rewriting} automates the replacement of one subterm by another that may not be strictly equal to it, but is equivalent to it, where this equivalence is determined {\em automatically} to be sufficient at that subterm occurrence. We extend that capability by introducing {\em patterned} congruence rules in the ACL2 theorem prover, to provide more control over the occurrences where such a replacement may be made. This extension enables additional automation of the rewriting process, which is important in industrial-scale applications. However, because this feature is so new (introduced January, 2014), we do not yet have industrial applications to verify its utility, so we present a small example that illustrates how it supports scaling to large proof efforts.