proposition: Lemma FirstStep_splits (H : forall r_o d d0 d1, refine (x0 <- opt2.fold_right (fun x else_case => If pre_test r_o d d0 d1 x Then pre_test_true r_o d d0 d1 x Else else_case) (ret nil) (opt.expanded_fallback_list_body G'); ret (r_o, x0)) (pre_retv r_o d d0 d1)) res (Hres : refineADT (opt_rindexed_spec_gen pre_retv) (ComputationalADT.LiftcADT res)) : FullySharpened (@string_spec G' G' eq_refl HSLM HSL).
proof: Proof. eexists. eapply transitivityT; [ | exact Hres ]. eapply transitivityT; [ apply (@FirstStep _ _ _ _) | ]. cbv [opt_rindexed_spec opt_rindexed_spec_gen]. hone method "splits". 2:apply reflexivityT. { setoid_rewrite General.refineEquiv_pick_eq'. simplify with monad laws. simpl; subst_body; subst. move H at bottom. cbv beta in H. apply H. } Defined.
imports: Coq.Strings.String Fiat.Common.List.ListFacts Fiat.ADTNotation.BuildADT Fiat.ADTNotation.BuildADTSig Fiat.ADT.ComputationalADT Fiat.ADTRefinement Fiat.ADTRefinement.BuildADTRefinements.HoneRepresentation Fiat.Parsers.ParserADTSpecification Fiat.Parsers.Refinement.IndexedAndAtMostOneNonTerminalReflective Fiat.Parsers.StringLike.Core Fiat.Parsers.ContextFreeGrammar.Precompute Fiat.Parsers.BaseTypes Fiat.Parsers.Splitters.RDPList Fiat.Parsers.ContextFreeGrammar.Carriers Fiat.Parsers.ContextFreeGrammar.PreNotations