proposition: Lemma terminals_disjoint_search_for_not' (str : @String Ascii.ascii HSLM) {nt its} (H_disjoint : disjoint ascii_beq (possible_terminals_of nt) (possible_first_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 (take n str) (possible_terminals_of nt) /\ ((length str <= n /\ might_be_empty_of_production its) \/ (for_first_char (drop n str) (fun ch => negb (list_bin ascii_beq ch (possible_terminals_of nt))) /\ n < length str)).
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.le_dec (length str) n); [ left | right ]. { split; trivial. pose proof (drop_length str n) as H. rewrite (proj2 (Nat.sub_0_le (length str) n)) in H by assumption. generalize dependent (drop n str); clear -pit HinV' HinL HSLP HSIP. intros. eapply might_be_empty_pr_parse_of_production; eassumption. } { split; try omega; []. eapply first_char_in__impl__for_first_char; [ | apply possible_first_ascii_parse_of_production; 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_item_nt pit). } 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