Search code examples
coq

apply tactic cannot find an instance for a variable

I have been trying out apply tactic in various scenarios and it seems to stuck in the following case when premises are like this:

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

When I try apply H2 in H1., it gives me the error:

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

Any way for me to bring forall e : nat, b -> g e as part of premises. This is the full working code with the above scenario:

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.
Solution

  • The Coq Reference manual, §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.

    Now, applying the above description to your case, we get the following, Coq tries to replace H1 : a with the conclusion of H2, i.e. g e. To do that it needs to instantiate the universally quantified variable e with some value, which Coq cannot obviously infer -- hence the error message you've seen.

    Another way to see that is to try a different variant of apply ... in ...:

    eapply H2 in H1.

    which will give you two subgoals:

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

    and

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

    The H1 hypothesis of the first subgoal shows what Coq was going for with the ordinary apply in tactic, but in the eapply in case the variable e got replaced with an existential variable (?e). If you are not familiar with existential variables yet, then they are sort of promise you make to Coq that you'll build terms for them later. You are supposed to build the terms implicitly, via unification.

    Anyways, specialize (H2 H1). might be what you want to do, or something like this

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