Search code examples
logiccoqcoq-tactic

How to prove (~Q -> ~P) - > (P -> Q) in Coq

I am trying to prove (~Q -> ~P) - > (P -> Q) in coq, which is the reverse of the contrapositive theorem (P-> Q) (~Q -> ~P). Currently I was thinking about using the same logic of proving the contrapositive theorem like this:

unfold not. intros P Q. intros A B C. apply B. apply A. apply C.

However I am stuck at the beginning. Maybe I need additional axioms to prove the reverse of the contrapositive theorem. Can anyone help me?

Solution 
  • Require Import Classical.

Lemma myproof :  forall (P Q : Prop), (~Q -> ~P) -> (P -> Q) . 
unfold not. intros P Q. intros A B.
destruct (classic Q) as [Q_holds|NQ_holds].
apply Q_holds.
apply False_ind.
apply A.
apply NQ_holds.
apply B.
Qed.