proposition: Lemma sum_filter : forall f : elt -> bool, Proper (E.eq==>Logic.eq) f -> forall s, (sum (fun x => if f x then 1 else 0) s) = (cardinal (filter f s)).
proof: Proof. unfold sum; intros f Hf. assert (st : Equivalence (@Logic.eq nat)) by (split; congruence). assert (cc : compat_opL (fun x => plus (if f x then 1 else 0))) by (repeat red; intros; rewrite Hf; auto). assert (ct : transposeL (fun x => plus (if f x then 1 else 0))) by (red; intros; lia). intros s;pattern s; apply set_rec. - intros. change elt with E.t. rewrite <- (fold_equal _ _ st _ cc ct 0 _ _ H). apply equal_2 in H; rewrite <- H, <-H0; auto. - intros; rewrite (fold_add _ _ st _ cc ct); auto. generalize (@add_filter_1 f Hf s0 (add x s0) x) (@add_filter_2 f Hf s0 (add x s0) x) . assert (~ In x (filter f s0)). + intro H1; rewrite (mem_1 (filter_1 Hf H1)) in H; discriminate H. + case (f x); simpl; intros. * rewrite (MP.cardinal_2 H1 (H2 (eq_refl true) (MP.Add_add s0 x))); auto. * rewrite <- (MP.Equal_cardinal (H3 (eq_refl false) (MP.Add_add s0 x))); auto. - intros; rewrite fold_empty;auto. rewrite MP.cardinal_1; auto. unfold Empty; intros. rewrite filter_iff; auto; set_iff; tauto. Qed.
imports: MSetProperties Zerob Sumbool Lia DecidableTypeEx