Can one prove by contraposition in intuitionistic logic?

I read that contraposition $\neg Q \rightarrow \neg P$ in intuitionistic logic is not generally equivalent to $P \rightarrow Q$. If this is right, in what case can this contraposition logical-equivalence be used in intuitionistic logic?

Contraposition in intuitionism can, sometimes, be used, but it's a delicate situation.

You can think of it this way. Intuitionistically, the meaning of $P\to Q$ is that any proof of $P$ can be turned into a proof of $Q$. Similarly, $\neg Q \to \neg P$ means that every proof of $\neg Q$ can be turned into a proof of $\neg P$.

If $P\to Q$ is true, and you are given a proof of $\neg Q$, can you construct a proof of $\neg P$ ? The answer is yes, as follows. Well, we are given a proof that there is no proof of $Q$. Suppose $P$ is true, then it can be turned into a proof of $Q$, but then we will have a proof of $Q\wedge \neg Q$, which is impossible. Thus we just showed that it is not the case that $P$ holds, thus $\neg P$ holds. In other words, $(P\to Q)\to (\neg Q \to \neg P)$.

In the other direction, suppose that $\neg Q \to \neg P$, and you are given a proof of $P$. Can you now construct a proof of $Q$? Well, not quite. The best you can do is as follows. Suppose I have a proof of $\neg Q$. I can turn it into a proof of $\neg P$, and then obtain a proof of $P\wedge \neg P$, which is impossible. It thus shows that $\neg Q$ can not be proven. That is, that $\neg \neg Q$ holds. In other words, $(\neg Q \to \neg P)\to (P\to \neg \neg Q)$.

In what case can this contraposition logical-equivalence be used in intuitionistic logic?

This is not straightforward to answer. What needs to be true is that $P$ and $Q$ need to act sufficiently like classical formulas. Here are two examples:

1. The negative translation embeds classical logic into intuitionistic logic, sending a formula $S$ to a formula $S^N$. If we compute this for an instance of contraposition, we obtain:

$$(\lnot R \to \lnot S) \to (S \to R))^N\\ (\lnot R \to \lnot S)^N \to (S \to R)^N\\ ((\lnot R)^N \to (\lnot R)^N \to (S^N \to R^N)\\ (\lnot R^N \to \lnot S^N) \to (S^N \to R^N)$$

Therefore $(\lnot R^N \to \lnot S^N) \to (S^N \to R^N)$ is intuitionistically valid for all $R,S$. In particular, if $P$ and $Q$ are equivalent to negative translations of other formulas, then contraposition holds for $P$ and $Q$.

2. Here is a different view. Suppose $Q_0$ is a fixed formula such that contraposition holds between $Q_0$ and all $P$: $$(\lnot Q_0 \to \lnot P) \to (P \to Q_0)$$

Then, letting $P$ be $\lnot \bot$, we have $\lnot P$ equivalent to $\bot$, and so from $$(\lnot Q_0 \to \lnot P) \to (P \to Q_0)$$ we obtain $$(\lnot \lnot Q_0) \to (\lnot \bot \to Q_0)$$ which is equivalent to $$\lnot \lnot Q_0 \to Q_0$$ Thus if $Q_0$ satisfies contraposition with all $P$, then $Q_0$ is equivalent to $\lnot\lnot Q_0$. The converse of this was shown by Ittay Weiss in another answer: if $Q_0$ is equivalent to $\lnot\lnot Q_0$ then $Q_0$ satisfies contraposition with all $P$.