# Library Coq.Lists.ListSet

``` ```
 A Library for finite sets, implemented as lists A Library with similar interface will soon be available under the name TreeSet in the theories/Trees directory
``` ```
 PolyList is loaded, but not exported. This allow to "hide" the definitions, functions and theorems of PolyList and to see only the ones of ListSet
``` Require Import List. Set Implicit Arguments. Section first_definitions.    Variable A : Set.    Hypothesis Aeq_dec : forall x y:A, {x = y} + {x <> y}.   Definition set := list A.   Definition empty_set : set := nil.   Fixpoint set_add (a:A) (x:set) {struct x} : set :=     match x with     | nil => a :: nil     | a1 :: x1 =>         match Aeq_dec a a1 with         | left _ => a1 :: x1         | right _ => a1 :: set_add a x1         end     end.   Fixpoint set_mem (a:A) (x:set) {struct x} : bool :=     match x with     | nil => false     | a1 :: x1 =>         match Aeq_dec a a1 with         | left _ => true         | right _ => set_mem a x1         end     end.   ```
 If `a` belongs to `x`, removes `a` from `x`. If not, does nothing
```   Fixpoint set_remove (a:A) (x:set) {struct x} : set :=     match x with     | nil => empty_set     | a1 :: x1 =>         match Aeq_dec a a1 with         | left _ => x1         | right _ => a1 :: set_remove a x1         end     end.   Fixpoint set_inter (x:set) : set -> set :=     match x with     | nil => fun y => nil     | a1 :: x1 =>         fun y =>           if set_mem a1 y then a1 :: set_inter x1 y else set_inter x1 y     end.   Fixpoint set_union (x y:set) {struct y} : set :=     match y with     | nil => x     | a1 :: y1 => set_add a1 (set_union x y1)     end.          ```
 returns the set of all els of `x` that does not belong to `y`
```   Fixpoint set_diff (x y:set) {struct x} : set :=     match x with     | nil => nil     | a1 :: x1 =>         if set_mem a1 y then set_diff x1 y else set_add a1 (set_diff x1 y)     end.       Definition set_In : A -> set -> Prop := In (A:=A).   Lemma set_In_dec : forall (a:A) (x:set), {set_In a x} + {~ set_In a x}.   Proof.     unfold set_In in |- *.     simple induction x.     auto.     intros a0 x0 Ha0. case (Aeq_dec a a0); intro eq.     rewrite eq; simpl in |- *; auto with datatypes.     elim Ha0.     auto with datatypes.     right; simpl in |- *; unfold not in |- *; intros [Hc1| Hc2];      auto with datatypes.   Qed.   Lemma set_mem_ind :    forall (B:Set) (P:B -> Prop) (y z:B) (a:A) (x:set),      (set_In a x -> P y) -> P z -> P (if set_mem a x then y else z).   Proof.     simple induction x; simpl in |- *; intros.     assumption.     elim (Aeq_dec a a0); auto with datatypes.   Qed.   Lemma set_mem_ind2 :    forall (B:Set) (P:B -> Prop) (y z:B) (a:A) (x:set),      (set_In a x -> P y) ->      (~ set_In a x -> P z) -> P (if set_mem a x then y else z).   Proof.     simple induction x; simpl in |- *; intros.     apply H0; red in |- *; trivial.     case (Aeq_dec a a0); auto with datatypes.     intro; apply H; intros; auto.     apply H1; red in |- *; intro.     case H3; auto.   Qed.     Lemma set_mem_correct1 :    forall (a:A) (x:set), set_mem a x = true -> set_In a x.   Proof.     simple induction x; simpl in |- *.     discriminate.     intros a0 l; elim (Aeq_dec a a0); auto with datatypes.   Qed.   Lemma set_mem_correct2 :    forall (a:A) (x:set), set_In a x -> set_mem a x = true.   Proof.     simple induction x; simpl in |- *.     intro Ha; elim Ha.     intros a0 l; elim (Aeq_dec a a0); auto with datatypes.     intros H1 H2 [H3| H4].     absurd (a0 = a); auto with datatypes.     auto with datatypes.   Qed.   Lemma set_mem_complete1 :    forall (a:A) (x:set), set_mem a x = false -> ~ set_In a x.   Proof.     simple induction x; simpl in |- *.     tauto.     intros a0 l; elim (Aeq_dec a a0).     intros; discriminate H0.     unfold not in |- *; intros; elim H1; auto with datatypes.   Qed.   Lemma set_mem_complete2 :    forall (a:A) (x:set), ~ set_In a x -> set_mem a x = false.   Proof.     simple induction x; simpl in |- *.     tauto.     intros a0 l; elim (Aeq_dec a a0).     intros; elim H0; auto with datatypes.     tauto.   Qed.   Lemma set_add_intro1 :    forall (a b:A) (x:set), set_In a x -> set_In a (set_add b x).   Proof.     unfold set_In in |- *; simple induction x; simpl in |- *.     auto with datatypes.     intros a0 l H [Ha0a| Hal].     elim (Aeq_dec b a0); left; assumption.     elim (Aeq_dec b a0); right; [ assumption | auto with datatypes ].   Qed.   Lemma set_add_intro2 :    forall (a b:A) (x:set), a = b -> set_In a (set_add b x).   Proof.     unfold set_In in |- *; simple induction x; simpl in |- *.     auto with datatypes.     intros a0 l H Hab.     elim (Aeq_dec b a0);      [ rewrite Hab; intro Hba0; rewrite Hba0; simpl in |- *; auto with datatypes | auto with datatypes ].   Qed.    Hint Resolve set_add_intro1 set_add_intro2.   Lemma set_add_intro :    forall (a b:A) (x:set), a = b \/ set_In a x -> set_In a (set_add b x).      Proof.     intros a b x [H1| H2]; auto with datatypes.   Qed.     Lemma set_add_elim :    forall (a b:A) (x:set), set_In a (set_add b x) -> a = b \/ set_In a x.   Proof.     unfold set_In in |- *.     simple induction x.     simpl in |- *; intros [H1| H2]; auto with datatypes.     simpl in |- *; do 3 intro.     elim (Aeq_dec b a0).     simpl in |- *; tauto.     simpl in |- *; intros; elim H0.     trivial with datatypes.     tauto.     tauto.   Qed.   Lemma set_add_elim2 :    forall (a b:A) (x:set), set_In a (set_add b x) -> a <> b -> set_In a x.    intros a b x H; case (set_add_elim _ _ _ H); intros; trivial.    case H1; trivial.    Qed.    Hint Resolve set_add_intro set_add_elim set_add_elim2.   Lemma set_add_not_empty : forall (a:A) (x:set), set_add a x <> empty_set.   Proof.     simple induction x; simpl in |- *.     discriminate.     intros; elim (Aeq_dec a a0); intros; discriminate.   Qed.   Lemma set_union_intro1 :    forall (a:A) (x y:set), set_In a x -> set_In a (set_union x y).   Proof.     simple induction y; simpl in |- *; auto with datatypes.   Qed.   Lemma set_union_intro2 :    forall (a:A) (x y:set), set_In a y -> set_In a (set_union x y).   Proof.     simple induction y; simpl in |- *.     tauto.     intros; elim H0; auto with datatypes.   Qed.    Hint Resolve set_union_intro2 set_union_intro1.   Lemma set_union_intro :    forall (a:A) (x y:set),      set_In a x \/ set_In a y -> set_In a (set_union x y).   Proof.     intros; elim H; auto with datatypes.   Qed.   Lemma set_union_elim :    forall (a:A) (x y:set),      set_In a (set_union x y) -> set_In a x \/ set_In a y.   Proof.     simple induction y; simpl in |- *.     auto with datatypes.     intros.     generalize (set_add_elim _ _ _ H0).     intros [H1| H1].     auto with datatypes.     tauto.   Qed.   Lemma set_union_emptyL :    forall (a:A) (x:set), set_In a (set_union empty_set x) -> set_In a x.     intros a x H; case (set_union_elim _ _ _ H); auto || contradiction.   Qed.   Lemma set_union_emptyR :    forall (a:A) (x:set), set_In a (set_union x empty_set) -> set_In a x.     intros a x H; case (set_union_elim _ _ _ H); auto || contradiction.   Qed.   Lemma set_inter_intro :    forall (a:A) (x y:set),      set_In a x -> set_In a y -> set_In a (set_inter x y).   Proof.     simple induction x.     auto with datatypes.     simpl in |- *; intros a0 l Hrec y [Ha0a| Hal] Hy.     simpl in |- *; rewrite Ha0a.     generalize (set_mem_correct1 a y).     generalize (set_mem_complete1 a y).     elim (set_mem a y); simpl in |- *; intros.     auto with datatypes.     absurd (set_In a y); auto with datatypes.     elim (set_mem a0 y); [ right; auto with datatypes | auto with datatypes ].   Qed.   Lemma set_inter_elim1 :    forall (a:A) (x y:set), set_In a (set_inter x y) -> set_In a x.   Proof.     simple induction x.     auto with datatypes.     simpl in |- *; intros a0 l Hrec y.     generalize (set_mem_correct1 a0 y).     elim (set_mem a0 y); simpl in |- *; intros.     elim H0; eauto with datatypes.     eauto with datatypes.   Qed.   Lemma set_inter_elim2 :    forall (a:A) (x y:set), set_In a (set_inter x y) -> set_In a y.   Proof.     simple induction x.     simpl in |- *; tauto.     simpl in |- *; intros a0 l Hrec y.     generalize (set_mem_correct1 a0 y).     elim (set_mem a0 y); simpl in |- *; intros.     elim H0;      [ intro Hr; rewrite <- Hr; eauto with datatypes | eauto with datatypes ].     eauto with datatypes.   Qed.    Hint Resolve set_inter_elim1 set_inter_elim2.   Lemma set_inter_elim :    forall (a:A) (x y:set),      set_In a (set_inter x y) -> set_In a x /\ set_In a y.   Proof.     eauto with datatypes.   Qed.   Lemma set_diff_intro :    forall (a:A) (x y:set),      set_In a x -> ~ set_In a y -> set_In a (set_diff x y).   Proof.     simple induction x.     simpl in |- *; tauto.     simpl in |- *; intros a0 l Hrec y [Ha0a| Hal] Hay.     rewrite Ha0a; generalize (set_mem_complete2 _ _ Hay).     elim (set_mem a y);      [ intro Habs; discriminate Habs | auto with datatypes ].     elim (set_mem a0 y); auto with datatypes.   Qed.   Lemma set_diff_elim1 :    forall (a:A) (x y:set), set_In a (set_diff x y) -> set_In a x.   Proof.     simple induction x.     simpl in |- *; tauto.     simpl in |- *; intros a0 l Hrec y; elim (set_mem a0 y).     eauto with datatypes.     intro; generalize (set_add_elim _ _ _ H).     intros [H1| H2]; eauto with datatypes.   Qed.   Lemma set_diff_elim2 :    forall (a:A) (x y:set), set_In a (set_diff x y) -> ~ set_In a y.   intros a x y; elim x; simpl in |- *.   intros; contradiction.   intros a0 l Hrec.   apply set_mem_ind2; auto.   intros H1 H2; case (set_add_elim _ _ _ H2); intros; auto.   rewrite H; trivial.   Qed.   Lemma set_diff_trivial : forall (a:A) (x:set), ~ set_In a (set_diff x x).   red in |- *; intros a x H.   apply (set_diff_elim2 _ _ _ H).   apply (set_diff_elim1 _ _ _ H).   Qed. Hint Resolve set_diff_intro set_diff_trivial. End first_definitions. Section other_definitions.    Variables A B : Set.   Definition set_prod : set A -> set B -> set (A * B) :=     list_prod (A:=A) (B:=B). ```
 `B^A`, set of applications from `A` to `B`
```   Definition set_power : set A -> set B -> set (set (A * B)) :=     list_power (A:=A) (B:=B).   Definition set_map : (A -> B) -> set A -> set B := map (A:=A) (B:=B).   Definition set_fold_left : (B -> A -> B) -> set A -> B -> B :=     fold_left (A:=B) (B:=A).   Definition set_fold_right (f:A -> B -> B) (x:set A)     (b:B) : B := fold_right f b x.   End other_definitions. Unset Implicit Arguments.```
Index