summaryrefslogtreecommitdiff
path: root/theories/FSets/FMapFacts.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/FSets/FMapFacts.v')
-rw-r--r--theories/FSets/FMapFacts.v55
1 files changed, 32 insertions, 23 deletions
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 8944f7ce..0c1448c9 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id: FMapFacts.v 12459 2009-11-02 18:51:43Z letouzey $ *)
-
(** * Finite maps library *)
(** This functor derives additional facts from [FMapInterface.S]. These
@@ -259,7 +257,7 @@ Qed.
Lemma mapi_inv : forall m x b (f : key -> elt -> elt'),
MapsTo x b (mapi f m) ->
- exists a, exists y, E.eq y x /\ b = f y a /\ MapsTo x a m.
+ exists a y, E.eq y x /\ b = f y a /\ MapsTo x a m.
Proof.
intros; case_eq (find x m); intros.
exists e.
@@ -654,7 +652,7 @@ Add Relation key E.eq
transitivity proved by E.eq_trans
as KeySetoid.
-Implicit Arguments Equal [[elt]].
+Arguments Equal {elt} m m'.
Add Parametric Relation (elt : Type) : (t elt) Equal
reflexivity proved by (@Equal_refl elt)
@@ -740,7 +738,7 @@ End WFacts_fun.
(** * Same facts for self-contained weak sets and for full maps *)
-Module WFacts (M:S) := WFacts_fun M.E M.
+Module WFacts (M:WS) := WFacts_fun M.E M.
Module Facts := WFacts.
(** * Additional Properties for weak maps
@@ -761,8 +759,8 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
Notation eqk := (@eq_key elt).
Instance eqk_equiv : Equivalence eqk.
- Proof. split; repeat red; eauto. Qed.
-
+ Proof. unfold eq_key; split; eauto. Qed.
+
Instance eqke_equiv : Equivalence eqke.
Proof.
unfold eq_key_elt; split; repeat red; firstorder.
@@ -834,8 +832,11 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
(** * Conversions between maps and association lists. *)
+ Definition uncurry {U V W : Type} (f : U -> V -> W) : U*V -> W :=
+ fun p => f (fst p) (snd p).
+
Definition of_list (l : list (key*elt)) :=
- List.fold_right (fun p => add (fst p) (snd p)) (empty _) l.
+ List.fold_right (uncurry (@add _)) (empty _) l.
Definition to_list := elements.
@@ -845,6 +846,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
Proof.
induction l as [|(k',e') l IH]; simpl; intros k e Hnodup.
rewrite empty_mapsto_iff, InA_nil; intuition.
+ unfold uncurry; simpl.
inversion_clear Hnodup as [| ? ? Hnotin Hnodup'].
specialize (IH k e Hnodup'); clear Hnodup'.
rewrite add_mapsto_iff, InA_cons, <- IH.
@@ -861,6 +863,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
Proof.
induction l as [|(k',e') l IH]; simpl; intros k Hnodup.
apply empty_o.
+ unfold uncurry; simpl.
inversion_clear Hnodup as [| ? ? Hnotin Hnodup'].
specialize (IH k Hnodup'); clear Hnodup'.
rewrite add_o, IH.
@@ -883,6 +886,14 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
(** * Fold *)
+ (** Alternative specification via [fold_right] *)
+
+ Lemma fold_spec_right m (A:Type)(i:A)(f : key -> elt -> A -> A) :
+ fold f m i = List.fold_right (uncurry f) i (rev (elements m)).
+ Proof.
+ rewrite fold_1. symmetry. apply fold_left_rev_right.
+ Qed.
+
(** ** Induction principles about fold contributed by S. Lescuyer *)
(** In the following lemma, the step hypothesis is deliberately restricted
@@ -897,8 +908,8 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
P m (fold f m i).
Proof.
intros A P f i m Hempty Hstep.
- rewrite fold_1, <- fold_left_rev_right.
- set (F:=fun (y : key * elt) (x : A) => f (fst y) (snd y) x).
+ rewrite fold_spec_right.
+ set (F:=uncurry f).
set (l:=rev (elements m)).
assert (Hstep' : forall k e a m' m'', InA eqke (k,e) l -> ~In k m' ->
Add k e m' m'' -> P m' a -> P m'' (F (k,e) a)).
@@ -983,8 +994,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
R (fold f m i) (fold g m j).
Proof.
intros A B R f g i j m Rempty Rstep.
- do 2 rewrite fold_1, <- fold_left_rev_right.
- set (l:=rev (elements m)).
+ rewrite 2 fold_spec_right. set (l:=rev (elements m)).
assert (Rstep' : forall k e a b, InA eqke (k,e) l ->
R a b -> R (f k e a) (g k e b)) by
(intros; apply Rstep; auto; rewrite elements_mapsto_iff, <- InA_rev; auto with *).
@@ -1099,14 +1109,15 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
Lemma fold_Equal : forall m1 m2 i, Equal m1 m2 ->
eqA (fold f m1 i) (fold f m2 i).
Proof.
- intros; do 2 rewrite fold_1; do 2 rewrite <- fold_left_rev_right.
+ intros.
+ rewrite 2 fold_spec_right.
assert (NoDupA eqk (rev (elements m1))) by (auto with *).
assert (NoDupA eqk (rev (elements m2))) by (auto with *).
apply fold_right_equivlistA_restr with (R:=complement eqk)(eqA:=eqke);
auto with *.
intros (k1,e1) (k2,e2) (Hk,He) a1 a2 Ha; simpl in *; apply Comp; auto.
unfold complement, eq_key, eq_key_elt; repeat red. intuition eauto.
- intros (k,e) (k',e'); unfold eq_key; simpl; auto.
+ intros (k,e) (k',e'); unfold eq_key, uncurry; simpl; auto.
rewrite <- NoDupA_altdef; auto.
intros (k,e).
rewrite 2 InA_rev, <- 2 elements_mapsto_iff, 2 find_mapsto_iff, H;
@@ -1116,8 +1127,9 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
Lemma fold_Add : forall m1 m2 k e i, ~In k m1 -> Add k e m1 m2 ->
eqA (fold f m2 i) (f k e (fold f m1 i)).
Proof.
- intros; do 2 rewrite fold_1; do 2 rewrite <- fold_left_rev_right.
- set (f':=fun y x0 => f (fst y) (snd y) x0) in *.
+ intros.
+ rewrite 2 fold_spec_right.
+ set (f':=uncurry f).
change (f k e (fold_right f' i (rev (elements m1))))
with (f' (k,e) (fold_right f' i (rev (elements m1)))).
assert (NoDupA eqk (rev (elements m1))) by (auto with *).
@@ -1126,7 +1138,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
(R:=complement eqk)(eqA:=eqke)(eqB:=eqA); auto with *.
intros (k1,e1) (k2,e2) (Hk,He) a a' Ha; unfold f'; simpl in *. apply Comp; auto.
unfold complement, eq_key_elt, eq_key; repeat red; intuition eauto.
- unfold f'; intros (k1,e1) (k2,e2); unfold eq_key; simpl; auto.
+ unfold f'; intros (k1,e1) (k2,e2); unfold eq_key, uncurry; simpl; auto.
rewrite <- NoDupA_altdef; auto.
rewrite InA_rev, <- elements_mapsto_iff by (auto with *). firstorder.
intros (a,b).
@@ -2130,8 +2142,7 @@ Module OrdProperties (M:S).
eqA (fold f m1 i) (fold f m2 i).
Proof.
intros m1 m2 A eqA st f i Hf Heq.
- do 2 rewrite fold_1.
- do 2 rewrite <- fold_left_rev_right.
+ rewrite 2 fold_spec_right.
apply fold_right_eqlistA with (eqA:=eqke) (eqB:=eqA); auto.
intros (k,e) (k',e') (Hk,He) a a' Ha; simpl in *; apply Hf; auto.
apply eqlistA_rev. apply elements_Equal_eqlistA. auto.
@@ -2142,8 +2153,7 @@ Module OrdProperties (M:S).
Above x m1 -> Add x e m1 m2 ->
eqA (fold f m2 i) (f x e (fold f m1 i)).
Proof.
- intros; do 2 rewrite fold_1; do 2 rewrite <- fold_left_rev_right.
- set (f':=fun y x0 => f (fst y) (snd y) x0) in *.
+ intros. rewrite 2 fold_spec_right. set (f':=uncurry f).
transitivity (fold_right f' i (rev (elements m1 ++ (x,e)::nil))).
apply fold_right_eqlistA with (eqA:=eqke) (eqB:=eqA); auto.
intros (k1,e1) (k2,e2) (Hk,He) a1 a2 Ha; unfold f'; simpl in *. apply P; auto.
@@ -2158,8 +2168,7 @@ Module OrdProperties (M:S).
Below x m1 -> Add x e m1 m2 ->
eqA (fold f m2 i) (fold f m1 (f x e i)).
Proof.
- intros; do 2 rewrite fold_1; do 2 rewrite <- fold_left_rev_right.
- set (f':=fun y x0 => f (fst y) (snd y) x0) in *.
+ intros. rewrite 2 fold_spec_right. set (f':=uncurry f).
transitivity (fold_right f' i (rev (((x,e)::nil)++elements m1))).
apply fold_right_eqlistA with (eqA:=eqke) (eqB:=eqA); auto.
intros (k1,e1) (k2,e2) (Hk,He) a1 a2 Ha; unfold f'; simpl in *; apply P; auto.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 04:14:28 +0000