Intuitionistic logic plus $A → B \lor C \vdash ( A → B ) \lor ( A → C )$

Are you familiar with Kripke semantic of intuitionistic logic (see Semantics of intuitionistic logic here)?$\def\imp{\rightarrow}$

Intuitively, a proposition is not interpreted as globally truth or false, but rather as the set of 'knowledge states' in which it is 'known'. Knowledge states may evolve, and the only restriction to the interpretation of propositions is that knowledge cannot be revoked.

Formally, you pick a Kripke frame, i.e. a set $W$ equipped with a preorder $\leq$, and interpret any propositional variable as a subset of $W$ that is closed under passing to $\leq$-greater elements. With the interpretations of the propositional variables fixed, you interpret $\lor$ and $\land$ as union and intersection, respectively. Also, you interpret $\bot$ as none of $W$ (the empty set) and $\top$ as all of $W$. The interesting part is the interpretation of implication: If $\psi$ and $\phi$ are interpreted as $A,B\subset W$, then $\psi\imp\phi$ is interpreted as the set of states $w\in W$ such that for any $v\in W$ with $w\leq v$ and $v\in A$, you also have $v\in B$. Appealing to the intuition again, it means that however knowledge evolves, whenever $\psi$ is known then so is $\phi$. For example, $\neg\neg\phi \equiv ( \phi \imp \bot ) \imp \bot$ is known at $w$ precisely if for any $v\in W$ with $w\leq v$ there is $z\in W$ with $w\leq z$ such that $\phi$ holds at $z$ - in other words, you can never refute $\phi$. This is much weaker than asserting that $\phi$ holds for all of $W$, as you can see e.g. from the example at the end of the post, where $W = \{0\to 1\}$.

Anyway, the Kripke semantics is sound for intuitionistic logic, so to prove that a formula is not an intuitionistic tautology, it suffices to provide some Kripke frame with an interpretation of the formulas' propositional variables such that the associated interpretation is not true in the whole Kripke frame.

Let's do this for $(A\imp (B\lor C))\imp ((A\imp B)\lor (A\imp C))$: Consider the frame $1\leftarrow 0\rightarrow 2$ and interpret $A$ as known only at $1,2$, $B$ as known only at $1$ and $C$ as known only at $2$. Then $A\imp B$ and $A\imp C$ are both not known at $0$ since there is an evolution which validates $A$ but does not validate $B$ (similarly $C$). However, $A\imp (B\lor C)$ is valid at $0$, since for any evolution from $0$ to either $1$ or $2$, either $B$ or $C$ is valid in the new state.

Concerning your second question: An example like the above can only exist if the frame $W$ under consideration has branches; if, in contrast, evolution is unique - meaning formally that for any three elements $u,v,w$ in the frame satisfying $u\leq v$ and $u\leq w$, we have either $v\leq w$ or $w\leq v$ - the formula $(A\imp (B\lor C))\imp ((A\imp B)\lor (A\imp C))$ does indeed hold under any interpretation.

Therefore, if you add $(A\imp (B\lor C))\imp ((A\imp B)\lor (A\imp C))$ as an axiom to intuitionistic logic, you will still have sound Kripke semantics when restricting to frames with unique evolution. Hence, to check that a formula is not a tautology with respect to this stronger calculus, it suffices to find an interpretation in such a uniquely evolving frame which does not validate the formula. For $\neg \neg A$, you can pick the frame $W = \{0\to 1\}$ and interpret $A$ as known at $1$ but unknown at $0$: Then $\neg\neg A$ is globally known (see above), but $A$ is not. Hence, $\neg \neg A \imp A$ is not a tautology in the enhanced calculus, and therefore the enhanced calculus is still strictly contained in classical propositional logic.

Here is an answer that builds on the intuition I had 4 years ago when asking this question. The idea is to use the BHK interpretation where a witness of $P→Q$ is a program that given any witness of $P$ as input will produce a witness of $Q$ as output. Intuitionistic logic proves only sentences that have such a witness.

Then to answer the first question, it suffices to find $A,B,C$ such that we can computably convert any given witness of $A$ into a witness of $B∨C$, but such that we cannot construct a witness for $A→B$ nor a witness for $A→C$. To do so, consider $A :≡ X∨Y$ and $B :≡ X$ and $C :≡ Y$ where $X,Y$ are distinct propositional variables. Then clearly $A→B∨C$ has a witness, and hence is intuitionistically provable. However, $A→B ≡ X∨Y→X$ has no witness, since a witness of $X∨Y$ may be a witness of $Y$ rather than $X$. Similarly, $A→C$ has no witness. Thus there is no witness of $(A→B)∨(A→C)$, and hence it is intuitionistically unprovable. Therefore the rule cannot be intuitionistically valid.

I do not see an obvious way to address the second question using the BHK interpretation, so for that please refer to Hanno's answer using Kripke frames. =)