proposition: Lemma filter_iff : forall m k e, MapsTo k e (filter f m) <-> MapsTo k e m /\ f k e = true.
proof: Proof. unfold filter. set (f':=fun k e m => if f k e then add k e m else m). intro m. pattern m, (fold f' m (empty _)). apply fold_rec. - intros m' Hm' k e. rewrite empty_mapsto_iff. intuition. elim (Hm' k e); auto. - intros k e acc m1 m2 Hke Hn Hadd IH k' e'. change (Equal m2 (add k e m1)) in Hadd; rewrite Hadd. unfold f'; simpl. case_eq (f k e); intros Hfke; simpl; rewrite !add_mapsto_iff, IH; clear IH; intuition. + rewrite <- Hfke; apply Hf; auto. + destruct (eq_dec k k') as [Hk|Hk]; [left|right]; auto. elim Hn; exists e'; rewrite Hk; auto. + assert (f k e = f k' e') by (apply Hf; auto). congruence. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface