I'm working on a homework assignment on designing and proving grammars, and I'm having a hard time deciding what claims to use in the proof of the design. For example, I have a the problem of designing a grammar $G$ such that $L(G) = \{\alpha_0 \alpha_1^n \alpha_2^n | n \in \mathbb{N} \}$. I've done this:
Let $x$ be a typical string: $x = \alpha_0 \alpha_1^n \alpha_2^n$
With the following productions:
$S \rightarrow \alpha_0 A \\A \rightarrow \lambda | \alpha_1 A \alpha_2$
Which gives the grammar: $G = (\{S,A\} \{\alpha_0, \alpha_1, \alpha_2\}, S, \{S \rightarrow \alpha_0 A,\ A \rightarrow \lambda | \alpha_1 A \alpha_2\})$
At this point in the professors examples, he comes up with claims that I'm supposed to prove in order to prove that $L \subseteq L(G)$ and $L(G) \subseteq L$. The only claim I can think of is $\forall n \ S \rightarrow^* \alpha_0 \alpha_1^n A \alpha_2^n$.
I have no idea if this claim is even useful, if there's more claims to solve, etc. There's another 11 problems of this, so I'm looking to understand how to come up with claims rather than just the answer to this.
My new solution:
Claim 1 $ \forall n S \Rightarrow^* \alpha_0 \alpha_1^n A \alpha_2^n $
Proof Claim 1
Base Case $n=0$: $ S \Rightarrow^* \alpha_0 \alpha_1^0 A \alpha_2^0 = \alpha_0 A $
Inductive Hypothesis: $\forall n \ S\Rightarrow^* \alpha_0 \alpha_1^n A \alpha_2^n$
Inductive Step $n=n+1$: $S \Rightarrow^* \alpha_0 \alpha_1^n \alpha_1 A \alpha_2 \alpha_2^n = \alpha_0 \alpha_1^{n+1} A \alpha_2^{n+1} $
One possibility is to use induction on the length of the derivation. Your claim goes in that direction. In your case things are relatively simple, because the grammar is linear and there is only one path to follow. So in $n+1$ steps you can derive $\alpha_0 \alpha_1^n \alpha_2^n$ and $\alpha_0 \alpha_1^n A \alpha_2^n$.
This can be proven by induction starting from $n=1$. All the words that are generated are thus of the form $\alpha_0 \alpha_1^n \alpha_2^n$ and in the desired language.
The inverse inclusion (all words of the generated language are generated by at least one derivation) is quite clear in this case: for $\alpha_0 \alpha_1^n \alpha_2^n$ briefly descibe the $n+1$-step derivation, if you want to do it in a very complete and correct manner.