# Library Coq.MSets.MSetToFiniteSet

# Finite sets library : conversion to old Finite_sets

Require Import Ensembles Finite_sets.
Require Import MSetInterface MSetProperties OrdersEx.

# Going from MSets with usual Leibniz equality

to the good old Ensembles and Finite_sets theory.
Module WS_to_Finite_set (U:UsualDecidableType)(M: WSetsOn U).
Module MP:= WPropertiesOn U M.
Import M MP FM Ensembles Finite_sets.
Definition mkEns : M.t -> Ensemble M.elt :=
fun s x => M.In x s.
Notation " !! " := mkEns.
Lemma In_In : forall s x, M.In x s <-> In _ (!! s) x.
Lemma Subset_Included : forall s s', s [<=] s' <-> Included _ (!! s) (!! s').
Notation " a === b " := (Same_set M.elt a b) (at level 70, no associativity).
Lemma Equal_Same_set : forall s s', s [=] s' <-> !! s === !! s'.
Lemma empty_Empty_Set : !! M.empty === Empty_set _.
Lemma Empty_Empty_set : forall s, Empty s -> !! s === Empty_set _.
Lemma singleton_Singleton : forall x, !!(M.singleton x) === Singleton _ x .
Lemma union_Union : forall s s', !!(union s s') === Union _ (!! s) (!! s').
Lemma inter_Intersection : forall s s', !!(inter s s') === Intersection _ (!! s) (!! s').
Lemma add_Add : forall x s, !!(add x s) === Add _ (!! s) x.
Lemma Add_Add : forall x s s', MP.Add x s s' -> !! s' === Add _ (!! s) x.
Lemma remove_Subtract : forall x s, !!(remove x s) === Subtract _ (!! s) x.
Lemma mkEns_Finite : forall s, Finite _ (!! s).
Lemma mkEns_cardinal : forall s, cardinal _ (!! s) (M.cardinal s).
we can even build a function from Finite Ensemble to MSet ... at least in Prop.
Lemma Ens_to_MSet : forall e : Ensemble M.elt, Finite _ e ->
exists s : M.t , !! s === e.
End WS_to_Finite_set.
Module S_to_Finite_set (U:UsualOrderedType)(M: SetsOn U) :=
WS_to_Finite_set U M.