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.
The behaviour you're looking for is available, but you need to use the specialize tactic, and it'll replace your implication rather than your consequent [reference].
Example with some proof context omitted:
H : P -> (forall x : X, Q x)
H1 : P
______________________________________(1/1)
False
specialize (H H1)
H : forall x : X, Q x
H1 : P
______________________________________(1/1)
False
I'm confused too, I think you found a quirk in "apply." I've seen similar restrictions on reasoning over innter quantifications documented in other features of older versions. (Specifically in CPDT if anyone can recall it...)