如何在Coq中解构evar？实现保留evar变量对的目标形式

问题背景 #

原证明脚本：

Theorem foo : exists p, p = (1, 1).
Proof. eexists ?[p]. destruct ?p.

执行上述脚本后，得到的目标为：

n, n0 : nat
  ============================
  (n, n0) = (1, 1)

希望找到一种解构?p的方式，让最终目标与执行eexists (?[p1], ?[p2]).后的目标一致，即：

(?p1, ?p2) = (1, 1)

解决方法 #

方法一：直接用refine构造带配对占位符的存在实例 #

跳过eexists加destruct的步骤，直接用refine策略生成带配对占位符的目标：

Theorem foo : exists p, p = (1, 1).
Proof. refine (exist _ (?[p1], ?[p2]) _).

执行后直接得到目标(?p1, ?p2) = (1, 1)，无需额外解构操作。

方法二：在eexists ?[p]后用change替换占位符形式 #

如果已经执行了eexists ?[p]，可以通过change策略将占位符?p替换为配对形式并保留占位符：

Theorem foo : exists p, p = (1, 1).
Proof.
  eexists ?[p].
  change ?p with (?[p1], ?[p2]).

此时目标会变为(?p1, ?p2) = (1, 1)，且上下文不会引入额外的nat变量。

内容的提问来源于stack exchange，提问作者andreas