When to use the contrapositive to prove a statment My question tries to address the intuition or situations when using the contrapositive to prove a mathematical statement is an adequate attempt.
Whenever we have a mathematical statement of the form $A \implies B$, we can always try to prove the contrapositive instead i.e. $\neg B \implies \neg A$. However, what I find interesting to think about is, when should this approach look promising? When is it a good idea when trying to prove something to use the contrapositive? What is the intuition that $A \implies B$ might be harder to do directly than if one tried to do the contrapositive?
I am looking more for a set of guidelines or intuitions or heuristics that might suggest that trying to use the contrapositive to prove the mathematical statement might be a good idea.
Some problems have structures that make it more "obvious" to try induction or contradiction. For example, in cases where a recursion is involved or something is iterating, sometimes induction is natural way of trying the problem. Or when some mathematical object has property X, then assuming it doesn't have property X can seem promising because assuming the opposite might lead to a contradiction. So I was wondering if there was something analogous to proving stuff using the contrapositive.
I was wondering if the community had a good set of heuristics for when they taught it could be a good idea to use the contrapositive in a proof.
Also, this question might benefit from some simple, but very insightful examples that show why the negation might be easier to prove. Also, I know that this intuition can be gained from experience, so providing good or solid examples could be a great way to contribute. Just don't forget to say what type of intuition you are trying to teach with your examples!
Note that I am probably not expecting an actual full proof super general magical algorithm because an algorithm like that could probably be used for automating prooving, which might imply something big like $P=NP$. (Obviously a proof of P vs NP is always interesting, but I think that asking the community to prove the P vs NP is not a realistic thing to ask...)
 A: Here are some examples, hope they help.  First an easy one.
Theorem.  Let $n$ be an integer.  If $n$ is even then $n^2$ is even.
Proof (outline).  Let $n$ be even.  Then $n=2k$ for some integer $k$, so $n^2=4k^2=2(2k^2)$, which is even.
Now try the converse by the same method.
Theorem.  Let $n$ be an integer.  If $n^2$ is even then $n$ is even.
Proof (attempted).  Suppose that $n^2$ is even, say $n^2=2k$.  Then $n=\sqrt{2k}$ and so...????  This seems hopeless, $\sqrt{2k}$ does not look like an integer at all, never mind proving that it's even!
Now try proving the converse by using its contrapositive.
Theorem.  Let $n$ be an integer.  If $n^2$ is even then $n$ is even.
Proof.  We have to prove that if $n$ is odd, then $n^2$ is odd.  So, let $n=2k+1$; then $n^2=4k^2+4k+1=2(2k^2+2k)+1$ which is odd.  Done!
I think the point here is that for the attempt at a direct proof we start with $n^2=2k$.  This implicitly gives us some information about $n$, but it's rather indirect and hard to get hold of.  Using the contrapositive begins with $n=2k+1$, which gives us very clear and usable information about $n$.
Perhaps you could put a heuristic in the following form: "try both ways, just for a couple of steps, and see if either looks notably easier than the other".
A: Contraposition is often helpful when an implication has multiple hypotheses, or when the hypothesis specifies multiple objects (perhaps infinitely many).
As a simple (and arguably artificial) example, compare, for $x$ a real number:
1(a). If $x^4 - x^3 + x^2 \neq 1$, then $x \neq 1$. (Not easy to see without implicit contraposition?)
1(b). If $x = 1$, then $x^4 - x^3 + x^2 = 1$. (Immediately obvious.)
Here's a classic from elementary real analysis, with $x$ again standing for a real number:
2(a). If $|x| \leq \frac{1}{n}$ for every positive integer $n$, then $x = 0$.
This is true, but awkward to prove directly because there are effectively infinitely many hypotheses (one for each positive $n$), yet no finite number of these hypotheses implies the conclusion.
2(b). If $x \neq 0$, there exists a positive integer $n$ such that $\frac{1}{n} < |x|$.
The contrapositive, which follows immediately from the Archimedean property, requires only a strategy for showing some hypothesis is violated if the conclusion is false.
3(a). If $f$ is a continuous, real-valued function on $[0, 1]$ and if
$$
\int_0^1 f(x) g(x)\, dx = 0\quad\text{for every continuous $g$,}
$$
then $f \equiv 0$.
3(b). If $f$ is a continuous, real-valued function on $[0, 1]$ that is not indentically zero, then
$$
\int_0^1 f(x) g(x)\, dx \neq 0\quad\text{for some continuous $g$.}
$$
Here contraposition is not especially helpful because the specific choice $f = g$ gives either direction. That is, 3(a) has infinitely many hypotheses, but one of them is sufficient to deduce the conclusion.
Contrast with the superficially similar-looking:
4(a). If $f$ is a continuous, real-valued function on $[0, 1]$ and if
$$
\int_0^1 f(x) g(x)\, dx = 0\quad\text{for every non-negative step function $g$,}
$$
then $f \equiv 0$.
4(b). If $f$ is a continuous, real-valued function on $[0, 1]$ that is not indentically zero, then
$$
\int_0^1 f(x) g(x)\, dx \neq 0\quad\text{for some non-negative step function $g$.}
$$
(Sketch of 4(b): If $f$ is not identically $0$, there is an $x_0$ in $(0, 1)$ such that $f(x_0) \neq 0$. By continuity, there exists a $\delta > 0$ such that $[x_0 - \delta, x_0 + \delta] \subset (0, 1)$ and $|f(x)| > |f(x_0)|/2$ for all $x$ with $|x - x_0| < \delta$. Let $g$ be the characteristic function of $[x_0 - \delta, x_0 + \delta]$.)
As in 2(a), the hypothesis of 4(a) comprises infinitely many conditions, and no finite number suffice. Here, the contrapositive 4(b) arises naturally, because in trying to establish 4(a) directly one is all but forced to ask how the conclusion could fail.
A: PS this Answer is just a rough draft, maybe I will add more later 
In general there are 6 ways to proof conditional theorems.
I think that if you want to prove $ P \to Q $ you have the following 6 options (they are more details later)


*

*Direct conditional proof

*Direct contrapositive proof

*Conditional indirect  proof

*Contrapositive indirect proof  

*Indirect proof 

*Indirect Contrapositive proof


Which way is easiest in your case depends on what the theorem you want to proof is, I think in general:


*

*start with what the easiest statements are.

*try to start with positive statements (negation just add an extra level of complexity)

*if only one of the formulas "$ P \lor \lnot P $ " $ ( \forall x P(x)  \lor  \forall x \lnot P(x) ) $ or "$ Q \lor \lnot Q $" $ ( \forall x Q(x) \lor \forall x  \lnot Q (x) )$  is provable, prefer the negation of that variable above the negation of the other variable.

*Direct conditional proof is best (it is constructive)

*Then then the methods 2, 3 and 4.

*Only use one of the Indirect proofs if everything else fails (because they do add an extra layer of negation), if you act this way possibly you will never have to use the indirect method again, although many will argue that the methods 3 and 4 are just indirect proof methods in disguise.  
PS 1 the names of the methods 2, 3, 4  and 6 are my own, there is no official terminology. (I just made them up while thinking about the question)
PS 2 off course there are many combinations possible of the 6 methods I mentioned, and it is even true that an "Conditional indirect proof" is a combination of an "Indirect proof" inside a "Direct proof" , but I organised them a bit so that all major methods (my opinion) are mentioned.
PS 3 all proofs methods that contain a "double negation elimination" (~~Elimination)  are not constructive (you proof that $ P \to Q $ is a theorem, but have not found a method to transform a P into a Q), but in fact all except the direct proof method contain ~~Eliminations. 
PS 4 Proof to get $ P \to Q $  from $ \lnot Q \to \lnot P $ :
This proof in itself contains a double negation elimination, so all proofs leading to $ \lnot Q \to \lnot P $ are not constructive.
1 | . . . ~Q -> ~P       proved before
2 | |____ P              Assumption
3 | | |__ ~Q             Assumption
4 | | | . ~P             1,3 -> Eliminations
5 | | | . contradiction  2,3 contradiction Introduction
. | | <----------------------- end subproof
6 | | . . ~~Q            3-5 ~ Introduction
7 | | . . Q              6   ~~Elimination
. | <------------------------- end subproof
8 | . . . P -> Q         2-7 ->Introduction

The different methods:
1) Direct Conditional proof


*

*Assume P

*some how get to Q

*implication introduction


Formal proof
1 | |____ P          Assumption
: | | : : ?????????     some aplications of inference rules
: | | : : ?????????     some aplications of inference rules
k | | . . Q             inference rule
. | <-------------------- end subproof
m | . . . P -> Q     1-k -> Introduction

2) Direct Contrapositive proof


*

*Assume ~Q

*some how get to ~P

*implication introduction


Formal proof
1 | |____ ~Q          Assumption
: | | : : ?????????      some aplications of inference rules
: | | : : ?????????      some aplications of inference rules
k | | . . ~P             inference rule
. | <--------------------- end subproof
m | . . . ~Q -> ~P    1-k ->  Introduction

3) Conditional Indirect proof


*

*Assume P

*Assume ~Q

*some contradiction

*Reductio ad absurdum 

*implication introduction


Formal proof
1 | |____ P              Assumption
: | | : : ?????????         some aplications of inference rules
: | | : : ?????????         some aplications of inference rules
a | | |__ ~Q             Second Assumption
: | | | : ?????????         some aplications of inference rules
: | | | : ?????????         some aplications of inference rules
i | | | . contradiction     contradiction Introduction
. | | <---------------------- end subproof
j | | . . ~~Q            a-i ~ Introduction
k | | . . Q              j   ~~Elimination
. | <------------------------ end subproof 
m | . . . P -> Q         1-k ->  Introduction

The results between line 1 and a maybe interesting of their own accoord, that is why this method is better than 5) Indirect proof
4) Contrapositive Indirect proof
This is  a variation of conditional indirect  proof method (no 3) the assumptions are reshuffeled. choose this method if from assuming ~Q more usefull things are provable than from assuming P. 


*

*Assume ~Q

*Assume P

*some contradiction

*Reductio ad absurdum 

*implication introduction


Formal proof
1 | |____ ~Q            Assumption
: | | : : ?????????         some aplications of inference rules
: | | : : ?????????         some aplications of inference rules
a | | |__ P             Second Assumption
: | | | : ?????????        some aplications of inference rules
: | | | : ?????????        some aplications of inference rules
i | | | . contradiction    contradiction Introduction 
. | | <---------------------- end subproof
k | | . . ~P            a-i ~ Introduction
. | <------------------------ end subproof
m | . . . ~Q -> P       1-k ->  Introduction

The results between line 1 and a maybe interesting off their own accoord, that is why this method is better than 6) Indirect contrapositive proof
5) Indirect proof


*

*Assume ~(P -> Q)

*some contradiction

*Reductio ad absurdum 


Formal proof
1 | |____ ~(P -> Q)     Assumption
2 | | : : ?????????         some aplications of inference rules
: | | : : ?????????         some aplications of inference rules
: | | : : ?????????         some aplications of inference rules
j | | : : ?????????         some aplications of inference rules
k | | . . Contradiction     contradiction Introduction
. | <------------------------ end subproof
m | . . . ~~(P -> Q)    1-k ~ Introduction
n | . . . P -> Q        m   ~~Elimination

Often (allways?) this proof can be replaced by a Conditional Indirect Proof (3), it is advisable to use that method.  
6) Indirect Contrapositive proof 


*

*Assume ~(~Q -> ~P)

*some contradiction

*Reductio ad absurdum 


Formal proof
1 | |____ ~(~Q -> ~P)    Assumption
2 | | : : ?????????          some aplications of inference rules
: | | : : ?????????          some aplications of inference rules
: | | : : ?????????          some aplications of inference rules
j | | : : ?????????          some aplications of inference rules
k | | . . Contradiction      contradiction Introduction
. | <------------------------ end subproof 
m | . . . ~~(~Q -> ~P)   1-k ~ Introduction
n | . . . ~Q -> ~P       m   ~~Elimination

Often (allways?) this proof can be replaced by an Contrapositive Indirect proof (4), it is advisable to use that method.
PS this Answer is (still) just a rough draft, maybe I will add more later
A: Look at another example: 
In the language of sets, it takes  the form
$$A\subset B\Longleftrightarrow B^c\subset A^c,$$
where $A^c$ is the complement of $A$.
A: One reason why doing a proof of $A\Rightarrow B$ by contradiction might be easier is the following. For a direct proof you can only use $A$ being true as your working ground, while a proof by contradiction gives you both $A$ and $\neg B$ to get started, so you can draw more conclusions.
In this case, we aren't even proving $\neg B \Rightarrow \neg A$ but $$A \wedge \neg B \Rightarrow \text{false}.$$
In the end, all of these are equivalent of course.
A: On what basis we think that, in general, a contrapositive argument is "more easy" to find that a direct one ?
In user86418's very useful list of examples, we have that :

(1) has "logical form" : $\forall x ( \lnot \phi(x) \rightarrow \lnot \psi(x) )$

So, when we contrapose it, we reduce it to : $\psi(x) \rightarrow \phi(x)$ that is the direct one.

(2) has the form : $\forall x (\forall n \phi (x,n) \rightarrow x = 0 )$; the contraposition give us : $ x \neq 0 \rightarrow \exists n \lnot \phi (x,n) $
(3) and (4) both are like : $\forall f ( \forall g  \int_0^1 f(x) g(x)\, dx = 0 \rightarrow f \equiv 0 )$.

The contrapositive is "if $f$ is not indentically zero" $\rightarrow \exists g \int_0^1 f(x) g(x)\, dx \neq 0$.
My suggestion is that, the last three cases support the idea that is not, in general, more easy to prove $(\lnot Q \rightarrow \lnot P)$ instead of the direct $(P \rightarrow Q)$, but is more easy to prove :

$(\lnot \psi \rightarrow \exists \lnot \phi)$

instead of :

$(\forall \phi \rightarrow \psi)$.

My suggestion (to be verified) is that the interplay between conditional and quantifiers is the relevant issue here.
