Apply tactic cannot find an instance of a variable
I have tested the tactics apply
in various scenarios and seem to be stuck in the following case where the premise looks like this:
H1 : a
H2 : a -> forall e : nat, b -> g e
============================
...
When I try apply H2 in H1.
it gives me an error:
Error: Unable to find an instance for the variable e.
In any case, I quote forall e : nat, b -> g e
as part of the premises. This is the complete working code with the above script:
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.
source to share
Coq Reference Manual, §8.2.5 :
The
apply
term tactic identifierin
tries to match the output of the identifier type with the independent clause of the term type by trying it from right to left. If successful, the hypothesis identifier statement is replaced by type of term.
Now, applying the above description to your case, we get the following: Coq is trying to replace H1 : a
with output H2
, i.e. g e
... To do this, you need to instantiate a generic quantized variable e
with some value that Coq cannot explicitly output - hence the error message you saw.
Another way to see that this is to try another option 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 hypothesis of the H1
first subgoal shows that Coq was going with the usual tactics apply in
, but in the case the eapply in
variable e
was replaced by an existential variable ( ?e
). If you are not already familiar with existential variables, then this is a kind of promise that you put into Coq that you will build them later. You have to construct terms implicitly through concatenation.
Anyway specialize (H2 H1).
could be what you want to do or something like this
pose proof (H2 H1) as H; clear H1; rename H into H1.
source to share