如果 P 是 Prop，为什么我不能使用精确的 P？

Question

我正在尝试证明对立性。我的证明如下。没用。

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

我的问题是，当完成

apply H

时，我得到以下目标

1 goal
P, Q : Prop
H : P -> Q
______________________________________(1/1)
P

所以，在我看来，我们必须证明

P

，并且我们的假设中有一个

P

。那么为什么我们不能只使用

exact P

呢？

Answer 1

您的假设中包含

P : Prop

与您的假设中包含

p : P

不同。

如果目标是证明

P

，则

exact x

必须与

x

一起使用，作为

P

类型的术语，即

P

的证明。

P

不是

P

的证明。

• P : Prop

  的意思是“让

  P

  是一个任意命题”。可能是真的，也可能是假的。

• p : P

  的意思是“让

  p

  成为

  P

  的证明”。这就是说

  P

  是真的。