coq - 记住表达式时如何命名假设？

Question

Coq 的文档一般告诫不要依赖内置的命名机制，而是选择自己的名称，以免命名机制的更改导致过去的证明无效。

在考虑表单的表达式时remember Expr as v，我们将变量设置v为表达式Expr。但是假设的名称是自动选择的，类似于Heqv，所以我们有：

Heqv: v = Expr

我怎样才能选择我自己的名字而不是Heqv？我总是可以使用该rename命令将其重命名为我喜欢的任何名称，但这并不能让我的证明独立于 Coq 中内置命名机制的假设未来变化。

Answer 1

如果您可以摆脱单独的平等，请尝试set (name := val). 使用unfold而不是rewrite使值恢复原状。

如果您需要的相等性超过rewrite <-，我知道没有内置的策略可以做到这一点。不过，您可以手动完成，也可以构建策略/符号。我只是把这个放在一起。（注意：我不是专家，这可能更容易完成。）

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 *.

使用 asremember_as_eq (2+2) four Heqfour获得与使用 相同的结果remember (2+2) as four。

---

注意：更新以处理更多案例，旧版本在价值和目标类型的某些组合上失败。如果您发现另一种适用于rewrite但不适用于此的情况，请发表评论。