如何在证明过程中将单个统一变量转化为目标

Question

我想以交互方式构造一个存在变量。我不能使用Grab存在主义变量，因为我需要在完成目标之前填充存在主义变量。

Minimal exmaple这里有一个最小的例子(因为它很简单，它有其他解决方案，但它说明了我的问题(

Context (A:Type).
Parameter P Q: A -> Prop.
Definition filter: forall {a}, P a -> A:= fun a Pa=> a.
Lemma my_lemma:
forall a b, Q b -> (Q b -> P a) ->
exists a (H: P a), P (filter H).
Proof.
intros ?? H H0.
do 2 eexists.

在这一点上，有两个解决方案不能回答我的问题：(1(我可以运行(eauto(，然后执行Grab Existential Variables，但假设eauto在实例化统一变量之前不会成功；(2( 我可以用instantiate(1:= H0 H)(甚至instantiate(1:= ltac:(eauto))(明确地传递证明项，但假设存在性的证明是乏味的，我们希望交互式地进行。

我们还能做什么？我们可以尝试使用cut或assert，就像这样：

match goal with
|[|- P (filter ?x)] =>
match type of x with
| ?T => assert (HH:T) by eauto
end
end.

但是HH不在统一变量的上下文中，所以它不能被实例化。

instantiate(1:=HH). (* Instance is not well-typed in the environment of ?H. *)

据我所知，解决这个问题的唯一方法是使用Show Existentials，手动复制变量的类型，将证明回滚到引入统一之前，并在那里构造变量。在这个例子中，它看起来像这样：

Lemma my_lemma:
forall a b, Q b -> (Q b -> P a) ->
exists a (H: P a), P (filter H).
Proof.
intros ?? H H0.
do 2 eexists.
Show Existentials.  
Restart. (* This command restores the proof editing process to the original goal. *)
intros ?? H H0.
assert (HH:P a) by eauto.
eexists; exists HH.
auto.
Qed.

显然，我希望避免这种工作流程。那么，无论如何，把存在变量变成子目标？

Answer 1

您的最佳选择可能是首先避免将存在变量创建为evar。您不必手动构造变量即可完成此操作；如果你能确定它是在哪里创建的，你就可以用unshelve t来包装进攻战术，这会把t创建的所有疏散都变成目标。如果相关策略深入某些自动化内部，并且难以识别或更改，那么这可能会很困难。