proposition: Lemma rdp_list_of_to_nonterminal : forall nt, is_true (rdp_list_is_valid_nonterminal rdp_list_initial_nonterminals_data nt) -> rdp_list_of_nonterminal (rdp_list_to_nonterminal nt) = nt.
proof: Proof. pose proof (nonterminals_unique G) as HNoDup. hnf in HNoDup. simpl in *. unfold rdp_list_to_nonterminal, rdp_list_of_nonterminal, rdp_list_is_valid_nonterminal, rdp_list_initial_nonterminals_data, default_to_nonterminal, default_of_nonterminal. intros nt H. apply (list_in_bl (fun n m => proj1 (Nat.eqb_eq n m))), in_up_to_iff in H. revert nt H. replace valid_nonterminals with (uniquize string_beq valid_nonterminals) by (rewrite HNoDup; reflexivity). induction valid_nonterminals as [|x xs IHxs]. { simpl; intros; omega. } { simpl in *. destruct (list_bin string_beq x (uniquize string_beq xs)) eqn:Hbin; try assumption. { apply (f_equal (@List.length _)) in HNoDup. simpl in *. pose proof (uniquize_shorter xs string_beq) as H'. rewrite HNoDup in H'. exfalso; clear -H'. omega. } apply (f_equal (@tl _)) in HNoDup; simpl @tl in HNoDup. specialize_by assumption. intros [|nt]. { simpl. rewrite (string_lb eq_refl); trivial. } { simpl Datatypes.length. intro H. apply Nat.succ_lt_mono in H. etransitivity; [ | eapply (f_equal S), (IHxs _ H); clear IHxs ]. rewrite first_index_default_S_cons; simpl. match goal with | [ |- context[string_beq ?x ?y] ] => destruct (string_beq x y) eqn:H' end; simpl; [ exfalso | reflexivity ]. clear -Hbin H H'. apply string_bl in H'. subst. rewrite list_in_lb in Hbin; [ congruence | apply @string_lb | ]. apply nth_In; assumption. } } 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