Library Coq.FSets.FSetBridge
This module implements bridges (as functors) from dependent
to/from non-dependent set signature.
From non-dependent signature S to dependent signature Sdep.
Module DepOfNodep (
Import M:
S) <:
Sdep with Module E :=
M.E.
Definition empty : {
s :
t |
Empty s}.
Definition is_empty :
forall s :
t, {
Empty s} + {~
Empty s}.
Definition mem :
forall (
x :
elt) (
s :
t), {
In x s} + {~
In x s}.
Definition Add (
x :
elt) (
s s' :
t) :=
forall y :
elt,
In y s' <->
E.eq x y \/
In y s.
Definition add :
forall (
x :
elt) (
s :
t), {
s' :
t |
Add x s s'}.
Definition singleton :
forall x :
elt, {
s :
t |
forall y :
elt,
In y s <->
E.eq x y}.
Definition remove :
forall (
x :
elt) (
s :
t),
{
s' :
t |
forall y :
elt,
In y s' <-> ~
E.eq x y /\
In y s}.
Definition union :
forall s s' :
t, {
s'' :
t |
forall x :
elt,
In x s'' <->
In x s \/
In x s'}.
Definition inter :
forall s s' :
t, {
s'' :
t |
forall x :
elt,
In x s'' <->
In x s /\
In x s'}.
Definition diff :
forall s s' :
t, {
s'' :
t |
forall x :
elt,
In x s'' <->
In x s /\ ~
In x s'}.
Definition equal :
forall s s' :
t, {
Equal s s'} + {~
Equal s s'}.
Definition subset :
forall s s' :
t, {
Subset s s'} + {~Subset
s s'}.
Definition elements :
forall s :
t,
{
l :
list elt |
sort E.lt l /\ (
forall x :
elt,
In x s <->
InA E.eq x l)}.
Definition fold :
forall (
A :
Type) (
f :
elt ->
A ->
A) (
s :
t) (
i :
A),
{
r :
A |
let (
l,_) :=
elements s in
r =
fold_left (
fun a e =>
f e a)
l i}.
Definition cardinal :
forall s :
t,
{
r :
nat |
let (
l,_) :=
elements s in r =
length l }.
Definition fdec (
P :
elt ->
Prop) (
Pdec :
forall x :
elt, {
P x} + {~
P x})
(
x :
elt) :=
if Pdec x then true else false.
Lemma compat_P_aux :
forall (
P :
elt ->
Prop) (
Pdec :
forall x :
elt, {
P x} + {~
P x}),
compat_P E.eq P ->
compat_bool E.eq (
fdec Pdec).
Hint Resolve compat_P_aux.
Definition filter :
forall (
P :
elt ->
Prop) (
Pdec :
forall x :
elt, {
P x} + {~
P x}) (
s :
t),
{
s' :
t |
compat_P E.eq P ->
forall x :
elt,
In x s' <->
In x s /\
P x}.
Definition for_all :
forall (
P :
elt ->
Prop) (
Pdec :
forall x :
elt, {
P x} + {~
P x}) (
s :
t),
{
compat_P E.eq P ->
For_all P s} + {
compat_P E.eq P -> ~
For_all P s}.
Definition exists_ :
forall (
P :
elt ->
Prop) (
Pdec :
forall x :
elt, {
P x} + {~
P x}) (
s :
t),
{
compat_P E.eq P ->
Exists P s} + {
compat_P E.eq P -> ~
Exists P s}.
Definition partition :
forall (
P :
elt ->
Prop) (
Pdec :
forall x :
elt, {
P x} + {~
P x}) (
s :
t),
{
partition :
t *
t |
let (
s1,
s2) :=
partition in
compat_P E.eq P ->
For_all P s1 /\
For_all (
fun x => ~
P x)
s2 /\
(
forall x :
elt,
In x s <->
In x s1 \/
In x s2)}.
Definition choose_aux:
forall s :
t,
{
x :
elt |
M.choose s =
Some x } + {
M.choose s =
None }.
Definition choose :
forall s :
t, {
x :
elt |
In x s} + {
Empty s}.
Lemma choose_ok1 :
forall s x,
M.choose s =
Some x <->
exists H:In
x s,
choose s =
inleft _ (
exist (
fun x =>
In x s)
x H).
Lemma choose_ok2 :
forall s,
M.choose s =
None <->
exists H:Empty
s,
choose s =
inright _ H.
Lemma choose_equal :
forall s s',
Equal s s' ->
match choose s,
choose s' with
|
inleft (
exist x _),
inleft (
exist x' _) =>
E.eq x x'
|
inright _,
inright _ =>
True
|
_,
_ =>
False
end.
Definition min_elt :
forall s :
t,
{
x :
elt |
In x s /\
For_all (
fun y => ~
E.lt y x)
s} + {
Empty s}.
Definition max_elt :
forall s :
t,
{
x :
elt |
In x s /\
For_all (
fun y => ~
E.lt x y)
s} + {
Empty s}.
Module E :=
E.
Definition elt :=
elt.
Definition t :=
t.
Definition In :=
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 :
t) :=
forall x :
elt,
In x s ->
P x.
Definition Exists (
P :
elt ->
Prop) (
s :
t) :=
exists x :
elt,
In x s /\
P x.
Definition eq_In :=
In_1.
Definition eq :=
Equal.
Definition lt :=
lt.
Definition eq_refl :=
eq_refl.
Definition eq_sym :=
eq_sym.
Definition eq_trans :=
eq_trans.
Definition lt_trans :=
lt_trans.
Definition lt_not_eq :=
lt_not_eq.
Definition compare :=
compare.
End DepOfNodep.
From dependent signature Sdep to non-dependent signature S.
Module NodepOfDep (
M:
Sdep) <:
S with Module E :=
M.E.
Import M.
Module ME :=
OrderedTypeFacts E.
Definition empty :
t :=
let (
s,
_) :=
empty in s.
Lemma empty_1 :
Empty empty.
Definition is_empty (
s :
t) :
bool :=
if is_empty s then true else false.
Lemma is_empty_1 :
forall s :
t,
Empty s ->
is_empty s =
true.
Lemma is_empty_2 :
forall s :
t,
is_empty s =
true ->
Empty s.
Definition mem (
x :
elt) (
s :
t) :
bool :=
if mem x s then true else false.
Lemma mem_1 :
forall (
s :
t) (
x :
elt),
In x s ->
mem x s =
true.
Lemma mem_2 :
forall (
s :
t) (
x :
elt),
mem x s =
true ->
In x s.
Definition eq_dec :=
equal.
Definition equal (
s s' :
t) :
bool :=
if equal s s' then true else false.
Lemma equal_1 :
forall s s' :
t,
Equal s s' ->
equal s s' =
true.
Lemma equal_2 :
forall s s' :
t,
equal s s' =
true ->
Equal s s'.
Definition subset (
s s' :
t) :
bool :=
if subset s s' then true else false.
Lemma subset_1 :
forall s s' :
t,
Subset s s' ->
subset s s' =
true.
Lemma subset_2 :
forall s s' :
t,
subset s s' =
true ->
Subset s s'.
Definition choose (
s :
t) :
option elt :=
match choose s with
|
inleft (
exist x _) =>
Some x
|
inright _ =>
None
end.
Lemma choose_1 :
forall (
s :
t) (
x :
elt),
choose s =
Some x ->
In x s.
Lemma choose_2 :
forall s :
t,
choose s =
None ->
Empty s.
Lemma choose_3 :
forall s s' x x',
choose s =
Some x ->
choose s' =
Some x' ->
Equal s s' ->
E.eq x x'.
Definition elements (
s :
t) :
list elt :=
let (
l,
_) :=
elements s in l.
Lemma elements_1 :
forall (
s :
t) (
x :
elt),
In x s ->
InA E.eq x (
elements s).
Lemma elements_2 :
forall (
s :
t) (
x :
elt),
InA E.eq x (
elements s) ->
In x s.
Lemma elements_3 :
forall s :
t,
sort E.lt (
elements s).
Hint Resolve elements_3.
Lemma elements_3w :
forall s :
t,
NoDupA E.eq (
elements s).
Definition min_elt (
s :
t) :
option elt :=
match min_elt s with
|
inleft (
exist x _) =>
Some x
|
inright _ =>
None
end.
Lemma min_elt_1 :
forall (
s :
t) (
x :
elt),
min_elt s =
Some x ->
In x s.
Lemma min_elt_2 :
forall (
s :
t) (
x y :
elt),
min_elt s =
Some x ->
In y s -> ~
E.lt y x.
Lemma min_elt_3 :
forall s :
t,
min_elt s =
None ->
Empty s.
Definition max_elt (
s :
t) :
option elt :=
match max_elt s with
|
inleft (
exist x _) =>
Some x
|
inright _ =>
None
end.
Lemma max_elt_1 :
forall (
s :
t) (
x :
elt),
max_elt s =
Some x ->
In x s.
Lemma max_elt_2 :
forall (
s :
t) (
x y :
elt),
max_elt s =
Some x ->
In y s -> ~
E.lt x y.
Lemma max_elt_3 :
forall s :
t,
max_elt s =
None ->
Empty s.
Definition add (
x :
elt) (
s :
t) :
t :=
let (
s',
_) :=
add x s in s'.
Lemma add_1 :
forall (
s :
t) (
x y :
elt),
E.eq x y ->
In y (
add x s).
Lemma add_2 :
forall (
s :
t) (
x y :
elt),
In y s ->
In y (
add x s).
Lemma add_3 :
forall (
s :
t) (
x y :
elt), ~
E.eq x y ->
In y (
add x s) ->
In y s.
Definition remove (
x :
elt) (
s :
t) :
t :=
let (
s',
_) :=
remove x s in s'.
Lemma remove_1 :
forall (
s :
t) (
x y :
elt),
E.eq x y -> ~
In y (
remove x s).
Lemma remove_2 :
forall (
s :
t) (
x y :
elt), ~
E.eq x y ->
In y s ->
In y (
remove x s).
Lemma remove_3 :
forall (
s :
t) (
x y :
elt),
In y (
remove x s) ->
In y s.
Definition singleton (
x :
elt) :
t :=
let (
s,
_) :=
singleton x in s.
Lemma singleton_1 :
forall x y :
elt,
In y (
singleton x) ->
E.eq x y.
Lemma singleton_2 :
forall x y :
elt,
E.eq x y ->
In y (
singleton x).
Definition union (
s s' :
t) :
t :=
let (
s'',
_) :=
union s s' in s''.
Lemma union_1 :
forall (
s s' :
t) (
x :
elt),
In x (
union s s') ->
In x s \/
In x s'.
Lemma union_2 :
forall (
s s' :
t) (
x :
elt),
In x s ->
In x (
union s s').
Lemma union_3 :
forall (
s s' :
t) (
x :
elt),
In x s' ->
In x (
union s s').
Definition inter (
s s' :
t) :
t :=
let (
s'',
_) :=
inter s s' in s''.
Lemma inter_1 :
forall (
s s' :
t) (
x :
elt),
In x (
inter s s') ->
In x s.
Lemma inter_2 :
forall (
s s' :
t) (
x :
elt),
In x (
inter s s') ->
In x s'.
Lemma inter_3 :
forall (
s s' :
t) (
x :
elt),
In x s ->
In x s' ->
In x (
inter s s').
Definition diff (
s s' :
t) :
t :=
let (
s'',
_) :=
diff s s' in s''.
Lemma diff_1 :
forall (
s s' :
t) (
x :
elt),
In x (
diff s s') ->
In x s.
Lemma diff_2 :
forall (
s s' :
t) (
x :
elt),
In x (
diff s s') -> ~
In x s'.
Lemma diff_3 :
forall (
s s' :
t) (
x :
elt),
In x s -> ~
In x s' ->
In x (
diff s s').
Definition cardinal (
s :
t) :
nat :=
let (
f,
_) :=
cardinal s in f.
Lemma cardinal_1 :
forall s,
cardinal s =
length (
elements s).
Definition fold (
B :
Type) (
f :
elt ->
B ->
B) (
i :
t)
(
s :
B) :
B :=
let (
fold,
_) :=
fold f i s in fold.
Lemma fold_1 :
forall (
s :
t) (
A :
Type) (
i :
A) (
f :
elt ->
A ->
A),
fold f s i =
fold_left (
fun a e =>
f e a) (
elements s)
i.
Definition f_dec :
forall (
f :
elt ->
bool) (
x :
elt), {
f x =
true} + {
f x <>
true}.
Lemma compat_P_aux :
forall f :
elt ->
bool,
compat_bool E.eq f ->
compat_P E.eq (
fun x =>
f x =
true).
Hint Resolve compat_P_aux.
Definition filter (
f :
elt ->
bool) (
s :
t) :
t :=
let (
s',
_) :=
filter (
P:=fun
x =>
f x =
true) (
f_dec f)
s in s'.
Lemma filter_1 :
forall (
s :
t) (
x :
elt) (
f :
elt ->
bool),
compat_bool E.eq f ->
In x (
filter f s) ->
In x s.
Lemma filter_2 :
forall (
s :
t) (
x :
elt) (
f :
elt ->
bool),
compat_bool E.eq f ->
In x (
filter f s) ->
f x =
true.
Lemma filter_3 :
forall (
s :
t) (
x :
elt) (
f :
elt ->
bool),
compat_bool E.eq f ->
In x s ->
f x =
true ->
In x (
filter f s).
Definition for_all (
f :
elt ->
bool) (
s :
t) :
bool :=
if for_all (
P:=fun
x =>
f x =
true) (
f_dec f)
s
then true
else false.
Lemma for_all_1 :
forall (
s :
t) (
f :
elt ->
bool),
compat_bool E.eq f ->
For_all (
fun x =>
f x =
true)
s ->
for_all f s =
true.
Lemma for_all_2 :
forall (
s :
t) (
f :
elt ->
bool),
compat_bool E.eq f ->
for_all f s =
true ->
For_all (
fun x =>
f x =
true)
s.
Definition exists_ (
f :
elt ->
bool) (
s :
t) :
bool :=
if exists_ (
P:=fun
x =>
f x =
true) (
f_dec f)
s
then true
else false.
Lemma exists_1 :
forall (
s :
t) (
f :
elt ->
bool),
compat_bool E.eq f ->
Exists (
fun x =>
f x =
true)
s ->
exists_ f s =
true.
Lemma exists_2 :
forall (
s :
t) (
f :
elt ->
bool),
compat_bool E.eq f ->
exists_ f s =
true ->
Exists (
fun x =>
f x =
true)
s.
Definition partition (
f :
elt ->
bool) (
s :
t) :
t *
t :=
let (
p,
_) :=
partition (
P:=fun
x =>
f x =
true) (
f_dec f)
s in p.
Lemma partition_1 :
forall (
s :
t) (
f :
elt ->
bool),
compat_bool E.eq f ->
Equal (
fst (
partition f s)) (
filter f s).
Lemma partition_2 :
forall (
s :
t) (
f :
elt ->
bool),
compat_bool E.eq f ->
Equal (
snd (
partition f s)) (
filter (
fun x =>
negb (
f x))
s).
Module E :=
E.
Definition elt :=
elt.
Definition t :=
t.
Definition In :=
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 Add (
x :
elt) (
s s' :
t) :=
forall y :
elt,
In y s' <->
E.eq y x \/
In y s.
Definition Empty s :=
forall a :
elt, ~
In a s.
Definition For_all (
P :
elt ->
Prop) (
s :
t) :=
forall x :
elt,
In x s ->
P x.
Definition Exists (
P :
elt ->
Prop) (
s :
t) :=
exists x :
elt,
In x s /\
P x.
Definition In_1 :=
eq_In.
Definition eq :=
Equal.
Definition lt :=
lt.
Definition eq_refl :=
eq_refl.
Definition eq_sym :=
eq_sym.
Definition eq_trans :=
eq_trans.
Definition lt_trans :=
lt_trans.
Definition lt_not_eq :=
lt_not_eq.
Definition compare :=
compare.
End NodepOfDep.