Discussion of the logical justification for the bind-var feature.

FGL's bind-var feature can be used to bind a free variable
in a rewrite rule to some arbitrary value. Here we discuss how the correctness
of that feature may be formalized. Note we discuss this with respect to

First we describe the requirements for using the

The justification for this is essentially that all free variables in a theorem are universally quantified. When we apply a rewrite rule, we start with the free variables of the LHS bound to the unifying substitution. We are free to bind any other variables that are mentioned in the theorem to whatever values we want, because the unifying substitution contains all variables of the LHS, so extending the unifying substitution to include additional variables won't change the value of the LHS under that substitution.

There is a technical problem with this when these free variables appear inside lambda bodies. ACL2 term translation ensures that all lambdas bind all the free variables of their bodies -- when it translates a lambda that has free variables in the body, it adds bindings for those variables to themselves. So if we have a rewrite rule like this:

(equal (foo x) (let* ((a (bar x)) (c (bind-var b (baz x a)))) ...))

then the outside of the RHS looks like this:

((lambda (a x b) ...) (bar x) x b)

We interpret the arguments of a lambda or function call before the body, and
normally if we encounter an unbound variable during symbolic execution we
produce an error. Therefore, we would run into an error when we process the
argument

A further complication is that when we bind a free variable due to
*major frame* produced by the current rewrite rule
application, which has a wholly new namespace for variables, and a *minor
frame*produced by each nesting of lambdas, which carries forward all
variable bindings from the previous minor frame and may shadow variable
bindings from the major frame. When we add a variable binding with

Finally we discuss how the

The correctness of a typical rewriter that takes an alist of variable bindings is along the lines of:

(equivalent-under-relation equiv-relation-context (eval-term input-term (eval-bindings bindings env)) (eval-term result-term env))

Here equiv-relation-context, input-term, and bindings are inputs to the rewriter, which produces result-term.

The exact such correctness statement for FGL involves various complications
that we won't discuss here, such as the distinction between input ACL2 terms
and output symbolic objects and various invariants of the interpreter state.
The main complication that we will discuss is that, rather than just an input
to the rewriter as would be the case in a typical rewriter, the relevant
bindings are changed (extended) by the rewriter as it (potentially) adds
variable bindings to the major frame due to

(equivalent-under-relation equiv-relation-context (eval-term input-term (append (eval-bindings output-minor-bindings env) (eval-bindings output-major-bindings env))) (eval-term result-term env))

(To simplify this slightly, we do show that the evaluation of the output and input minor bindings is equivalent.)

This is reasonable and true, but it isn't sufficiently strong to be inductively proved. The problem is that if we successively rewrite two terms, the output major bindings from the second term may be different from those from the first, so the inductive assumption from the first term doesn't help us anymore.

To fix this, we instead prove, approximately:

(forall ext (implies (eval-alist-extension-p ext (append (eval-bindings output-minor-bindings env) (eval-bindings output-major-bindings env))) (equivalent-under-relation equiv-relation-context (eval-term input-term ext) (eval-term result-term env))))

Where