proposition: Lemma split_list_completeT_production_is_reachable {it its offset len pf splits idx} (Hlen : len = 0 \/ offset + len <= length str) (H : split_list_completeT (G := G) splits) (Hreachable : full_production_carrierT_reachableT idx) (Hvalid : production_carrier_valid idx) (Heq : to_production idx = it::its) : split_list_completeT_for (G := G) (len0 := len0) (valid := valid) it its (substring offset len str) pf (splits idx str offset len).
proof: Proof. specialize (fun nt Hvalid => H len0 valid str offset len pf nt Hvalid Hlen). hnf in Hreachable. destruct Hreachable as [nt [count [idx' [[Hr0 Hr1] Hr2]]]]. specialize (H nt). erewrite <- nonterminal_to_production_correct in H by assumption. apply initial_nonterminals_correct in Hr0. specialize_by assumption. subst. generalize dependent (nonterminal_to_production (of_nonterminal nt)). intro p; induction p as [|x xs IHxs]; simpl. { intros ? []. } { intros H [H'|H']; subst; destruct_head prod; specialize_by assumption; trivial; []. clear dependent xs. generalize dependent idx'. induction count as [|count IHcount]; simpl in *; intros. { repeat match goal with | [ H : ?x = _::_, H' : context[match ?x with _ => _ end] |- _ ] => rewrite H in H' | [ H : _ |- _ ] => apply Forall_tails_id in H | _ => solve [ eauto with nocore ] end. } { specialize (IHcount (production_tl idx')). specialize_by assumption. rewrite production_tl_correct in IHcount. apply IHcount; clear IHcount. destruct (to_production idx'); simpl in *; destruct_head prod; trivial. } } 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