A meta-rule system that lets the ACL2 rewriter pass around contextual information. Similar to Dave Greve's NARY. This extends ACL2's notion of congruence-based rewriting.

The motivating example: We have the following two theorems:(defthm mod-n-first-arg-of-plus-context (implies (and (rationalp x) (rationalp y) (rationalp n) (not (equal n 0))) (equal (mod (+ (mod x n) y) n) (mod (+ x y) n)))) (defthm mod-n-second-arg-of-plus-context (implies (and (rationalp x) (rationalp y) (rationalp n) (not (equal n 0))) (equal (mod (+ x (mod y n)) n) (mod (+ x y) n))))Basically, if we have addition in a mod N context, then each of the terms of the sum is also in a mod N context. Now suppose we have:

(defthm foo-bar-under-mod (equal (mod (foo m n) n) (mod (bar m n) n)))This allows us to rewrite (foo m n) to (bar m n) under a mod N context. But perhaps we want to prove:

(implies (and (rationalp a) ... (rationalp n) (not (equal n 0))) (equal (mod (+ a b c d (foo m n) e) n) (mod (+ a b c d (bar m n) e) n)))Logically, the three theorems we have are sufficent to prove this last one. But it's painful because the rewrite rules don't really help us. What we really want is to be able to say: When rewriting a sum under mod N context, we may rewrite all its terms under a mod N context. So here's how our meta rule accomplishes that. We take our two context theorems and tell our meta rule to use them:

(add-context-rule mod (:rewrite mod-n-first-arg-of-plus-context)) (add-context-rule mod (:rewrite mod-n-second-arg-of-plus-context))A special thing about each of these rules is that the LHS unifies with the RHS, and there is only one variable in the substitution that isn't bound to itself after this unification. Namely, in the first rule,