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

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 尝试用 H2 的结论替换 H1 : a，即 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 做出的承诺，您稍后会为它们建立术语。您应该通过统一隐式构建术语。

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

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

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

apply tactic cannot find an instance for a variable

coq