proposition: Lemma parse_nonterminal_or_abort_correct (p : nat * nat) (valid : nonterminals_listT) (Hvalid_len : nonterminals_length valid <= snd p) (offset len : nat) (Hlen : len = 0 \/ offset + len <= length str) (pf : len <= fst p) (nt : nonterminal_carrierT) (Hvalid : is_valid_nonterminal initial_nonterminals_data nt) : parse_nt_is_correct (substring offset len str) nt (@parse_nonterminal_or_abort p valid Hvalid_len offset len Hlen pf nt) (GenericRecognizer.parse_nonterminal_or_abort str p valid offset pf nt).
proof: Proof. expand_once. revert valid Hvalid_len offset len Hlen pf nt Hvalid. match goal with | [ |- context[Fix ?Wf _ _ ?p] ] => induction (Wf p) as [?? IH]; intros end. match goal with | [ |- ?R ?x ?y ] => set (x' := x) end. rewrite Fix5_eq by (intros; apply parse_nonterminal_step_ext; eauto with nocore); subst x'. destruct_head prod. R_etransitivity_eq. { eapply parse_nonterminal_step_correct; first [ intros; eapply IH; eassumption | assumption ]. } { match goal with | [ |- bool_of_sum ?x = bool_of_sum ?y ] => destruct x, y; try reflexivity; exfalso; eauto with nocore end. } Unshelve. assumption. assumption. assumption. assumption. assumption. 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