proposition: Lemma cardinal_union_inter_12 : forall s1 s2, cardinal (union s1 s2) + cardinal (inter s1 s2) = cardinal s1 + cardinal s2.
proof: Proof. intro s1; case s1; clear s1; intros l1 wr1. intro s2; case s2; clear s2; intros l2 wr2. revert l1 wr1 l2 wr2; unfold without_red, cardinal; simpl. fix cardinal_union_inter_12 3. intros l1 wr1 l2; case l2; clear l2; simpl. intros _; reflexivity. intros a2 l2; generalize (mem_bool_ok _ _ eq_bool_ok a2 l2); case_eq (mem_bool eq_bool a2 l2). intros _ _ Abs; discriminate. intros a2_not_in_l2_bool a2_not_in_l2 wr2; generalize (mem_bool_ok _ _ eq_bool_ok a2 l1); case (mem_bool eq_bool a2 l1). intro a2_in_l1. rewrite length_remove_not_common; simpl. do 2 rewrite <- plus_n_Sm; rewrite (cardinal_union_inter_12 l1 wr1 l2 wr2); reflexivity. intro a2_not_in_l1. rewrite <- plus_n_Sm. rewrite <- (cardinal_union_inter_12 l1 wr1 l2 wr2). assert (L : forall l1' l1'', length (add_without_red (l1' ++ a2 :: l1'') l2) = S (length (add_without_red (l1' ++ l1'') l2))). clear l1 wr1 a2_not_in_l1 a2_not_in_l2 wr2; revert l2 a2 a2_not_in_l2_bool. fix L 1. intro l2; case l2; clear l2; simpl. intros a2 _ l1' l1''; do 2 rewrite length_app; simpl; rewrite plus_n_Sm; reflexivity. intros a2 l2 a; assert (eq_bool_sym : eq_bool a2 a = eq_bool a a2). generalize (eq_bool_ok a2 a) (eq_bool_ok a a2); case (eq_bool a2 a); case (eq_bool a a2). intros _ _; reflexivity. intros a2_eq_a a_diff_a2; apply False_rect; apply a_diff_a2; symmetry; assumption. intros a2_diff_a a_eq_a2; apply False_rect; apply a2_diff_a; symmetry; assumption. intros _ _; reflexivity. intros a_not_in_l2_bool l1' l1''; revert a_not_in_l2_bool; rewrite (mem_bool_app eq_bool a2 l1' (a :: l1'')). simpl; rewrite eq_bool_sym; case (eq_bool a a2); simpl. intro; discriminate. intro a_not_in_l2_bool; rewrite <- (mem_bool_app eq_bool a2 l1' l1''); case (mem_bool eq_bool a2 (l1' ++ l1'')). apply (L l2 a a_not_in_l2_bool l1' l1''). apply (L l2 a a_not_in_l2_bool (a2 :: l1') l1''). assert (L' := L nil l1); simpl in L'; rewrite L'; simpl; reflexivity. Qed.
imports: Coq(Relations List Setoid Arith FunInd) CoLoR(decidable_set more_list list_permut)