how to name the assumption when remembering an expression?

Question

The documentation for Coq carries the general admonition not to rely on the builtin naming mechanism, but select one's own names, lest the changes in the naming mechanism render past proofs invalid.

When considering expressions of the form remember Expr as v, we set the variable v to the expression Expr. But the name of the assumption is selected automatically, and is something like Heqv, so we have:

Heqv: v = Expr

How can I select my own name instead of Heqv? I can always rename it to whatever I like using the rename command, but that doesn't keep my proofs independent of the hypothetical future changes in the builtin naming mechanism in Coq.

Answer 1

If you may get rid of the separate equality, try set (name := val). Use unfold instead of rewrite to get the value back in place.

If you need the equality for more than the rewrite <-, I know of no built in tactic that does this. You can do it manually, though, or build a tactic / notation. I just threw this together. (Note: I'm not an expert, this might be done more easily.)

Tactic Notation "remember_as_eq" constr(expr) ident(vname) ident(eqname) :=
  let v     := fresh in
  let HHelp := fresh in
    set (v := expr);
    (assert (HHelp : sigT (fun x => x = v)) by ( apply (existT _ v); reflexivity));
    inversion HHelp as [vname eqname];
    unfold v in *; clear v HHelp;
    rewrite <- eqname in *.

Use as remember_as_eq (2+2) four Heqfour to get the same result as with remember (2+2) as four.

---

Note: Updated to handle more cases, the old version failed on some combinations of value and goal type. Leave a comment if you find another case that works with rewrite but not this one.