# Finite sets library

This file proposes an implementation of the non-dependant interface FSetInterface.S using strictly ordered list.

Require Export FSetInterface.

# Functions over lists

First, we provide sets as lists which are not necessarily sorted. The specs are proved under the additional condition of being sorted. And the functions returning sets are proved to preserve this invariant.

Module Raw (X: OrderedType).

Module MX := OrderedTypeFacts X.
Import MX.

Definition elt := X.t.
Definition t := list elt.

Definition empty : t := nil.

Definition is_empty (l : t) : bool := if l then true else false.

## The set operations.

Fixpoint mem (x : elt) (s : t) {struct s} : bool :=
match s with
| nil => false
| y :: l =>
match X.compare x y with
| LT _ => false
| EQ _ => true
| GT _ => mem x l
end
end.

Fixpoint add (x : elt) (s : t) {struct s} : t :=
match s with
| nil => x :: nil
| y :: l =>
match X.compare x y with
| LT _ => x :: s
| EQ _ => s
| GT _ => y :: add x l
end
end.

Definition singleton (x : elt) : t := x :: nil.

Fixpoint remove (x : elt) (s : t) {struct s} : t :=
match s with
| nil => nil
| y :: l =>
match X.compare x y with
| LT _ => s
| EQ _ => l
| GT _ => y :: remove x l
end
end.

Fixpoint union (s : t) : t -> t :=
match s with
| nil => fun s' => s'
| x :: l =>
(fix union_aux (s' : t) : t :=
match s' with
| nil => s
| x' :: l' =>
match X.compare x x' with
| LT _ => x :: union l s'
| EQ _ => x :: union l l'
| GT _ => x' :: union_aux l'
end
end)
end.

Fixpoint inter (s : t) : t -> t :=
match s with
| nil => fun _ => nil
| x :: l =>
(fix inter_aux (s' : t) : t :=
match s' with
| nil => nil
| x' :: l' =>
match X.compare x x' with
| LT _ => inter l s'
| EQ _ => x :: inter l l'
| GT _ => inter_aux l'
end
end)
end.

Fixpoint diff (s : t) : t -> t :=
match s with
| nil => fun _ => nil
| x :: l =>
(fix diff_aux (s' : t) : t :=
match s' with
| nil => s
| x' :: l' =>
match X.compare x x' with
| LT _ => x :: diff l s'
| EQ _ => diff l l'
| GT _ => diff_aux l'
end
end)
end.

Fixpoint equal (s : t) : t -> bool :=
fun s' : t =>
match s, s' with
| nil, nil => true
| x :: l, x' :: l' =>
match X.compare x x' with
| EQ _ => equal l l'
| _ => false
end
| _, _ => false
end.

Fixpoint subset (s s' : t) {struct s'} : bool :=
match s, s' with
| nil, _ => true
| x :: l, x' :: l' =>
match X.compare x x' with
| LT _ => false
| EQ _ => subset l l'
| GT _ => subset s l'
end
| _, _ => false
end.

Fixpoint fold (B : Type) (f : elt -> B -> B) (s : t) {struct s} :
B -> B := fun i => match s with
| nil => i
| x :: l => fold f l (f x i)
end.

Fixpoint filter (f : elt -> bool) (s : t) {struct s} : t :=
match s with
| nil => nil
| x :: l => if f x then x :: filter f l else filter f l
end.

Fixpoint for_all (f : elt -> bool) (s : t) {struct s} : bool :=
match s with
| nil => true
| x :: l => if f x then for_all f l else false
end.

Fixpoint exists_ (f : elt -> bool) (s : t) {struct s} : bool :=
match s with
| nil => false
| x :: l => if f x then true else exists_ f l
end.

Fixpoint partition (f : elt -> bool) (s : t) {struct s} :
t * t :=
match s with
| nil => (nil, nil)
| x :: l =>
let (s1, s2) := partition f l in
if f x then (x :: s1, s2) else (s1, x :: s2)
end.

Definition cardinal (s : t) : nat := length s.

Definition elements (x : t) : list elt := x.

Definition min_elt (s : t) : option elt :=
match s with
| nil => None
| x :: _ => Some x
end.

Fixpoint max_elt (s : t) : option elt :=
match s with
| nil => None
| x :: nil => Some x
| _ :: l => max_elt l
end.

Definition choose := min_elt.

## Proofs of set operation specifications.

Section ForNotations.

Notation Sort := (sort X.lt).
Notation Inf := (lelistA X.lt).
Notation In := (InA X.eq).

Definition Equal s s' := forall a : elt, In a s <-> In a s'.
Definition Subset s s' := forall a : elt, In a s -> In a s'.
Definition Empty s := forall a : elt, ~ In a s.
Definition For_all (P : elt -> Prop) s := forall x, In x s -> P x.
Definition Exists (P : elt -> Prop) (s : t) := exists x, In x s /\ P x.

Lemma mem_1 :
forall (s : t) (Hs : Sort s) (x : elt), In x s -> mem x s = true.

Lemma mem_2 : forall (s : t) (x : elt), mem x s = true -> In x s.

forall (s : t) (x a : elt), Inf a s -> X.lt a x -> Inf a (add x s).

Lemma add_sort : forall (s : t) (Hs : Sort s) (x : elt), Sort (add x s).

forall (s : t) (Hs : Sort s) (x y : elt), X.eq x y -> In y (add x s).

forall (s : t) (Hs : Sort s) (x y : elt), In y s -> In y (add x s).

forall (s : t) (Hs : Sort s) (x y : elt),
~ X.eq x y -> In y (add x s) -> In y s.

Lemma remove_Inf :
forall (s : t) (Hs : Sort s) (x a : elt), Inf a s -> Inf a (remove x s).
Hint Resolve remove_Inf.

Lemma remove_sort :
forall (s : t) (Hs : Sort s) (x : elt), Sort (remove x s).

Lemma remove_1 :
forall (s : t) (Hs : Sort s) (x y : elt), X.eq x y -> ~ In y (remove x s).

Lemma remove_2 :
forall (s : t) (Hs : Sort s) (x y : elt),
~ X.eq x y -> In y s -> In y (remove x s).

Lemma remove_3 :
forall (s : t) (Hs : Sort s) (x y : elt), In y (remove x s) -> In y s.

Lemma singleton_sort : forall x : elt, Sort (singleton x).

Lemma singleton_1 : forall x y : elt, In y (singleton x) -> X.eq x y.

Lemma singleton_2 : forall x y : elt, X.eq x y -> In y (singleton x).

Ltac DoubleInd :=
simple induction s;
[ simpl; auto; try solve [ intros; inversion H ]
| intros x l Hrec; simple induction s';
[ simpl; auto; try solve [ intros; inversion H ]
| intros x' l' Hrec' Hs Hs'; inversion Hs; inversion Hs'; subst;
simpl ] ].

Lemma union_Inf :
forall (s s' : t) (Hs : Sort s) (Hs' : Sort s') (a : elt),
Inf a s -> Inf a s' -> Inf a (union s s').
Hint Resolve union_Inf.

Lemma union_sort :
forall (s s' : t) (Hs : Sort s) (Hs' : Sort s'), Sort (union s s').

Lemma union_1 :
forall (s s' : t) (Hs : Sort s) (Hs' : Sort s') (x : elt),
In x (union s s') -> In x s \/ In x s'.

Lemma union_2 :
forall (s s' : t) (Hs : Sort s) (Hs' : Sort s') (x : elt),
In x s -> In x (union s s').

Lemma union_3 :
forall (s s' : t) (Hs : Sort s) (Hs' : Sort s') (x : elt),
In x s' -> In x (union s s').

Lemma inter_Inf :
forall (s s' : t) (Hs : Sort s) (Hs' : Sort s') (a : elt),
Inf a s -> Inf a s' -> Inf a (inter s s').
Hint Resolve inter_Inf.

Lemma inter_sort :
forall (s s' : t) (Hs : Sort s) (Hs' : Sort s'), Sort (inter s s').

Lemma inter_1 :
forall (s s' : t) (Hs : Sort s) (Hs' : Sort s') (x : elt),
In x (inter s s') -> In x s.

Lemma inter_2 :
forall (s s' : t) (Hs : Sort s) (Hs' : Sort s') (x : elt),
In x (inter s s') -> In x s'.

Lemma inter_3 :
forall (s s' : t) (Hs : Sort s) (Hs' : Sort s') (x : elt),
In x s -> In x s' -> In x (inter s s').

Lemma diff_Inf :
forall (s s' : t) (Hs : Sort s) (Hs' : Sort s') (a : elt),
Inf a s -> Inf a s' -> Inf a (diff s s').
Hint Resolve diff_Inf.

Lemma diff_sort :
forall (s s' : t) (Hs : Sort s) (Hs' : Sort s'), Sort (diff s s').

Lemma diff_1 :
forall (s s' : t) (Hs : Sort s) (Hs' : Sort s') (x : elt),
In x (diff s s') -> In x s.

Lemma diff_2 :
forall (s s' : t) (Hs : Sort s) (Hs' : Sort s') (x : elt),
In x (diff s s') -> ~ In x s'.

Lemma diff_3 :
forall (s s' : t) (Hs : Sort s) (Hs' : Sort s') (x : elt),
In x s -> ~ In x s' -> In x (diff s s').

Lemma equal_1 :
forall (s s' : t) (Hs : Sort s) (Hs' : Sort s'),
Equal s s' -> equal s s' = true.

Lemma equal_2 : forall s s' : t, equal s s' = true -> Equal s s'.

Lemma subset_1 :
forall (s s' : t) (Hs : Sort s) (Hs' : Sort s'),
Subset s s' -> subset s s' = true.

Lemma subset_2 : forall s s' : t, subset s s' = true -> Subset s s'.

Lemma empty_sort : Sort empty.

Lemma empty_1 : Empty empty.

Lemma is_empty_1 : forall s : t, Empty s -> is_empty s = true.

Lemma is_empty_2 : forall s : t, is_empty s = true -> Empty s.

Lemma elements_1 : forall (s : t) (x : elt), In x s -> In x (elements s).

Lemma elements_2 : forall (s : t) (x : elt), In x (elements s) -> In x s.

Lemma elements_3 : forall (s : t) (Hs : Sort s), Sort (elements s).

Lemma elements_3w : forall (s : t) (Hs : Sort s), NoDupA X.eq (elements s).

Lemma min_elt_1 : forall (s : t) (x : elt), min_elt s = Some x -> In x s.

Lemma min_elt_2 :
forall (s : t) (Hs : Sort s) (x y : elt),
min_elt s = Some x -> In y s -> ~ X.lt y x.

Lemma min_elt_3 : forall s : t, min_elt s = None -> Empty s.

Lemma max_elt_1 : forall (s : t) (x : elt), max_elt s = Some x -> In x s.

Lemma max_elt_2 :
forall (s : t) (Hs : Sort s) (x y : elt),
max_elt s = Some x -> In y s -> ~ X.lt x y.

Lemma max_elt_3 : forall s : t, max_elt s = None -> Empty s.

Definition choose_1 :
forall (s : t) (x : elt), choose s = Some x -> In x s := min_elt_1.

Definition choose_2 : forall s : t, choose s = None -> Empty s := min_elt_3.

Lemma choose_3: forall s s', Sort s -> Sort s' -> forall x x',
choose s = Some x -> choose s' = Some x' -> Equal s s' -> X.eq x x'.

Lemma fold_1 :
forall (s : t) (Hs : Sort s) (A : Type) (i : A) (f : elt -> A -> A),
fold f s i = fold_left (fun a e => f e a) (elements s) i.

Lemma cardinal_1 :
forall (s : t) (Hs : Sort s),
cardinal s = length (elements s).

Lemma filter_Inf :
forall (s : t) (Hs : Sort s) (x : elt) (f : elt -> bool),
Inf x s -> Inf x (filter f s).

Lemma filter_sort :
forall (s : t) (Hs : Sort s) (f : elt -> bool), Sort (filter f s).

Lemma filter_1 :
forall (s : t) (x : elt) (f : elt -> bool),
compat_bool X.eq f -> In x (filter f s) -> In x s.

Lemma filter_2 :
forall (s : t) (x : elt) (f : elt -> bool),
compat_bool X.eq f -> In x (filter f s) -> f x = true.

Lemma filter_3 :
forall (s : t) (x : elt) (f : elt -> bool),
compat_bool X.eq f -> In x s -> f x = true -> In x (filter f s).

Lemma for_all_1 :
forall (s : t) (f : elt -> bool),
compat_bool X.eq f ->
For_all (fun x => f x = true) s -> for_all f s = true.

Lemma for_all_2 :
forall (s : t) (f : elt -> bool),
compat_bool X.eq f ->
for_all f s = true -> For_all (fun x => f x = true) s.

Lemma exists_1 :
forall (s : t) (f : elt -> bool),
compat_bool X.eq f -> Exists (fun x => f x = true) s -> exists_ f s = true.

Lemma exists_2 :
forall (s : t) (f : elt -> bool),
compat_bool X.eq f -> exists_ f s = true -> Exists (fun x => f x = true) s.

Lemma partition_Inf_1 :
forall (s : t) (Hs : Sort s) (f : elt -> bool) (x : elt),
Inf x s -> Inf x (fst (partition f s)).

Lemma partition_Inf_2 :
forall (s : t) (Hs : Sort s) (f : elt -> bool) (x : elt),
Inf x s -> Inf x (snd (partition f s)).

Lemma partition_sort_1 :
forall (s : t) (Hs : Sort s) (f : elt -> bool), Sort (fst (partition f s)).

Lemma partition_sort_2 :
forall (s : t) (Hs : Sort s) (f : elt -> bool), Sort (snd (partition f s)).

Lemma partition_1 :
forall (s : t) (f : elt -> bool),
compat_bool X.eq f -> Equal (fst (partition f s)) (filter f s).

Lemma partition_2 :
forall (s : t) (f : elt -> bool),
compat_bool X.eq f ->
Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).

Definition eq : t -> t -> Prop := Equal.

Lemma eq_refl : forall s : t, eq s s.

Lemma eq_sym : forall s s' : t, eq s s' -> eq s' s.

Lemma eq_trans : forall s s' s'' : t, eq s s' -> eq s' s'' -> eq s s''.

Inductive lt : t -> t -> Prop :=
| lt_nil : forall (x : elt) (s : t), lt nil (x :: s)
| lt_cons_lt :
forall (x y : elt) (s s' : t), X.lt x y -> lt (x :: s) (y :: s')
| lt_cons_eq :
forall (x y : elt) (s s' : t),
X.eq x y -> lt s s' -> lt (x :: s) (y :: s').
Hint Constructors lt.

Lemma lt_trans : forall s s' s'' : t, lt s s' -> lt s' s'' -> lt s s''.

Lemma lt_not_eq :
forall (s s' : t) (Hs : Sort s) (Hs' : Sort s'), lt s s' -> ~ eq s s'.

Definition compare :
forall (s s' : t) (Hs : Sort s) (Hs' : Sort s'), Compare lt eq s s'.

End ForNotations.
Hint Constructors lt.

End Raw.

# Encapsulation

Now, in order to really provide a functor implementing S, we need to encapsulate everything into a type of strictly ordered lists.

Module Make (X: OrderedType) <: S with Module E := X.

Module Raw := Raw X.
Module E := X.

Record slist := {this :> Raw.t; sorted : sort E.lt this}.
Definition t := slist.
Definition elt := E.t.

Definition In (x : elt) (s : t) : Prop := InA E.eq x s.(this).
Definition Equal (s s':t) : Prop := forall a : elt, In a s <-> In a s'.
Definition Subset (s s':t) : Prop := forall a : elt, In a s -> In a s'.
Definition Empty (s:t) : Prop := forall a : elt, ~ In a s.
Definition For_all (P : elt -> Prop)(s:t) : Prop := forall x, In x s -> P x.
Definition Exists (P : elt -> Prop)(s:t) : Prop := exists x, In x s /\ P x.

Definition mem (x : elt) (s : t) : bool := Raw.mem x s.
Definition add (x : elt)(s : t) : t := Build_slist (Raw.add_sort (sorted s) x).
Definition remove (x : elt)(s : t) : t := Build_slist (Raw.remove_sort (sorted s) x).
Definition singleton (x : elt) : t := Build_slist (Raw.singleton_sort x).
Definition union (s s' : t) : t :=
Build_slist (Raw.union_sort (sorted s) (sorted s')).
Definition inter (s s' : t) : t :=
Build_slist (Raw.inter_sort (sorted s) (sorted s')).
Definition diff (s s' : t) : t :=
Build_slist (Raw.diff_sort (sorted s) (sorted s')).
Definition equal (s s' : t) : bool := Raw.equal s s'.
Definition subset (s s' : t) : bool := Raw.subset s s'.
Definition empty : t := Build_slist Raw.empty_sort.
Definition is_empty (s : t) : bool := Raw.is_empty s.
Definition elements (s : t) : list elt := Raw.elements s.
Definition min_elt (s : t) : option elt := Raw.min_elt s.
Definition max_elt (s : t) : option elt := Raw.max_elt s.
Definition choose (s : t) : option elt := Raw.choose s.
Definition fold (B : Type) (f : elt -> B -> B) (s : t) : B -> B := Raw.fold (B:=B) f s.
Definition cardinal (s : t) : nat := Raw.cardinal s.
Definition filter (f : elt -> bool) (s : t) : t :=
Build_slist (Raw.filter_sort (sorted s) f).
Definition for_all (f : elt -> bool) (s : t) : bool := Raw.for_all f s.
Definition exists_ (f : elt -> bool) (s : t) : bool := Raw.exists_ f s.
Definition partition (f : elt -> bool) (s : t) : t * t :=
let p := Raw.partition f s in
(Build_slist (this:=fst p) (Raw.partition_sort_1 (sorted s) f),
Build_slist (this:=snd p) (Raw.partition_sort_2 (sorted s) f)).
Definition eq (s s' : t) : Prop := Raw.eq s s'.
Definition lt (s s' : t) : Prop := Raw.lt s s'.

Section Spec.
Variable s s' s'': t.
Variable x y : elt.

Lemma In_1 : E.eq x y -> In x s -> In y s.

Lemma mem_1 : In x s -> mem x s = true.
Lemma mem_2 : mem x s = true -> In x s.

Lemma equal_1 : Equal s s' -> equal s s' = true.
Lemma equal_2 : equal s s' = true -> Equal s s'.

Lemma subset_1 : Subset s s' -> subset s s' = true.
Lemma subset_2 : subset s s' = true -> Subset s s'.

Lemma empty_1 : Empty empty.

Lemma is_empty_1 : Empty s -> is_empty s = true.
Lemma is_empty_2 : is_empty s = true -> Empty s.

Lemma add_1 : E.eq x y -> In y (add x s).
Lemma add_2 : In y s -> In y (add x s).
Lemma add_3 : ~ E.eq x y -> In y (add x s) -> In y s.

Lemma remove_1 : E.eq x y -> ~ In y (remove x s).
Lemma remove_2 : ~ E.eq x y -> In y s -> In y (remove x s).
Lemma remove_3 : In y (remove x s) -> In y s.

Lemma singleton_1 : In y (singleton x) -> E.eq x y.
Lemma singleton_2 : E.eq x y -> In y (singleton x).

Lemma union_1 : In x (union s s') -> In x s \/ In x s'.
Lemma union_2 : In x s -> In x (union s s').
Lemma union_3 : In x s' -> In x (union s s').

Lemma inter_1 : In x (inter s s') -> In x s.
Lemma inter_2 : In x (inter s s') -> In x s'.
Lemma inter_3 : In x s -> In x s' -> In x (inter s s').

Lemma diff_1 : In x (diff s s') -> In x s.
Lemma diff_2 : In x (diff s s') -> ~ In x s'.
Lemma diff_3 : In x s -> ~ In x s' -> In x (diff s s').

Lemma fold_1 : forall (A : Type) (i : A) (f : elt -> A -> A),
fold f s i = fold_left (fun a e => f e a) (elements s) i.

Lemma cardinal_1 : cardinal s = length (elements s).

Section Filter.

Variable f : elt -> bool.

Lemma filter_1 : compat_bool E.eq f -> In x (filter f s) -> In x s.
Lemma filter_2 : compat_bool E.eq f -> In x (filter f s) -> f x = true.
Lemma filter_3 :
compat_bool E.eq f -> In x s -> f x = true -> In x (filter f s).

Lemma for_all_1 :
compat_bool E.eq f ->
For_all (fun x => f x = true) s -> for_all f s = true.
Lemma for_all_2 :
compat_bool E.eq f ->
for_all f s = true -> For_all (fun x => f x = true) s.

Lemma exists_1 :
compat_bool E.eq f ->
Exists (fun x => f x = true) s -> exists_ f s = true.
Lemma exists_2 :
compat_bool E.eq f ->
exists_ f s = true -> Exists (fun x => f x = true) s.

Lemma partition_1 :
compat_bool E.eq f -> Equal (fst (partition f s)) (filter f s).
Lemma partition_2 :
compat_bool E.eq f ->
Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).

End Filter.

Lemma elements_1 : In x s -> InA E.eq x (elements s).
Lemma elements_2 : InA E.eq x (elements s) -> In x s.
Lemma elements_3 : sort E.lt (elements s).
Lemma elements_3w : NoDupA E.eq (elements s).

Lemma min_elt_1 : min_elt s = Some x -> In x s.
Lemma min_elt_2 : min_elt s = Some x -> In y s -> ~ E.lt y x.
Lemma min_elt_3 : min_elt s = None -> Empty s.

Lemma max_elt_1 : max_elt s = Some x -> In x s.
Lemma max_elt_2 : max_elt s = Some x -> In y s -> ~ E.lt x y.
Lemma max_elt_3 : max_elt s = None -> Empty s.

Lemma choose_1 : choose s = Some x -> In x s.
Lemma choose_2 : choose s = None -> Empty s.
Lemma choose_3 : choose s = Some x -> choose s' = Some y ->
Equal s s' -> E.eq x y.

Lemma eq_refl : eq s s.
Lemma eq_sym : eq s s' -> eq s' s.
Lemma eq_trans : eq s s' -> eq s' s'' -> eq s s''.

Lemma lt_trans : lt s s' -> lt s' s'' -> lt s s''.
Lemma lt_not_eq : lt s s' -> ~ eq s s'.

Definition compare : Compare lt eq s s'.

Definition eq_dec : { eq s s' } + { ~ eq s s' }.

End Spec.

End Make.