proposition: Lemma production_reachable_convert idx p (H : to_production idx = p) (H' : full_production_carrierT_reachableT idx) : production_is_reachable G p.
proof: Proof. subst. destruct H' as [nt H']; exists nt. destruct H' as [count [idx' [[Hvalid H0] H1]]]; subst. erewrite <- nonterminal_to_production_correct by assumption. induction (nonterminal_to_production (of_nonterminal nt)) as [|x xs IHxs]; simpl in *. { destruct_head False. } { destruct_head or; destruct_head sum; subst; specialize_by assumption. { clear IHxs. induction count as [|count IHcount]; simpl. { eexists nil; simpl. split; [ assumption | left; reflexivity ]. } { rewrite apply_n_commute, production_tl_correct. destruct IHcount as [prefix IHcount]. match goal with | [ |- context[_ ++ tl ?ls] ] => exists (match ls with | nil => prefix | x::_ => prefix ++ [x] end); destruct ls eqn:Heq; simpl in * end; rewrite ?app_nil_r, <- ?app_assoc in IHcount; rewrite ?app_nil_r, <- ?app_assoc; assumption. } } { destruct IHxs as [prefix [H0 H1]]. exists prefix. split; [ assumption | right; assumption ]. } } Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.Arith.EqNat Coq.Arith.Compare_dec Coq.Arith.Wf_nat Coq.ZArith.ZArith Fiat.Common.List.Operations Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.BaseTypes Fiat.Parsers.GenericBaseTypes Fiat.Parsers.GenericCorrectnessBaseTypes Fiat.Parsers.StringLike.Properties Fiat.Parsers.MinimalParse Fiat.Parsers.CorrectnessBaseTypes Fiat.Parsers.BaseTypesLemmas Fiat.Parsers.ContextFreeGrammar.Properties Fiat.Parsers.WellFoundedParse Fiat.Parsers.MinimalParseOfParse Fiat.Parsers.GenericRecognizer Fiat.Parsers.GenericRecognizerExt Fiat.Common.Wf Fiat.Common.Wf1 Fiat.Common.List.ListFacts Fiat.Common.NatFacts Fiat.Common.UIP Fiat.Common