# 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 G$$ is context free since it is the intersection of a regular language and a $$CFG$$, therefore we can test if $$1^* \cap G$$ is empty since it is decidable to check if a $$CFG$$ is empty. If $$1^* \cap 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 teminal 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).
I was forgetting 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 CFG, does not implies 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).