# Library Coq.Lists.ListSet

A Library for finite sets, implemented as lists

List is loaded, but not exported. This allow to "hide" the definitions, functions and theorems of List and to see only the ones of ListSet

Require Import List.

Section first_definitions.

Variable A : Type.
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) : 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) : 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) : 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) : 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) : 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}.

Lemma set_mem_ind :
forall (B:Type) (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).

Lemma set_mem_ind2 :
forall (B:Type) (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).

Lemma set_mem_correct1 :
forall (a:A) (x:set), set_mem a x = true -> set_In a x.

Lemma set_mem_correct2 :
forall (a:A) (x:set), set_In a x -> set_mem a x = true.

Lemma set_mem_complete1 :
forall (a:A) (x:set), set_mem a x = false -> ~ set_In a x.

Lemma set_mem_complete2 :
forall (a:A) (x:set), ~ set_In a x -> set_mem a x = false.

forall (a b:A) (x:set), set_In a x -> set_In a (set_add b x).

forall (a b:A) (x:set), a = b -> set_In a (set_add b x).

forall (a b:A) (x:set), a = b \/ set_In a x -> set_In a (set_add b x).

forall (a b:A) (x:set), set_In a (set_add b x) -> a = b \/ set_In a x.

forall (a b:A) (x:set), set_In a (set_add b x) -> a <> b -> set_In a x.

Lemma set_union_intro1 :
forall (a:A) (x y:set), set_In a x -> set_In a (set_union x y).

Lemma set_union_intro2 :
forall (a:A) (x y:set), set_In a y -> set_In a (set_union x y).

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).

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.

Lemma set_union_emptyL :
forall (a:A) (x:set), set_In a (set_union empty_set x) -> set_In a x.

Lemma set_union_emptyR :
forall (a:A) (x:set), set_In a (set_union x empty_set) -> set_In a x.

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).

Lemma set_inter_elim1 :
forall (a:A) (x y:set), set_In a (set_inter x y) -> set_In a x.

Lemma set_inter_elim2 :
forall (a:A) (x y:set), set_In a (set_inter x y) -> set_In a y.

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.

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).

Lemma set_diff_elim1 :
forall (a:A) (x y:set), set_In a (set_diff x y) -> set_In a x.

Lemma set_diff_elim2 :
forall (a:A) (x y:set), set_In a (set_diff x y) -> ~ set_In a y.

Lemma set_diff_trivial : forall (a:A) (x:set), ~ set_In a (set_diff x x).

Hint Resolve set_diff_intro set_diff_trivial.

End first_definitions.

Section other_definitions.

Definition set_prod : forall {A B:Type}, set A -> set B -> set (A * B) :=
list_prod.

B^A, set of applications from A to B
Definition set_power : forall {A B:Type}, set A -> set B -> set (set (A * B)) :=
list_power.

Definition set_fold_left {A B:Type} : (B -> A -> B) -> set A -> B -> B :=
fold_left (A:=B) (B:=A).

Definition set_fold_right {A B:Type} (f:A -> B -> B) (x:set A)
(b:B) : B := fold_right f b x.

Definition set_map {A B:Type} (Aeq_dec : forall x y:B, {x = y} + {x <> y})
(f : A -> B) (x : set A) : set B :=
set_fold_right (fun a => set_add Aeq_dec (f a)) x (empty_set B).

End other_definitions.