proposition: Lemma terminals_disjoint_rev_search_for_not' (str : @String Ascii.ascii HSLM) {nt its} (H_disjoint : disjoint ascii_beq (possible_last_terminals_of nt) (possible_terminals_of_production its)) {n} (pit : parse_of_item G (StringLike.take n str) (NonTerminal nt)) (pits : parse_of_production G (StringLike.drop n str) its) (H_reachable : production_is_reachable G (NonTerminal nt :: its)) : forall_chars__char_in (drop n str) (possible_terminals_of_production its) /\ ((n = 0 /\ might_be_empty_of nt) \/ (for_last_char (take n str) (fun ch => negb (list_bin ascii_beq ch (possible_terminals_of_production its))) /\ n > 0)).
proof: Proof. destruct H_reachable as [ nt' [ prefix [ HinV HinL ] ] ]. pose proof HinV as HinV'; rewrite <- (@initial_nonterminals_correct _ G (@rdp_list_predata _ G) (@rdp_list_rdata' _ G)) in HinV'. apply and_comm; split. { destruct (Compare_dec.zerop n); [ left | right ]. { split; trivial; []; subst. eapply might_be_empty_pr_parse_of_item_nt; try eassumption. rewrite take_length; reflexivity. } { split; try omega; []. eapply last_char_in__impl__for_last_char; [ | apply possible_last_ascii_parse_of_item_nt; eassumption ]. intros ch H'. apply Bool.negb_true_iff, Bool.not_true_iff_false. intro H''. apply list_in_bl in H''; [ | apply (@ascii_bl) ]. eapply fold_right_andb_map_in in H_disjoint; [ | eassumption ]. apply Bool.negb_true_iff, Bool.not_true_iff_false in H_disjoint. apply H_disjoint. apply list_in_lb; [ apply (@ascii_lb) | assumption ]. } } { apply all_possible_ascii_of_parse_of_production; assumption. } Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Init.Wf Coq.Arith.Wf_nat Coq.ZArith.ZArith Coq.Lists.List Coq.Strings.String Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Parsers.ContextFreeGrammar.Equality Coq.Program.Equality Coq.MSets.MSetPositive Fiat.Common Fiat.Common.Equality Fiat.Common.Wf Fiat.Common.Enumerable Fiat.Common.LogicFacts Fiat.Parsers.Splitters.RDPList Fiat.Parsers.Splitters.BruteForce Fiat.Parsers.ParserInterface Fiat.Parsers.BaseTypes Fiat.Parsers.CorrectnessBaseTypes Fiat.Parsers.BooleanRecognizerFull Fiat.Parsers.BooleanRecognizerCorrect Fiat.Common.List.Operations Fiat.Parsers.StringLike.Core Fiat.Parsers.StringLike.ForallChars Fiat.Parsers.StringLike.FirstChar Fiat.Parsers.StringLike.FirstCharSuchThat Fiat.Parsers.StringLike.LastChar Fiat.Parsers.StringLike.LastCharSuchThat Fiat.Parsers.StringLike.Properties Fiat.Parsers.MinimalParseOfParse Fiat.Parsers.ContextFreeGrammar.Properties Fiat.Parsers.ContextFreeGrammar.Fold Fiat.Parsers.BaseTypesLemmas Fiat.Parsers.ContextFreeGrammar.Valid Fiat.Parsers.ContextFreeGrammar.ValidProperties Fiat.Parsers.ContextFreeGrammar.ValidReflective Fiat.Parsers.Refinement.DisjointLemmasEarlyDeclarations Fiat.Parsers.Refinement.PossibleTerminalsSets Fiat.Common.BoolFacts