Library Coq.FSets.FSetToFiniteSet


Finite sets library : conversion to old Finite_sets


Require Import Ensembles Finite_sets.
Require Import FSetInterface FSetProperties OrderedTypeEx DecidableTypeEx.

Going from FSets with usual Leibniz equality

to the good old Ensembles and Finite_sets theory.

Module WS_to_Finite_set (U:UsualDecidableType)(M: WSfun U).
 Module MP:= WProperties_fun 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 FSet ... at least in Prop.

 Lemma Ens_to_FSet : 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: Sfun U) :=
  WS_to_Finite_set U M.