Some suggestions about FMap by P. Casteran:

 - clarifications about Equality on maps
   Caveat: name change, what used to be Equal is now Equivb
 - the prefered equality predicate (the new Equal) is declared 
   a setoid equality, along with several morphisms 
 - beginning of a filter/for_all/exists_/partition section in FMapFacts



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10608 85f007b7-540e-0410-9357-904b9bb8a0f7

7 files changed, 464 insertions, 101 deletions

diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index 974e9d1ae3..af3cdb8018 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -1167,7 +1167,7 @@ Qed.
 
 (** * Comparison *)
 
-Definition Equal (cmp:elt->elt->bool) m m' := 
+Definition Equivb (cmp:elt->elt->bool) m m' := 
   (forall k, In k m <-> In k m') /\ 
   (forall k e e', MapsTo k e m -> MapsTo k e' m' -> cmp e e' = true).  
 
@@ -1346,7 +1346,7 @@ Defined.
 Definition equal (cmp: elt -> elt -> bool) s s' := 
  equal_aux cmp (cons s End, cons s' End).
 
-Lemma equal_aux_Equal : forall cmp e, sorted_e e#1 -> sorted_e e#2 ->
+Lemma equal_aux_Equivb : forall cmp e, sorted_e e#1 -> sorted_e e#2 ->
  (equal_aux cmp e = L.equal cmp (flatten_e e#1) (flatten_e e#2)).
 Proof.
  intros cmp e; functional induction equal_aux cmp e; intros; clearf;
@@ -1359,10 +1359,10 @@ Proof.
  rewrite <- H11, <- H13; auto.
 Qed.
 
-Lemma Equal_elements : forall cmp s s', 
- Equal cmp s s' <-> L.Equal cmp (elements s) (elements s').
+Lemma Equivb_elements : forall cmp s s', 
+ Equivb cmp s s' <-> L.Equivb cmp (elements s) (elements s').
 Proof.
-unfold Equal, L.Equal; split; split; intros.
+unfold Equivb, L.Equivb; split; split; intros.
 do 2 rewrite elements_in; firstorder.
 destruct H.
 apply (H2 k); rewrite <- elements_mapsto; auto.
@@ -1371,16 +1371,16 @@ destruct H.
 apply (H2 k); unfold L.PX.MapsTo; rewrite elements_mapsto; auto.
 Qed.
 
-Lemma equal_Equal : forall cmp s s', bst s -> bst s' -> 
- (equal cmp s s' = true <-> Equal cmp s s').
+Lemma equal_Equivb : forall cmp s s', bst s -> bst s' -> 
+ (equal cmp s s' = true <-> Equivb cmp s s').
 Proof.
  intros; unfold equal.
  destruct (@cons_1 s End); auto.
  inversion 2.
  destruct (@cons_1 s' End); auto.
  inversion 2.
- rewrite equal_aux_Equal; simpl; auto.
- rewrite Equal_elements.
+ rewrite equal_aux_Equivb; simpl; auto.
+ rewrite Equivb_elements.
  rewrite H2, H4.
  simpl; do 2 rewrite <- app_nil_end.
  split; [apply L.equal_2|apply L.equal_1]; auto.
@@ -1783,31 +1783,33 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Lemma cardinal_1 : forall m, cardinal m = length (elements m).
  Proof. intro m; exact (@Raw.elements_cardinal elt m.(this)). Qed.
 
- Definition Equal cmp m m' := 
+ Definition Equal m m' := forall y, find y m = find y m'.
+ Definition Equiv (eq_elt:elt->elt->Prop) m m' := 
    (forall k, In k m <-> In k m') /\ 
-   (forall k e e', MapsTo k e m -> MapsTo k e' m' -> cmp e e' = true).  
+   (forall k e e', MapsTo k e m -> MapsTo k e' m' -> eq_elt e e').
+ Definition Equivb cmp := Equiv (Cmp cmp).
 
- Lemma Equal_Equal : forall cmp m m', Equal cmp m m' <-> Raw.Equal cmp m m'.
+ Lemma Equivb_Equivb : forall cmp m m', Equivb cmp m m' <-> Raw.Equivb cmp m m'.
  Proof. 
- intros; unfold Equal, Raw.Equal, In; intuition.
+ intros; unfold Equivb, Equiv, Raw.Equivb, In; intuition.
  generalize (H0 k); do 2 rewrite Raw.In_alt; intuition.
  generalize (H0 k); do 2 rewrite Raw.In_alt; intuition.
  generalize (H0 k); do 2 rewrite <- Raw.In_alt; intuition.
  generalize (H0 k); do 2 rewrite <- Raw.In_alt; intuition.
- Qed. 
+ Qed.
 
  Lemma equal_1 : forall m m' cmp, 
-   Equal cmp m m' -> equal cmp m m' = true. 
+   Equivb cmp m m' -> equal cmp m m' = true. 
  Proof. 
- unfold equal; intros (m,b,a) (m',b',a') cmp; rewrite Equal_Equal; 
-  intros; simpl in *; rewrite Raw.equal_Equal; auto.
+ unfold equal; intros (m,b,a) (m',b',a') cmp; rewrite Equivb_Equivb; 
+  intros; simpl in *; rewrite Raw.equal_Equivb; auto.
  Qed. 
 
  Lemma equal_2 : forall m m' cmp, 
-   equal cmp m m' = true -> Equal cmp m m'.
+   equal cmp m m' = true -> Equivb cmp m m'.
  Proof. 
- unfold equal; intros (m,b,a) (m',b',a') cmp; rewrite Equal_Equal; 
-  intros; simpl in *; rewrite <-Raw.equal_Equal; auto.
+ unfold equal; intros (m,b,a) (m',b',a') cmp; rewrite Equivb_Equivb; 
+  intros; simpl in *; rewrite <-Raw.equal_Equivb; auto.
  Qed.  
 
  End Elt.
@@ -1965,23 +1967,23 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
     rewrite H0, H2, <-app_nil_end, <-app_nil_end in *; auto.
   Defined.
 
-  Lemma eq_1 : forall m m', Equal cmp m m' -> eq m m'.
+  Lemma eq_1 : forall m m', Equivb cmp m m' -> eq m m'.
   Proof.
   intros m m'.
   unfold eq.
-  rewrite Equal_Equal.
-  rewrite Raw.Equal_elements.
+  rewrite Equivb_Equivb.
+  rewrite Raw.Equivb_elements.
   intros.
   apply LO.eq_1.
   auto.
   Qed.
 
-  Lemma eq_2 : forall m m', eq m m' -> Equal cmp m m'.
+  Lemma eq_2 : forall m m', eq m m' -> Equivb cmp m m'.
   Proof.
   intros m m'.
   unfold eq.
-  rewrite Equal_Equal.
-  rewrite Raw.Equal_elements.
+  rewrite Equivb_Equivb.
+  rewrite Raw.Equivb_elements.
   intros.
   generalize (LO.eq_2 H).
   auto.
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 64702b6870..aecc043e06 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -27,6 +27,11 @@ Module WFacts (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).
+Proof.
+ destruct b; destruct b'; intuition.
+Qed.
+
 Lemma MapsTo_fun : forall (elt:Set) m x (e e':elt), 
   MapsTo x e m -> MapsTo x e' m -> e=e'.
 Proof.
@@ -43,11 +48,6 @@ Implicit Type m: t elt.
 Implicit Type x y z: key.
 Implicit Type e: elt.
 
-Lemma MapsTo_iff : forall m x y e, E.eq x y -> (MapsTo x e m <-> MapsTo y e m).
-Proof.
-split; apply MapsTo_1; auto.
-Qed.
-
 Lemma In_iff : forall m x y, E.eq x y -> (In x m <-> In y m).
 Proof.
 unfold In.
@@ -56,12 +56,34 @@ apply (MapsTo_1 H H0); auto.
 apply (MapsTo_1 (E.eq_sym H) H0); auto.
 Qed.
 
+Lemma MapsTo_iff : forall m x y e, E.eq x y -> (MapsTo x e m <-> MapsTo y e m).
+Proof.
+split; apply MapsTo_1; auto.
+Qed.
+
+Lemma mem_in_iff : forall m x, In x m <-> mem x m = true.
+Proof.
+split; [apply mem_1|apply mem_2].
+Qed.
+
+Lemma not_mem_in_iff : forall m x, ~In x m <-> mem x m = false.
+Proof.
+intros; rewrite mem_in_iff; destruct (mem x m); intuition.
+Qed.
+
+Lemma In_dec : forall m x, { In x m } + { ~ In x m }.
+Proof.
+ intros.
+ generalize (mem_in_iff m x).
+ destruct (mem x m); [left|right]; intuition.
+Qed.
+
 Lemma find_mapsto_iff : forall m x e, MapsTo x e m <-> find x m = Some e.
 Proof.
 split; [apply find_1|apply find_2].
 Qed.
 
-Lemma not_find_mapsto_iff : forall m x, ~In x m <-> find x m = None.
+Lemma not_find_in_iff : forall m x, ~In x m <-> find x m = None.
 Proof.
 intros.
 generalize (find_mapsto_iff m x); destruct (find x m).
@@ -73,17 +95,13 @@ intros; intros (e,H1).
 rewrite H in H1; discriminate.
 Qed.
 
-Lemma mem_in_iff : forall m x, In x m <-> mem x m = true.
-Proof.
-split; [apply mem_1|apply mem_2].
-Qed.
-
-Lemma not_mem_in_iff : forall m x, ~In x m <-> mem x m = false.
+Lemma in_find_iff : forall m x, In x m <-> find x m <> None.
 Proof.
-intros; rewrite mem_in_iff; destruct (mem x m); intuition.
+intros; rewrite <- not_find_in_iff, mem_in_iff.
+destruct mem; intuition.
 Qed.
 
-Lemma equal_iff : forall m m' cmp, Equal cmp m m' <-> equal cmp m m' = true.
+Lemma equal_iff : forall m m' cmp, Equivb cmp m m' <-> equal cmp m m' = true.
 Proof. 
 split; [apply equal_1|apply equal_2].
 Qed.
@@ -550,6 +568,177 @@ Qed.
 
 End BoolSpec.
 
+Section Equalities. 
+
+Variable elt:Set.
+
+(** * 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 elt) m m'.
+Proof.
+ unfold Equal, Equiv; split; intros.
+ split; intros.
+ rewrite in_find_iff, in_find_iff, H; intuition.
+ rewrite find_mapsto_iff in H0,H1; congruence.
+ destruct H.
+ narrow H with y.
+ narrow H0 with y.
+ do 2 rewrite in_find_iff in H.
+ generalize (find_mapsto_iff m y)(find_mapsto_iff m' y).
+ do 2 destruct find; auto; intros.
+ f_equal; apply H0; [rewrite H1|rewrite H2]; auto.
+ destruct H as [H _]; now elim H.
+ destruct H as [_ H]; now elim H.
+Qed.
+
+(** [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'.
+Proof.
+ unfold Equivb, Equiv, Cmp; intuition.
+ red in H; rewrite H; eauto.
+ red in H; rewrite <-H; eauto.
+Qed.
+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'.
+Proof.
+ intros; rewrite Equal_Equiv.
+ apply Equiv_Equivb; auto.
+Qed.
+
+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'.
+Proof.
+intros; apply Equal_Equivb.
+unfold cmp; clear cmp; intros.
+destruct eq_elt_dec; now intuition.
+Qed.
+
+End Equalities.
+
+(** * [Equal] is a setoid equality. *)
+
+Lemma Equal_refl : forall (elt:Set)(m : t elt), Equal m m.
+Proof. red; reflexivity. Qed.
+
+Lemma Equal_sym : forall (elt:Set)(m m' : t elt), 
+ Equal m m' -> Equal m' m.
+Proof. unfold Equal; auto. Qed.
+
+Lemma Equal_trans : forall (elt:Set)(m m' m'' : t elt), 
+ Equal m m' -> Equal m' m'' -> Equal m m''.
+Proof. unfold Equal; congruence. Qed.
+
+Definition Equal_ST : forall elt:Set, Setoid_Theory (t elt) (@Equal _).
+Proof. 
+constructor; [apply Equal_refl | apply Equal_sym | apply Equal_trans].
+Qed.
+
+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.
+
+Add Relation t Equal 
+ reflexivity proved by Equal_refl
+ symmetry proved by Equal_sym
+ transitivity proved by Equal_trans
+ as EqualSetoid.
+
+Add Morphism In with signature E.eq ==> Equal ==> iff as In_m.
+Proof.
+unfold Equal; intros elt k k' Hk m m' Hm.
+rewrite (In_iff m Hk), in_find_iff, in_find_iff, Hm; intuition.
+Qed.
+
+Add Morphism MapsTo 
+ with signature E.eq ==> Logic.eq ==> Equal ==> iff as MapsTo_m.
+Proof.
+unfold Equal; intros elt k k' Hk e m m' Hm.
+rewrite (MapsTo_iff m e Hk), find_mapsto_iff, find_mapsto_iff, Hm; 
+ intuition.
+Qed.
+
+Add Morphism Empty with signature Equal ==> iff as Empty_m.
+Proof.
+unfold Empty; intros elt m m' Hm; intuition.
+rewrite <-Hm in H0; eauto.
+rewrite Hm in H0; eauto.
+Qed.
+
+Add Morphism is_empty with signature Equal ==> Logic.eq as is_empty_m.
+Proof.
+intros elt m m' Hm.
+rewrite eq_bool_alt, <-is_empty_iff, <-is_empty_iff, Hm; intuition.
+Qed.
+
+Add Morphism mem with signature E.eq ==> Equal ==> Logic.eq as mem_m.
+Proof.
+intros elt k k' Hk m m' Hm.
+rewrite eq_bool_alt, <- mem_in_iff, <-mem_in_iff, Hk, Hm; intuition.
+Qed.
+
+Add Morphism find with signature E.eq ==> Equal ==> Logic.eq as find_m.
+Proof.
+intros elt k k' Hk m m' Hm.
+generalize (find_mapsto_iff m k)(find_mapsto_iff m' k')
+ (not_find_in_iff m k)(not_find_in_iff m' k'); 
+do 2 destruct find; auto; intros.
+rewrite <- H, Hk, Hm, H0; auto.
+rewrite <- H1, Hk, Hm, H2; auto.
+symmetry; rewrite <- H2, <-Hk, <-Hm, H1; auto.
+Qed.
+
+Add Morphism add with signature 
+ E.eq ==> Logic.eq ==> Equal ==> Equal as add_m.
+Proof.
+intros elt k k' Hk e m m' Hm y.
+rewrite add_o, add_o; do 2 destruct eq_dec; auto.
+elim n; rewrite <-Hk; auto.
+elim n; rewrite Hk; auto.
+Qed.
+
+Add Morphism remove with signature
+ E.eq ==> Equal ==> Equal as remove_m.
+Proof.
+intros elt k k' Hk m m' Hm y.
+rewrite remove_o, remove_o; do 2 destruct eq_dec; auto.
+elim n; rewrite <-Hk; auto.
+elim n; rewrite Hk; auto.
+Qed.
+
+Add Morphism map with signature Logic.eq ==> Equal ==> Equal as map_m.
+Proof.
+intros elt elt' f m m' Hm y.
+rewrite map_o, map_o, Hm; auto.
+Qed.
+
+(* Later: Add Morphism cardinal *)
+
+(* old name: *)
+Notation not_find_mapsto_iff := not_find_in_iff.
+
 End WFacts.
 
 (** * Same facts for full maps *)
@@ -571,7 +760,6 @@ Module WProperties (E:DecidableType)(M:WSfun E).
  Section Elt. 
   Variable elt:Set.
 
-  Definition Equal (m m':t elt) := forall y, find y m = find y m'.
   Definition Add x (e:elt) m m' := forall y, find y m' = find y (add x e m).
 
   Notation eqke := (@eq_key_elt elt).
@@ -698,7 +886,8 @@ Module WProperties (E:DecidableType)(M:WSfun E).
   destruct (elements m); intuition; discriminate.
   Qed.
  
-  Lemma Equal_cardinal : forall m m', Equal m m' -> cardinal m = cardinal m'.
+  Lemma Equal_cardinal : forall m m' : t elt, 
+    Equal m m' -> cardinal m = cardinal m'.
   Proof.
   intros; do 2 rewrite cardinal_fold.
   apply fold_Equal with (eqA:=@eq _); auto.
@@ -770,8 +959,152 @@ Module WProperties (E:DecidableType)(M:WSfun E).
   inversion H1; auto with map.
   Qed.
 
+  (** * Let's emulate some functions not present 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))).
+
+  Section Specs.
+  Variable f : key -> elt -> bool.
+  Hypothesis Hf : forall e, compat_bool E.eq (fun k => f k e).
+
+  Lemma filter_iff : forall m k e, 
+   MapsTo k e (filter f m) <-> MapsTo k e m /\ f k e = true.
+  Proof.
+  unfold filter; intros.
+  rewrite fold_1.
+  rewrite <- fold_left_rev_right.
+  rewrite (elements_mapsto_iff m).
+  rewrite <- (InA_rev eqke (k,e) (elements m)).
+  assert (NoDupA eqk (rev (elements m))).
+   apply NoDupA_rev; auto; try apply elements_3w; auto.
+   intros (k1,e1); compute; auto.
+   intros (k1,e1)(k2,e2); compute; auto.
+   intros (k1,e1)(k2,e2)(k3,e3); compute; eauto.
+  induction (rev (elements m)); simpl; auto.
+  
+  rewrite empty_mapsto_iff.
+  intuition.
+  inversion H1.
+
+  destruct a as (k',e'); simpl.
+  inversion_clear H.
+  case_eq (f k' e'); intros; simpl;
+   try rewrite add_mapsto_iff; rewrite IHl; clear IHl; intuition.
+  constructor; red; auto.
+  rewrite (Hf e' H2),H4 in H; auto.
+  inversion_clear H3.
+  compute in H2; destruct H2; auto.
+  destruct (E.eq_dec k' k); auto.
+  elim H0.
+  rewrite InA_alt in *; destruct H2 as (w,Hw); exists w; intuition.
+  red in H2; red; simpl in *; intuition.
+  rewrite e0; auto.
+  inversion_clear H3; auto.
+  compute in H2; destruct H2.
+  rewrite (Hf e H2),H3,H in H4; discriminate.
+  Qed.
+  
+  Lemma for_all_iff : forall m,
+   for_all f m = true <-> (forall k e, MapsTo k e m -> f k e = true).
+  Proof.
+  cut (forall m : t elt,
+       for_all f m = true <->
+       (forall k e, InA eqke (k,e) (rev (elements m)) -> f k e = true)).
+  intros; rewrite H; split; intros.
+  apply H0; rewrite InA_rev, <- elements_mapsto_iff; auto.
+  apply H0; rewrite InA_rev, <- elements_mapsto_iff in H1; auto.
+
+  unfold for_all; intros.
+  rewrite fold_1.
+  rewrite <- fold_left_rev_right.
+  assert (NoDupA eqk (rev (elements m))).
+   apply NoDupA_rev; auto; try apply elements_3w; auto.
+   intros (k1,e1); compute; auto.
+   intros (k1,e1)(k2,e2); compute; auto.
+   intros (k1,e1)(k2,e2)(k3,e3); compute; eauto.
+  induction (rev (elements m)); simpl; auto.
+  
+  intuition.
+  inversion H1.
+
+  destruct a as (k,e); simpl.
+  inversion_clear H.
+  case_eq (f k e); intros; simpl;
+   try rewrite IHl; clear IHl; intuition.
+  inversion_clear H3; auto.
+  compute in H4; destruct H4.
+  rewrite (Hf e0 H3), H4; auto.
+  rewrite <-H, <-(H2 k e); auto.
+  constructor; red; auto.
+  Qed.
+  
+  Lemma exists_iff : forall m,
+   exists_ f m = true <-> 
+   (exists p, MapsTo (fst p) (snd p) m /\ f (fst p) (snd p) = true).
+  Proof.
+  cut (forall m : t elt,
+       exists_ f m = true <->
+       (exists p, InA eqke p (rev (elements m)) 
+         /\ f (fst p) (snd p) = true)).
+  intros; rewrite H; split; intros.
+  destruct H0 as ((k,e),Hke); exists (k,e).
+  rewrite InA_rev, <-elements_mapsto_iff in Hke; auto.
+  destruct H0 as ((k,e),Hke); exists (k,e).
+  rewrite InA_rev, <-elements_mapsto_iff; auto.
+  unfold exists_; intros.
+  rewrite fold_1.
+  rewrite <- fold_left_rev_right.
+  assert (NoDupA eqk (rev (elements m))).
+   apply NoDupA_rev; auto; try apply elements_3w; auto.
+   intros (k1,e1); compute; auto.
+   intros (k1,e1)(k2,e2); compute; auto.
+   intros (k1,e1)(k2,e2)(k3,e3); compute; eauto.
+  induction (rev (elements m)); simpl; auto.
+  
+  intuition; try discriminate.
+  destruct H0 as ((k,e),(Hke,_)); inversion Hke.
+
+  destruct a as (k,e); simpl.
+  inversion_clear H.
+  case_eq (f k e); intros; simpl;
+   try rewrite IHl; clear IHl; intuition.
+  exists (k,e); simpl; split; auto.
+  constructor; red; auto.
+  destruct H2 as ((k',e'),(Hke',Hf')); exists (k',e'); simpl; auto.
+  destruct H2 as ((k',e'),(Hke',Hf')); simpl in *.
+  inversion_clear Hke'.
+  compute in H2; destruct H2.
+  rewrite (Hf e' H2), H3,H in Hf'; discriminate.
+  exists (k',e'); auto.
+  Qed.
+  End Specs.
+
+  (** 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 Morphism cardinal with signature Equal ==> Logic.eq as cardinal_m.
+ Proof. intros; apply Equal_cardinal; auto. Qed.
+
 End WProperties.
 
 (** * Same Properties for full maps *)
@@ -797,7 +1130,7 @@ Module OrdProperties (M:S).
   Notation eqk := (@eqk elt).
   Notation ltk := (@ltk elt).
   Notation cardinal := (@cardinal elt).
-  Notation Equal := (@P.Equal elt).
+  Notation Equal := (@Equal elt).
   Notation Add := (@Add elt).
 
   Definition Above x (m:t elt) := forall y, In y m -> E.lt y x.
@@ -1254,3 +1587,5 @@ End OrdProperties.
 
 
 
+
+
diff --git a/theories/FSets/FMapIntMap.v b/theories/FSets/FMapIntMap.v
index 9673d667df..0c180fcbd1 100644
--- a/theories/FSets/FMapIntMap.v
+++ b/theories/FSets/FMapIntMap.v
@@ -324,9 +324,11 @@ Module MapIntMap <: S with Module E:=NUsualOrderedType.
   Lemma cardinal_1 : forall m, cardinal m = length (elements m).
   Proof. exact (@MapCard_as_length _). Qed.
 
-  Definition Equal cmp m m' := 
-         (forall k, In k m <-> In k m') /\ 
-         (forall k e e', MapsTo k e m -> MapsTo k e' m' -> cmp e e' = true).  
+  Definition Equal m m' := forall y, find y m = find y m'.
+  Definition Equiv (eq_elt:A->A->Prop) m m' := 
+    (forall k, In k m <-> In k m') /\ 
+    (forall k e e', MapsTo k e m -> MapsTo k e' m' -> eq_elt e e').  
+  Definition Equivb (cmp: A->A->bool) := Equiv (Cmp cmp).
 
   (** unfortunately, the [MapFold] of [IntMap] isn't compatible with 
    the FMap interface. We use a naive version for now : *)
@@ -600,14 +602,14 @@ Module MapIntMap <: S with Module E:=NUsualOrderedType.
   
   Lemma equal_1 : 
     forall (A:Set)(m: t A)(m': t A)(cmp: A -> A -> bool), 
-    Equal cmp m m' -> equal cmp m m' = true. 
+    Equivb cmp m m' -> equal cmp m m' = true. 
   Proof.
-  unfold equal, Equal.
+  unfold equal, Equivb, Equiv, Cmp.
   intros.
   apply L.equal_1.
   apply elements_3.
   apply elements_3.
-  unfold L.Equal.
+  unfold L.Equivb.
   destruct H.
   split; intros.
   do 2 rewrite elements_in; auto.
@@ -618,9 +620,9 @@ Module MapIntMap <: S with Module E:=NUsualOrderedType.
 
   Lemma equal_2 : 
     forall (A:Set)(m: t A)(m': t A)(cmp: A -> A -> bool), 
-    equal cmp m m' = true -> Equal cmp m m'.
+    equal cmp m m' = true -> Equivb cmp m m'.
   Proof.
-  unfold equal, Equal.
+  unfold equal, Equivb, Equiv, Cmp.
   intros.
   destruct (L.equal_2 (elements_3 m) (elements_3 m') H); clear H.
   split.
diff --git a/theories/FSets/FMapInterface.v b/theories/FSets/FMapInterface.v
index 01362936c3..9a7d4ab82b 100644
--- a/theories/FSets/FMapInterface.v
+++ b/theories/FSets/FMapInterface.v
@@ -48,6 +48,7 @@ Unset Strict Implicit.
 *)
 
 
+Definition Cmp (elt:Set)(cmp:elt->elt->bool) e1 e2 := cmp e1 e2 = true.
 
 (** ** Weak signature for maps
    
@@ -191,19 +192,37 @@ Module Type WSfun (E : EqualityType).
       Parameter fold_1 :
 	forall (A : Type) (i : A) (f : key -> elt -> A -> A),
         fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i.
+
+    (** Equality of maps *)
  
-   Definition Equal cmp m m' := 
+    (** Caveat: there are at least three distinct equality predicates on maps.
+      - The simpliest (and maybe most natural) way is to consider keys up to 
+        their equivalence [E.eq], but elements up to Leibniz equality, in 
+        the spirit of [eq_key_elt] above. This leads to predicate [Equal].
+      - Unfortunately, this [Equal] predicate can't be used to describe
+        the [equal] function, since this function (for compatibility with 
+        ocaml) expects a boolean comparison [cmp] that may identify more 
+        elements than Leibniz. So logical specification of [equal] is done 
+        via another predicate [Equivb]
+      - This predicate [Equivb] is quite ad-hoc with its boolean [cmp],
+        it can be generalized in a [Equiv] expecting a more general
+        (possibly non-decidable) equality predicate on elements *)
+
+     Definition Equal m m' := forall y, find y m = find y m'.
+     Definition Equiv (eq_elt:elt->elt->Prop) m m' := 
          (forall k, In k m <-> In k m') /\ 
-         (forall k e e', MapsTo k e m -> MapsTo k e' m' -> cmp e e' = true).  
+         (forall k e e', MapsTo k e m -> MapsTo k e' m' -> eq_elt e e').  
+     Definition Equivb (cmp: elt->elt->bool) := Equiv (Cmp cmp).
+
+     (** Specification of [equal] *)
 
-   Variable cmp : elt -> elt -> bool. 
+     Variable cmp : elt -> elt -> bool. 
 
-   (** Specification of [equal] *)
-     Parameter equal_1 : Equal cmp m m' -> equal cmp m m' = true. 
-     Parameter equal_2 : equal cmp m m' = true -> Equal cmp m m'.
+     Parameter equal_1 : Equivb cmp m m' -> equal cmp m m' = true.
+     Parameter equal_2 : equal cmp m m' = true -> Equivb cmp m m'.
 
-    End Spec. 
-   End Types. 
+    End Spec.
+   End Types.
 
     (** Specification of [map] *)
       Parameter map_1 : forall (elt elt':Set)(m: t elt)(x:key)(e:elt)(f:elt->elt'), 
@@ -296,8 +315,8 @@ Module Type Sord.
 
   Definition cmp e e' := match Data.compare e e' with EQ _ => true | _ => false end.	
 
-  Parameter eq_1 : forall m m', Equal cmp m m' -> eq m m'.
-  Parameter eq_2 : forall m m', eq m m' -> Equal cmp m m'.
+  Parameter eq_1 : forall m m', Equivb cmp m m' -> eq m m'.
+  Parameter eq_2 : forall m m', eq m m' -> Equivb cmp m m'.
 
   Parameter compare : forall m1 m2, Compare lt eq m1 m2.
   (** Total ordering between maps. [Data.compare] is a total ordering 
diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v
index 63144afe7b..a47d431b34 100644
--- a/theories/FSets/FMapList.v
+++ b/theories/FSets/FMapList.v
@@ -377,29 +377,24 @@ Function equal (cmp:elt->elt->bool)(m m' : t elt) { struct m } : bool :=
    | _, _ => false 
   end.
 
-Definition Equal cmp m m' := 
+Definition Equivb cmp m m' := 
   (forall k, In k m <-> In k m') /\ 
   (forall k e e', MapsTo k e m -> MapsTo k e' m' -> cmp e e' = true).  
 
 Lemma equal_1 : forall m (Hm:Sort m) m' (Hm': Sort m') cmp, 
-  Equal cmp m m' -> equal cmp m m' = true. 
+  Equivb cmp m m' -> equal cmp m m' = true. 
 Proof. 
  intros m Hm m' Hm' cmp; generalize Hm Hm'; clear Hm Hm'.
- functional induction (equal cmp m m'); simpl; subst;auto; unfold Equal;
- intuition; subst;   match goal with 
-     | [H: X.compare _ _ = _ |- _ ] => clear H
-     | _ => idtac
-   end.
-
-
-
+ functional induction (equal cmp m m'); simpl; subst;auto; unfold Equivb;
+ intuition; subst.
+ match goal with H: X.compare _ _ = _ |- _ => clear H end.
  assert (cmp_e_e':cmp e e' = true).
   apply H1 with x; auto.
  rewrite cmp_e_e'; simpl.
  apply IHb; auto.
  inversion_clear Hm; auto.
  inversion_clear Hm'; auto.
- unfold Equal; intuition.
+ unfold Equivb; intuition.
  destruct (H0 k).
  assert (In k ((x,e) ::l)).
   destruct H as (e'', hyp); exists e''; auto.
@@ -462,14 +457,12 @@ Qed.
 
 
 Lemma equal_2 : forall m (Hm:Sort m) m' (Hm:Sort m') cmp, 
-  equal cmp m m' = true -> Equal cmp m m'.
+  equal cmp m m' = true -> Equivb cmp m m'.
 Proof.
  intros m Hm m' Hm' cmp; generalize Hm Hm'; clear Hm Hm'.
- functional induction (equal cmp m m'); simpl; subst;auto; unfold Equal; 
-  intuition; try discriminate; subst; match goal with 
-     | [H: X.compare _ _ = _ |- _ ] => clear H
-     | _ => idtac
-   end. 
+ functional induction (equal cmp m m'); simpl; subst;auto; unfold Equivb; 
+  intuition; try discriminate; subst; 
+  try match goal with H: X.compare _ _ = _ |- _ => clear H end.
 
  inversion H0.
 
@@ -505,13 +498,13 @@ Proof.
  elim (Sort_Inf_NotIn H2 H3).
  exists e0; apply MapsTo_eq with k; auto; order.
  apply H8 with k; auto.
-Qed. 
+Qed.
 
-(** This lemma isn't part of the spec of [Equal], but is used in [FMapAVL] *)
+(** This lemma isn't part of the spec of [Equivb], but is used in [FMapAVL] *)
 
 Lemma equal_cons : forall cmp l1 l2 x y, Sort (x::l1) -> Sort (y::l2) ->
   eqk x y -> cmp (snd x) (snd y) = true -> 
-  (Equal cmp l1 l2 <-> Equal cmp (x :: l1) (y :: l2)).
+  (Equivb cmp l1 l2 <-> Equivb cmp (x :: l1) (y :: l2)).
 Proof.
  intros.
  inversion H; subst.
@@ -1070,7 +1063,12 @@ Section Elt.
  Definition MapsTo x e m : Prop := Raw.PX.MapsTo x e m.(this).
  Definition In x m : Prop := Raw.PX.In x m.(this).
  Definition Empty m : Prop := Raw.Empty m.(this).
- Definition Equal cmp m m' : Prop := @Raw.Equal elt cmp m.(this) m'.(this).
+
+ Definition Equal m m' := forall y, find y m = find y m'.
+ Definition Equiv (eq_elt:elt->elt->Prop) m m' := 
+         (forall k, In k m <-> In k m') /\ 
+         (forall k e e', MapsTo k e m -> MapsTo k e' m' -> eq_elt e e').  
+ Definition Equivb cmp m m' : Prop := @Raw.Equivb elt cmp m.(this) m'.(this).
 
  Definition eq_key : (key*elt) -> (key*elt) -> Prop := @Raw.PX.eqk elt.
  Definition eq_key_elt : (key*elt) -> (key*elt) -> Prop:= @Raw.PX.eqke elt.
@@ -1127,9 +1125,9 @@ Section Elt.
         fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i.
  Proof. intros m; exact (@Raw.fold_1 elt m.(this)). Qed.
 
- Lemma equal_1 : forall m m' cmp, Equal cmp m m' -> equal cmp m m' = true. 
+ Lemma equal_1 : forall m m' cmp, Equivb cmp m m' -> equal cmp m m' = true. 
  Proof. intros m m'; exact (@Raw.equal_1 elt m.(this) m.(sorted) m'.(this) m'.(sorted)). Qed.
- Lemma equal_2 : forall m m' cmp, equal cmp m m' = true -> Equal cmp m m'.
+ Lemma equal_2 : forall m m' cmp, equal cmp m m' = true -> Equivb cmp m m'.
  Proof. intros m m'; exact (@Raw.equal_2 elt m.(this) m.(sorted) m'.(this) m'.(sorted)). Qed.
 
  End Elt.
@@ -1238,7 +1236,7 @@ Proof.
  unfold equal, eq in H6; simpl in H6; auto.
 Qed.
 
-Lemma eq_1 : forall m m', Equal cmp m m' -> eq m m'.
+Lemma eq_1 : forall m m', Equivb cmp m m' -> eq m m'.
 Proof.
  intros.
  generalize (@equal_1 D.t m m' cmp).
@@ -1246,7 +1244,7 @@ Proof.
  intuition.
 Qed.
 
-Lemma eq_2 : forall m m', eq m m' -> Equal cmp m m'.
+Lemma eq_2 : forall m m', eq m m' -> Equivb cmp m m'.
 Proof.
  intros.
  generalize (@equal_2 D.t m m' cmp).
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index b00c6b4934..1273e5403a 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -1006,12 +1006,15 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
            && equal cmp l1 l2 && equal cmp r1 r2
      end.
 
-  Definition Equal (A:Set)(cmp:A->A->bool)(m m':t A) := 
+  Definition Equal (A:Set)(m m':t A) := 
+    forall y, find y m = find y m'.
+  Definition Equiv (A:Set)(eq_elt:A->A->Prop) m m' := 
     (forall k, In k m <-> In k m') /\ 
-    (forall k e e', MapsTo k e m -> MapsTo k e' m' -> cmp e e' = true).  
+    (forall k e e', MapsTo k e m -> MapsTo k e' m' -> eq_elt e e').  
+  Definition Equivb (A:Set)(cmp: A->A->bool) := Equiv (Cmp cmp).
 
   Lemma equal_1 : forall (A:Set)(m m':t A)(cmp:A->A->bool), 
-    Equal cmp m m' -> equal cmp m m' = true. 
+    Equivb cmp m m' -> equal cmp m m' = true. 
   Proof. 
   induction m.
   (* m = Leaf *)
@@ -1045,11 +1048,11 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
   destruct H2; red in H2; simpl in H2; discriminate.
   (* m' = Node *)
   destruct 1.
-  assert (Equal cmp m1 m'1).
+  assert (Equivb cmp m1 m'1).
     split.
     intros k; generalize (H (xO k)); unfold In, MapsTo; simpl; auto.
     intros k e e'; generalize (H0 (xO k) e e'); unfold In, MapsTo; simpl; auto.
-  assert (Equal cmp m2 m'2).
+  assert (Equivb cmp m2 m'2).
     split.
     intros k; generalize (H (xI k)); unfold In, MapsTo; simpl; auto.
     intros k e e'; generalize (H0 (xI k) e e'); unfold In, MapsTo; simpl; auto.
@@ -1065,7 +1068,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
   Qed.
 
   Lemma equal_2 : forall (A:Set)(m m':t A)(cmp:A->A->bool), 
-    equal cmp m m' = true -> Equal cmp m m'. 
+    equal cmp m m' = true -> Equivb cmp m m'. 
   Proof. 
   induction m.
   (* m = Leaf *)
diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v
index a40e3acf03..0be7351cc6 100644
--- a/theories/FSets/FMapWeakList.v
+++ b/theories/FSets/FMapWeakList.v
@@ -372,7 +372,7 @@ Definition Submap cmp m m' :=
   (forall k, In k m -> In k m') /\ 
   (forall k e e', MapsTo k e m -> MapsTo k e' m' -> cmp e e' = true).  
 
-Definition Equal cmp m m' := 
+Definition Equivb cmp m m' := 
   (forall k, In k m <-> In k m') /\ 
   (forall k e e', MapsTo k e m -> MapsTo k e' m' -> cmp e e' = true).  
 
@@ -439,17 +439,17 @@ Qed.
 (** Specification of [equal] *)
 
 Lemma equal_1 : forall m (Hm:NoDupA m) m' (Hm': NoDupA m') cmp, 
-  Equal cmp m m' -> equal cmp m m' = true. 
+  Equivb cmp m m' -> equal cmp m m' = true. 
 Proof. 
- unfold Equal, equal.
+ unfold Equivb, equal.
  intuition.
  apply andb_true_intro; split; apply submap_1; unfold Submap; firstorder.
 Qed.
 
 Lemma equal_2 : forall m (Hm:NoDupA m) m' (Hm':NoDupA m') cmp, 
-  equal cmp m m' = true -> Equal cmp m m'.
+  equal cmp m m' = true -> Equivb cmp m m'.
 Proof.
- unfold Equal, equal.
+ unfold Equivb, equal.
  intros.
  destruct (andb_prop _ _ H); clear H.
  generalize (submap_2 Hm Hm' H0).
@@ -899,11 +899,15 @@ Section Elt.
  Definition cardinal m := length m.(this).
  Definition fold (A:Type)(f:key->elt->A->A) m (i:A) : A := @Raw.fold elt A f m.(this) i.
  Definition equal cmp m m' : bool := @Raw.equal elt cmp m.(this) m'.(this).
-
  Definition MapsTo x e m : Prop := Raw.PX.MapsTo x e m.(this).
  Definition In x m : Prop := Raw.PX.In x m.(this).
  Definition Empty m : Prop := Raw.Empty m.(this).
- Definition Equal cmp m m' : Prop := @Raw.Equal elt cmp m.(this) m'.(this).
+
+ Definition Equal m m' := forall y, find y m = find y m'.
+ Definition Equiv (eq_elt:elt->elt->Prop) m m' := 
+         (forall k, In k m <-> In k m') /\ 
+         (forall k e e', MapsTo k e m -> MapsTo k e' m' -> eq_elt e e').  
+ Definition Equivb cmp m m' : Prop := @Raw.Equivb elt cmp m.(this) m'.(this).
 
  Definition eq_key : (key*elt) -> (key*elt) -> Prop := @Raw.PX.eqk elt.
  Definition eq_key_elt : (key*elt) -> (key*elt) -> Prop:= @Raw.PX.eqke elt.
@@ -957,9 +961,9 @@ Section Elt.
         fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i.
  Proof. intros m; exact (@Raw.fold_1 elt m.(this)). Qed.
 
- Lemma equal_1 : forall m m' cmp, Equal cmp m m' -> equal cmp m m' = true. 
+ Lemma equal_1 : forall m m' cmp, Equivb cmp m m' -> equal cmp m m' = true. 
  Proof. intros m m'; exact (@Raw.equal_1 elt m.(this) m.(NoDup) m'.(this) m'.(NoDup)). Qed.
- Lemma equal_2 : forall m m' cmp, equal cmp m m' = true -> Equal cmp m m'.
+ Lemma equal_2 : forall m m' cmp, equal cmp m m' = true -> Equivb cmp m m'.
  Proof. intros m m'; exact (@Raw.equal_2 elt m.(this) m.(NoDup) m'.(this) m'.(NoDup)). Qed.
 
  End Elt.