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. Such (classic) 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 automatically to be sufficient at that subterm occurrence. We extend that capability by introducing 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.