diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-10-29 23:52:01 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-10-29 23:52:01 +0000 |
commit | 65ceda87c740b9f5a81ebf5a7873036c081b402c (patch) | |
tree | c52308544582bc5c4dcec7bd4fc6e792bba91961 /theories/FSets/FMapList.v | |
parent | 172a2711fde878a907e66bead74b9102583dca82 (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/FMapList.v')
-rw-r--r-- | theories/FSets/FMapList.v | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v index 60a48396d..b2cedaabb 100644 --- a/theories/FSets/FMapList.v +++ b/theories/FSets/FMapList.v @@ -347,6 +347,13 @@ Proof. auto. Qed. +Lemma elements_3w : forall m (Hm:Sort m), NoDupA eqk (elements m). +Proof. + intros. + apply Sort_NoDupA. + apply elements_3; auto. +Qed. + (** * [fold] *) Function fold (A:Type)(f:key->elt->A->A)(m:t elt) (acc:A) {struct m} : A := @@ -1113,6 +1120,8 @@ Section Elt. Proof. intros m; exact (@Raw.elements_2 elt m.(this)). Qed. Lemma elements_3 : forall m, sort lt_key (elements m). Proof. intros m; exact (@Raw.elements_3 elt m.(this) m.(sorted)). Qed. + Lemma elements_3w : forall m, NoDupA eq_key (elements m). + Proof. intros m; exact (@Raw.elements_3w elt m.(this) m.(sorted)). Qed. Lemma fold_1 : forall m (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. |