Search code examples
coq

Why I can't use exact P if P is a Prop?

I am trying to prove contraposition. And my proof is like the following. It doesn't work.

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

My question is, after apply H, I get the following goal

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

So, IMO, we have to prove P, and we have a P in our hypothesis. So why can't we just use exact P?

Solution

  • To have P : Prop in your assumptions is not the same as having a p : P in your assumptions.

    If the goal is to prove P, exact x must be used with x as a term of type P, i.e, a proof of P. P is not a proof of P.

    • P : Prop means "let P be an arbitrary proposition". It could be true, it could be false.
    • p : P means "let p be a proof of P". That's what means that P is true.