proposition: Lemma lift_parse_prod {str' offset len0_minus_len a it its} (H : (minimal_parse_of_item (G := G) len0 valid (substring offset (len0 - max (len0 - a) len0_minus_len) str') it * minimal_parse_of_production (G := G) len0 valid (substring (offset + a) (len0 - (len0_minus_len + a)) str') its)%type) : minimal_parse_of_item (G := G) len0 valid (take a (substring offset (len0 - len0_minus_len) str')) it * minimal_parse_of_production (G := G) len0 valid (drop a (substring offset (len0 - len0_minus_len) str')) its.
proof: Proof. destruct H as [pi pp]; split. { eapply expand_minimal_parse_of_item_beq; [ | eassumption ]. rewrite take_take, <- Nat.sub_min_distr_l, sub_twice. rewrite (Nat.min_comm len0), <- !Nat.min_assoc, min_minus_r. reflexivity. } { eapply expand_minimal_parse_of_production_beq; [ | eassumption ]. rewrite drop_take, StringLike.drop_drop, (Nat.add_comm a offset), Nat.sub_add_distr. reflexivity. } Defined.
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