proposition: Lemma rdp_list_nonterminal_to_production_correct : forall nt, List.In nt (Valid_nonterminals G) -> List.map rdp_list_to_production (rdp_list_nonterminal_to_production (rdp_list_of_nonterminal nt)) = Lookup G nt.
proof: Proof. intros nt Hvalid. unfold rdp_list_to_production, rdp_list_nonterminal_to_production, default_to_production. rewrite map_map; simpl. rewrite !rdp_list_to_of_nonterminal by assumption. rewrite <- list_to_productions_to_nonterminal. change default_to_nonterminal with rdp_list_to_nonterminal. rewrite rdp_list_to_of_nonterminal by assumption. induction (Lookup_string G nt) as [|p ps IHps]; simpl. { reflexivity. } { simpl. rewrite Nat.sub_diag; simpl. apply f_equal. etransitivity; [ | apply IHps ]; clear IHps. apply map_ext_in. intros a H; apply in_up_to_iff in H. rewrite Nat.sub_succ_r. destruct (Datatypes.length ps - a) eqn:H'; try omega; []. reflexivity. } Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.ZArith.ZArith Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Parsers.BaseTypes Fiat.Parsers.ContextFreeGrammar.Carriers Fiat.Common Fiat.Common.Equality Fiat.Common.List.Operations Fiat.Common.List.ListFacts