``` ```

# Sets over types with decidable equality

(** version 1.0
``` ```
 Usage example for a set of naturals ```Require Esets. Module NatEq <: Esets.EQ. Definition dom := nat. Definition dom_eq_dec := eq_nat_dec. End NatEq. Module NatSet := Esets.MakeSet(NatEq). ```
``` Require Import List Elists. Set Implicit Arguments. ```
 A signature for a data type with decidable equality
``` Module Type EQ.   Parameter dom : Set.   Parameter dom_eq_dec : forall (x y : dom), {x = y} + {x <> y}. End EQ. Module MakeSet (Param : EQ) .   Import Param.   Definition set := list dom. ```
 The empty set
```   Definition empty : set := nil. ```
 Membership
```   Fixpoint In (x: dom) (l:set) {struct l} : bool :=     match l with     | nil => false     | b :: m => if dom_eq_dec x b then                    true                 else In x m     end.   Fixpoint incl (s1 s2 : set) { struct s1} : bool :=     match s1 with       nil => true     | x :: s11 =>         match In x s2 with            true => incl s11 s2          | _ => false         end     end. ```
 Set equality
```   Definition seq (s1 s2: set) : bool :=     match incl s1 s2, incl s2 s1 with       true, true => true     | _, _ => false     end.    Hint Unfold seq. ```
 Add an element to a set
```   Fixpoint add (v: dom) (s : set) { struct s } : set :=     match s with      | nil => v :: nil      | v' :: t => if dom_eq_dec v v' then s else v' :: add v t     end. ```
 Remove an element from a set
```   Fixpoint remove (s : set) (v : dom) {struct s} : set :=     match s with       | nil => nil       | v' :: s' =>         if dom_eq_dec v v'           then s'           else v' :: remove s' v     end. ```
 Set union
```   Fixpoint union (s1 s2 : set) {struct s1} : set :=     match s1 with       | nil => s2       | v :: s1' => add v (union s1' s2)     end.   Fixpoint intersect (s1 s2 : set) {struct s1} : set :=     match s1 with       | nil => nil       | v :: s1' =>         if In v s2           then v :: intersect s1' s2           else intersect s1' s2     end. ```
 A fold operation
```   Definition fold (A: Type) (f: A -> dom -> A) (s: set) (start: A) : A     := Elists.fold f s start. ```
 forall operation
```   Fixpoint setall (f: dom -> bool) (s: set) { struct s } : bool :=     match s with       nil => true     | h::t => if f h then setall f t else false    end. ```
 exists operation
```   Fixpoint setexists (f: dom -> bool) (s: set) { struct s } : bool :=     match s with       nil => false     | h::t => if f h then true else setexists f t    end. ```
 The elements of a set, as a list
```   Definition elems (s : set) : list dom := s. ```

```    Ltac setSimpl :=     repeat match goal with       | [ |- context[if dom_eq_dec ?V1 ?V2 then _ else _] ] =>               destruct (dom_eq_dec V1 V2); try subst; simpl; intuition       | [ H : context[if dom_eq_dec ?V1 ?V2 then _ else _] |- _ ] =>               destruct (dom_eq_dec V1 V2); try subst; simpl; intuition       | [ H : context[nil] |- _ ] => progress simpl in H       | [ H : context[_ :: _] |- _ ] => progress simpl in H       | [ |- context[nil] ] => progress simpl       | [ |- context[_ :: _] ] => progress simpl     end.   Theorem In_dec: forall v s,         {In v s = true} + {In v s = false}. ```

### Theorems about `In`

Theorem In_empty : forall x, In x empty = false. unfold empty; simpl; auto. Qed. Hint Resolve In_empty.

Theorem In_list: forall x s, List.In x s <-> In x s = true. intros. induction s; simpl; intuition; try discriminate. subst. destruct (dom_eq_dec x x); auto. elim n; auto.

destruct (dom_eq_dec x a); auto.

destruct (dom_eq_dec x a). intuition. right. auto. Qed.

(** *** Theorems about `add`
```   Theorem In_add : forall v v' s,       In v (add v' s) = true -> v = v' \/ In v s = true.   Theorem In_add_eq : forall v s, In v (add v s) = true.    Hint Resolve In_add_eq.   Theorem In_add_already: forall v v' s,       In v s = true -> In v (add v' s) = true.    Hint Resolve In_add_already.   Theorem In_add_neq : forall s v v',     v <> v' -> In v' (add v s) = In v' s.    Hint Resolve In_add_neq.   Lemma In_eq : forall a t,        In a (a :: t) = true.    Hint Resolve In_eq. ```

### Theorems about `incl`

```   Theorem incl_empty : forall s, incl empty s = true.    Hint Resolve incl_empty.          Theorem incl_empty_empty: forall s, incl s empty = true -> s = empty.   Theorem incl_ok : forall s1 s2,     incl s1 s2 = true <-> (forall x, In x s1 = true -> In x s2 = true).   Theorem incl_refl : forall s,       incl s s = true.    Hint Resolve incl_refl.   Theorem incl_false : forall s1 s2,     incl s1 s2 = false     -> exists x, In x s1 = true /\ In x s2 = false.   Theorem incl_trans : forall s1 s2,     incl s1 s2 = true     -> forall s3, incl s2 s3 = true -> incl s1 s3 = true.   Theorem incl_In : forall s1 s2,     incl s1 s2 = true -> forall x, In x s1 = true -> In x s2 = true.   Theorem incl_add : forall s v,     incl s (add v s) = true.    Hint Resolve incl_add.   Theorem incl_union_left : forall s1 s1' s2,     incl s1 s1' = true -> incl s1 (union s1' s2) = true.    Hint Resolve incl_union_left.   Theorem incl_union_right : forall s1 s2 s2',     incl s2 s2' = true -> incl s2 (union s1 s2') = true.    Hint Resolve incl_union_right. ```

### Theorems about `seq`

```   Theorem seq_refl : forall s : set, seq s s = true.    Hint Resolve seq_refl.   Theorem seq_trans : forall x y z:set, seq x y = true ->                                       seq y z = true ->                                       seq x z = true.      Theorem seq_sym : forall x y:set, seq x y = true -> seq y x = true.    ```

### Theorems about `union`

```   Theorem union_empty_left : forall s : set, seq (union empty s) s = true.    Hint Resolve union_empty_left.   Theorem union_empty_right : forall s:set, seq s (union s empty) = true.    Hint Resolve union_empty_right.      Theorem union_comm : forall s1 s2:set, seq (union s1 s2) (union s2 s1) = true.    Hint Resolve union_comm.      Theorem union_ass :    forall s1 s2 s3:set,           seq (union (union s1 s2) s3) (union s1 (union s2 s3)) = true.    Hint Resolve union_ass.      Theorem seq_union_left : forall s1 s2 s:set,                            seq s1 s2 = true ->                            seq (union s1 s) (union s2 s) = true.    Hint Resolve seq_union_left.      Lemma seq_union_right : forall s1 s2 s:set,                           seq s1 s2 = true ->                           seq (union s s1) (union s s2) = true.    Hint Resolve seq_union_right.   Theorem union_congr : forall s1 s1' s2 s2' : set,                         seq s1 s1' = true ->                         seq s2 s2' = true ->                         seq (union s1 s2) (union s1' s2') = true.   Theorem In_union_left : forall v s1 s2,     In v s1 = true -> In v (union s1 s2) = true.    Hint Resolve In_union_left.   Theorem In_union_right : forall v s1 s2,     In v s2 = true -> In v (union s1 s2) = true.    Hint Resolve In_union_right.   Theorem In_union : forall v s1 s2,     In v (union s1 s2) = true -> In v s1 = true \/ In v s2 = true.   Lemma union_idempotent' : forall s s',     incl s s' = true -> union s s' = s'.   Theorem union_idempotent : forall s,      union s s = s.    Hint Resolve union_idempotent. ```

### Theorems about `intersect`

```   Theorem In_intersect : forall v s' s,     In v (intersect s s') = true     -> In v s = true /\ In v s' = true.   Theorem In_intersect' : forall v s' s,     In v (intersect s s') = false     -> In v s = false \/ In v s' = false.   Theorem elems_ok : forall s x,     List.In x (elems s) <-> In x s = true.   Theorem elems_remove : forall s x ls,     elems s = x :: ls     -> elems (remove s x) = ls. ```

### Theorems about `remove`

```   Theorem In_remove : forall x x' s,     In x s = true     -> x <> x'     -> In x (remove s x') = true. ```

### Theorems about `fold`

``` ```
 Fold transitions from property P0 to property P1, if P0 holds initially P1 is established at some element, and both are preserved. Must invoke with a specific P0. Use fold_monotone_1 if P0 = P1 and fold_monotone_2 if P0 = True
```   Theorem fold_monotone_gen: forall (Acc:Type)                                 (P0: Acc -> Prop)                                 (s: set)                                 (start: Acc)                                 (f: Acc -> dom -> Acc)                                 (P1: Acc -> Prop),           P0 start ->           (forall x acc, In x s = true -> P0 acc -> P0 (f acc x)) ->              (exists x: dom, In x s = true /\                           forall acc, P0 acc -> P1 (f acc x)) ->              (forall x acc, In x s = true -> P1 acc -> P1 (f acc x)) ->              P1 (fold f s start). ```
 Fold for a monotonic function is monotonic
```   Theorem fold_monotone_1: forall (Acc:Type)                                 (s: set)                                 (start: Acc)                                 (f: Acc -> dom -> Acc)                                 (P: Acc -> Prop),           P start ->           (forall x acc, In x s = true -> P acc -> P (f acc x)) ->           P (fold f s start). ```
 Fold for a monotonic function establishes a property, if the property is established by some element in the list and the folded function is monotone.
```   Theorem fold_monotone_2: forall (Acc:Type)                                 (s: set)                                 (start: Acc)                                 (f: Acc -> dom -> Acc)                                 (P: Acc -> Prop),           (exists x: dom, In x s = true /\ forall acc, P (f acc x)) ->           (forall x acc, In x s = true -> P acc -> P (f acc x)) ->           P (fold f s start).      Definition dom := dom. End MakeSet. ```

## History

``` ```
 version 1.0 (Oct 21, 2006). First version.
``` ```
Index