proposition: Theorem inclusion_exclusion (l : list set) : cardinal (list_union l) = sum (map (fun l' => cardinal (list_intersection l') * alternating_sign (1 + length l')) (filter nonempty (sublists l))).
proof: Proof. match goal with |- context [ map ?F ] => set (f := F) end. remember (length l) as n. revert l Heqn. induction n; intros l En. destruct l; [ | discriminate]. unfold list_union, f. simpl. rewrite cardinal_empty. reflexivity. destruct l as [| a l]; [ discriminate | ]. simpl in En. injection En as En. simpl. rewrite cardinal_binary_union. rewrite filter_app, map_app, sum_app. rewrite IHn; auto. pose (la := map (fun b => a ∩ b) l). replace (# (a ∩ list_union l)) with (# (list_union la)); swap 1 2. { apply cardinal_set_eq. unfold la; clear. induction l. simpl. iftac. simpl. rewrite IHl. iftac. } rewrite IHn; swap 1 2. { unfold la. rewrite map_length. auto. } match goal with |- ?a + ?b - ?c = ?b + ?d => cut (a - c = d) end. { intros <-. ring. } unfold la. clear la n En IHn. rewrite filter_map_always; auto. rewrite (sublists_proper l). simpl. unfold f at 2. simpl. ring_simplify. unfold Z.sub. f_equal. rewrite sublists_map. generalize (sublists l); clear l; intros l. replace (filter nonempty (map (map (fun b : set => a ∩ b)) l)) with (map (map (fun b : set => a ∩ b)) (filter nonempty l)); swap 1 2. { induction l as [| b l IHl]. reflexivity. simpl. destruct b; simpl; congruence. } induction l as [| b l IHl]. reflexivity. simpl. destruct b as [| x xs]. simpl. congruence. simpl. rewrite <-IHl. ring_simplify. match goal with |- - ?x - ?b = - ?b + ?y => cut (x = - y) end. { intros ->. ring. } unfold f. clear IHl l f. simpl (alternating_sign _). rewrite map_length. ring_simplify. match goal with |- ?x * ?b = ?b * ?y => cut (x = y) end. { intros ->. ring. } simpl. apply cardinal_set_eq. induction xs as [ | x' xs IHxs ]. simpl. iftac. simpl. rewrite IHxs. cut (fold_right binary_intersection a xs == a ∩ fold_right binary_intersection a xs). { intros ->. iftac. } clear. induction xs. simpl. iftac. simpl. rewrite IHxs. iftac. Qed.
imports: Lists.List ZArith Setoid Coq.Classes.Morphisms Lia