In Coq (or Rocq), can't a lemma with a universal conclusion be applied to other premises?
When I prove with Coq (or Rocq), I find that sometimes if a hypothesis is "P" and another is "P -> forall x, Q x", I cannot make "forall x, Q x" a new premise by modus ponens.
Here is an example:
Theorem post_forall: forall (X: Type) (P: Prop) (Q: X -> Prop),
(P -> forall x, Q x) -> forall x, P -> Q x.
Proof.
(*
Here is a correct proof:
intros X P Q.
intros H.
intros y.
intros H1.
generalize dependent y.
apply H.
apply H1.
Qed.
*)
intros X P Q.
intros H.
intros y.
intros H1.
generalize dependent y.
apply H in H1.
(** STUCK HERE,
But Why cannot we do this???
They look the same.
*)
Admitted.
The proof will be stuck in the line "apply H in H1" and Coq returns that "Unable to find an instance for the variable x."
But must "x" be instantiated? It looks unnecessary. What is the difference between the two proofs?
I asked both DeepSeek and ChatGPT. Neither of them could provide a satisfiable answer.
I also guessed that it could be the variable occurrence problem in the antecedent. But if it were, the tactic "generalize dependent" should have failed.
Answer
See the documentation: a simple fix is to use eapply H in H1, or just conclude the proof with exact (H H1).
Alternatively, note that you don't really need tactics here: the whole proof is just fun X P Q H x p => H p x.
![Next-js App-Router dynamic route: ‘params should be awaited’ warning in /api/…/[id]/… handler — why and how to fix?](/_next/image?url=https%3A%2F%2Fcdn.sanity.io%2Fimages%2F80wy3gkl%2Fproduction%2F3a6e81eb886bdc1ee75a15416d662d0f5bc7ea85-1280x720.png&w=3840&q=75)