proposition: Lemma fold_cnt_correct nt nt_idx (Hnt : of_nonterminal nt = nt_idx) : Pnt initial_nonterminals_data nt (fold_cnt (productions G) nt nt_idx).
proof: Proof. unfold fold_cnt, productions. repeat match goal with | _ => progress subst | _ => rewrite ListFacts.nth_error_nth | _ => progress unfold option_map in * | _ => progress break_innermost_match_step | _ => progress break_innermost_match_hyps_step | _ => progress inversion_option | _ => progress destruct_head' sig | _ => progress destruct_head' and | _ => progress cbn [fst snd plus] in * | [ H : nth_error (map _ _) _ = Some _ |- _ ] => apply ListFacts.nth_error_map'_strong in H | [ H : nth_error (enumerate _ _) _ = _ |- _ ] => rewrite ListFacts.nth_error_enumerate in H | [ H : nth_error (map ?f ?ls) ?idx = None |- _ ] => let H' := fresh in destruct (nth_error ls idx) eqn:H'; [ eapply map_nth_error in H'; rewrite H in H'; congruence | clear H ] end. { match goal with | [ H : nth_error _ (of_nonterminal ?nt) = Some ?x |- _ ] => assert (fst x = nt); [ pose proof H as H'; rewrite nth_error_default_to_nonterminal in H' | subst nt ] end. { break_innermost_match_hyps; try congruence; inversion_option; subst. cbn [fst]. change default_to_nonterminal with (rdp_list_to_nonterminal (G:=G)). unfold of_nonterminal, predata, rdp_list_predata. rewrite rdp_list_to_of_nonterminal; [ reflexivity | ]. apply initial_nonterminals_correct, rdp_list_is_valid_nonterminal_nth_error. congruence. } { apply fold_cnt_correct; reflexivity. } } { apply Pnt_redundant; [ reflexivity | ]. match goal with |- ?x = false => destruct x eqn:Hb end; [ | reflexivity ]. exfalso. eapply rdp_list_is_valid_nonterminal_nth_error; try eassumption; assumption. } Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.ZArith.ZArith Fiat.Parsers.ContextFreeGrammar.Carriers Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.BaseTypes Fiat.Parsers.BaseTypesLemmas Fiat.Parsers.Splitters.RDPList Fiat.Parsers.ContextFreeGrammar.Precompute Fiat.Common Fiat.Common.List.Operations Fiat.Common.Equality Fiat.Common.OptionFacts