时间戳

首页 > 解决方案 > 如何重命名假设中的存在量化变量？

coq - 如何重命名假设中的存在量化变量？

问题描述

有没有一种简单的方法可以重命名假设中的存在变量？有时变量名称会令人困惑，因为在不相关的假设中会重复使用相同的名称。

例如，我想更改H1 : exists p : nat, n0 = p * 2为H1 : exists pminus1 : nat, n0 = pminus1 * 2.

标签： coqcoq-tactic

解决方案

这是一段代码：

match goal with
  an_h : @ex _ (?f) |- _ =>
  let new_f := eval lazy beta in (fun pminus_one => f pminus_one) in
  assert (my_h : @ex _ new_f) by exact an_h; clear an_h
end.

推荐阅读