How to name an assumption when memorizing an expression?

Question

The documentation for Coq carries a general warning not to rely on the built-in naming mechanism, but choose one proper name so that changes to the naming mechanism do not reflect past evidence.

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

Heqv: v = Expr

How can I choose my own name instead of Heqv ? I can always rename it to whatever I like using the rename command, but that does not make my evidence independent of the hypothetical future changes to the built-in naming mechanism in Coq.

Answer 1

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

If you need equality more than rewrite <- , I don't know any built-in tactics that do this. You can do it manually, or build tactics / naming. I just threw it together. (Note: I am not an expert, this can 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 for some combinations of values ​​and target type. Leave a comment if you find another case that works with rewrite , but not this one.