Library Coq.FSets.FSetToFiniteSet
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.