Hi, 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?
As often in Rocq “forward” reasoning (you produce new knowledge from hypothesis, instead of refining the current goal) is handled by another tactic. Here specialize can do the trick:
Theorem post_forall: forall (X: Type) (P: Prop) (Q: X -> Prop),
(P -> forall x, Q x) -> forall x, P -> Q x.
Proof.
intros X P Q.
intros H.
intros y.
intros H1.
specialize (H H1) as hyp.
Actually you can also do it by pose proof (H H1) as hyp.
Indeed, it is unnecessary (and even counterproductive) in your case, but the system has no way to know it. It just tries to instantiate all the quantifiers and fails to do so. That is why you should use a less fancy tactic than apply here. In addition to specialize and pose proof which were already mentioned, there are also assert (hyp := H H1) and refine (_ (H H1)).
Is there any reason why Coq is designed to prove in this way? If the tactic “apply” behaved like “specialize” in my case, would Coq’s soundness be harmed?
I guess that Coq tends to prevent any universally quantified statements from being conclusions. In logic, it can be tough to prove a universal conclusion from non-universal premises.
It does not have anything to do with soundness. (Tactics are only meant to produce tentative proof terms, be they correct or not. It is only at the point of Qed where they will be checked for correctness, independent of which tactics produced them. Obviously, a tactic that would always produce an incorrect proof term would be completely useless, so tactics have to produce sound proofs as often as possible, but that is no strong requirement.)
The behavior of apply in is just a matter of specification. It is designed to replace a hypothesis by the consequent of a lemma, using the original hypothesis as one of the antecedents, and making all the other antecedents into subgoals. For example, if you have a goal Γ; H: P |- G and a lemma L: P -> Q -> R, you will obtain two goals after doing apply L in H, which are Γ; H: R |- G and Γ |- Q.
An issue appears when Q happens to depend on a universally quantified variable (e.g., L: P -> forall x, Q x -> R). The second goal is now Γ |- Q x, but what is x here? That is why apply L in H complains. But if you use eapply L in H instead, then the prover leaves an existential variable there: Γ |- Q ?x. (That is the main difference between tactics foo and efoo, that is, the ability to leave existential variables around when something has no obvious instance yet.)
If apply in was always behaving like specialize, there would be no point in having two different tactics. If the behavior of apply in does not suit your proof style, just use a different tactic.
I think I have understood your answer, and I wrote an analogous example. Of course, it met the same problem:
Theorem simu_forall: forall (P R Q: Prop),
(P -> (R -> Q)) -> (R -> (P -> Q)).
Proof.
intros P R Q.
intros H.
intros Y.
intros H1.
generalize dependent Y. (*goal : R -> Q*)
apply H in H1. (*two goals: R -> Q
and R*)
(** STUCK HERE, *)
Admitted.
It is weird for me that
“apply H in H1”
will take Q as the final postcondition of H.
However, typically in mathematical logic, we take the first “->” as the main connective and “(R->Q)” as the postcondition of H.