RENAME_TAC
Q.RENAME_TAC : term quotation list -> tactic
Renames free variables or subterms within a goal.
A call to RENAME_TAC qs searches the current goal for matches to the
patterns in the list qs, and then substitutes out the matches (in the
"reverse direction") so that the goal becomes one that uses the names
from qs. This can cause subterms within the goal to turn into simple
variables, but the usual intention is to rename free variables into the
variables that appear in the patterns.
The matching is done without reference to the goal's existing free
variables. If a variable in qs clashes with an existing variable in
the goal, then the goal's variable will be renamed away. It is
sufficient for variables to have the same name to "clash"; they need not
also have the same type. The search for matches begins by attempting to
find matches against the whole of the goal, against whole assumptions,
for sub-terms within the goal, and then sub-terms of assumptions.
These four different flavours of searching can additionally be
controlled by adding comments (* ... *) to the end of the relevant
quotation. The string in the comment has its whitespace stripped, and is
then split into fields using the pipe character | as a separator. If
the string consisting of the single character g is present, the
pattern is checked against the entirety of the goal's conclusion; the
string of character a causes a check against each individual
assumption; the strings sg and sa cause checks against sub-terms
present in the conclusion, or in any assumption respectively.
If multiple matches are possible, a variant tactic, Q.kRENAME_TAC, can
be used: this tactic takes an additional "continuation" tactic argument
that can be used to discriminate between these matches.
Patterns can use underscores to match anything without any change in the goal's naming being introduced. Underscores can match against sub-terms that include bound variables. Matching is first-order.
Failure
Fails if it is impossible to consistently match the combination of
patterns in the provided list of quotations (qs).
Example
If the goal is of the form
x < y, y < z ?- x < f a
then invoking Q.RENAME_TAC [`b < c`, `a < b`] will produce the
sub-goal:
a < b, b < c ?- a < f a'
where the goal's original a variable (which is not even of type
num), has been renamed away from a because that variable occurs in
the patterns. (If the right hand side of the inequality was simply a
and was thus of type num, it would also be renamed to a'.)
If Q.RENAME_TAC [`b < c`] is invoked on the same initial goal, the
result is:
b < y, y < z ?- b < c
illustrating the way in which variables can eliminate more complicated sub-terms.
The useful way in which underscores in patterns can be used to "dodge" terms including bound variables is illustrated in the next example, where the initial goal is:
(!a. f a < z), z < c ?- z < d
After applying Q.RENAME_TAC [`_ < x`, `x < c`], the goal becomes
(!a. f a < x), x < c' ?- x < c
The goal was chosen for the match to the second pattern because the goal is considered first. If the initial goal had been
(!a. f a < z), z < c ?- z < d /\ P z
then the result of the same application would be
(!a. f a < z), z < c ?- x < d /\ P x
because whole assumptions are considered before sub-terms of the goal.
The pattern-specification comments can be important when selecting for
certain assumptions. Here, Q.RENAME_TAC [‘x < _ (* a *)’] will fail
because there is no assumption of the required shape, even though the
shape appears as a subterm in the assumptions, and is the shape of the
goal's conclusion:
~(a < b) ?- c < d
Similarly, using the comment (* a|sg *) would also fail because the
pattern is not present as a sub-term of the goal's conclusion.
Comments
This function is also available under the name bossLib.rename.
Note that Q.RENAME_TAC [q] is not the same as Q.RENAME1_TAC q. The
latter pays attention to the goal's free variables, using these to
constrain the match to the pattern. In contrast, Q.RENAME_TAC
completely ignores all of the goal's free variables, such that using an
existing name in a pattern doesn't make any difference to the matching
behaviour.