如何在 Coq 中销毁 evars？

Question

在以下证明脚本中：

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

我们最终达到了目标：

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

有没有一种方法可以破坏

?p

，这样我们最终会得到与使用

eexists (?[p1], ?[p2]).

而不是

eexists ?[p].

时相同的目标？即：

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

Answer 1

destruct <term>

将所有出现的

<term>

替换为应用于其参数（在上下文中作为变量生成）的构造函数，每个构造函数有一个目标。使用 evar，您可以通过自己实例化来选择应应用哪个构造函数，例如与

instantiate (p := (?[p1], ?[p2])).