Coq的文档带有一般警告,不依赖于内置命名机制,而是选择自己的名称,以免命名机制中的更改过去证明无效.
在考虑表单的表达式时remember Expr as v
,我们将变量v
设置为表达式Expr
.但是假设的名称是自动选择的,就像这样Heqv
,我们有:
Heqv: v = Expr
我怎样才能选择自己的名字而不是Heqv
?我总是可以使用rename
命令将它重命名为我喜欢的任何内容,但这并不能保证我的证明不依赖于Coq中内置命名机制的假设未来变化.
如果你可以摆脱单独的平等,试试吧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 *.
Run Code Online (Sandbox Code Playgroud)
使用尽可能remember_as_eq (2+2) four Heqfour
得到相同的结果与remember (2+2) as four
.
注意:更新以处理更多情况,旧版本在某些值和目标类型组合上失败.如果您发现另一个适用rewrite
但不适用此案例的案例,请发表评论.