如何在Coq中证明指定引理？证明出现统一错误求助

待证明的引理 #

Lemma x: forall P Q: Set -> Prop,
              forall f: Set -> Set, 
            forall x, (P x -> Q (f x)) -> 
               (exists x, P x) -> (exists x, Q x).

错误的证明尝试 #

Lemma x: forall P Q: Set -> Prop,
              forall f: Set -> Set, 
            forall x, (P x -> Q (f x)) -> 
               (exists x, P x) -> (exists x, Q x).
Proof.
  intros P Q f x H1 [x0 H2].
  exists (f x0).
  apply H1.
  assumption.
Qed.

触发的错误信息 #

在环境
P, Q : Set -> Prop
f : Set -> Set
x : Set
H1 : P x -> Q (f x)
x0 : Set
H2 : P x0
中，无法将"Q (f x)"与"Q (f x0)"统一。

问题原因 #

错误出在intros步骤：你把全称量词forall x, (P x -> Q (f x))拆成了变量x和假设H1，导致H1仅对这个特定的x成立，而非对任意x都成立。但我们需要的是能作用于存在量词给出的x0的通用蕴含关系。

正确的证明 #

调整intros步骤，让H1直接捕获全称量词的约束：

Lemma x: forall P Q: Set -> Prop,
              forall f: Set -> Set, 
            (forall x, P x -> Q (f x)) -> 
               (exists x, P x) -> (exists x, Q x).
Proof.
  intros P Q f H1 [x0 H2].
  exists (f x0).
  apply H1.
  assumption.
Qed.

或者保持原引理的写法（不修改引理结构），只需在intros时不要单独绑定x：

Lemma x: forall P Q: Set -> Prop,
              forall f: Set -> Set, 
            forall x, (P x -> Q (f x)) -> 
               (exists x, P x) -> (exists x, Q x).
Proof.
  intros P Q f H1 [x0 H2].
  exists (f x0).
  apply H1.
  assumption.
Qed.

这里Coq会自动将H1解析为forall x, P x -> Q (f x)，后续apply H1就能作用于x0，顺利完成证明。

内容的提问来源于stack exchange，提问作者lukmik