``` ```

# Sets built with lists

``` Set Implicit Arguments. Require Import Relations. Require Import List. Require Import more_list. Require Import list_permut. Require Import Arith. Module Type S. Declare Module Import EDS : decidable_set.ES. Declare Module Import LP : list_permut.S with Module EDS := EDS. Fixpoint without_red (l : list A) {struct l} : Prop :=   match l with   | nil => True   | e :: le => if (mem_dec e le : sumbool _ _) then False else without_red le   end. Record t : Set :=   mk_set   {      support : list A;      is_a_set : without_red support   }. Definition mem e s := mem e s.(support). Axiom mem_dec : forall e s, {mem e s}+{~mem e s}. Definition cardinal s := List.length s.(support). Definition subset s1 s2 : Prop :=   forall e, mem e s1 -> mem e s2. Axiom cardinal_subset :   forall s1 s2, subset s1 s2 -> cardinal s1 <= cardinal s2. End S. ```

## Definition of sets using lists.

``` Module Make (EDS1 : decidable_set.ES) <: S with Module EDS:= EDS1. Module Import EDS := EDS1. Module Import LP := list_permut.Make (EDS). Function without_red (l : list A) {struct l} : Prop :=   match l with   | nil => True   | e :: le => if (mem_dec e le : sumbool _ _) then False else without_red le   end. Lemma without_red_remove :   forall e l1 l2, without_red (l1 ++ e :: l2) -> without_red (l1 ++ l2). Proof. intros e l1; generalize e; clear e; induction l1 as [ | e1 l1]; intros e l2; simpl. destruct (mem_dec e l2); trivial; contradiction. destruct (mem_dec e1 (l1 ++ e :: l2)) as [ | not_in_e1]. contradiction. destruct (mem_dec e1 (l1 ++ l2)) as [ in_e1 | _]. intros _; apply not_in_e1; apply mem_insert; trivial. intro; apply (IHl1 e l2); trivial. Qed. Lemma without_red_not_in :   forall e l1 l2, without_red (l1 ++ e :: l2) -> ~mem e (l1 ++ l2). Proof. intros e l1; induction l1 as [ | e1 l1]; simpl. intros l2; destruct (mem_dec e l2); trivial; contradiction. intros l2; destruct (mem_dec e1 (l1 ++ e :: l2)) as [ | e1_not_in_l1_e_l2]. contradiction. intros wr [e1_eq_e | e_in_l1_l2]. apply e1_not_in_l1_e_l2; subst; setoid_rewrite <- mem_or_app; right; left; trivial. symmetry; trivial. apply (IHl1 l2 wr e_in_l1_l2). Qed. Lemma add_prf :   forall e l1 l2, without_red (l1 ++ l2) -> ~mem e (l1 ++ l2) ->   without_red (l1 ++ e :: l2). Proof. intros e l1; generalize e; clear e; induction l1 as [ | e1 l1]; intros e l2 wr12 e_not_in_l1_l2. simpl; destruct (mem_dec e l2) as [e_in_l2 | _]; trivial. apply e_not_in_l1_l2; trivial. simpl; destruct (mem_dec e1 (l1 ++ e :: l2)) as [e1_in_l1_e_l2 | _ ]. absurd (mem e1 (l1 ++ l2)). apply (without_red_not_in e1 nil (l1 ++ l2)); trivial. apply diff_mem_remove with e; trivial; intro; apply e_not_in_l1_l2; subst; left; symmetry; trivial. apply IHl1. apply (without_red_remove e1 nil (l1 ++ l2)); trivial. intro; apply e_not_in_l1_l2; right; trivial. Qed. Lemma without_red_permut :  forall l1 l2, without_red l1 -> LP.permut l1 l2 -> without_red l2. Proof. intro l1; functional induction (without_red l1) as [ | | H1 e1 l1 H2 e1_not_in_l1 _H IH]. intros l2 _ P; rewrite (permut_nil (permut_sym P)); simpl; trivial. contradiction. intros l2 wr1 P; assert (e1_in_l2 := cons_permut_mem (equiv_refl _ _ eq_proof e1) P). destruct (mem_split_set _ _ e1_in_l2) as [e1' [l2' [l2'' [e1_eq_e1' H]]]]. simpl in e1_eq_e1'; simpl in H; subst l2. setoid_rewrite <- permut_cons_inside in P; trivial. apply add_prf. apply IH; trivial. intro H; simpl in wr1; apply e1_not_in_l1. setoid_rewrite e1_eq_e1'; setoid_rewrite P; trivial. Qed. Function remove_red (l : list A) : list A :=   match l with   | nil => nil   | e :: le =>            if (mem_dec e le : sumbool _ _)            then remove_red le            else e :: (remove_red le)    end. Lemma included_remove_red : forall e l, mem e (remove_red l) -> mem e l. Proof. intros x l; functional induction (remove_red l)    as [ | H1 e l H2 e_in_l _H IH | H1 e l H2 e_not_in_l _H IH ]. trivial. intro; right; apply IH; trivial. intros [x_eq_e | H]; [left | right; apply IH]; trivial. Qed. Lemma remove_red_included : forall e l, mem e l -> mem e (remove_red l). Proof. intros x l x_in_l; functional induction (remove_red l)    as [ | H1 e l H2 e_in_l _H IH | H1 e l H2 e_not_in_l _H IH ]. trivial. apply IH; simpl in x_in_l; destruct x_in_l as [x_eq_e | x_in_l]; trivial. setoid_rewrite x_eq_e; trivial. simpl in x_in_l; destruct x_in_l as [x_eq_e | x_in_l]; [left | right; apply IH]; trivial. Qed. Lemma without_red_remove_red : forall l, without_red (remove_red l). Proof. intros l; functional induction (remove_red l)    as [ | H1 e l H2 e_in_l _H IH | H1 e l H2 e_not_in_l _H IH ]; simpl; trivial. destruct (mem_dec e (remove_red l)) as [e_in_rl | e_not_in_rl]. apply e_not_in_l; apply included_remove_red; trivial. trivial. Qed. Record t : Set :=   mk_set   {      support : list A;      is_a_set : without_red support   }. Definition mem e s := mem e s.(support). Lemma mem_dec : forall e s, {mem e s}+{~mem e s}. Proof. intros e s; unfold mem; apply (LP.mem_dec). Defined. Lemma eq_mem_mem :   forall s e e', eq_A e e' -> mem e s -> mem e' s. Proof. intros s e e' e_eq_e' e_mem_s; destruct (mem_split_set _ _ e_mem_s) as [a [l' [l'' [e_eq_a H]]]]. unfold mem; rewrite H. rewrite <- LP.mem_or_app; right; left. transitivity e; trivial. symmetry; trivial. Qed. Definition add e s :=   match mem_dec e s with   | left _ => s   | right R => mk_set (e :: s.(support)) (add_prf e nil s.(support) s.(is_a_set) R)   end. Lemma add_1 : forall e s, mem e (add e s). Proof. intros e s; unfold mem, add; simpl; destruct (mem_dec e s) as [e_in_s | e_not_in_s]. trivial. left; reflexivity. Qed. Lemma add_2 : forall e e' s, mem e s -> mem e (add e' s). Proof. intros e e' s; unfold mem, add; simpl; destruct (mem_dec e' s) as [e'_in_s | e'_not_in_s]. trivial. right; trivial. Qed. Lemma add_12 : forall e e' s, mem e (add e' s) -> eq_A e e' \/ mem e s. Proof. intros e e' s; unfold mem, add; simpl; destruct (mem_dec e' s) as [e'_in_s | e'_not_in_s]. right; trivial. intros [e'_eq_e | e_in_s]; [left | right]; trivial. Qed. Function filter_aux (P : A -> Prop) (P_dec : forall e : A, {P e}+{~ P e})    (l : list A) {struct l} : list A :=   match l with   | nil => nil   | e :: le =>            if (P_dec e : sumbool _ _)            then e :: (filter_aux P P_dec le)            else filter_aux P P_dec le    end. Lemma included_filter_aux :   forall P P_dec e l,   LP.mem e (filter_aux P P_dec l) -> LP.mem e l. Proof. intros P P_dec x l; functional induction (filter_aux P P_dec l)     as [ | H1 e l H2 P_e _H IH | H1 e l H2 not_P_e _H IH ]. trivial. intros [x_eq_e | x_in_fl]; [left | right; apply IH]; trivial. intros x_in_fl; right; apply IH; trivial. Qed. Lemma without_red_filter_aux :   forall P P_dec l, without_red l -> without_red (filter_aux P P_dec l). Proof. intros P P_dec l Wl; functional induction (filter_aux P P_dec l)     as [ | H1 e l H2 P_e _H IH | H1 e l H2 not_P_e _H IH ]. trivial. simpl in *; destruct (LP.mem_dec e l) as [ in_e_l | not_in_e_l]; [ contradiction | destruct (LP.mem_dec e (filter_aux P P_dec l)) as [ in_e_rrle | _]]. absurd (LP.mem e l); [ idtac | apply included_filter_aux with P P_dec]; trivial. apply IH; trivial. simpl in *; destruct (LP.mem_dec e l) as [ in_e_l | not_in_e_l]; [ contradiction | apply IH; trivial]. Qed. Definition filter (P : A -> Prop) P_dec s   (P_compat : forall e e', eq_A e e' -> (P e <-> P e')) :=    mk_set (filter_aux P P_dec s.(support))                (without_red_filter_aux P P_dec _ s.(is_a_set)). Lemma filter_1_list :   forall (P : A -> Prop) P_dec l e   (P_compat : forall e e', eq_A e e' -> (P e <-> P e')),   LP.mem e l -> P e -> LP.mem e (filter_aux P P_dec l). Proof. intros P P_dec l e P_compat e_in_l P_e; functional induction (filter_aux P P_dec l)     as [ | H1 e' l H2 P_e' _H IH | H1 e' l H2 not_P_e _H IH ]. contradiction. destruct e_in_l as [e_eq_e' | e_in_l]; [left | right; apply IH]; trivial. destruct e_in_l as [e_eq_e' | e_in_l]. absurd (P e'); trivial. setoid_rewrite <- (P_compat e e'); trivial. apply IH; trivial. Qed. Lemma filter_1 :   forall (P : A -> Prop) P_dec s P_compat e,   mem e s -> P e -> mem e (filter P P_dec s P_compat). Proof. unfold mem, support; intros P P_dec [l wr] P_compat e e_in_s P_e; simpl; apply filter_1_list; trivial. Qed. Lemma filter_2_list :  forall (P : A -> Prop) P_dec l e   (P_compat : forall e e', eq_A e e' -> (P e <-> P e')),   LP.mem e (filter_aux P P_dec l) -> LP.mem e l /\ P e. Proof. intros P P_dec l e P_compat H; functional induction (filter_aux P P_dec l)     as [ | H1 e' l H2 P_e' _H IH | H1 e' l H2 not_P_e _H IH ]. contradiction. destruct H as [e_eq_e' | e_in_fl]; split. left; trivial. setoid_rewrite (P_compat e e'); trivial. right; apply (proj1 (IH e_in_fl)). apply (proj2 (IH e_in_fl)). split; [right | idtac]; destruct (IH H); trivial. Qed. Lemma filter_2 :  forall (P : A -> Prop) P_dec s P_compat e,   mem e (filter P P_dec s P_compat) -> mem e s /\ P e. Proof. unfold mem, support; intros P P_dec [l wr] e E e_in_l_and_P_e. apply filter_2_list with P_dec; trivial. Qed. Lemma without_red_nil : without_red nil. Proof. simpl; trivial. Qed. Definition empty : t :=   mk_set nil without_red_nil. Lemma without_red_singleton : forall e : A, without_red (e :: nil). Proof. intro e; simpl; generalize (LP.mem_dec e nil). unfold EDS.A, A in *. destruct (LP.mem_dec e (@nil EDS1.A)); simpl; trivial. Qed. Definition singleton (e : A) : t :=   mk_set (e :: nil) (without_red_singleton e). Definition make_set (l : list A) : t :=   mk_set (remove_red l) (without_red_remove_red l). Function add_without_red (acc l : list A) {struct l} : list A :=   match l with   | nil => acc   | e :: le =>      if (LP.mem_dec e acc : sumbool _ _)      then add_without_red acc le      else add_without_red (e :: acc) le   end. Lemma without_red_add_without_red :   forall l1 l2, without_red l1 -> without_red (add_without_red l1 l2). Proof. intros l1 l2 Wl1; functional induction (add_without_red l1 l2)     as [ | l1 H1 e l2 H2 e_in_l1 _H IH | l1 H1 e l2 H2 e_not_in_l1 _H IH ]. trivial. apply IH; trivial. apply IH; simpl; rewrite _H; trivial. Qed. Definition union s1 s2 :=   mk_set (add_without_red s1.(support) s2.(support))                (without_red_add_without_red s1.(support) s2.(support) s1.(is_a_set)). Lemma union_1_aux : forall (l1 l2 : list A) (e : A), LP.mem e l1 -> LP.mem e (add_without_red l1 l2). Proof. intros l1 l2; generalize l1; clear l1; induction l2 as [ | e2 l2]. intros; trivial. intros l1 e e_in_l1; simpl; case (LP.mem_dec e2 l1); intro; apply IHl2; trivial. right; trivial. Qed. Lemma union_1 : forall s1 s2 e, mem e s1 -> mem e (union s1 s2). Proof. unfold mem; intros [l1 wr1] [l2 wr2] e; simpl; apply union_1_aux. Qed. Lemma union_2_aux : forall (l1 l2 : list A) (e : A), LP.mem e l2 -> LP.mem e (add_without_red l1 l2). Proof. intros l1 l2 e e_in_l2; functional induction (add_without_red l1 l2)     as [ | l1 H1 e2 l2 H2 e2_in_l1 _H IH | l1 H1 e2 l2 H2 e2_not_in_l1 _H IH ]. contradiction. destruct e_in_l2 as [e_eq_e2 | e_in_l2]. setoid_rewrite e_eq_e2; apply union_1_aux; trivial. apply IH; trivial. destruct e_in_l2 as [e_eq_e2 | e_in_l2]. setoid_rewrite e_eq_e2; apply union_1_aux; left; reflexivity. apply IH; trivial. Qed. Lemma union_2 : forall s1 s2 e, mem e s2 -> mem e (union s1 s2). Proof. unfold mem; intros [l1 wr1] [l2 wr2] e; simpl; apply union_2_aux. Qed. Lemma union_12_aux : forall (l1 l2 : list A) (e : A), LP.mem e (add_without_red l1 l2) ->        LP.mem e l1 \/ LP.mem e l2. Proof. intros l1 l2 e e_in_l1_l2; functional induction (add_without_red l1 l2)     as [ | l1 H1 e2 l2 H2 e2_in_l1 _H IH | l1 H1 e2 l2 H2 e2_not_in_l1 _H IH ]. left; trivial. destruct (IH e_in_l1_l2) as [e_in_l1 | e_in_l2]; [left | do 2 right]; trivial. destruct (IH e_in_l1_l2) as [[e_eq_e2 | e_in_l1] | e_in_l2]; [ right; left | left | do 2 right]; trivial. Qed. Lemma union_12 :   forall s1 s2 e, mem e (union s1 s2) -> mem e s1 \/ mem e s2. Proof. unfold mem; intros [l1 wr1] [l2 wr2] e; simpl; apply union_12_aux. Qed. Function remove_not_common (acc l1 l2 : list A) {struct l2} : list A :=   match l2 with   | nil => acc   | e :: l =>       if (LP.mem_dec e l1 : sumbool _ _)       then remove_not_common (e :: acc) l1 l       else remove_not_common acc l1 l   end. Lemma without_red_remove_not_common_aux :   forall acc l1 l2, (forall e, LP.mem e acc /\ LP.mem e l2 -> False) ->                            without_red acc -> without_red l1 -> without_red l2 ->                            without_red (remove_not_common acc l1 l2). Proof. intros acc l1 l2 H Wa Wl1 Wl2; functional induction (remove_not_common acc l1 l2)     as [ | acc l1 H1 e l2 H2 e_in_l1 _H IH | acc l1 H1 e l2 H2 e_not_in_l1 _H IH]. trivial. simpl in Wl2; destruct (LP.mem_dec e l2) as [ _ | e_not_in_l2]; [contradiction | idtac]; apply IH; trivial. intros a [[a_eq_e | a_in_acc] a_in_l2]; [apply e_not_in_l2; subst | apply (H a); split; [idtac | right]]; trivial. setoid_rewrite <- a_eq_e; trivial. simpl; destruct (LP.mem_dec e acc); [apply (H e); split; [idtac | left] | idtac ]; trivial. reflexivity. simpl in Wl2; destruct (LP.mem_dec e l2) as [ _ | e_not_in_l2]; [contradiction | idtac]; apply IH; trivial. intros a [ a_in_acc a_in_l2]; apply (H a); split; [idtac | right]; trivial. Qed. Lemma without_red_remove_not_common :   forall l1 l2, without_red l1 -> without_red l2 ->                     without_red (remove_not_common nil l1 l2). Proof. intros l1 l2 wr1 wr2; apply without_red_remove_not_common_aux; trivial. intros e [ H _ ]; contradiction. simpl; trivial. Qed. Definition inter s1 s2 :=   mk_set (remove_not_common nil s1.(support) s2.(support))                (without_red_remove_not_common _ _ s1.(is_a_set) s2.(is_a_set)). Lemma inter_1_aux :   forall acc l1 l2 e, LP.mem e (remove_not_common acc l1 l2) ->   LP.mem e acc \/ LP.mem e l1. Proof. intros acc l1 l2 e e_in_acc_l1; functional induction (remove_not_common acc l1 l2)     as [ | acc l1 H1 e2 l2 H2 e2_in_l1 _H IH | acc l1 H1 e2 l2 H2 e2_not_in_l1 _H IH]. left; trivial. destruct (IH e_in_acc_l1) as [[e_eq_e2 | e_in_acc] | e_in_l1]; [ subst; right | left | right ]; trivial. setoid_rewrite e_eq_e2; trivial. apply IH; trivial. Qed. Lemma inter_1 : forall s1 s2 e, mem e (inter s1 s2) -> mem e s1. Proof. intros [l1 wr1] [l2 wr2] e H; simpl. generalize (inter_1_aux nil l1 l2 e H). intros [ H' | H']; trivial; contradiction. Qed. Lemma inter_2_aux :   forall acc l1 l2 e, LP.mem e (remove_not_common acc l1 l2) ->   LP.mem e acc \/ LP.mem e l2. Proof. intros acc l1 l2 e e_in_acc_l2; functional induction (remove_not_common acc l1 l2)     as [ | acc l1 H1 e2 l2 H2 e2_in_l1 _H IH | acc l1 H1 e2 l2 H2 e2_not_in_l1 _H IH]. left; trivial. destruct (IH e_in_acc_l2) as [[e_eq_e2 | e_in_acc] | e_in_l1]; [ subst; right; left | left | right; right ]; trivial. destruct (IH e_in_acc_l2) as [e_in_acc | e_in_l2]; [left | right; right]; trivial. Qed. Lemma inter_2 : forall s1 s2 e, mem e (inter s1 s2) -> mem e s2. Proof. intros [l1 wr1] [l2 wr2] e H; simpl. generalize (inter_2_aux nil l1 l2 e H). intros [ H' | H']; trivial; contradiction. Qed. Lemma inter_12_aux :   forall acc l1 l2 e, LP.mem e l1 -> LP.mem e l2 ->   LP.mem e (remove_not_common acc l1 l2). Proof. assert (H : forall acc l1 l2 e, LP.mem e acc ->                     LP.mem e (remove_not_common acc l1 l2)). intros acc l1 l2 e e_in_acc; functional induction (remove_not_common acc l1 l2)     as [ | acc l1 H1 e2 l2 H2 e2_in_l1 _H IH | acc l1 H1 e2 l2 H2 e2_not_in_l1 _H IH]. trivial. apply IH; right; trivial. apply IH; trivial. intros acc l1 l2 e e_in_l1 e_in_l2; functional induction (remove_not_common acc l1 l2)     as [ | acc l1 H1 e2 l2 H2 e2_in_l1 _H IH | acc l1 H1 e2 l2 H2 e2_not_in_l1 _H IH]. contradiction. destruct e_in_l2 as [e_eq_e2 | e_in_l2]; [subst; apply H; left | apply IH]; trivial. destruct e_in_l2 as [e_eq_e2 | e_in_l2]. absurd (LP.mem e2 l1); trivial. setoid_rewrite <- e_eq_e2; trivial. apply IH; trivial. Qed. Lemma inter_12 :   forall s1 s2 e, mem e s1 -> mem e s2 -> mem e (inter s1 s2). Proof. intros [l1 wr1] [l2 wr2] e e_in_l1 e_in_l2; refine (inter_12_aux nil l1 l2 e _ _); trivial. Qed. Definition subset s1 s2 : Prop :=   forall e, mem e s1 -> mem e s2. Lemma subset_dec : forall s1 s2, {subset s1 s2} + {~ subset s1 s2}. Proof. intros [l1 wr1] [l2 wr2]; unfold subset, mem; simpl; functional induction (without_red l1) as [ | | H1 e1 l1 H2 e1_not_in_l1 _H IH]. left; intros; contradiction. contradiction. destruct (LP.mem_dec e1 l2) as [ e1_in_l2 | e1_not_in_l2 ]. destruct (IH wr1) as [s1_in_s2 | s1_not_in_s2]. left; intros e [e_eq_e1 | e_in_l1]; [subst | apply s1_in_s2]; trivial. setoid_rewrite e_eq_e1; trivial. right; intro H; apply s1_not_in_s2; intros e e_in_l1; apply H; right; trivial. right; intro H; apply e1_not_in_l2; apply H; left; trivial. reflexivity. Qed. Lemma subset_union_1 :   forall s1 s2, subset s1 (union s1 s2). Proof. intros s1 s2 e; apply union_1. Qed. Lemma subset_union_2 :   forall s1 s2, subset s2 (union s1 s2). Proof. intros s1 s2 e; apply union_2. Qed. Lemma subset_inter_1 :   forall s1 s2, subset (inter s1 s2) s1. Proof. intros s1 s2 e; apply inter_1. Qed. Lemma subset_inter_2 :   forall s1 s2, subset (inter s1 s2) s2. Proof. intros s1 s2 e; apply inter_2. Qed. Definition eq_set s1 s2 :=   forall e, mem e s1 <-> mem e s2. Lemma eq_set_dec : forall s1 s2, {eq_set s1 s2} + {~eq_set s1 s2}. Proof. intros s1 s2; destruct (subset_dec s1 s2) as [ s1_incl_s2 | s1_not_incl_s2 ]. destruct (subset_dec s2 s1) as [ s2_incl_s1 | s2_not_incl_s1 ]. left; intro e; intuition. right; intro s1_eq_s2; apply s2_not_incl_s1; intros e e_in_s2; generalize (s1_eq_s2 e); intuition. right; intro s1_eq_s2; apply s1_not_incl_s2; intros e e_in_s1; generalize (s1_eq_s2 e); intuition. Qed. Lemma eq_set_refl : forall s, eq_set s s. Proof. intros s e; split; trivial. Qed. Lemma eq_set_sym :   forall s1 s2, eq_set s1 s2 -> eq_set s2 s1. Proof. intros s1 s2 H e; generalize (H e); intuition. Qed. Lemma eq_set_trans :   forall s1 s2 s3, eq_set s1 s2 -> eq_set s2 s3 -> eq_set s1 s3. Proof. intros s1 s2 s3 s1_eq_s2 s2_eq_s3 e; generalize (s1_eq_s2 e) (s2_eq_s3 e); intuition. Qed. Lemma add_comm :   forall e1 e2 s, eq_set (add e1 (add e2 s)) (add e2 (add e1 s)). Proof. assert (H : forall e1 e2 s, subset (add e1 (add e2 s)) (add e2 (add e1 s))). intros e1 e2 s e; intro H. destruct (add_12 _ _ _ H) as [e_eq_e1 | e_in_e2_s]. unfold mem; setoid_rewrite e_eq_e1; apply add_2; subst; apply add_1. destruct (add_12 _ _ _ e_in_e2_s) as [e_eq_e2 | e_in_s]. unfold mem; setoid_rewrite e_eq_e2; apply add_1. do 2 apply add_2; trivial. intros e1 e2 s; split; apply H. Qed. Lemma union_empty_1 :   forall s, eq_set s (union empty s). Proof. intros s e; generalize (union_12_aux nil (support s) e); simpl. intuition. apply union_2; trivial. Qed. Lemma union_empty_2 :   forall s, eq_set s (union s empty). Proof. intros s e; simpl; intuition. Qed. Lemma union_comm :   forall s1 s2, eq_set (union s1 s2) (union s2 s1). Proof. intros s1 s2 e; generalize (union_12 s1 s2 e) (union_1 s1 s2 e) (union_2 s1 s2 e) (union_12 s2 s1 e) (union_1 s2 s1 e) (union_2 s2 s1 e); intuition. Qed. Lemma union_assoc :   forall s1 s2 s3, eq_set (union s1 (union s2 s3)) (union (union s1 s2) s3). Proof. intros s1 s2 s3 e; generalize (union_12 s1 (union s2 s3) e) (union_1 s1 (union s2 s3) e)  (union_2 s1 (union s2 s3) e) (union_12 s2 s3 e) (union_1 s2 s3 e) (union_2 s2 s3 e) (union_12 (union s1 s2) s3 e) (union_1 (union s1 s2) s3 e)   (union_2 (union s1 s2) s3 e) (union_12 s1 s2 e) (union_1 s1 s2 e) (union_2 s1 s2 e); intuition. Qed. Lemma subset_filter :   forall (P1 P2 : A -> Prop) P1_dec P2_dec s1 s2 P1_compat P2_compat,   subset s1 s2 -> (forall e, P1 e -> P2 e) ->   subset (filter P1 P1_dec s1 P1_compat) (filter P2 P2_dec s2 P2_compat). Proof. intros P1 P2 P1_dec P2_dec s1 s2 P1_compat P2_compat Hs HP e H. apply filter_1. apply (Hs e). apply (proj1 (filter_2 _ _ _ P1_compat _ H)). apply HP. apply (proj2 (filter_2 _ _ _ P1_compat _ H)). Qed. Lemma filter_union :   forall P P_dec s1 s2 P_compat,   eq_set (filter P P_dec (union s1 s2) P_compat)              (union (filter P P_dec s1 P_compat) (filter P P_dec s2 P_compat)). Proof. intros P P_dec [l1 wr1] [l2 wr2] P_compat e; split; unfold mem; simpl. intro H; destruct (filter_2_list _ P_dec _ _ P_compat H) as [H' Pe]; destruct (union_12_aux _ _ _ H'); [ apply union_1_aux | apply union_2_aux] ; apply filter_1_list; trivial. intro H; destruct (union_12_aux _ _ _ H) as [ H' | H']; destruct (filter_2_list _ P_dec _ _ P_compat H') as [H'' Pe]; apply filter_1_list; trivial; [ apply union_1_aux | apply union_2_aux] ; trivial. Qed. Lemma subset_compat_1 :   forall s1 s1' s2, eq_set s1 s1' -> subset s1 s2 -> subset s1' s2. Proof. intros s1 s1' s2 s1_eq_s1' H e e_in_s1'; apply H; generalize (s1_eq_s1' e); intuition. Qed. Lemma subset_compat_2 :   forall s1 s2 s2', eq_set s2 s2' -> subset s1 s2 -> subset s1 s2'. Proof. intros s1 s2 s2' s2_eq_s2' H e e_in_s1; generalize (s2_eq_s2' e) (H e e_in_s1); intuition. Qed. Lemma subset_compat :    forall s1 s1' s2 s2', eq_set s1 s1' -> eq_set s2 s2' ->                                     subset s1 s2 -> subset s1' s2'. Proof. intros s1 s1' s2 s2' s1_eq_s1' s2_eq_s2' H e e_in_s1'; generalize (s1_eq_s1' e) (s2_eq_s2' e) (H e); intuition. Qed. Lemma union_compat_subset_1 :   forall s1 s2 s, subset s1 s2 -> subset (union s1 s) (union s2 s). Proof. intros [l1 wr1] [l2 wr2] [l wr]; unfold subset; simpl; intros H e e_in_ll1. generalize (union_12_aux _ _ _ e_in_ll1); intros [ e_in_l | e_in_l1]; trivial. apply union_1; apply H; trivial. apply union_2; trivial. Qed. Lemma union_compat_subset_2 :   forall s1 s2 s, subset s1 s2 -> subset (union s s1) (union s s2). Proof. intros [l1 wr1] [l2 wr2] [l wr]; unfold subset; simpl; intros H e e_in_ll1. generalize (union_12_aux _ _ _ e_in_ll1); intros [ e_in_l | e_in_l1]; trivial. apply union_1; trivial. apply union_2; apply H; trivial. Qed. Lemma union_compat_eq_set :   forall s1 s1' s2 s2', eq_set s1 s1' -> eq_set s2 s2' ->     eq_set (union s1 s2) (union s1' s2'). Proof. intros s1 s1' s2 s2' s1_eq_s1' s2_eq_s2' e; split; intro H. generalize (union_12 s1 s2 e H); intros [e_in_s1 | e_in_s2]. apply union_1; generalize (s1_eq_s1' e); intuition. apply union_2; generalize (s2_eq_s2' e); intuition. generalize (union_12 s1' s2' e H); intros [e_in_s1' | e_in_s2']. apply union_1; generalize (s1_eq_s1' e); intuition. apply union_2; generalize (s2_eq_s2' e); intuition. Qed. Lemma subset_subset_union :   forall s1 s2 s, subset s1 s -> subset s2 s -> subset (union s1 s2) s. Proof. intros s1 s2 s H1 H2 e H. destruct (union_12 _ _ _ H); [ apply H1 | apply H2]; trivial. Qed. Definition cardinal s := List.length s.(support). Lemma cardinal_subset :   forall s1 s2, subset s1 s2 -> cardinal s1 <= cardinal s2. Proof. intros [l1 wr1] [l2 wr2]; unfold cardinal, subset, mem; simpl in *; generalize l2 wr2; clear l2 wr2; functional induction (without_red l1) as [ | | H1 e1 l1 H2 e1_not_in_l1 _H IH]. auto with arith. contradiction. intros l2 wr2 H. assert (e1_in_l2 : LP.mem e1 l2). apply H; left; reflexivity. destruct (LP.mem_split_set _ _ e1_in_l2) as [e1' [l2' [l2'' [e1_eq_e1' H']]]]; simpl in e1_eq_e1'; simpl in H'; subst l2. rewrite length_add; simpl; apply le_n_S; apply IH. trivial. apply (without_red_remove e1' l2' l2''); trivial. intros e e_in_l1; apply diff_mem_remove with e1'. intro e_eq_e1'; apply e1_not_in_l1; setoid_rewrite e1_eq_e1'; setoid_rewrite <- e_eq_e1'; trivial. apply H; right; trivial. Qed. Lemma cardinal_union_1 :   forall s1 s2, cardinal s1 <= cardinal (union s1 s2). Proof. intros s1 s2; apply cardinal_subset; apply subset_union_1. Qed. Lemma cardinal_union_2 :   forall s1 s2, cardinal s2 <= cardinal (union s1 s2). Proof. intros s1 s2; apply cardinal_subset; apply subset_union_2. Qed. Lemma cardinal_union_inter_12 :   forall s1 s2, cardinal (union s1 s2) + cardinal (inter s1 s2) = cardinal s1 + cardinal s2. Proof. intros [l1 wr1] [l2 wr2]; unfold cardinal, subset, mem; simpl. rewrite (plus_n_O (length l1 + length l2)); replace 0 with (length (A:= A) nil); trivial; generalize (nil (A:=A)). functional induction (add_without_red l1 l2)     as [ | l1 H1 e2 l2 H2 e2_in_l1 _H IH | l1 H1 e2 l2 H2 e2_not_in_l1 _H IH ]; intros l. simpl; rewrite <- plus_n_O; trivial. simpl; destruct (LP.mem_dec e2 l1) as [ e2_in_l1' | e2_not_in_l1]; [idtac | absurd (LP.mem e2 l1); trivial]. rewrite IH; trivial. do 2 rewrite <- plus_assoc; apply (f_equal (fun n => length l1 + n)); simpl; rewrite plus_comm; simpl; rewrite plus_comm; trivial. apply (without_red_remove e2 nil); trivial. assert (wr1' := add_prf e2 nil l1 wr1 e2_not_in_l1). assert (wr2' := without_red_remove e2 nil l2 wr2). assert (H := IH wr1' wr2' l). rewrite (plus_comm (length l1)); simpl; destruct (LP.mem_dec e2 l1) as [ e2_in_l1 | e2_not_in_l1']; [ absurd (LP.mem e2 l1); trivial | rewrite (plus_comm (length l2)); simpl in H; rewrite <- H; apply (f_equal (fun n => length (add_without_red (e2 :: l1) l2) + n))]. assert (e2_not_in_l2 := without_red_not_in e2 nil l2 wr2). clear IH wr2 wr2' H e2_not_in_l1 e2_not_in_l1' _H wr1 wr1'; simpl in e2_not_in_l2; functional induction (remove_not_common l l1 l2)    as [ | l l1 H1 e l2 H2 e_in_l1 _H IH | l l1 H1 e l2 H2 e_not_in_l1 _H IH ]. trivial. rewrite IH. simpl. destruct (LP.mem_dec e (e2 :: l1)) as [ _ | e_not_in_e2_l1]. trivial. absurd (LP.mem e l1); trivial. intros _; apply e_not_in_e2_l1; right; trivial. intros e2_in_l2; apply e2_not_in_l2; right; trivial. rewrite IH. simpl. destruct (LP.mem_dec e (e2 :: l1)) as [ [e2_eq_e | e_in_l1] | e_not_in_e2_l1]. absurd (EDS.eq_A e e2); trivial. intros _; apply e2_not_in_l2; left; symmetry ; trivial. absurd (LP.mem e l1); trivial. trivial. intros e2_in_l2; apply e2_not_in_l2; right; trivial. Qed. Lemma cardinal_union:   forall s1 s2, cardinal (union s1 s2) = cardinal s1 + cardinal s2 - cardinal (inter s1 s2). Proof. intros s1 s2; assert (H := cardinal_union_inter_12 s1 s2). apply plus_minus; apply sym_eq; rewrite plus_comm; trivial. Qed. Lemma cardinal_eq_set : forall s1 s2, eq_set s1 s2 -> cardinal s1 = cardinal s2. Proof. intros s1 s2 s1_eq_s2; apply le_antisym; apply cardinal_subset; intros e e_in_si; generalize (s1_eq_s2 e); intuition. Qed. Lemma subset_cardinal_not_eq_not_eq_set :  forall s1 s2 e, subset s1 s2 -> ~mem e s1 -> mem e s2 ->   cardinal s1 < cardinal s2. Proof. intros [l1 wr1] [l2 wr2]; unfold cardinal, subset, mem; simpl; generalize l2 wr2; clear l2 wr2; functional induction (without_red l1)    as [ | | H1 e1 l1 H2 e1_not_in_l1 _H IH]. intros l2 _ e _ _ e_in_l2; destruct l2 as [ | e2 l2]; [contradiction | simpl; auto with arith]. contradiction. intros l2 wr2 e H e_not_in_e1_l1 e_in_l2. assert (e1_in_l2 : LP.mem e1 l2). apply H; left; reflexivity. destruct (LP.mem_split_set _ _ e1_in_l2) as [e1' [l2' [l2'' [e1_eq_e1' H']]]]; simpl in e1_eq_e1'; simpl in H'; subst l2. rewrite length_add; simpl; apply lt_n_S; refine (IH wr1 (l2' ++ l2'') _ e _ _ _); trivial. apply (without_red_remove e1'); trivial. intros a a_in_l1; apply diff_mem_remove with e1'. intro a_eq_e1'; absurd (LP.mem e1 l1); trivial. setoid_rewrite e1_eq_e1'; setoid_rewrite <- a_eq_e1'; trivial. apply H; right; trivial. intro; apply e_not_in_e1_l1; right; trivial. apply diff_mem_remove with e1'; trivial. intro; apply e_not_in_e1_l1. left; transitivity e1'; trivial; symmetry; trivial. Qed. Lemma eq_set_list_permut_support :   forall s1 s2, eq_set s1 s2 -> permut s1.(support) s2.(support). Proof. intros [l1 wr1] [l2 wr2]; unfold eq_set, mem; simpl; generalize l2 wr2; clear l2 wr2; induction l1 as [ | e1 l1]. intros [ | e2 l2] _ H. auto. assert False. generalize (H e2); simpl; intros [_ Abs]; apply Abs; left; reflexivity. contradiction. intros l2 wr2 H. assert (e1_in_l2 : LP.mem e1 l2). setoid_rewrite <- H; left; reflexivity; trivial. destruct (mem_split_set _ _ e1_in_l2) as [e1' [l2' [l2'' [e1_eq_e1' H']]]]; simpl in e1_eq_e1'; simpl in H'; subst l2. setoid_rewrite <- permut_cons_inside; trivial. apply IHl1; trivial. apply (without_red_remove e1 nil); trivial. apply (without_red_remove e1'); trivial. intros e; split; intro H'. apply diff_mem_remove with e1'. intro e_eq_e1'; apply (without_red_not_in e1 nil l1 wr1). simpl; setoid_rewrite e1_eq_e1'; setoid_rewrite <- e_eq_e1'; trivial. setoid_rewrite <- (H e); right; trivial. apply (@diff_mem_remove nil l1 e1). intro e_eq_e1; apply (without_red_not_in e1' l2' l2'' wr2). setoid_rewrite <- e1_eq_e1'; setoid_rewrite <- e_eq_e1; trivial. setoid_rewrite (H e); apply mem_insert; trivial. Qed. Definition not_mem_dec s : forall e, {~mem e s}+{~~mem e s}. Proof. intros s e; destruct (mem_dec e s) as [e_in_s | e_not_in_s]. right; intro e_not_in_s; apply e_not_in_s; trivial. left; trivial. Defined. Lemma not_mem_eq : forall s e e', eq_A e e' -> (~mem e s <-> ~mem e' s). Proof. intros s e e' e_eq_e'; split. intros e_not_in_s e'_in_s; apply e_not_in_s. apply eq_mem_mem with e'; trivial; symmetry; trivial. intros e'_not_in_s e_in_s; apply e'_not_in_s. apply eq_mem_mem with e; trivial. Qed. Definition set_diff s1 s2 := filter _ (not_mem_dec s2) s1 (not_mem_eq s2). Lemma subset_set_diff :    forall s1 s2 s2', subset s2 s2' -> cardinal (set_diff s1 s2') <= cardinal (set_diff s1 s2). Proof. unfold set_diff, filter, cardinal; simpl; intros [s1 prf]; induction s1 as [ | a1 s1]; intros s2 s2' s2_in_s2'; simpl. auto with arith. destruct (not_mem_dec s2' a1) as [a1_not_in_s2' | a1_in_s2']; destruct (not_mem_dec s2 a1) as [a1_not_in_s2 | a1_in_s2]; simpl. apply le_n_S; refine (IHs1 _ s2 s2' s2_in_s2'). apply (without_red_remove a1 nil s1 prf). assert (a1_mem_s2 : mem a1 s2). destruct (mem_dec a1 s2) as [a1_mem_s2 | a1_not_mem_s2]; trivial. absurd (~mem a1 s2); trivial. absurd (mem a1 s2'); trivial. apply s2_in_s2'; trivial. apply le_S; refine (IHs1 _ s2 s2' s2_in_s2'). apply (without_red_remove a1 nil s1 prf). refine (IHs1 _ s2 s2' s2_in_s2'). apply (without_red_remove a1 nil s1 prf). Qed. 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. 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. destruct (not_mem_dec s2' a1) as [a1_not_in_s2' | a1_in_s2']; destruct (not_mem_dec s2 a1) as [a1_not_in_s2 | a1_in_s2]; simpl. unfold mem in e_mem_s1; simpl in e_mem_s1. destruct (EDS.eq_dec e a1) as [e_eq_a1 | e_diff_a1]. absurd (mem a1 s2'); trivial. apply eq_mem_mem with e; trivial. unfold lt; apply le_n_S; refine (IHs1 (without_red_remove a1 nil s1 prf) s2 s2' s2_in_s2' _). exists e; repeat split; trivial. destruct e_mem_s1 as [e_eq_a1 | e_mem_s1]; trivial. absurd (EDS.eq_A e a1); trivial. assert (a1_mem_s2 : mem a1 s2). destruct (mem_dec a1 s2) as [a1_mem_s2 | a1_not_mem_s2]; trivial. absurd (~mem a1 s2); trivial. absurd (mem a1 s2'); trivial. apply s2_in_s2'; trivial. unfold lt; apply le_n_S. assert (H := (subset_set_diff (mk_set s1 (without_red_remove a1 nil s1 prf))) _ _ s2_in_s2'). unfold cardinal, set_diff in H; simpl in H; exact H. refine (IHs1 (without_red_remove a1 nil s1 prf) s2 s2' s2_in_s2' _). exists e; repeat split; trivial. destruct e_mem_s1 as [e_eq_a1 | e_mem_s1]; trivial. absurd (~mem a1 s2); trivial. intro; apply e_not_mem_s2. apply eq_mem_mem with a1; trivial. symmetry; trivial. Qed. End Make. ```