proposition: Lemma adt_based_splitter_splits_for_complete : forall (str : String) (idx : default_production_carrierT) (offset : nat) (len : nat), split_list_is_complete_idx G str offset len idx (msplits idx offset len (` str)).
proof: Proof. repeat (hnf; cbv zeta; intro). destruct_head_hnf' sig. destruct_head' ex. unfold length, take, drop, adt_based_StringLike, adt_based_StringLikeMin, proj1_sig in *. repeat match goal with | [ H : context[_ <= mlength _] |- _ ] => erewrite @mlength_eq in H by first [ eassumption | eapply mtake_R, mdrop_R; eassumption ] | _ => erewrite @mlength_eq by first [ eassumption | eapply mtake_R, mdrop_R; eassumption ] end. match goal with | [ H : AbsR ?Ok ?str ?st |- context[msplits ?arg1 ?arg2 ?arg3 ?st] ] => let T := type of Ok in let impl := (match eval cbv beta in T with refineADT _ (LiftcADT ?impl) => constr:(impl) end) in let H' := fresh in pose proof (ADTRefinementPreservesMethods Ok splits _ _ H arg1 arg2 arg3 ((cMethods impl splits st arg1 arg2 arg3)) (ReturnComputes _)) as H'; change (msplits arg1 arg2 arg3 st) with (snd (premsplits st arg1 arg2 arg3)); match type of H' with | context G[cMethods _ splits] => let G' := context G[premsplits] in change G' in H' end end. simpl Methods in *. computes_to_inv; subst. simpl @fst in *. simpl @snd in *. match goal with | [ H : ?x = premsplits _ _ _ _ |- _ ] => rewrite <- H; clear H; simpl @snd end. lazymatch goal with | [ H : split_list_is_complete_idx _ _ _ _ _ _, H' : ?n <= _, p0 : parse_of_item _ _ _, p1 : parse_of_production _ _ _, H'' : production_is_reachable _ _, Heq : default_to_production _ = _::_ |- List.In ?n ?v ] => hnf in H; specialize (fun pf' idx H0'' H0' H1' => H pf' idx _ _ Heq n H' H'' (@transfer_parse_of_item Ascii.ascii adt_based_StringLikeMin stringlike_stringlikemin adt_based_StringLike stringlike_stringlike G (fun s1 s2 => AbsR (projT2 splitter_impl) s2 (` s1)) H0'' _ _ _ H0' p0) (@transfer_parse_of_production Ascii.ascii adt_based_StringLikeMin stringlike_stringlikemin adt_based_StringLike stringlike_stringlike G (fun s1 s2 => AbsR (projT2 splitter_impl) s2 (` s1)) H0'' _ _ _ H1' p1)); apply H; clear H p0 p1; try assumption end; [ split | | ]; handle_rep; eauto with parser_adt_method_db. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.String Coq.ZArith.ZArith Fiat.ADTNotation.BuildADT Fiat.ADTNotation.BuildADTSig Fiat.ADT.ComputationalADT Fiat.ADTRefinement.GeneralRefinements Fiat.Parsers.ParserInterface Fiat.Parsers.ParserADTSpecification Fiat.Parsers.ContextFreeGrammar.Properties Fiat.Parsers.ContextFreeGrammar.Transfer Fiat.Parsers.ContextFreeGrammar.TransferProperties Fiat.Parsers.ContextFreeGrammar.Carriers Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.ADTRefinement.Core Fiat.Common Fiat.Common.Equality Fiat.Common.BoundedLookup Fiat.Common.StringOperations Fiat.Common.StringFacts Fiat.ADTNotation.BuildComputationalADT Fiat.Parsers.StringLike.Core Fiat.Parsers.StringLike.Properties