proposition: Lemma ret_fold_fold_ret_lemma : forall {TElem TAcc} (f: TAcc -> TElem -> TAcc) lst (init: TAcc) init_comp, Monad.equiv (ret init) init_comp -> Monad.equiv (ret (fold_left f lst init)) (fold_left (fun (acc: Comp TAcc) x => (a <- acc; ret (f a x))%comp) lst init_comp).
proof: Proof. induction lst; simpl; intros. - trivial. - etransitivity; [ apply IHlst | reflexivity ]. unfold Monad.equiv in *; repeat (cleanup_pure || computes_to_inv || subst). + eapply BindComputes; try rewrite <- H; apply ReturnComputes. + rewrite <- H in *; computes_to_inv; subst; apply ReturnComputes. Qed.
imports: CertifiedExtraction.Extraction.Internal CertifiedExtraction.Extraction.External.Core CertifiedExtraction.Extraction.External.Loops CertifiedExtraction.Extraction.External.GenericADTMethods CertifiedExtraction.Extraction.External.FacadeADTs