proposition: Lemma parse_nonterminal_correct' (nt : nonterminal_carrierT) : parse_nt_is_correct str nt (@parse_nonterminal (to_nonterminal nt)) (GenericRecognizer.parse_nonterminal str (to_nonterminal nt)).
proof: Proof. expand_once. repeat eq_t'. destruct (Utils.dec (is_valid_nonterminal initial_nonterminals_data nt)) as [H|H]. { rewrite of_to_nonterminal by assumption. apply parse_nonterminal'_correct. } { destruct (Utils.dec (is_valid_nonterminal initial_nonterminals_data (of_nonterminal (to_nonterminal nt)))) as [H'|H']. { apply initial_nonterminals_correct, initial_nonterminals_correct' in H'. congruence. } { unfold GenericRecognizer.parse_nonterminal'. unfold GenericRecognizer.parse_nonterminal_or_abort. rewrite Fix5_eq by (intros; apply parse_nonterminal_step_ext; assumption). unfold GenericRecognizer.parse_nonterminal_step at 1. simpl. rewrite H', Bool.andb_false_r; simpl. edestruct lt_dec; try omega; simpl. repeat eq_t'. R_etransitivity_eq; [ eapply ret_nt_invalid_is_correct | ]. symmetry. unfold parse_nonterminal'; repeat eq_t'. unfold parse_nonterminal'_substring; repeat eq_t'. congruence. } } Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.Arith.EqNat Coq.Arith.Compare_dec Coq.Arith.Wf_nat Coq.ZArith.ZArith Fiat.Common.List.Operations Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.BaseTypes Fiat.Parsers.GenericBaseTypes Fiat.Parsers.GenericCorrectnessBaseTypes Fiat.Parsers.StringLike.Properties Fiat.Parsers.MinimalParse Fiat.Parsers.CorrectnessBaseTypes Fiat.Parsers.BaseTypesLemmas Fiat.Parsers.ContextFreeGrammar.Properties Fiat.Parsers.WellFoundedParse Fiat.Parsers.MinimalParseOfParse Fiat.Parsers.GenericRecognizer Fiat.Parsers.GenericRecognizerExt Fiat.Common.Wf Fiat.Common.Wf1 Fiat.Common.List.ListFacts Fiat.Common.NatFacts Fiat.Common.UIP Fiat.Common