在以下证明脚本中:
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)
destruct <term>
<term>
用应用于其参数(在上下文中生成为变量)的构造函数替换所有出现的,每个构造函数都有一个目标。使用 evar,您可以通过自己进行实例化来选择应应用哪个构造函数,例如使用instantiate (p := (?[p1], ?[p2])).