proposition: Lemma revmap_fold_comp_generalized : forall {A B} (f: A -> B) (seq: list A) base, Monad.equiv (fold_left (fun cacc elem => (acc <- cacc; ret (f elem :: acc))%comp) seq base) ( b <- base; ret ((@revmap A B f seq) ++ b)).
proof: Proof. intros; etransitivity. 2: apply Monad.computes_under_bind; intros; rewrite <- revmap_fold_generalized; apply SetoidMorphisms.equiv_refl. generalize dependent base; induction seq; simpl; [ | setoid_rewrite IHseq ]; split; intros; computes_to_inv; subst; eauto using BindComputes. Qed.
imports: CertifiedExtraction.Extraction.Internal CertifiedExtraction.Extraction.External.Core CertifiedExtraction.Extraction.External.Loops CertifiedExtraction.Extraction.External.GenericADTMethods CertifiedExtraction.Extraction.External.FacadeADTs