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, x is bound to (mod x n), but y and n are bound to themselves. This is the requirement for a context rule. It is used as follows. Suppose we've come to the MOD term on the LHS of the theorem above. Our meta rule operates by trying to apply rewrite rules backwards! So first, we unify our term, (mod (+ a b c d (foo m n) e) n), with the RHS of the first rule, (mod (+ x y) n). This works and we have x bound to a, y bound to (+ b c d (foo m n) e), and n bound to n. We then simplify the term corresponding to x in the LHS under this substitution. This is just (mod a n), which probably doesn't simplify to anything. So this application fails. We then try the second rule. This causes y, which is bound to (+ b c d (foo m n) e), to be rewritten under mod N. Now, our meta rule fires recursively on this sum, so each element is rewritten under a mod N context. Specifically, when we get to (foo m n), we can apply foo-bar-under-mod. To do: performance tuning; get it working under equivalences other than equal; add mechanism for disabling certain context-propagation rules; add ttree stuff when it becomes available.