# CFG that generates $1^*$ is decidable

I read somewhere that the problem which asks whether or not a CFG $$G$$ generates $$1^*$$ is decidable. The proof goes like this:

$$1^* \cap L(G)$$ is context free since it is the intersection of a regular language and a CFL, therefore we can test if $$1^* \cap L(G)$$ is empty since it is decidable to check if the language produced by a CFG is empty. If $$1^* \cap L(G)$$ is empty, reject, otherwise, accept.

I have doubts however with this proof since it only shows that some string in $$1^*$$ is generated by $$G$$, but not whether $$G$$ generates all strings in $$1^*$$.

Moreover, if this proof is correct, we can use the same proof outline under the alphabet $$\Sigma=\{0,1\}$$ to show that $$G$$ generates $$\Sigma^*$$, or that $$\Sigma^* \subseteq G$$. However, it is known that it is undecidable whether $$R \subseteq G$$, where $$R$$ is a regular language, and $$G$$ is a CFG (by setting $$R=\Sigma^*$$, and $$\Sigma=\{0,1\}$$.

But to show that a CFG generates $$1^*$$ is decidable, the only way I can think of is to use something similar to the proof that it is decidable for a PCP instance to generate some string in $$1^*$$ (i.e., $$w=v$$, where $$w,v \in 1^*$$), i.e. we can check if the CFG has rule $$S \rightarrow S1$$, then accept. Otherwise, if it has rules of the form $$S \rightarrow 1^aS1^b$$ such that $$a > b$$, and rules of the form $$S \rightarrow 1^cS1^d$$ such that $$c < d$$, then accept... But is there a simpler way to solve this problem?

Maybe you're confusing two different problems. The algorithm you are describing shows that the problem of testing whether a CFG generates some string from $$1^∗$$ is decidable (e.g., see here at page 21). Anyway, the problem of testing whether a CFG generates all the strings of the language $$1^∗$$ is truly decidable. Consider all production rules to be simple (I mean, no "$$|$$" on the right), and eliminate all productions including a terminal character different from 1 on the right. Now you have a CFG over a terminal alphabet of a single letter, and then it generates a regular language (see here). All that remains is to test if two regular languages are equal. Moreover, there are effective procedures to convert a CFG over a one-letter (terminal) alphabet into a regular grammar (e.g., see here).
On the last part of your question: the fact that it is undecidable whether $$R\subseteq G$$, where $$R$$ is a regular language, and $$G$$ is a CFL, does not imply that for some specific regular languages you can not decide the inclusion. For example, if $$R$$ is finite (possibly empty), then testing for $$R\subseteq G$$ is decidable (see the first link above).