coq - 如何在证明过程中将单个统一变量变成目标

Question

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

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

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 创建的所有 evar 转换为目标。如果相关策略深入到某些自动化中并且难以识别或更改，这可能会很困难。