proposition: Corollary refine_foldComp_invariant : forall {A S S'} (P : S -> S' -> Prop) (f : S -> A -> Comp S) (f' : S' -> A -> Comp S') (z : S) (xs : list A), pointwise_relation2 refine (fun st_o a => st_n <- f st_o a; {st_n' | P st_n st_n'}) (fun st_o a => st_o' <- {st_o' | P st_o st_o'}; f' st_o' a) -> refine (st_n <- foldComp f z xs; {st_n' | P st_n st_n'}) (z' <- { z' | P z z'}; foldComp f' z' xs).
proof: Proof. intros. apply refine_bind_pick; intros. setoid_rewrite <- refineEquiv_unit_bind. simplify with monad laws. eapply refine_foldComp_invariant'; eauto; intros. intros ?. rewrite (H _ _). refine pick val z'; trivial. simplify with monad laws. reflexivity. refine pick val st_n'; trivial. reflexivity. Qed.
imports: Fiat.Common Fiat.Computation.Core Fiat.Computation.SetoidMorphisms Fiat.ADT Coq.Lists.List