proposition: Lemma fold_cnt'_correct (valid0 : nonterminals_listT) (valid0_len : nat) (Hlen : nonterminals_length valid0 <= valid0_len) (Hsub : sub_nonterminals_listT valid0 initial_nonterminals_data) : forall nt nt_idx, of_nonterminal nt = nt_idx -> Pnt valid0 nt (fold_cnt' (compiled_productions G) valid0_len valid0 nt nt_idx).
proof: Proof. revert valid0 Hsub Hlen. induction valid0_len as [|valid0_len IH]. { intros; apply fold_nt_step_correct0; assumption. } { simpl. intros valid0 Hsub Hlen nt nt_idx Hnt. match goal with | [ |- context[if ?e then _ else _] ] => destruct e eqn:Hvalid end. { apply Pnt_lift; [ subst; assumption.. | ]. rewrite (eq_opt_Lookup_idx G), <- list_to_productions_to_nonterminal by reflexivity. change (Lookup_string G) with (Lookup G); subst. change default_to_nonterminal with to_nonterminal. rewrite to_of_nonterminal by (apply initial_nonterminals_correct, Hsub; assumption). apply fold_productions'_correct. { apply sub_nonterminals_listT_remove_2; assumption. } { apply IH. { apply sub_nonterminals_listT_remove_2; assumption. } { apply (fun n m => proj2 (Nat.succ_le_mono n m)). etransitivity; [ | exact Hlen ]. apply (remove_nonterminal_dec valid0 (of_nonterminal nt) Hvalid). } } } { apply Pnt_redundant; subst; 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