Library Coq.FSets.FMapFacts
Finite maps library
This functor derives additional facts from
FMapInterface.S. These
facts are mainly the specifications of
FMapInterface.S written using
different styles: equivalence and boolean equalities.
Specifications written using equivalences
Section IffSpec.
Variable elt elt' elt'':
Type.
Implicit Type m:
t elt.
Implicit Type x y z:
key.
Implicit Type e:
elt.
Lemma In_iff :
forall m x y,
E.eq x y -> (
In x m <-> In y m).
Lemma MapsTo_iff :
forall m x y e,
E.eq x y -> (
MapsTo x e m <-> MapsTo y e m).
Lemma mem_in_iff :
forall m x,
In x m <-> mem x m = true.
Lemma not_mem_in_iff :
forall m x,
~In x m <-> mem x m = false.
Lemma In_dec :
forall m x,
{ In x m } + { ~ In x m }.
Lemma find_mapsto_iff :
forall m x e,
MapsTo x e m <-> find x m = Some e.
Lemma not_find_in_iff :
forall m x,
~In x m <-> find x m = None.
Lemma in_find_iff :
forall m x,
In x m <-> find x m <> None.
Lemma equal_iff :
forall m m' cmp,
Equivb cmp m m' <-> equal cmp m m' = true.
Lemma empty_mapsto_iff :
forall x e,
MapsTo x e (
empty elt)
<-> False.
Lemma empty_in_iff :
forall x,
In x (
empty elt)
<-> False.
Lemma is_empty_iff :
forall m,
Empty m <-> is_empty m = true.
Lemma add_mapsto_iff :
forall m x y e e',
MapsTo y e' (
add x e m)
<->
(E.eq x y /\ e=e') \/
(~E.eq x y /\ MapsTo y e' m).
Lemma add_in_iff :
forall m x y e,
In y (
add x e m)
<-> E.eq x y \/ In y m.
Lemma add_neq_mapsto_iff :
forall m x y e e',
~ E.eq x y -> (
MapsTo y e' (
add x e m)
<-> MapsTo y e' m).
Lemma add_neq_in_iff :
forall m x y e,
~ E.eq x y -> (
In y (
add x e m)
<-> In y m).
Lemma remove_mapsto_iff :
forall m x y e,
MapsTo y e (
remove x m)
<-> ~E.eq x y /\ MapsTo y e m.
Lemma remove_in_iff :
forall m x y,
In y (
remove x m)
<-> ~E.eq x y /\ In y m.
Lemma remove_neq_mapsto_iff :
forall m x y e,
~ E.eq x y -> (
MapsTo y e (
remove x m)
<-> MapsTo y e m).
Lemma remove_neq_in_iff :
forall m x y,
~ E.eq x y -> (
In y (
remove x m)
<-> In y m).
Lemma elements_mapsto_iff :
forall m x e,
MapsTo x e m <-> InA (@
eq_key_elt _)
(x,e) (
elements m).
Lemma elements_in_iff :
forall m x,
In x m <-> exists e, InA (@
eq_key_elt _)
(x,e) (
elements m).
Lemma map_mapsto_iff :
forall m x b (
f :
elt ->
elt'),
MapsTo x b (
map f m)
<-> exists a, b = f a /\ MapsTo x a m.
Lemma map_in_iff :
forall m x (
f :
elt ->
elt'),
In x (
map f m)
<-> In x m.
Lemma mapi_in_iff :
forall m x (
f:
key->
elt->
elt'),
In x (
mapi f m)
<-> In x m.
Unfortunately, we don't have simple equivalences for mapi
and MapsTo. The only correct one needs compatibility of f.
Things are even worse for map2 : we don't try to state any
equivalence, see instead boolean results below.
Useful tactic for simplifying expressions like In y (add x e (remove z m))
Specifications written using boolean predicates
Section BoolSpec.
Lemma mem_find_b :
forall (
elt:
Type)(
m:
t elt)(
x:
key),
mem x m = if find x m then true else false.
Variable elt elt' elt'' :
Type.
Implicit Types m :
t elt.
Implicit Types x y z :
key.
Implicit Types e :
elt.
Lemma mem_b :
forall m x y,
E.eq x y ->
mem x m = mem y m.
Lemma find_o :
forall m x y,
E.eq x y ->
find x m = find y m.
Lemma empty_o :
forall x,
find x (
empty elt)
= None.
Lemma empty_a :
forall x,
mem x (
empty elt)
= false.
Lemma add_eq_o :
forall m x y e,
E.eq x y ->
find y (
add x e m)
= Some e.
Lemma add_neq_o :
forall m x y e,
~ E.eq x y ->
find y (
add x e m)
= find y m.
Hint Resolve add_neq_o :
map.
Lemma add_o :
forall m x y e,
find y (
add x e m)
= if eq_dec x y then Some e else find y m.
Lemma add_eq_b :
forall m x y e,
E.eq x y ->
mem y (
add x e m)
= true.
Lemma add_neq_b :
forall m x y e,
~E.eq x y ->
mem y (
add x e m)
= mem y m.
Lemma add_b :
forall m x y e,
mem y (
add x e m)
= eqb x y || mem y m.
Lemma remove_eq_o :
forall m x y,
E.eq x y ->
find y (
remove x m)
= None.
Hint Resolve remove_eq_o :
map.
Lemma remove_neq_o :
forall m x y,
~ E.eq x y ->
find y (
remove x m)
= find y m.
Hint Resolve remove_neq_o :
map.
Lemma remove_o :
forall m x y,
find y (
remove x m)
= if eq_dec x y then None else find y m.
Lemma remove_eq_b :
forall m x y,
E.eq x y ->
mem y (
remove x m)
= false.
Lemma remove_neq_b :
forall m x y,
~ E.eq x y ->
mem y (
remove x m)
= mem y m.
Lemma remove_b :
forall m x y,
mem y (
remove x m)
= negb (
eqb x y)
&& mem y m.
Definition option_map (
A B:
Type)(
f:
A->
B)(
o:
option A) :
option B :=
match o with
|
Some a =>
Some (
f a)
|
None =>
None
end.
Lemma map_o :
forall m x (
f:
elt->
elt'),
find x (
map f m)
= option_map f (
find x m).
Lemma map_b :
forall m x (
f:
elt->
elt'),
mem x (
map f m)
= mem x m.
Lemma mapi_b :
forall m x (
f:
key->
elt->
elt'),
mem x (
mapi f m)
= mem x m.
Lemma mapi_o :
forall m x (
f:
key->
elt->
elt'),
(
forall x y e,
E.eq x y ->
f x e = f y e) ->
find x (
mapi f m)
= option_map (
f x) (
find x m).
Lemma map2_1bis :
forall (
m:
t elt)(
m':
t elt')
x
(
f:
option elt->
option elt'->
option elt''),
f None None = None ->
find x (
map2 f m m')
= f (
find x m) (
find x m').
Lemma elements_o :
forall m x,
find x m = findA (
eqb x) (
elements m).
Lemma elements_b :
forall m x,
mem x m = existsb (
fun p =>
eqb x (
fst p)) (
elements m).
End BoolSpec.
Section Equalities.
Variable elt:
Type.
Another characterisation of Equal
Relations between Equal, Equiv and Equivb.
First,
Equal is
Equiv with Leibniz on elements.
Equivb and Equiv and equivalent when eq_elt and cmp
are related.
Composition of the two last results: relation between Equal
and Equivb.
Equal is a setoid equality.
Same facts for self-contained weak sets and for full maps
Additional Properties for weak maps
Results about
fold,
elements, induction principles...
Complements about InA, NoDupA and findA
Conversions between maps and association lists.
Fold
Alternative specification via
fold_right
Induction principles about fold contributed by S. Lescuyer
In the following lemma, the step hypothesis is deliberately restricted
to the precise map m we are considering.
Same, with empty and add instead of Empty and Add. In this
case, P must be compatible with equality of sets
fold_rec_weak is a weaker principle than fold_rec_bis :
the step hypothesis must here be applicable anywhere.
At the same time, it looks more like an induction principle,
and hence can be easier to use.
From the induction principle on fold, we can deduce some general
induction principles on maps.
fold can be used to reconstruct the same initial set.
Additional properties of fold
When a function
f is compatible and allows transpositions, we can
compute
fold f in any order.
This is more convenient than a compat_op eqke ....
In fact, every compat_op, compat_bool, etc, should
become a Proper someday.
As noticed by P. Casteran, asking for the general
SetoidList.transpose
here is too restrictive. Think for instance of
f being
M.add :
in general,
M.add k e (M.add k e' m) is not equivalent to
M.add k e' (M.add k e m). Fortunately, we will never encounter this
situation during a real
fold, since the keys received by this
fold
are unique. Hence we can ask the transposition property to hold only
for non-equal keys.
This idea could be push slightly further, by asking the transposition
property to hold only for (non-equal) keys living in the map given to
fold. Please contact us if you need such a version.
FSets could also benefit from a restricted
transpose, but for this
case the gain is unclear.
Additional notions over maps
Emulation of some functions lacking in the interface
update adds to m1 all the bindings of m2. It can be seen as
an union operator which gives priority to its 2nd argument
in case of binding conflit.
restrict keeps from m1 only the bindings whose key is in m2.
It can be seen as an inter operator, with priority to its 1st argument
in case of binding conflit.
diff erases from m1 all bindings whose key is in m2.
Definition diff (
m1 m2 :
t elt) :=
filter (
fun k _ =>
negb (
mem k m2))
m1.
Section Specs.
Variable f :
key ->
elt ->
bool.
Hypothesis Hf :
Proper (
E.eq==>eq==>eq)
f.
Lemma filter_iff :
forall m k e,
MapsTo k e (
filter f m)
<-> MapsTo k e m /\ f k e = true.
Lemma for_all_iff :
forall m,
for_all f m = true <-> (forall k e,
MapsTo k e m ->
f k e = true).
Lemma exists_iff :
forall m,
exists_ f m = true <->
(exists p, MapsTo (
fst p) (
snd p)
m /\ f (
fst p) (
snd p)
= true).
End Specs.
Lemma Disjoint_alt :
forall m m',
Disjoint m m' <->
(forall k e e',
MapsTo k e m ->
MapsTo k e' m' ->
False).
Section Partition.
Variable f :
key ->
elt ->
bool.
Hypothesis Hf :
Proper (
E.eq==>eq==>eq)
f.
Lemma partition_iff_1 :
forall m m1 k e,
m1 = fst (
partition f m) ->
(
MapsTo k e m1 <-> MapsTo k e m /\ f k e = true).
Lemma partition_iff_2 :
forall m m2 k e,
m2 = snd (
partition f m) ->
(
MapsTo k e m2 <-> MapsTo k e m /\ f k e = false).
Lemma partition_Partition :
forall m m1 m2,
partition f m = (m1,m2) ->
Partition m m1 m2.
End Partition.
Lemma Partition_In :
forall m m1 m2 k,
Partition m m1 m2 ->
In k m ->
{In k m1}+{In k m2}.
Lemma Disjoint_sym :
forall m1 m2,
Disjoint m1 m2 ->
Disjoint m2 m1.
Lemma Partition_sym :
forall m m1 m2,
Partition m m1 m2 ->
Partition m m2 m1.
Lemma Partition_Empty :
forall m m1 m2,
Partition m m1 m2 ->
(
Empty m <-> (Empty m1 /\ Empty m2)).
Lemma Partition_Add :
forall m m' x e ,
~In x m ->
Add x e m m' ->
forall m1 m2,
Partition m' m1 m2 ->
exists m3, (Add x e m3 m1 /\ Partition m m3 m2 \/
Add x e m3 m2 /\ Partition m m1 m3).
Lemma Partition_fold :
forall (
A:
Type)(
eqA:
A->
A->
Prop)(
st:
Equivalence eqA)(
f:
key->
elt->
A->
A),
Proper (
E.eq==>eq==>eqA==>eqA)
f ->
transpose_neqkey eqA f ->
forall m m1 m2 i,
Partition m m1 m2 ->
eqA (
fold f m i) (
fold f m1 (
fold f m2 i)).
Lemma Partition_cardinal :
forall m m1 m2,
Partition m m1 m2 ->
cardinal m = cardinal m1 + cardinal m2.
Lemma Partition_partition :
forall m m1 m2,
Partition m m1 m2 ->
let f :=
fun k (
_:
elt) =>
mem k m1 in
Equal m1 (
fst (
partition f m))
/\ Equal m2 (
snd (
partition f m)).
Lemma update_mapsto_iff :
forall m m' k e,
MapsTo k e (
update m m')
<->
(MapsTo k e m' \/ (MapsTo k e m /\ ~In k m')).
Lemma update_dec :
forall m m' k e,
MapsTo k e (
update m m') ->
{ MapsTo k e m' } + { MapsTo k e m /\ ~In k m'}.
Lemma update_in_iff :
forall m m' k,
In k (
update m m')
<-> In k m \/ In k m'.
Lemma diff_mapsto_iff :
forall m m' k e,
MapsTo k e (
diff m m')
<-> MapsTo k e m /\ ~In k m'.
Lemma diff_in_iff :
forall m m' k,
In k (
diff m m')
<-> In k m /\ ~In k m'.
Lemma restrict_mapsto_iff :
forall m m' k e,
MapsTo k e (
restrict m m')
<-> MapsTo k e m /\ In k m'.
Lemma restrict_in_iff :
forall m m' k,
In k (
restrict m m')
<-> In k m /\ In k m'.
specialized versions analyzing only keys (resp. elements)
Same Properties for self-contained weak maps and for full maps
Properties specific to maps with ordered keys
Module OrdProperties (
M:
S).
Module Import ME :=
OrderedTypeFacts M.E.
Module Import O:=
KeyOrderedType M.E.
Module Import P:=
Properties M.
Import F.
Import M.
Section Elt.
Variable elt:
Type.
Notation eqke := (@
eqke elt).
Notation eqk := (@
eqk elt).
Notation ltk := (@
ltk elt).
Notation cardinal := (@
cardinal elt).
Notation Equal := (@
Equal elt).
Notation Add := (@
Add elt).
Definition Above x (
m:
t elt) :=
forall y,
In y m ->
E.lt y x.
Definition Below x (
m:
t elt) :=
forall y,
In y m ->
E.lt x y.
Section Elements.
Lemma sort_equivlistA_eqlistA :
forall l l' :
list (
key*elt),
sort ltk l ->
sort ltk l' ->
equivlistA eqke l l' ->
eqlistA eqke l l'.
Ltac clean_eauto :=
unfold O.eqke,
O.ltk;
simpl;
intuition;
eauto.
Definition gtb (
p p':
key*elt) :=
match E.compare (
fst p) (
fst p')
with GT _ =>
true |
_ =>
false end.
Definition leb p :=
fun p' =>
negb (
gtb p p').
Definition elements_lt p m :=
List.filter (
gtb p) (
elements m).
Definition elements_ge p m :=
List.filter (
leb p) (
elements m).
Lemma gtb_1 :
forall p p',
gtb p p' = true <-> ltk p' p.
Lemma leb_1 :
forall p p',
leb p p' = true <-> ~ltk p' p.
Lemma gtb_compat :
forall p,
Proper (
eqke==>eq) (
gtb p).
Lemma leb_compat :
forall p,
Proper (
eqke==>eq) (
leb p).
Hint Resolve gtb_compat leb_compat elements_3 :
map.
Lemma elements_split :
forall p m,
elements m = elements_lt p m ++ elements_ge p m.
Lemma elements_Add :
forall m m' x e,
~In x m ->
Add x e m m' ->
eqlistA eqke (
elements m')
(
elements_lt (x,e) m ++ (x,e):: elements_ge (x,e) m).
Lemma elements_Add_Above :
forall m m' x e,
Above x m ->
Add x e m m' ->
eqlistA eqke (
elements m') (
elements m ++ (x,e)::nil).
Lemma elements_Add_Below :
forall m m' x e,
Below x m ->
Add x e m m' ->
eqlistA eqke (
elements m') (
(x,e)::elements m).
Lemma elements_Equal_eqlistA :
forall (
m m':
t elt),
Equal m m' ->
eqlistA eqke (
elements m) (
elements m').
End Elements.
Section Min_Max_Elt.
We emulate two max_elt and min_elt functions.
Fixpoint max_elt_aux (
l:
list (
key*elt)) :=
match l with
|
nil =>
None
|
(x,e)::nil =>
Some (x,e)
|
(x,e)::l =>
max_elt_aux l
end.
Definition max_elt m :=
max_elt_aux (
elements m).
Lemma max_elt_Above :
forall m x e,
max_elt m = Some (x,e) ->
Above x (
remove x m).
Lemma max_elt_MapsTo :
forall m x e,
max_elt m = Some (x,e) ->
MapsTo x e m.
Lemma max_elt_Empty :
forall m,
max_elt m = None ->
Empty m.
Definition min_elt m :
option (
key*elt) :=
match elements m with
|
nil =>
None
|
(x,e)::_ =>
Some (x,e)
end.
Lemma min_elt_Below :
forall m x e,
min_elt m = Some (x,e) ->
Below x (
remove x m).
Lemma min_elt_MapsTo :
forall m x e,
min_elt m = Some (x,e) ->
MapsTo x e m.
Lemma min_elt_Empty :
forall m,
min_elt m = None ->
Empty m.
End Min_Max_Elt.
Section Induction_Principles.
Lemma map_induction_max :
forall P :
t elt ->
Type,
(
forall m,
Empty m ->
P m) ->
(
forall m m',
P m ->
forall x e,
Above x m ->
Add x e m m' ->
P m') ->
forall m,
P m.
Lemma map_induction_min :
forall P :
t elt ->
Type,
(
forall m,
Empty m ->
P m) ->
(
forall m m',
P m ->
forall x e,
Below x m ->
Add x e m m' ->
P m') ->
forall m,
P m.
End Induction_Principles.
Section Fold_properties.
The following lemma has already been proved on Weak Maps,
but with one additionnal hypothesis (some transpose fact).