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

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

使用尽可能remember_as_eq (2+2) four Heqfour得到相同的结果与remember (2+2) as four.

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