aboutsummaryrefslogtreecommitdiff
path: root/theories/FSets/FMapIntMap.v
diff options
context:
space:
mode:
authorletouzey2007-10-29 23:52:01 +0000
committerletouzey2007-10-29 23:52:01 +0000
commit65ceda87c740b9f5a81ebf5a7873036c081b402c (patch)
treec52308544582bc5c4dcec7bd4fc6e792bba91961 /theories/FSets/FMapIntMap.v
parent172a2711fde878a907e66bead74b9102583dca82 (diff)
Revision of the FSetWeak Interface, so that it becomes a precise
subtype of the FSet Interface (and idem for FMapWeak / FMap). 1) No eq_dec is officially required in FSetWeakInterface.S.E (EqualityType instead of DecidableType). But of course, implementations still needs this eq_dec. 2) elements_3 differs in FSet and FSetWeak (sort vs. nodup). In FSetWeak we rename it into elements_3w, whereas in FSet we artificially add elements_3w along to the original elements_3. Initial steps toward factorization of FSetFacts and FSetWeakFacts, and so on... Even if it's not required, FSetWeakList provides a eq_dec on sets, allowing weak sets of weak sets. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10271 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/FSets/FMapIntMap.v')
-rw-r--r--theories/FSets/FMapIntMap.v8
1 files changed, 7 insertions, 1 deletions
diff --git a/theories/FSets/FMapIntMap.v b/theories/FSets/FMapIntMap.v
index 6ad24f1cc5..b5fe6722b0 100644
--- a/theories/FSets/FMapIntMap.v
+++ b/theories/FSets/FMapIntMap.v
@@ -258,7 +258,13 @@ Module MapIntMap <: S with Module E:=NUsualOrderedType.
apply alist_sorted_sort.
apply alist_of_Map_sorts.
Qed.
-
+
+ Lemma elements_3w : NoDupA eq_key (elements m).
+ Proof.
+ change eq_key with (@PE.eqk A).
+ apply PE.Sort_NoDupA; apply elements_3; auto.
+ Qed.
+
Lemma elements_1 :
MapsTo x e m -> InA eq_key_elt (x,e) (elements m).
Proof.