为何在Coq中无法对Prop类型的P使用exact P？

你在这里犯了一个关键混淆：上下文中的P : Prop表示P是一个命题，而非我们已经拥有了P的证明。exact P试图用命题本身作为它的证明，这在Coq里完全不成立——命题和命题的证明是完全不同的两类对象。

再看你的证明流程，执行destruct H0后已经丢掉了关键假设：H0是¬Q（也就是Q→False），destruct H0会直接要求你提供Q的证明来导出False，但你后续的步骤偏离了正确逻辑，导致上下文丢失了核心假设，才出现需要证明P却无证明可用的局面。

正确的证明步骤 #

Theorem contrapositive : forall (P Q : Prop),
  (P -> Q) -> (~Q -> ~P).
Proof.
  intros P Q H H0.  (* 引入所有假设：P、Q为命题，H是P→Q，H0是¬Q *)
  intro p.           (* 要证明¬P，需先假设P成立，再推导出False *)
  apply H0.          (* 要得到False，只需证明Q（因为H0是Q→False） *)
  apply H.           (* 要证明Q，用H: P→Q，传入我们假设的P的证明p *)
  exact p.           (* 这里的p是刚才引入的P的证明 *)
Qed.

更简洁的版本 #

Theorem contrapositive : forall (P Q : Prop),
  (P -> Q) -> (~Q -> ~P).
Proof.
  intros P Q H H0 p.
  apply H0, H.
  exact p.
Qed.

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