Library Coq.FSets.FSetToFiniteSet
Finite sets library : conversion to old Finite_sets
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.