diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2015-03-04 15:12:46 +0100 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2015-03-04 15:22:12 +0100 |
| commit | d169ecbac96fe2a8a6a44395ad7fa83612e725c4 (patch) | |
| tree | 320ae485363f28f62ff56e51ce9a6743e8658498 /theories/Lists/SetoidList.v | |
| parent | caf8907992fdfe655af95fa74e9c749be98c430c (diff) | |
Introducing MMaps, a modernized FMaps.
NB: this is work-in-progress, there is currently only one
provided implementation (MMapWeakList).
In the same spirit as MSets w.r.t FSets, the main difference between
MMaps and former FMaps is the use of a new version of OrderedType
(see Orders.v instead of obsolete OrderedType.v).
We also try to benefit more from recent notions such as Proper.
For most function specifications, the style has changed : we now use
equations over "find" instead of "MapsTo" predicates, whenever possible
(cf. Maps in Compcert for a source of inspiration). Former specs are
now derived in FMapFacts, so this is mostly a matter of taste.
Two changes inspired by the current Maps of OCaml:
- "elements" is now "bindings"
- "map2" is now "merge" (and its function argument also receives a key).
We now use a maximal implicit argument for "empty".
Diffstat (limited to 'theories/Lists/SetoidList.v')
| -rw-r--r-- | theories/Lists/SetoidList.v | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v index b57c3f046..c95fb4d5c 100644 --- a/theories/Lists/SetoidList.v +++ b/theories/Lists/SetoidList.v @@ -613,18 +613,18 @@ induction s1; simpl; auto; intros. Qed. Lemma fold_right_equivlistA_restr2 : - forall s s' (i j:B) (heqij: eqB i j), + forall s s' i j, NoDupA s -> NoDupA s' -> ForallOrdPairs R s -> - eqB i j -> - equivlistA s s' -> eqB (fold_right f i s) (fold_right f j s'). + equivlistA s s' -> eqB i j -> + eqB (fold_right f i s) (fold_right f j s'). Proof. simple induction s. destruct s'; simpl. intros. assumption. unfold equivlistA; intros. - destruct (H3 a). + destruct (H2 a). assert (InA a nil) by auto; inv. - intros x l Hrec s' i j heqij N N' F eqij E; simpl in *. + intros x l Hrec s' i j N N' F E eqij; simpl in *. assert (InA x s') by (rewrite <- (E x); auto). destruct (InA_split H) as (s1,(y,(s2,(H1,H2)))). subst s'. @@ -649,7 +649,6 @@ Proof. red; intros; rewrite E; auto. Qed. - Lemma fold_right_add_restr2 : forall s' s i j x, NoDupA s -> NoDupA s' -> eqB i j -> ForallOrdPairs R s' -> ~ InA x s -> equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f j s)). |