I am learning Coq and I just discovered that it is constructive.
That's one way I can prove that "contradiction implies everything" and it works:
Theorem contradiction_implies_anything: forall P Q : Prop, P -> ~P -> Q.
Proof.
intros P Q p not_p.
contradiction.
Qed.
Note that no Q was constructed, so I assume contradiction is built-in into the Coq proof engine. It seems to me that otherwise one has to show how Q is consructed, and it isn't possible for any Q, thus the theorem above can not be proved then. In particular I can not prove the theorem above in the following (pseudo) code:
intros P Q p not_p.
introduce P \/ Q. # here I have to construct Q, right?.. that's the point where Coq's "constructivity" becomes an obstruction
introduce ~P \/ Q. # same here
run case analysis on both and figure out that Q must be true.
Qed.
Am I right?
contradiction isn't actually necessary here, and there are two main reasons why:
~ P is a standard library notation for P -> False, which means that if you have hypotheses P and ~ P, you can apply ~ P to P to get False.
The standard library defines False like so: Inductive False : Prop :=. That means that if you destruct a hypothesis of type False, the resulting case analysis will have zero cases. That is to say, your proof will be done!
So, to summarize, you can prove your theorem like so:
Theorem contradiction_implies_anything: forall P Q : Prop, P -> ~P -> Q.
Proof.
intros P Q p not_p.
apply not_p in p.
destruct p.
Qed.