proposition: Lemma simplify_monad_laws_first_step {A B C} (c : Comp A) (f : A -> B * C) v (H : refine (x0 <- c; ret (f x0)) v) : refine (r_o' <- a <- c; ret (f a); r_n' <- { r_n0 | fst r_o' = r_n0 }; ret (r_n', snd r_o')) v.
proof: Proof. simplify with monad laws. setoid_rewrite General.refine_pick_eq'. simplify with monad laws. rewrite <- H. apply General.refine_under_bind; intros. rewrite <- surjective_pairing; reflexivity. Qed.
imports: Coq.NArith.BinNat Fiat.ADTRefinement Fiat.ADTNotation.BuildADT Fiat.ADTRefinement.GeneralBuildADTRefinements Fiat.ADTRefinement.BuildADTRefinements.HoneRepresentation Fiat.ADTNotation.BuildADTSig Fiat.Parsers.Refinement.IndexedAndAtMostOneNonTerminalReflective Fiat.Parsers.Refinement.IndexedAndAtMostOneNonTerminalReflectiveOpt Fiat.Parsers.ParserADTSpecification Fiat.Parsers.Refinement.ReductionTactics Fiat.Parsers.Refinement.PreTactics Fiat.Parsers.ContextFreeGrammar.Notations Fiat.Parsers.StringLike.String Fiat.Parsers.Refinement.DisjointLemmasEarlyDeclarations Fiat.Parsers.ContextFreeGrammar.Equality Fiat.Common.Equality Fiat.Computation.Refinements.General Fiat.Parsers.Refinement.FinishingLemma