Using `apply .. in` when conclusion contains forall

Using Coq
1

Hello,

I have just started using coq and couldn’t find a solution to this Problem.

Question

How can I use the apply .. in tactic, when the desired conclusion begins with ∀?

(Toy) Example:

I am trying to prove the following theorem:

Theorem noworks : forall (X : Type) (P : X -> Prop) (A : Prop) (x' : X),
  A -> (A -> (forall x, P x)) -> P x'.

This proof attempt where I try using the premises to arrive at ∀x P x fails.

Proof.
  intros X P A x HA Himp. apply Himp in HA.

 > Output: Unable to find an instance for the variable x.

If however I replace the ∀x P x in the theorem by a helper definition, the Proof works the intended way.

Definition helper (X : Type) (P : X -> Prop) : Prop :=
  forall x, P x.

Theorem works : forall (X : Type) (P : X -> Prop) (A : Prop) (x' : X),
  A -> (A -> helper X P) -> P x'.
(*           ^^^^^^^^^^        *)
Proof.
  intros X P A x HA Himp. apply Himp in HA. unfold helper in HA. apply HA.
Qed.

I’d also appreciate any tips on how to troubleshoot these kinds of issues (e.g. using the documentation).

Thanks for your help!

2

Hello,

It’s a bit of a quirky behavior of the apply tactic. When you apply Himp, it tries to give you a goal containing what is interpreted as the conclusion of the hypothesis. To do so, it considers that anything to the left of an arrow is an hypothesis that should be discharged, and anything quantified should be instantiated.
So as long as it’s “hypotheses”, it just gives you new goals. I.e. if you had instead:

Theorem noworks : forall (X : Type) (P : X → Prop) (A : Prop) (x’ : X),
A → (A → (A → P x’)) → P x’.

Then apply Himp in HA would work and generate a second goal, asking for a proof of A.
However when it comes to quantifiers, apply does not generate goals for them, hence the failure. You can instead use eapply (where the e stands for existential) to introduce evars when it finds quantifiers that it cannot instantiate. I.e. coming back to your initial example, eapply Himp in HA works and gives you an hypothesis of the form HA: P ?x that you can use to conclude your goal since Coq will then happily unify ?x with x.

Finally you sometimes want to keep the quantifier in your hypothesis, in particular because you might want to use it for two different values of X. One simple way to do so here is to use specialize instead of apply: specialize (Himp HA) will do what you want.

Hope it helps,
Yannick

1 Like