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

1 files changed, 10 insertions, 8 deletions

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.