proposition: Lemma rdp_list_production_carrier_valid_reachable (idx : rdp_list_production_carrierT) (Hvalid : rdp_list_production_carrier_valid idx) : production_is_reachable G (rdp_list_to_production idx).
proof: Proof. unfold production_is_reachable, rdp_list_production_carrier_valid, default_production_carrier_valid, rdp_list_production_carrierT in *. repeat setoid_rewrite Bool.andb_true_iff in Hvalid. repeat setoid_rewrite Compare_dec.leb_iff in Hvalid. destruct_head and. simpl in *. exists (rdp_list_to_nonterminal (fst idx)). unfold rdp_list_to_production, default_to_production in *; simpl in *. match goal with | [ |- context[In (_ ++ Operations.List.drop ?n ?ls)%list _] ] => exists (Operations.List.take n ls) end. rewrite app_take_drop. split. { apply rdp_list_initial_nonterminals_correct'. unfold rdp_list_is_valid_nonterminal, rdp_list_initial_nonterminals_data. fix_list_bin_eq. apply list_in_lb; [ apply Nat.eqb_eq | ]. rewrite map_length. apply in_up_to; assumption. } { unfold rdp_list_to_nonterminal. rewrite list_to_productions_to_nonterminal. destruct (Lookup_idx G (fst idx)) eqn:Heq. { simpl in *. omega. } { apply nth_In. simpl; omega. } } 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