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

Question

Coq 的文档中普遍告诫不要依赖内置的命名机制，而是选择自己的名字，以免命名机制的变化使过去的证明无效。

考虑形式 remember Expr as v 的表达式时，我们设置变量 v到表达式 Expr .但是假设的名称是自动选择的，类似于 Heqv ，所以我们有:
Heqv: v = Expr
如何选择我自己的名字而不是 Heqv ?我可以随时使用 rename 将其重命名为我喜欢的任何名称。命令，但这并不能使我的证明独立于 Coq 中内置命名机制的假设 future 变化。

Answer 1

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

如果您需要的相等性超过 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 *.

用作 remember_as_eq (2+2) four Heqfour获得与 remember (2+2) as four 相同的结果.

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