Library Coq.FSets.FSetCompat
Compatibility functors between FSetInterface and MSetInterface.
From new Weak Sets to old ones
Module Backport_WSets
(
E:
DecidableType.DecidableType)
(
M:
MSetInterface.WSets with Definition E.t :=
E.t
with Definition E.eq :=
E.eq)
<:
FSetInterface.WSfun E.
Definition elt :=
E.t.
Definition t :=
M.t.
Implicit Type s :
t.
Implicit Type x y :
elt.
Implicit Type f :
elt ->
bool.
Definition In :
elt ->
t ->
Prop :=
M.In.
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 :=
exists x, In x s /\ P x.
Definition empty :
t :=
M.empty.
Definition is_empty :
t ->
bool :=
M.is_empty.
Definition mem :
elt ->
t ->
bool :=
M.mem.
Definition add :
elt ->
t ->
t :=
M.add.
Definition singleton :
elt ->
t :=
M.singleton.
Definition remove :
elt ->
t ->
t :=
M.remove.
Definition union :
t ->
t ->
t :=
M.union.
Definition inter :
t ->
t ->
t :=
M.inter.
Definition diff :
t ->
t ->
t :=
M.diff.
Definition eq :
t ->
t ->
Prop :=
M.eq.
Definition eq_dec :
forall s s´,
{eq s s´}+{~eq s s´}:=
M.eq_dec.
Definition equal :
t ->
t ->
bool :=
M.equal.
Definition subset :
t ->
t ->
bool :=
M.subset.
Definition fold :
forall A :
Type, (
elt ->
A ->
A) ->
t ->
A ->
A :=
M.fold.
Definition for_all : (
elt ->
bool) ->
t ->
bool :=
M.for_all.
Definition exists_ : (
elt ->
bool) ->
t ->
bool :=
M.exists_.
Definition filter : (
elt ->
bool) ->
t ->
t :=
M.filter.
Definition partition : (
elt ->
bool) ->
t ->
t * t:=
M.partition.
Definition cardinal :
t ->
nat :=
M.cardinal.
Definition elements :
t ->
list elt :=
M.elements.
Definition choose :
t ->
option elt :=
M.choose.
Module MF :=
MSetFacts.WFacts M.
Definition In_1 :
forall s x y,
E.eq x y ->
In x s ->
In y s
:=
MF.In_1.
Definition eq_refl :
forall s,
eq s s
:= @
Equivalence_Reflexive _ _ M.eq_equiv.
Definition eq_sym :
forall s s´,
eq s s´ ->
eq s´ s
:= @
Equivalence_Symmetric _ _ M.eq_equiv.
Definition eq_trans :
forall s s´ s´´,
eq s s´ ->
eq s´ s´´ ->
eq s s´´
:= @
Equivalence_Transitive _ _ M.eq_equiv.
Definition mem_1 :
forall s x,
In x s ->
mem x s = true
:=
MF.mem_1.
Definition mem_2 :
forall s x,
mem x s = true ->
In x s
:=
MF.mem_2.
Definition equal_1 :
forall s s´,
Equal s s´ ->
equal s s´ = true
:=
MF.equal_1.
Definition equal_2 :
forall s s´,
equal s s´ = true ->
Equal s s´
:=
MF.equal_2.
Definition subset_1 :
forall s s´,
Subset s s´ ->
subset s s´ = true
:=
MF.subset_1.
Definition subset_2 :
forall s s´,
subset s s´ = true ->
Subset s s´
:=
MF.subset_2.
Definition empty_1 :
Empty empty :=
MF.empty_1.
Definition is_empty_1 :
forall s,
Empty s ->
is_empty s = true
:=
MF.is_empty_1.
Definition is_empty_2 :
forall s,
is_empty s = true ->
Empty s
:=
MF.is_empty_2.
Definition add_1 :
forall s x y,
E.eq x y ->
In y (
add x s)
:=
MF.add_1.
Definition add_2 :
forall s x y,
In y s ->
In y (
add x s)
:=
MF.add_2.
Definition add_3 :
forall s x y,
~ E.eq x y ->
In y (
add x s) ->
In y s
:=
MF.add_3.
Definition remove_1 :
forall s x y,
E.eq x y ->
~ In y (
remove x s)
:=
MF.remove_1.
Definition remove_2 :
forall s x y,
~ E.eq x y ->
In y s ->
In y (
remove x s)
:=
MF.remove_2.
Definition remove_3 :
forall s x y,
In y (
remove x s) ->
In y s
:=
MF.remove_3.
Definition union_1 :
forall s s´ x,
In x (
union s s´) ->
In x s \/ In x s´
:=
MF.union_1.
Definition union_2 :
forall s s´ x,
In x s ->
In x (
union s s´)
:=
MF.union_2.
Definition union_3 :
forall s s´ x,
In x s´ ->
In x (
union s s´)
:=
MF.union_3.
Definition inter_1 :
forall s s´ x,
In x (
inter s s´) ->
In x s
:=
MF.inter_1.
Definition inter_2 :
forall s s´ x,
In x (
inter s s´) ->
In x s´
:=
MF.inter_2.
Definition inter_3 :
forall s s´ x,
In x s ->
In x s´ ->
In x (
inter s s´)
:=
MF.inter_3.
Definition diff_1 :
forall s s´ x,
In x (
diff s s´) ->
In x s
:=
MF.diff_1.
Definition diff_2 :
forall s s´ x,
In x (
diff s s´) ->
~ In x s´
:=
MF.diff_2.
Definition diff_3 :
forall s s´ x,
In x s ->
~ In x s´ ->
In x (
diff s s´)
:=
MF.diff_3.
Definition singleton_1 :
forall x y,
In y (
singleton x) ->
E.eq x y
:=
MF.singleton_1.
Definition singleton_2 :
forall x y,
E.eq x y ->
In y (
singleton x)
:=
MF.singleton_2.
Definition fold_1 :
forall s (
A :
Type) (
i :
A) (
f :
elt ->
A ->
A),
fold f s i = fold_left (
fun a e =>
f e a) (
elements s)
i
:=
MF.fold_1.
Definition cardinal_1 :
forall s,
cardinal s = length (
elements s)
:=
MF.cardinal_1.
Definition filter_1 :
forall s x f,
compat_bool E.eq f ->
In x (
filter f s) ->
In x s
:=
MF.filter_1.
Definition filter_2 :
forall s x f,
compat_bool E.eq f ->
In x (
filter f s) ->
f x = true
:=
MF.filter_2.
Definition filter_3 :
forall s x f,
compat_bool E.eq f ->
In x s ->
f x = true ->
In x (
filter f s)
:=
MF.filter_3.
Definition for_all_1 :
forall s f,
compat_bool E.eq f ->
For_all (
fun x =>
f x = true)
s ->
for_all f s = true
:=
MF.for_all_1.
Definition for_all_2 :
forall s f,
compat_bool E.eq f ->
for_all f s = true ->
For_all (
fun x =>
f x = true)
s
:=
MF.for_all_2.
Definition exists_1 :
forall s f,
compat_bool E.eq f ->
Exists (
fun x =>
f x = true)
s ->
exists_ f s = true
:=
MF.exists_1.
Definition exists_2 :
forall s f,
compat_bool E.eq f ->
exists_ f s = true ->
Exists (
fun x =>
f x = true)
s
:=
MF.exists_2.
Definition partition_1 :
forall s f,
compat_bool E.eq f ->
Equal (
fst (
partition f s)) (
filter f s)
:=
MF.partition_1.
Definition partition_2 :
forall s f,
compat_bool E.eq f ->
Equal (
snd (
partition f s)) (
filter (
fun x =>
negb (
f x))
s)
:=
MF.partition_2.
Definition choose_1 :
forall s x,
choose s = Some x ->
In x s
:=
MF.choose_1.
Definition choose_2 :
forall s,
choose s = None ->
Empty s
:=
MF.choose_2.
Definition elements_1 :
forall s x,
In x s ->
InA E.eq x (
elements s)
:=
MF.elements_1.
Definition elements_2 :
forall s x,
InA E.eq x (
elements s) ->
In x s
:=
MF.elements_2.
Definition elements_3w :
forall s,
NoDupA E.eq (
elements s)
:=
MF.elements_3w.
End Backport_WSets.
From new Sets to new ones
Module Backport_Sets
(
E:
OrderedType.OrderedType)
(
M:
MSetInterface.Sets with Definition E.t :=
E.t
with Definition E.eq :=
E.eq
with Definition E.lt :=
E.lt)
<:
FSetInterface.S with Module E:=
E.
Include Backport_WSets E M.
Implicit Type s :
t.
Implicit Type x y :
elt.
Definition lt :
t ->
t ->
Prop :=
M.lt.
Definition min_elt :
t ->
option elt :=
M.min_elt.
Definition max_elt :
t ->
option elt :=
M.max_elt.
Definition min_elt_1 :
forall s x,
min_elt s = Some x ->
In x s
:=
M.min_elt_spec1.
Definition min_elt_2 :
forall s x y,
min_elt s = Some x ->
In y s ->
~ E.lt y x
:=
M.min_elt_spec2.
Definition min_elt_3 :
forall s,
min_elt s = None ->
Empty s
:=
M.min_elt_spec3.
Definition max_elt_1 :
forall s x,
max_elt s = Some x ->
In x s
:=
M.max_elt_spec1.
Definition max_elt_2 :
forall s x y,
max_elt s = Some x ->
In y s ->
~ E.lt x y
:=
M.max_elt_spec2.
Definition max_elt_3 :
forall s,
max_elt s = None ->
Empty s
:=
M.max_elt_spec3.
Definition elements_3 :
forall s,
sort E.lt (
elements s)
:=
M.elements_spec2.
Definition choose_3 :
forall s s´ x y,
choose s = Some x ->
choose s´ = Some y ->
Equal s s´ ->
E.eq x y
:=
M.choose_spec3.
Definition lt_trans :
forall s s´ s´´,
lt s s´ ->
lt s´ s´´ ->
lt s s´´
:= @
StrictOrder_Transitive _ _ M.lt_strorder.
Lemma lt_not_eq :
forall s s´,
lt s s´ ->
~ eq s s´.
Definition compare :
forall s s´,
Compare lt eq s s´.
Module E :=
E.
End Backport_Sets.
From old Weak Sets to new ones.
Module Update_WSets
(
E:
Equalities.DecidableType)
(
M:
FSetInterface.WS with Definition E.t :=
E.t
with Definition E.eq :=
E.eq)
<:
MSetInterface.WSetsOn E.
Definition elt :=
E.t.
Definition t :=
M.t.
Implicit Type s :
t.
Implicit Type x y :
elt.
Implicit Type f :
elt ->
bool.
Definition In :
elt ->
t ->
Prop :=
M.In.
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 :=
exists x, In x s /\ P x.
Definition empty :
t :=
M.empty.
Definition is_empty :
t ->
bool :=
M.is_empty.
Definition mem :
elt ->
t ->
bool :=
M.mem.
Definition add :
elt ->
t ->
t :=
M.add.
Definition singleton :
elt ->
t :=
M.singleton.
Definition remove :
elt ->
t ->
t :=
M.remove.
Definition union :
t ->
t ->
t :=
M.union.
Definition inter :
t ->
t ->
t :=
M.inter.
Definition diff :
t ->
t ->
t :=
M.diff.
Definition eq :
t ->
t ->
Prop :=
M.eq.
Definition eq_dec :
forall s s´,
{eq s s´}+{~eq s s´}:=
M.eq_dec.
Definition equal :
t ->
t ->
bool :=
M.equal.
Definition subset :
t ->
t ->
bool :=
M.subset.
Definition fold :
forall A :
Type, (
elt ->
A ->
A) ->
t ->
A ->
A :=
M.fold.
Definition for_all : (
elt ->
bool) ->
t ->
bool :=
M.for_all.
Definition exists_ : (
elt ->
bool) ->
t ->
bool :=
M.exists_.
Definition filter : (
elt ->
bool) ->
t ->
t :=
M.filter.
Definition partition : (
elt ->
bool) ->
t ->
t * t:=
M.partition.
Definition cardinal :
t ->
nat :=
M.cardinal.
Definition elements :
t ->
list elt :=
M.elements.
Definition choose :
t ->
option elt :=
M.choose.
Module MF :=
FSetFacts.WFacts M.
Instance In_compat :
Proper (
E.eq==>Logic.eq==>iff)
In.
Instance eq_equiv :
Equivalence eq :=
_.
Section Spec.
Variable s s´:
t.
Variable x y :
elt.
Lemma mem_spec :
mem x s = true <-> In x s.
Lemma equal_spec :
equal s s´ = true <-> Equal s s´.
Lemma subset_spec :
subset s s´ = true <-> Subset s s´.
Definition empty_spec :
Empty empty :=
M.empty_1.
Lemma is_empty_spec :
is_empty s = true <-> Empty s.
Lemma add_spec :
In y (
add x s)
<-> E.eq y x \/ In y s.
Lemma remove_spec :
In y (
remove x s)
<-> In y s /\ ~E.eq y x.
Lemma singleton_spec :
In y (
singleton x)
<-> E.eq y x.
Definition union_spec :
In x (
union s s´)
<-> In x s \/ In x s´
:= @
MF.union_iff s s´ x.
Definition inter_spec :
In x (
inter s s´)
<-> In x s /\ In x s´
:= @
MF.inter_iff s s´ x.
Definition diff_spec :
In x (
diff s s´)
<-> In x s /\ ~In x s´
:= @
MF.diff_iff s s´ x.
Definition fold_spec :
forall (
A :
Type) (
i :
A) (
f :
elt ->
A ->
A),
fold f s i = fold_left (
flip f) (
elements s)
i
:= @
M.fold_1 s.
Definition cardinal_spec :
cardinal s = length (
elements s)
:= @
M.cardinal_1 s.
Lemma elements_spec1 :
InA E.eq x (
elements s)
<-> In x s.
Definition elements_spec2w :
NoDupA E.eq (
elements s)
:= @
M.elements_3w s.
Definition choose_spec1 :
choose s = Some x ->
In x s
:= @
M.choose_1 s x.
Definition choose_spec2 :
choose s = None ->
Empty s
:= @
M.choose_2 s.
Definition filter_spec :
forall f,
Proper (
E.eq==>Logic.eq)
f ->
(
In x (
filter f s)
<-> In x s /\ f x = true)
:= @
MF.filter_iff s x.
Definition partition_spec1 :
forall f,
Proper (
E.eq==>Logic.eq)
f ->
Equal (
fst (
partition f s)) (
filter f s)
:= @
M.partition_1 s.
Definition partition_spec2 :
forall f,
Proper (
E.eq==>Logic.eq)
f ->
Equal (
snd (
partition f s)) (
filter (
fun x =>
negb (
f x))
s)
:= @
M.partition_2 s.
Lemma for_all_spec :
forall f,
Proper (
E.eq==>Logic.eq)
f ->
(
for_all f s = true <-> For_all (
fun x =>
f x = true)
s).
Lemma exists_spec :
forall f,
Proper (
E.eq==>Logic.eq)
f ->
(
exists_ f s = true <-> Exists (
fun x =>
f x = true)
s).
End Spec.
End Update_WSets.
From old Sets to new ones.