proposition: Lemma parse_nonterminal_reified_opt_interp_precorrect : rinterp_parse (parse_nonterminal_reified G nt _) = proj1_sig (parse_nonterminal_preopt Hvalid str nt).
proof: Proof. clear splitdata_correct HSLP. cbv [rinterp_parse parse_nonterminal_reified]. change @opt.interp_has_parse_term with @interp_has_parse_term. cbv [interp_has_parse_term]. cbv [proj1_sig parse_nonterminal_preopt]. match goal with | [ |- ?f ?x = ?g ?y ] => replace x with y end. Focus 2. { unfold rdp_list_of_nonterminal, Carriers.default_of_nonterminal. cbv [pregrammar_productions pregrammar'_of_pregrammar]. rewrite !List.map_length, !List.map_map; simpl. reflexivity. } Unfocus. unfold interp_Term; simpl; fold @interp_Term; rewrite <- !interp_Term_syntactify_rproductions; reflexivity. Qed.
imports: Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Parsers.ContextFreeGrammar.ValidReflective Fiat.Parsers.BaseTypes Fiat.Parsers.BooleanRecognizerOptimized Fiat.Parsers.Reflective.Syntax Fiat.Parsers.Reflective.ParserSyntax Fiat.Parsers.Reflective.Semantics Fiat.Parsers.Reflective.ParserSemantics Fiat.Parsers.Reflective.SemanticsOptimized Fiat.Parsers.Reflective.ParserSemanticsOptimized Fiat.Parsers.Reflective.Morphisms Fiat.Parsers.Reflective.ParserReify Fiat.Parsers.Splitters.RDPList Fiat.Common