Let $P$ be a quantifier-free decidable formula, i.e. one can prove $P \lor \lnot P$. Does it follow that $\lnot \lnot P \to P$ intuitionistically?
Informally, a decidability of a formula means local LEM, but is it correct to treat it as "a piece of classical logic"?
On
Here is another constructive proof. Assume $P \lor \lnot P$. Then either $P$ holds or $\lnot P$ holds. So we can reason by cases. If $P$ holds then $\lnot \lnot P \to P$ holds trivially. If $\lnot P$ holds, because $\lnot \lnot P$ is an abbreviation for $(\lnot P) \to \bot$, then $\bot$ holds, and by the principle of explosion (ex falso), $P$ holds. In either case, $\lnot \lnot P \to P$ holds.
The deeper point is that if we already know $A \lor B$ then we can prove a formula $C$ constructively by proving it under assumption $A$ and also by proving it under assumption $B$. Usually, the issue is that we cannot prove $P \lor \lnot P$ constructively, so we cannot reason by cases in that way. In other words, it is not that proof by cases is invalid constructively, it's that we have to prove that our cases are exhaustive (e.g. $P \lor \lnot P)$, which is often more difficult than in the classical case, making proof by cases a less broadly useful method.
Although the statement $\neg P\vee P$ is not a theorem in intuitionist logic, the conditional claim $\neg P\vee P\vdash \neg\neg P\to P$ may be constructed, through use of Explosion and Disjunctive Elimination.