proposition: Lemma strict_subset_set_diff : forall s1 s2 s2', subset s2 s2' -> (exists e, mem e s1 /\ mem e s2' /\ ~mem e s2) -> cardinal (set_diff s1 s2') < cardinal (set_diff s1 s2).
proof: Proof. unfold set_diff, filter, cardinal; simpl; intros [s1 prf]; induction s1 as [ | a1 s1]; intros s2 s2' s2_in_s2' [e [e_mem_s1 [e_mem_s2' e_not_mem_s2]]]; simpl. contradiction. assert (prf1 := without_red_remove a1 nil s1 prf); simpl in prf1. generalize (eq_bool_ok e a1); case_eq (eq_bool e a1). intros e_eq_a1 e_eq_a1'. assert (a1_mem_s2' : mem_bool EDS1.eq_bool a1 (support s2') = true). generalize (mem_bool_ok _ _ eq_bool_ok a1 (support s2')). case (mem_bool EDS1.eq_bool a1 (support s2')). intros _; apply eq_refl. intro a1_not_mem_s2'; apply False_rect; apply a1_not_mem_s2'. apply (mem_eq_mem EDS1.eq_proof e _ (support s2') e_eq_a1' e_mem_s2'). rewrite a1_mem_s2'; simpl. assert (a1_not_mem_s2 : negb (mem_bool EDS1.eq_bool a1 (support s2)) = true). rewrite <- (not_mem_compat s2 e_eq_a1'). generalize (mem_bool_ok _ _ eq_bool_ok e (support s2)). case (mem_bool EDS1.eq_bool e (support s2)). intro e_mem_s2; apply False_rect; apply e_not_mem_s2; assumption. intros _; apply eq_refl. rewrite a1_not_mem_s2. simpl; apply le_n_S. apply (subset_set_diff (mk_set prf1) s2_in_s2'). intros e_diff_a1 e_diff_a1'. assert (He : exists e : EDS1.A, mem e (mk_set prf1) /\ mem e s2' /\ ~ mem e s2). exists e; repeat split; [idtac | assumption | assumption]. revert e_mem_s1; unfold mem; simpl. intros [e_eq_a1 | e_mem_s1]; [apply False_rect; apply e_diff_a1' | idtac]; assumption. assert (H := IHs1 prf1 _ _ s2_in_s2' He). simpl in H. set (l := filter_aux (fun e : EDS1.A => negb (mem_bool EDS1.eq_bool e (support s2))) s1) in *. set (l' := filter_aux (fun e : EDS1.A => negb (mem_bool EDS1.eq_bool e (support s2'))) s1) in *. generalize (s2_in_s2' a1); unfold mem. generalize (mem_bool_ok _ _ eq_bool_ok a1 (support s2')); case (mem_bool EDS1.eq_bool a1 (support s2')). generalize (mem_bool_ok _ _ eq_bool_ok a1 (support s2)); case (mem_bool EDS1.eq_bool a1 (support s2)). intros _ _ _; assumption. intros _ _ _; simpl; apply le_S; assumption. generalize (mem_bool_ok _ _ eq_bool_ok a1 (support s2)); case (mem_bool EDS1.eq_bool a1 (support s2)). intros a1_in_s2 a1_not_in_s2' Sub; apply False_rect. apply a1_not_in_s2'; apply Sub; apply a1_in_s2. intros _ _ _; simpl; apply le_n_S; assumption. Qed.
imports: Coq(Relations List Setoid Arith FunInd) CoLoR(decidable_set more_list list_permut)