proposition: Theorem compMap_filter : forall (A B : Set)(eqda : EqDec A)(eqdb : EqDec B)(ls : list A)(c : A -> Comp B)(P : A -> bool) x, (forall a, In a ls -> well_formed_comp (c a)) -> evalDist (compMap _ c (filter P ls)) x == evalDist (ps <-$ compMap _ (fun a => b <-$ (c a); ret (a, b)) ls; ret (snd (unzip (filter (fun p => P (fst p)) ps)))) x.
proof: Proof. induction ls; intuition. unfold filter. unfold compMap. comp_simp. simpl. intuition. rewrite filter_cons. case_eq (P a); intuition. unfold compMap. fold compMap. inline_first. comp_skip. comp_simp. eapply eqRat_trans. comp_skip. eapply eqRat_refl. inline_first. comp_skip. comp_simp. dist_compute. unfold compMap. fold compMap. inline_first. comp_irr_r. comp_simp. rewrite IHls. inline_first. comp_skip. comp_simp. dist_compute. intuition. Qed.
imports: FCF.FCF Permutation