From 65ceda87c740b9f5a81ebf5a7873036c081b402c Mon Sep 17 00:00:00 2001 From: letouzey Date: Mon, 29 Oct 2007 23:52:01 +0000 Subject: 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 --- theories/FSets/FMapAVL.v | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'theories/FSets/FMapAVL.v') diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index 6e4c4b26f..b7947cddd 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -1070,6 +1070,10 @@ Proof. Qed. Hint Resolve elements_sort. +Lemma elements_nodup : forall s : t elt, bst s -> NoDupA eqk (elements s). +Proof. + intros; apply Sort_NoDupA; auto. +Qed. (** * Fold *) @@ -1816,6 +1820,9 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. Lemma elements_3 : forall m, sort lt_key (elements m). Proof. intros m; exact (@Raw.elements_sort elt m.(this) m.(is_bst)). Qed. + Lemma elements_3w : forall m, NoDupA eq_key (elements m). + Proof. intros m; exact (@Raw.elements_nodup elt m.(this) m.(is_bst)). 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). -- cgit v1.2.3