coq - 应用策略找不到变量的实例

Question

我一直在尝试apply战术在各种场景中，当前提是这样时，它似乎陷入了以下情况:

  H1 : a
  H2 : a -> forall e : nat, b -> g e
  ============================
   ...

当我尝试时 apply H2 in H1. ，它给了我错误:

Error: Unable to find an instance for the variable e.

有什么办法可以带 forall e : nat, b -> g e作为处所的一部分。这是上述场景的完整工作代码:

Lemma test : forall {a b c : Prop} {g : nat} (f : nat -> Prop),
    a /\ (a -> forall {e : nat}, b -> f e) -> c.
Proof.
  intros a b c f g.
  intros [H1 H2].
  (* apply H2 in H1. *)
Abort.

Answer 1

Coq 引用手册，§8.2.5 :

The tactic apply term in ident tries to match the conclusion of the type of ident against a non-dependent premise of the type of term, trying them from right to left. If it succeeds, the statement of hypothesis ident is replaced by the conclusion of the type of term.

现在，将上述描述应用于您的案例，我们得到以下结果，Coq 尝试替换 H1 : a与 H2 的结论，即 g e .为此，它需要实例化通用量化变量 e带有一些 Coq 无法明显推断出的值——因此是您看到的错误消息。

另一种查看方式是尝试 apply ... in ... 的不同变体。 :

eapply H2 in H1.

这将为您提供两个子目标:

  ...
  H2 : a -> forall e : nat, b -> g e
  H1 : g ?e
  ============================
  c

和

  ...
  H1 : a
  H2 : a -> forall e : nat, b -> g e
  ============================
  b

H1第一个子目标的假设显示了 Coq 对普通 apply in 的意图战术，但在 eapply in案例变量 e被存在变量( ?e )替换。如果您还不熟悉存在变量，那么它们是您向 Coq 做出的 promise ，您将在以后为它们构建术语。您应该通过统一隐式构建这些术语。

无论如何， specialize (H2 H1).可能是你想要做的，或者像这样的

pose proof (H2 H1) as H; clear H1; rename H into H1.