# Policies on introducing free variables when rewriting?

When using a fact like x = y <=> x + z = y + z as a rewrite rule, it can be desirable to introduce an unused free variable into the result of the rewrite rather than z, because that keeps open the most options for subsequent substitutions.

Do any proof assistants treat this situation by any means other than automatic renaming or something equivalent? For example, one might require a fresh variable name as an input to the rewriting tactic, or simply leave free variable names as-is? If so, do they have a rationale?

Or is this issue perhaps obviated by the framework or context in which rewriting is done in proof assistants, e.g. working backward from the desired result?

If I understand correctly, what you are talking about is treated using existential variables in Coq. These are variables but on the "meta" level, meaning that they stand for a term yet-to-be-defined. They are used all over the place to handle implicit arguments, unification, and so on. But you can also introduce and use them by means of dedicated tactics (those are usually called etac where tac is another tactic), typically in cases such as yours.

As an example, see the following proof script:

Require Import Nat Arith.

Lemma foo (x y z : nat) : x + z = y + z -> x = y.
Proof.
intros H.
exact H.
Qed.


Here the eapply tactic applies the lemma Nat.add_cancel_r (exactly the equivalence you talk about), but since it is not able to find a value for z, it simply introduces an existential variable ?p, and the goal becomes x + ?p = y + ?p. Next, the exact tactic says that this is exactly the hypothesis H, which triggers unification, and solves ?p to be z.

• Yes, I believe you are indeed understanding my question, thanks. Apr 23, 2022 at 16:42
• Are you aware of a good introduction to existential variables in Coq, with rationale? A reference to it would be most welcome. Apr 23, 2022 at 16:50

In Metamath, the MMJ2 proof assistant introduces work variables, which names are constructed with a & prefix, a letter giving the type code of the variable, like C for a "class" variable, and a kind of De Bruijn index for identifying the variable.

In the example below which corresponds to your formula, I typed in the last line as qed::addcan2ad |- ( ph -> A = B ), and the proof assistant has filled in the required essential hypotheses d1 to d4, naming the newly introduced variable &C1 on the way.

$( <MM> <PROOF_ASST> THEOREM=meta_var LOC_AFTER=? !d1:: |- ( ph -> A e. CC ) !d2:: |- ( ph -> B e. CC ) !d3:: |- ( ph -> &C1 e. CC ) !d4:: |- ( ph -> ( A + &C1 ) = ( B + &C1 ) ) qed:d1,d2,d3,d4:addcan2ad |- ( ph -> A = B )$)


For my point of view, the main rationale for using names with a & prefix for work variables is that it is guaranteed that those names will not collide with the names any other regular variables.

Also, one can immediately tell a work variable from a regular variable, just from the naming, so it is obvious that these will eventually need to be substituted for some actual terms.

This copy of the MMJ2 documentation page about work variables has more details and goes more in-depth on the differences between a regular variable and a work variable.

• PS. In MMJ2 those are named "Work Variables" and documented here: github.com/digama0/mmj2/blob/master/doc/WorkVariables.html (does anyone know a place where this page is served, and not just in HTML format?) Apr 24, 2022 at 4:50
• Thanks much. Can you summarize your understanding of the rationale for this behavior in your answer? Apr 25, 2022 at 6:38
• I added it @CrisP, I ended up copying the documentation page in question, it's much easier to browse like that, even though it's obvious it is ancient! Apr 25, 2022 at 15:26