Proof in constructive mathematics using decidability.

Question

I am working in constructive mathematics that means without the law of excluded middle. One may also interpret this as working in inuitionistic logic.

Lets assume I have some set $A$ such that I know that $0 \in A$ is decidable. I have another statement $B$. I want to prove that $B \Rightarrow (0 \in A)$. Is the following proof strategy justified in constructive mathematics:

I make a case distinction:

Case 1: $0 \in A$, hence nothing to show.

Case 2: $ 0 \notin A$. Then bla bla bla bla bla $\rightarrow$ contradiction. Hence we must have $0 \in A$.

To be more precise: The contradiction I get in Case 2 is $\neg B$. (this is a contradiction since I assumed $B$).

I am not sure which of the following logical expressions is used in this proof. Either

$B \rightarrow \neg A \rightarrow \neg B \rightarrow A$

or

$\neg \neg A \rightarrow A$

($\neg A$ is short for $0 \notin A$).

Answer 1

By "$0 \in A$" is decidable, we just mean $0 \in A \lor 0 \not \in A$.

Given that assumption, if you can prove $\lnot \lnot (0 \in A)$, you can prove $0 \in A$. As you know $\lnot \lnot (0 \in A)$ is $\lnot (0 \in A) \to \bot$.

The proof of $0 \in A$ is as follows.

Case 1: $0 \in A$. Done.

Case 2: $0 \not \in A$, i.e. $\lnot (0 \in A)$. Then, from $\lnot (0 \in A) \to \bot$, we obtain $\bot$. Then, from the contradiction rule $\bot \to 0 \in A$, we have $0 \in A$.

Answer 2

You know $A\lor\neg A$ and $\neg A\to\neg B$, and you want to prove $B\to A$:

Assume $B$, and we then seek to prove $A$.

Do case analysis on $A\lor\neg A$ (which we already know holds).

In the case $A$ we're done.

In the case $\neg A$, apply $\neg A\to\neg B$ to get $\neg B$. Together with the assumption $B$, this is a contradiction, and by the principle of explosion we're allowed to conclude $A$.

In both cases we could conclude $A$, so $A$, and therefore (discharging the hypothesis) $B\to A$.

All of this is perfectly valid intuitionistcally.