Contextual-rewriting
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.
