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.

Require Import Bool DecidableType DecidableTypeEx OrderedType Morphisms.
Require Export FMapInterface.
Set Implicit Arguments.

Local Ltac Tauto.intuition_solver ::= auto with bool map.

#[global]
Hint Extern 1 (Equivalence _) => constructor; congruence : core.

Facts about weak maps

Module WFacts_fun (E:DecidableType)(Import M:WSfun E).

Notation eq_dec := E.eq_dec.
Definition eqb x y := if eq_dec x y then true else false.

Lemma eq_bool_alt : forall b b', b =b' <-> (b =true <-> b'=true ).

Lemma eq_option_alt : forall (elt:Type)(o o':option elt),
o =o' <-> (forall e, o =Some e <-> o'=Some e ).

Lemma MapsTo_fun : forall (elt:Type) m x (e e':elt),
MapsTo x e m -> MapsTo x e' m -> e =e'.

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.

Lemma mapi_inv : forall m x b (f : key -> elt -> elt'),
MapsTo x b (mapi f m) ->
exists a y , E.eq y x /\ b = f y a /\ MapsTo x a m.

Lemma mapi_1bis : forall m x e (f:key ->elt ->elt'),
(forall x y e, E.eq x y -> f x e = f y e ) ->
MapsTo x e m -> MapsTo x (f x e) (mapi f m).

Lemma mapi_mapsto_iff : forall m x b (f:key ->elt ->elt'),
(forall x y e, E.eq x y -> f x e = f y e ) ->
(MapsTo x b (mapi f m) <-> exists a , b = f x a /\ MapsTo x a m ).

Things are even worse for map2 : we don't try to state any equivalence, see instead boolean results below.

End IffSpec.

Useful tactic for simplifying expressions like In y (add x e (remove z m))

Ltac map_iff :=
repeat (progress (
  rewrite add_mapsto_iff || rewrite add_in_iff ||
  rewrite remove_mapsto_iff || rewrite remove_in_iff ||
  rewrite empty_mapsto_iff || rewrite empty_in_iff ||
  rewrite map_mapsto_iff || rewrite map_in_iff ||
  rewrite mapi_in_iff)).

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.
#[local]
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.
#[local]
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.
#[local]
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.

Lemma map_o : forall m x (f:elt ->elt'),
find x (map f m) = Datatypes.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) = Datatypes.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

Lemma Equal_mapsto_iff : forall m1 m2 : t elt,
Equal m1 m2 <-> (forall k e, MapsTo k e m1 <-> MapsTo k e m2 ).

Relations between Equal, Equiv and Equivb.

First, Equal is Equiv with Leibniz on elements.

Lemma Equal_Equiv : forall (m m' : t elt),
Equal m m' <-> Equiv Logic.eq m m'.

Equivb and Equiv and equivalent when eq_elt and cmp are related.

Section Cmp.
Variable eq_elt : elt ->elt ->Prop.
Variable cmp : elt ->elt ->bool.

Definition compat_cmp :=
forall e e', cmp e e' = true <-> eq_elt e e'.

Lemma Equiv_Equivb : compat_cmp ->
forall m m', Equiv eq_elt m m' <-> Equivb cmp m m'.
End Cmp.

Composition of the two last results: relation between Equal and Equivb.

Lemma Equal_Equivb : forall cmp,
(forall e e', cmp e e' = true <-> e = e') ->
forall (m m':t elt), Equal m m' <-> Equivb cmp m m'.

Lemma Equal_Equivb_eqdec :
forall eq_elt_dec : (forall e e', { e = e' } + { e <> e' }),
let cmp := fun e e' => if eq_elt_dec e e' then true else false in
forall (m m':t elt), Equal m m' <-> Equivb cmp m m'.

End Equalities.

Equal is a setoid equality.

Lemma Equal_refl : forall (elt:Type)(m : t elt), Equal m m.

Lemma Equal_sym : forall (elt:Type)(m m' : t elt),
Equal m m' -> Equal m' m.

Lemma Equal_trans : forall (elt:Type)(m m' m'' : t elt),
Equal m m' -> Equal m' m'' -> Equal m m''.

Definition Equal_ST : forall elt:Type, Equivalence (@Equal elt).

Add Relation key E.eq
reflexivity proved by E.eq_refl
symmetry proved by E.eq_sym
transitivity proved by E.eq_trans
as KeySetoid.

Arguments Equal {elt} m m'.

Add Parametric Relation (elt : Type) : (t elt) Equal
reflexivity proved by (@Equal_refl elt)
symmetry proved by (@Equal_sym elt)
transitivity proved by (@Equal_trans elt)
as EqualSetoid.

Add Parametric Morphism elt : (@In elt)
with signature E.eq ==> Equal ==> iff as In_m.

Add Parametric Morphism elt : (@MapsTo elt)
with signature E.eq ==> eq ==> Equal ==> iff as MapsTo_m.

Add Parametric Morphism elt : (@Empty elt)
with signature Equal ==> iff as Empty_m.

Add Parametric Morphism elt : (@is_empty elt)
with signature Equal ==> eq as is_empty_m.

Add Parametric Morphism elt : (@mem elt)
with signature E.eq ==> Equal ==> eq as mem_m.

Add Parametric Morphism elt : (@find elt)
with signature E.eq ==> Equal ==> eq as find_m.

Add Parametric Morphism elt : (@add elt)
with signature E.eq ==> eq ==> Equal ==> Equal as add_m.

Add Parametric Morphism elt : (@remove elt)
with signature E.eq ==> Equal ==> Equal as remove_m.

Add Parametric Morphism elt elt' : (@map elt elt')
with signature eq ==> Equal ==> Equal as map_m.

Notation not_find_mapsto_iff := not_find_in_iff.

End WFacts_fun.

Same facts for self-contained weak sets and for full maps

Module WFacts (M:WS) := WFacts_fun M.E M.
Module Facts := WFacts.

Additional Properties for weak maps

Results about fold, elements, induction principles...

Module WProperties_fun (E:DecidableType)(M:WSfun E).
Module Import F:=WFacts_fun E M.
Import M.

Section Elt.
  Variable elt:Type.

  Definition Add x (e:elt) m m' := forall y, find y m' = find y (add x e m).

  Lemma Add_transpose_neqkey : forall k1 k2 e1 e2 m1 m2 m3,
    ~ E.eq k1 k2 -> Add k1 e1 m1 m2 -> Add k2 e2 m2 m3 ->
    { m | Add k2 e2 m1 m /\ Add k1 e1 m m3 }.

  Notation eqke := (@eq_key_elt elt).
  Notation eqk := (@eq_key elt).

  Instance eqk_equiv : Equivalence eqk.

  Instance eqke_equiv : Equivalence eqke.

Complements about InA, NoDupA and findA

  Lemma InA_eqke_eqk : forall k1 k2 e1 e2 l,
    E.eq k1 k2 -> InA eqke (k1 ,e1 ) l -> InA eqk (k2 ,e2 ) l.

  Lemma NoDupA_eqk_eqke : forall l, NoDupA eqk l -> NoDupA eqke l.

  Lemma findA_rev : forall l k, NoDupA eqk l ->
    findA (eqb k) l = findA (eqb k) (rev l).

Elements

Lemma elements_Empty : forall m:t elt, Empty m <-> elements m = nil.

Lemma elements_empty : elements (@empty elt) = nil.

Conversions between maps and association lists.

  Definition uncurry {U V W : Type} (f : U -> V -> W) : U *V -> W :=
   fun p => f (fst p) (snd p).

  Definition of_list :=
    List.fold_right (uncurry (@add _)) (empty elt).

  Definition to_list := elements.

  Lemma of_list_1 : forall l k e,
    NoDupA eqk l ->
    (MapsTo k e (of_list l) <-> InA eqke (k ,e ) l ).

  Lemma of_list_1b : forall l k,
    NoDupA eqk l ->
    find k (of_list l) = findA (eqb k) l.

  Lemma of_list_2 : forall l, NoDupA eqk l ->
    equivlistA eqke l (to_list (of_list l)).

  Lemma of_list_3 : forall s, Equal (of_list (to_list s)) s.

Fold

Alternative specification via fold_right

Lemma fold_spec_right m (A:Type)(i:A)(f : key -> elt -> A -> A) :
fold f m i = List.fold_right (uncurry f) i (rev (elements m)).

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.

  Lemma fold_rec :
    forall (A:Type)(P : t elt -> A -> Type)(f : key -> elt -> A -> A),
     forall (i:A)(m:t elt),
      (forall m, Empty m -> P m i ) ->
      (forall k e a m' m'', MapsTo k e m -> ~In k m' ->
         Add k e m' m'' -> P m' a -> P m'' (f k e a)) ->
      P m (fold f m i).

Same, with empty and add instead of Empty and Add. In this case, P must be compatible with equality of sets

  Theorem fold_rec_bis :
    forall (A:Type)(P : t elt -> A -> Type)(f : key -> elt -> A -> A),
     forall (i:A)(m:t elt),
     (forall m m' a, Equal m m' -> P m a -> P m' a ) ->
     (P (empty _) i ) ->
     (forall k e a m', MapsTo k e m -> ~In k m' ->
       P m' a -> P (add k e m') (f k e a)) ->
     P m (fold f m i).

  Lemma fold_rec_nodep :
    forall (A:Type)(P : A -> Type)(f : key -> elt -> A -> A)(i:A)(m:t elt),
     P i -> (forall k e a, MapsTo k e m -> P a -> P (f k e a)) ->
     P (fold f m i).

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.

  Lemma fold_rec_weak :
    forall (A:Type)(P : t elt -> A -> Type)(f : key -> elt -> A -> A)(i:A),
    (forall m m' a, Equal m m' -> P m a -> P m' a ) ->
    P (empty _) i ->
    (forall k e a m, ~In k m -> P m a -> P (add k e m) (f k e a)) ->
    forall m, P m (fold f m i).

  Lemma fold_rel :
    forall (A B:Type)(R : A -> B -> Type)
     (f : key -> elt -> A -> A)(g : key -> elt -> B -> B)(i : A)(j : B)
     (m : t elt),
     R i j ->
     (forall k e a b, MapsTo k e m -> R a b -> R (f k e a) (g k e b)) ->
     R (fold f m i) (fold g m j).

From the induction principle on fold, we can deduce some general induction principles on maps.

  Lemma map_induction :
   forall P : t elt -> Type,
   (forall m, Empty m -> P m ) ->
   (forall m m', P m -> forall x e, ~In x m -> Add x e m m' -> P m') ->
   forall m, P m.

  Lemma map_induction_bis :
   forall P : t elt -> Type,
   (forall m m', Equal m m' -> P m -> P m') ->
   P (empty _) ->
   (forall x e m, ~In x m -> P m -> P (add x e m)) ->
   forall m, P m.

fold can be used to reconstruct the same initial set.

Lemma fold_identity : forall m : t elt, Equal (fold (@add _) m (empty _)) m.

Section Fold_More.

Additional properties of fold

When a function f is compatible and allows transpositions, we can compute fold f in any order.

Variables (A:Type)(eqA:A ->A ->Prop)(st:Equivalence eqA)(f:key ->elt ->A ->A).

This is more convenient than a compat_op eqke .... In fact, every compat_op, compat_bool, etc, should become a Proper someday.

  Hypothesis Comp : Proper (E.eq ==>eq ==>eqA ==>eqA) f.

  Lemma fold_init :
   forall m i i', eqA i i' -> eqA (fold f m i) (fold f m i').

  Lemma fold_Empty :
   forall m i, Empty m -> eqA (fold f m i) i.

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.

  Definition transpose_neqkey :=
    forall k k' e e' a, ~E.eq k k' ->
      eqA (f k e (f k' e' a)) (f k' e' (f k e a)).

  Hypothesis Tra : transpose_neqkey.

  Lemma fold_commutes : forall i m k e, ~In k m ->
   eqA (fold f m (f k e i)) (f k e (fold f m i)).

  #[local]
  Hint Resolve NoDupA_eqk_eqke NoDupA_rev elements_3w : map.

  Lemma fold_Equal : forall m1 m2 i, Equal m1 m2 ->
   eqA (fold f m1 i) (fold f m2 i).

  Lemma fold_Equal2 : forall m1 m2 i j, Equal m1 m2 -> eqA i j ->
    eqA (fold f m1 i) (fold f m2 j).

  Lemma fold_Add : forall m1 m2 k e i, ~In k m1 -> Add k e m1 m2 ->
   eqA (fold f m2 i) (f k e (fold f m1 i)).

  Lemma fold_add : forall m k e i, ~In k m ->
   eqA (fold f (add k e m) i) (f k e (fold f m i)).

  End Fold_More.

Cardinal

  Lemma cardinal_fold : forall m : t elt,
   cardinal m = fold (fun _ _ => S) m 0.

  Lemma cardinal_Empty : forall m : t elt,
   Empty m <-> cardinal m = 0.

  Lemma Equal_cardinal : forall m m' : t elt,
    Equal m m' -> cardinal m = cardinal m'.

  Lemma cardinal_1 : forall m : t elt, Empty m -> cardinal m = 0.

  Lemma cardinal_2 :
    forall m m' x e, ~ In x m -> Add x e m m' -> cardinal m' = S (cardinal m).

  Lemma cardinal_Add_In:
    forall m m' x e, In x m -> Add x e m m' -> cardinal m' = cardinal m.

  Lemma cardinal_inv_1 : forall m : t elt,
   cardinal m = 0 -> Empty m.
  #[local]
  Hint Resolve cardinal_inv_1 : map.

  Lemma cardinal_inv_2 :
   forall m n, cardinal m = S n -> { p : key *elt | MapsTo (fst p) (snd p) m }.

  Lemma cardinal_inv_2b :
   forall m, cardinal m <> 0 -> { p : key *elt | MapsTo (fst p) (snd p) m }.

Additional notions over maps

  Definition Disjoint (m m' : t elt) :=
   forall k, ~(In k m /\ In k m').

  Definition Partition (m m1 m2 : t elt) :=
    Disjoint m1 m2 /\
    (forall k e, MapsTo k e m <-> MapsTo k e m1 \/ MapsTo k e m2 ).

Emulation of some functions lacking in the interface

  Definition filter (f : key -> elt -> bool)(m : t elt) :=
   fold (fun k e m => if f k e then add k e m else m) m (empty _).

  Definition for_all (f : key -> elt -> bool)(m : t elt) :=
   fold (fun k e b => if f k e then b else false) m true.

  Definition exists_ (f : key -> elt -> bool)(m : t elt) :=
   fold (fun k e b => if f k e then true else b) m false.

  Definition partition (f : key -> elt -> bool)(m : t elt) :=
   (filter f m , filter (fun k e => negb (f k e)) m ).

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.

Definition update (m1 m2 : t elt) := fold (@add _) m2 m1.

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.

Definition restrict (m1 m2 : t elt) := filter (fun k _ => mem k m2) m1.

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)

  Definition filter_dom (f : key -> bool) := filter (fun k _ => f k).
  Definition filter_range (f : elt -> bool) := filter (fun _ => f).
  Definition for_all_dom (f : key -> bool) := for_all (fun k _ => f k).
  Definition for_all_range (f : elt -> bool) := for_all (fun _ => f).
  Definition exists_dom (f : key -> bool) := exists_ (fun k _ => f k).
  Definition exists_range (f : elt -> bool) := exists_ (fun _ => f).
  Definition partition_dom (f : key -> bool) := partition (fun k _ => f k).
  Definition partition_range (f : elt -> bool) := partition (fun _ => f).

End Elt.

Add Parametric Morphism elt : (@cardinal elt)
   with signature Equal ==> eq as cardinal_m.

Add Parametric Morphism elt : (@Disjoint elt)
   with signature Equal ==> Equal ==> iff as Disjoint_m.

Add Parametric Morphism elt : (@Partition elt)
   with signature Equal ==> Equal ==> Equal ==> iff as Partition_m.

Add Parametric Morphism elt : (@update elt)
   with signature Equal ==> Equal ==> Equal as update_m.

Add Parametric Morphism elt : (@restrict elt)
   with signature Equal ==> Equal ==> Equal as restrict_m.

Add Parametric Morphism elt : (@diff elt)
   with signature Equal ==> Equal ==> Equal as diff_m.

End WProperties_fun.

Same Properties for self-contained weak maps and for full maps

Module WProperties (M:WS) := WProperties_fun M.E M.
Module Properties := WProperties.

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).

  #[local]
  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 additional hypothesis (some transpose fact).

  Lemma fold_Equal : forall m1 m2 (A:Type)(eqA:A ->A ->Prop)(st:Equivalence eqA)
   (f:key ->elt ->A ->A)(i:A),
   Proper (E.eq ==>eq ==>eqA ==>eqA) f ->
   Equal m1 m2 ->
   eqA (fold f m1 i) (fold f m2 i).

  Lemma fold_Add_Above : forall m1 m2 x e (A:Type)(eqA:A ->A ->Prop)(st:Equivalence eqA)
   (f:key ->elt ->A ->A)(i:A) (P:Proper (E.eq ==>eq ==>eqA ==>eqA) f),
   Above x m1 -> Add x e m1 m2 ->
   eqA (fold f m2 i) (f x e (fold f m1 i)).

  Lemma fold_Add_Below : forall m1 m2 x e (A:Type)(eqA:A ->A ->Prop)(st:Equivalence eqA)
   (f:key ->elt ->A ->A)(i:A) (P:Proper (E.eq ==>eq ==>eqA ==>eqA) f),
   Below x m1 -> Add x e m1 m2 ->
   eqA (fold f m2 i) (fold f m1 (f x e i)).

  End Fold_properties.

End Elt.

End OrdProperties.