diff options
Diffstat (limited to 'theories/FSets/FMapFacts.v')
| -rw-r--r-- | theories/FSets/FMapFacts.v | 1276 |
1 files changed, 943 insertions, 333 deletions
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index 05cd1892..df12166e 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id: FMapFacts.v 11359 2008-09-04 09:43:36Z notin $ *) +(* $Id: FMapFacts.v 11720 2008-12-28 07:12:15Z letouzey $ *) (** * Finite maps library *) @@ -20,9 +20,14 @@ Require Export FMapInterface. Set Implicit Arguments. Unset Strict Implicit. +Hint Extern 1 (Equivalence _) => constructor; congruence. + +Notation Leibniz := (@eq _) (only parsing). + + (** * Facts about weak maps *) -Module WFacts (E:DecidableType)(Import M:WSfun E). +Module WFacts_fun (E:DecidableType)(Import M:WSfun E). Notation eq_dec := E.eq_dec. Definition eqb x y := if eq_dec x y then true else false. @@ -32,6 +37,15 @@ Proof. destruct b; destruct b'; intuition. Qed. +Lemma eq_option_alt : forall (elt:Type)(o o':option elt), + o=o' <-> (forall e, o=Some e <-> o'=Some e). +Proof. +split; intros. +subst; split; auto. +destruct o; destruct o'; try rewrite H; auto. +symmetry; rewrite <- H; auto. +Qed. + Lemma MapsTo_fun : forall (elt:Type) m x (e e':elt), MapsTo x e m -> MapsTo x e' m -> e=e'. Proof. @@ -85,14 +99,10 @@ Qed. Lemma not_find_in_iff : forall m x, ~In x m <-> find x m = None. Proof. -intros. -generalize (find_mapsto_iff m x); destruct (find x m). -split; intros; try discriminate. -destruct H0. -exists e; rewrite H; auto. -split; auto. -intros; intros (e,H1). -rewrite H in H1; discriminate. +split; intros. +rewrite eq_option_alt. intro e. rewrite <- find_mapsto_iff. +split; intro H'; try discriminate. elim H; exists e; auto. +intros (e,He); rewrite find_mapsto_iff,H in He; discriminate. Qed. Lemma in_find_iff : forall m x, In x m <-> find x m <> None. @@ -334,21 +344,14 @@ Qed. Lemma find_o : forall m x y, E.eq x y -> find x m = find y m. Proof. -intros. -generalize (find_mapsto_iff m x) (find_mapsto_iff m y) (fun e => MapsTo_iff m e H). -destruct (find x m); destruct (find y m); intros. -rewrite <- H0; rewrite H2; rewrite H1; auto. -symmetry; rewrite <- H1; rewrite <- H2; rewrite H0; auto. -rewrite <- H0; rewrite H2; rewrite H1; auto. -auto. +intros. rewrite eq_option_alt. intro e. rewrite <- 2 find_mapsto_iff. +apply MapsTo_iff; auto. Qed. Lemma empty_o : forall x, find x (empty elt) = None. Proof. -intros. -case_eq (find x (empty elt)); intros; auto. -generalize (find_2 H). -rewrite empty_mapsto_iff; intuition. +intros. rewrite eq_option_alt. intro e. +rewrite <- find_mapsto_iff, empty_mapsto_iff; now intuition. Qed. Lemma empty_a : forall x, mem x (empty elt) = false. @@ -368,15 +371,12 @@ Qed. Lemma add_neq_o : forall m x y e, ~ E.eq x y -> find y (add x e m) = find y m. Proof. -intros. -case_eq (find y m); intros; auto with map. -case_eq (find y (add x e m)); intros; auto with map. -rewrite <- H0; symmetry. -apply find_1; apply add_3 with x e; auto with map. +intros. rewrite eq_option_alt. intro e'. rewrite <- 2 find_mapsto_iff. +apply add_neq_mapsto_iff; auto. Qed. Hint Resolve add_neq_o : map. -Lemma add_o : forall m x y e, +Lemma add_o : forall m x y e, find y (add x e m) = if eq_dec x y then Some e else find y m. Proof. intros; destruct (eq_dec x y); auto with map. @@ -404,45 +404,38 @@ Qed. Lemma remove_eq_o : forall m x y, E.eq x y -> find y (remove x m) = None. Proof. -intros. -generalize (remove_1 (m:=m) H). -generalize (find_mapsto_iff (remove x m) y). -destruct (find y (remove x m)); auto. -destruct 2. -exists e; rewrite H0; auto. +intros. rewrite eq_option_alt. intro e. +rewrite <- find_mapsto_iff, remove_mapsto_iff; now intuition. Qed. Hint Resolve remove_eq_o : map. -Lemma remove_neq_o : forall m x y, - ~ E.eq x y -> find y (remove x m) = find y m. +Lemma remove_neq_o : forall m x y, + ~ E.eq x y -> find y (remove x m) = find y m. Proof. -intros. -case_eq (find y m); intros; auto with map. -case_eq (find y (remove x m)); intros; auto with map. -rewrite <- H0; symmetry. -apply find_1; apply remove_3 with x; auto with map. +intros. rewrite eq_option_alt. intro e. +rewrite <- find_mapsto_iff, remove_neq_mapsto_iff; now intuition. Qed. Hint Resolve remove_neq_o : map. -Lemma remove_o : forall m x y, +Lemma remove_o : forall m x y, find y (remove x m) = if eq_dec x y then None else find y m. Proof. intros; destruct (eq_dec x y); auto with map. Qed. -Lemma remove_eq_b : forall m x y, +Lemma remove_eq_b : forall m x y, E.eq x y -> mem y (remove x m) = false. Proof. intros; rewrite mem_find_b; rewrite remove_eq_o; auto. Qed. -Lemma remove_neq_b : forall m x y, +Lemma remove_neq_b : forall m x y, ~ E.eq x y -> mem y (remove x m) = mem y m. Proof. intros; do 2 rewrite mem_find_b; rewrite remove_neq_o; auto. Qed. -Lemma remove_b : forall m x y, +Lemma remove_b : forall m x y, mem y (remove x m) = negb (eqb x y) && mem y m. Proof. intros; do 2 rewrite mem_find_b; rewrite remove_o; unfold eqb. @@ -506,7 +499,7 @@ Qed. Lemma map2_1bis : forall (m: t elt)(m': t elt') x (f:option elt->option elt'->option elt''), f None None = None -> - find x (map2 f m m') = f (find x m) (find x m'). + find x (map2 f m m') = f (find x m) (find x m'). Proof. intros. case_eq (find x m); intros. @@ -525,23 +518,16 @@ rewrite (find_1 H4) in H0; discriminate. rewrite (find_1 H4) in H1; discriminate. Qed. -Lemma elements_o : forall m x, +Lemma elements_o : forall m x, find x m = findA (eqb x) (elements m). Proof. -intros. -assert (forall e, find x m = Some e <-> InA (eq_key_elt (elt:=elt)) (x,e) (elements m)). - intros; rewrite <- find_mapsto_iff; apply elements_mapsto_iff. -assert (H0:=elements_3w m). -generalize (fun e => @findA_NoDupA _ _ _ E.eq_sym E.eq_trans eq_dec (elements m) x e H0). -fold (eqb x). -destruct (find x m); destruct (findA (eqb x) (elements m)); - simpl; auto; intros. -symmetry; rewrite <- H1; rewrite <- H; auto. -symmetry; rewrite <- H1; rewrite <- H; auto. -rewrite H; rewrite H1; auto. -Qed. - -Lemma elements_b : forall m x, +intros. rewrite eq_option_alt. intro e. +rewrite <- find_mapsto_iff, elements_mapsto_iff. +unfold eqb. +rewrite <- findA_NoDupA; intuition; try apply elements_3w; eauto. +Qed. + +Lemma elements_b : forall m x, mem x m = existsb (fun p => eqb x (fst p)) (elements m). Proof. intros. @@ -568,30 +554,41 @@ Qed. End BoolSpec. -Section Equalities. +Section Equalities. Variable elt:Type. + (** Another characterisation of [Equal] *) + +Lemma Equal_mapsto_iff : forall m1 m2 : t elt, + Equal m1 m2 <-> (forall k e, MapsTo k e m1 <-> MapsTo k e m2). +Proof. +intros m1 m2. split; [intros Heq k e|intros Hiff]. +rewrite 2 find_mapsto_iff, Heq. split; auto. +intro k. rewrite eq_option_alt. intro e. +rewrite <- 2 find_mapsto_iff; auto. +Qed. + (** * Relations between [Equal], [Equiv] and [Equivb]. *) (** First, [Equal] is [Equiv] with Leibniz on elements. *) -Lemma Equal_Equiv : forall (m m' : t elt), +Lemma Equal_Equiv : forall (m m' : t elt), Equal m m' <-> Equiv (@Logic.eq elt) m m'. Proof. - unfold Equal, Equiv; split; intros. - split; intros. - rewrite in_find_iff, in_find_iff, H; intuition. - rewrite find_mapsto_iff in H0,H1; congruence. - destruct H. - specialize (H y). - specialize (H0 y). - do 2 rewrite in_find_iff in H. - generalize (find_mapsto_iff m y)(find_mapsto_iff m' y). - do 2 destruct find; auto; intros. - f_equal; apply H0; [rewrite H1|rewrite H2]; auto. - destruct H as [H _]; now elim H. - destruct H as [_ H]; now elim H. +intros. rewrite Equal_mapsto_iff. split; intros. +split. +split; intros (e,Hin); exists e; [rewrite <- H|rewrite H]; auto. +intros; apply MapsTo_fun with m k; auto; rewrite H; auto. +split; intros H'. +destruct H. +assert (Hin : In k m') by (rewrite <- H; exists e; auto). +destruct Hin as (e',He'). +rewrite (H0 k e e'); auto. +destruct H. +assert (Hin : In k m) by (rewrite H; exists e; auto). +destruct Hin as (e',He'). +rewrite <- (H0 k e' e); auto. Qed. (** [Equivb] and [Equiv] and equivalent when [eq_elt] and [cmp] @@ -649,8 +646,8 @@ Lemma Equal_trans : forall (elt:Type)(m m' m'' : t elt), Equal m m' -> Equal m' m'' -> Equal m m''. Proof. unfold Equal; congruence. Qed. -Definition Equal_ST : forall elt:Type, Setoid_Theory (t elt) (@Equal _). -Proof. +Definition Equal_ST : forall elt:Type, Equivalence (@Equal elt). +Proof. constructor; red; [apply Equal_refl | apply Equal_sym | apply Equal_trans]. Qed. @@ -660,8 +657,6 @@ Add Relation key E.eq transitivity proved by E.eq_trans as KeySetoid. -Typeclasses unfold key. - Implicit Arguments Equal [[elt]]. Add Parametric Relation (elt : Type) : (t elt) Equal @@ -670,52 +665,52 @@ Add Parametric Relation (elt : Type) : (t elt) Equal transitivity proved by (@Equal_trans elt) as EqualSetoid. -Add Parametric Morphism elt : (@In elt) with signature E.eq ==> Equal ==> iff as In_m. +Add Parametric Morphism elt : (@In elt) + with signature E.eq ==> Equal ==> iff as In_m. Proof. unfold Equal; intros k k' Hk m m' Hm. rewrite (In_iff m Hk), in_find_iff, in_find_iff, Hm; intuition. Qed. Add Parametric Morphism elt : (@MapsTo elt) - with signature E.eq ==> @Logic.eq _ ==> Equal ==> iff as MapsTo_m. + with signature E.eq ==> Leibniz ==> Equal ==> iff as MapsTo_m. Proof. unfold Equal; intros k k' Hk e m m' Hm. -rewrite (MapsTo_iff m e Hk), find_mapsto_iff, find_mapsto_iff, Hm; +rewrite (MapsTo_iff m e Hk), find_mapsto_iff, find_mapsto_iff, Hm; intuition. Qed. -Add Parametric Morphism elt : (@Empty elt) with signature Equal ==> iff as Empty_m. +Add Parametric Morphism elt : (@Empty elt) + with signature Equal ==> iff as Empty_m. Proof. unfold Empty; intros m m' Hm; intuition. rewrite <-Hm in H0; eauto. rewrite Hm in H0; eauto. Qed. -Add Parametric Morphism elt : (@is_empty elt) with signature Equal ==> @Logic.eq _ as is_empty_m. +Add Parametric Morphism elt : (@is_empty elt) + with signature Equal ==> Leibniz as is_empty_m. Proof. intros m m' Hm. rewrite eq_bool_alt, <-is_empty_iff, <-is_empty_iff, Hm; intuition. Qed. -Add Parametric Morphism elt : (@mem elt) with signature E.eq ==> Equal ==> @Logic.eq _ as mem_m. +Add Parametric Morphism elt : (@mem elt) + with signature E.eq ==> Equal ==> Leibniz as mem_m. Proof. intros k k' Hk m m' Hm. rewrite eq_bool_alt, <- mem_in_iff, <-mem_in_iff, Hk, Hm; intuition. Qed. -Add Parametric Morphism elt : (@find elt) with signature E.eq ==> Equal ==> @Logic.eq _ as find_m. +Add Parametric Morphism elt : (@find elt) + with signature E.eq ==> Equal ==> Leibniz as find_m. Proof. -intros k k' Hk m m' Hm. -generalize (find_mapsto_iff m k)(find_mapsto_iff m' k') - (not_find_in_iff m k)(not_find_in_iff m' k'); -do 2 destruct find; auto; intros. -rewrite <- H, Hk, Hm, H0; auto. -rewrite <- H1, Hk, Hm, H2; auto. -symmetry; rewrite <- H2, <-Hk, <-Hm, H1; auto. +intros k k' Hk m m' Hm. rewrite eq_option_alt. intro e. +rewrite <- 2 find_mapsto_iff, Hk, Hm. split; auto. Qed. -Add Parametric Morphism elt : (@add elt) with signature - E.eq ==> @Logic.eq _ ==> Equal ==> Equal as add_m. +Add Parametric Morphism elt : (@add elt) + with signature E.eq ==> Leibniz ==> Equal ==> Equal as add_m. Proof. intros k k' Hk e m m' Hm y. rewrite add_o, add_o; do 2 destruct eq_dec; auto. @@ -723,8 +718,8 @@ elim n; rewrite <-Hk; auto. elim n; rewrite Hk; auto. Qed. -Add Parametric Morphism elt : (@remove elt) with signature - E.eq ==> Equal ==> Equal as remove_m. +Add Parametric Morphism elt : (@remove elt) + with signature E.eq ==> Equal ==> Equal as remove_m. Proof. intros k k' Hk m m' Hm y. rewrite remove_o, remove_o; do 2 destruct eq_dec; auto. @@ -732,7 +727,8 @@ elim n; rewrite <-Hk; auto. elim n; rewrite Hk; auto. Qed. -Add Parametric Morphism elt elt' : (@map elt elt') with signature @Logic.eq _ ==> Equal ==> Equal as map_m. +Add Parametric Morphism elt elt' : (@map elt elt') + with signature Leibniz ==> Equal ==> Equal as map_m. Proof. intros f m m' Hm y. rewrite map_o, map_o, Hm; auto. @@ -743,25 +739,23 @@ Qed. (* old name: *) Notation not_find_mapsto_iff := not_find_in_iff. -End WFacts. +End WFacts_fun. -(** * Same facts for full maps *) +(** * Same facts for self-contained weak sets and for full maps *) -Module Facts (M:S). - Module D := OT_as_DT M.E. - Include WFacts D M. -End Facts. +Module WFacts (M:S) := WFacts_fun M.E M. +Module Facts := WFacts. + +(** * Additional Properties for weak maps -(** * Additional Properties for weak maps - Results about [fold], [elements], induction principles... *) -Module WProperties (E:DecidableType)(M:WSfun E). - Module Import F:=WFacts E M. +Module WProperties_fun (E:DecidableType)(M:WSfun E). + Module Import F:=WFacts_fun E M. Import M. - Section Elt. + Section Elt. Variable elt:Type. Definition Add x (e:elt) m m' := forall y, find y m' = find y (add x e m). @@ -769,6 +763,44 @@ Module WProperties (E:DecidableType)(M:WSfun E). Notation eqke := (@eq_key_elt elt). Notation eqk := (@eq_key elt). + (** Complements about InA, NoDupA and findA *) + + Lemma InA_eqke_eqk : forall k1 k2 e1 e2 l, + E.eq k1 k2 -> InA eqke (k1,e1) l -> InA eqk (k2,e2) l. + Proof. + intros k1 k2 e1 e2 l Hk. rewrite 2 InA_alt. + intros ((k',e') & (Hk',He') & H); simpl in *. + exists (k',e'); split; auto. + red; simpl; eauto. + Qed. + + Lemma NoDupA_eqk_eqke : forall l, NoDupA eqk l -> NoDupA eqke l. + Proof. + induction 1; auto. + constructor; auto. + destruct x as (k,e). + eauto using InA_eqke_eqk. + Qed. + + Lemma findA_rev : forall l k, NoDupA eqk l -> + findA (eqb k) l = findA (eqb k) (rev l). + Proof. + intros. + case_eq (findA (eqb k) l). + intros. symmetry. + unfold eqb. + rewrite <- findA_NoDupA, InA_rev, findA_NoDupA + by eauto using NoDupA_rev; eauto. + case_eq (findA (eqb k) (rev l)); auto. + intros e. + unfold eqb. + rewrite <- findA_NoDupA, InA_rev, findA_NoDupA + by eauto using NoDupA_rev. + intro Eq; rewrite Eq; auto. + Qed. + + (** * Elements *) + Lemma elements_Empty : forall m:t elt, Empty m <-> elements m = nil. Proof. intros. @@ -793,29 +825,268 @@ Module WProperties (E:DecidableType)(M:WSfun E). rewrite <-elements_Empty; apply empty_1. Qed. - Lemma fold_Empty : forall m (A:Type)(f:key->elt->A->A)(i:A), - Empty m -> fold f m i = i. + (** * Conversions between maps and association lists. *) + + Definition of_list (l : list (key*elt)) := + List.fold_right (fun p => add (fst p) (snd p)) (empty _) l. + + Definition to_list := elements. + + Lemma of_list_1 : forall l k e, + NoDupA eqk l -> + (MapsTo k e (of_list l) <-> InA eqke (k,e) l). + Proof. + induction l as [|(k',e') l IH]; simpl; intros k e Hnodup. + rewrite empty_mapsto_iff, InA_nil; intuition. + inversion_clear Hnodup as [| ? ? Hnotin Hnodup']. + specialize (IH k e Hnodup'); clear Hnodup'. + rewrite add_mapsto_iff, InA_cons, <- IH. + unfold eq_key_elt at 1; simpl. + split; destruct 1 as [H|H]; try (intuition;fail). + destruct (eq_dec k k'); [left|right]; split; auto. + contradict Hnotin. + apply InA_eqke_eqk with k e; intuition. + Qed. + + Lemma of_list_1b : forall l k, + NoDupA eqk l -> + find k (of_list l) = findA (eqb k) l. + Proof. + induction l as [|(k',e') l IH]; simpl; intros k Hnodup. + apply empty_o. + inversion_clear Hnodup as [| ? ? Hnotin Hnodup']. + specialize (IH k Hnodup'); clear Hnodup'. + rewrite add_o, IH. + unfold eqb; do 2 destruct eq_dec; auto; elim n; eauto. + Qed. + + Lemma of_list_2 : forall l, NoDupA eqk l -> + equivlistA eqke l (to_list (of_list l)). + Proof. + intros l Hnodup (k,e). + rewrite <- elements_mapsto_iff, of_list_1; intuition. + Qed. + + Lemma of_list_3 : forall s, Equal (of_list (to_list s)) s. + Proof. + intros s k. + rewrite of_list_1b, elements_o; auto. + apply elements_3w. + Qed. + + (** * Fold *) + + (** ** Induction principles about fold contributed by S. Lescuyer *) + + (** In the following lemma, the step hypothesis is deliberately restricted + to the precise map m we are considering. *) + + Lemma fold_rec : + forall (A:Type)(P : t elt -> A -> Type)(f : key -> elt -> A -> A), + forall (i:A)(m:t elt), + (forall m, Empty m -> P m i) -> + (forall k e a m' m'', MapsTo k e m -> ~In k m' -> + Add k e m' m'' -> P m' a -> P m'' (f k e a)) -> + 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). + 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)). + intros k e a m' m'' H ? ? ?; eapply Hstep; eauto. + revert H; unfold l; rewrite InA_rev, elements_mapsto_iff; auto. + assert (Hdup : NoDupA eqk l). + unfold l. apply NoDupA_rev; try red; eauto. apply elements_3w. + assert (Hsame : forall k, find k m = findA (eqb k) l). + intros k. unfold l. rewrite elements_o, findA_rev; auto. + apply elements_3w. + clearbody l. clearbody F. clear Hstep f. revert m Hsame. induction l. + (* empty *) + intros m Hsame; simpl. + apply Hempty. intros k e. + rewrite find_mapsto_iff, Hsame; simpl; discriminate. + (* step *) + intros m Hsame; destruct a as (k,e); simpl. + apply Hstep' with (of_list l); auto. + rewrite InA_cons; left; red; auto. + inversion_clear Hdup. contradict H. destruct H as (e',He'). + apply InA_eqke_eqk with k e'; auto. + rewrite <- of_list_1; auto. + intro k'. rewrite Hsame, add_o, of_list_1b. simpl. + unfold eqb. do 2 destruct eq_dec; auto; elim n; eauto. + inversion_clear Hdup; auto. + apply IHl. + intros; eapply Hstep'; eauto. + inversion_clear Hdup; auto. + intros; apply of_list_1b. inversion_clear Hdup; auto. + Qed. + + (** Same, with [empty] and [add] instead of [Empty] and [Add]. In this + case, [P] must be compatible with equality of sets *) + + Theorem fold_rec_bis : + forall (A:Type)(P : t elt -> A -> Type)(f : key -> elt -> A -> A), + forall (i:A)(m:t elt), + (forall m m' a, Equal m m' -> P m a -> P m' a) -> + (P (empty _) i) -> + (forall k e a m', MapsTo k e m -> ~In k m' -> + P m' a -> P (add k e m') (f k e a)) -> + P m (fold f m i). + Proof. + intros A P f i m Pmorphism Pempty Pstep. + apply fold_rec; intros. + apply Pmorphism with (empty _); auto. intro k. rewrite empty_o. + case_eq (find k m0); auto; intros e'; rewrite <- find_mapsto_iff. + intro H'; elim (H k e'); auto. + apply Pmorphism with (add k e m'); try intro; auto. + Qed. + + Lemma fold_rec_nodep : + forall (A:Type)(P : A -> Type)(f : key -> elt -> A -> A)(i:A)(m:t elt), + P i -> (forall k e a, MapsTo k e m -> P a -> P (f k e a)) -> + P (fold f m i). + Proof. + intros; apply fold_rec_bis with (P:=fun _ => P); auto. + Qed. + + (** [fold_rec_weak] is a weaker principle than [fold_rec_bis] : + the step hypothesis must here be applicable anywhere. + At the same time, it looks more like an induction principle, + and hence can be easier to use. *) + + Lemma fold_rec_weak : + forall (A:Type)(P : t elt -> A -> Type)(f : key -> elt -> A -> A)(i:A), + (forall m m' a, Equal m m' -> P m a -> P m' a) -> + P (empty _) i -> + (forall k e a m, ~In k m -> P m a -> P (add k e m) (f k e a)) -> + forall m, P m (fold f m i). + Proof. + intros; apply fold_rec_bis; auto. + Qed. + + Lemma fold_rel : + forall (A B:Type)(R : A -> B -> Type) + (f : key -> elt -> A -> A)(g : key -> elt -> B -> B)(i : A)(j : B) + (m : t elt), + R i j -> + (forall k e a b, MapsTo k e m -> R a b -> R (f k e a) (g k e b)) -> + 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)). + 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). + clearbody l; clear Rstep m. + induction l; simpl; auto. + apply Rstep'; auto. + destruct a; simpl; rewrite InA_cons; left; red; auto. + Qed. + + (** From the induction principle on [fold], we can deduce some general + induction principles on maps. *) + + Lemma map_induction : + forall P : t elt -> Type, + (forall m, Empty m -> P m) -> + (forall m m', P m -> forall x e, ~In x m -> Add x e m m' -> P m') -> + forall m, P m. + Proof. + intros. apply (@fold_rec _ (fun s _ => P s) (fun _ _ _ => tt) tt m); eauto. + Qed. + + Lemma map_induction_bis : + forall P : t elt -> Type, + (forall m m', Equal m m' -> P m -> P m') -> + P (empty _) -> + (forall x e m, ~In x m -> P m -> P (add x e m)) -> + forall m, P m. Proof. intros. - rewrite fold_1. - rewrite elements_Empty in H; rewrite H; simpl; auto. + apply (@fold_rec_bis _ (fun s _ => P s) (fun _ _ _ => tt) tt m); eauto. Qed. - Lemma NoDupA_eqk_eqke : forall l, NoDupA eqk l -> NoDupA eqke l. + (** [fold] can be used to reconstruct the same initial set. *) + + Lemma fold_identity : forall m : t elt, Equal (fold (@add _) m (empty _)) m. Proof. - induction 1; auto. - constructor; auto. - contradict H. - destruct x as (x,y). - rewrite InA_alt in *; destruct H as ((a,b),((H1,H2),H3)); simpl in *. - exists (a,b); auto. + intros. + apply fold_rec with (P:=fun m acc => Equal acc m); auto with map. + intros m' Heq k'. + rewrite empty_o. + case_eq (find k' m'); auto; intros e'; rewrite <- find_mapsto_iff. + intro; elim (Heq k' e'); auto. + intros k e a m' m'' _ _ Hadd Heq k'. + rewrite Hadd, 2 add_o, Heq; auto. + Qed. + + Section Fold_More. + + (** ** Additional properties of fold *) + + (** When a function [f] is compatible and allows transpositions, we can + compute [fold f] in any order. *) + + Variables (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA)(f:key->elt->A->A). + + (** This is more convenient than a [compat_op eqke ...]. + In fact, every [compat_op], [compat_bool], etc, should + become a [Morphism] someday. *) + Hypothesis Comp : Morphism (E.eq==>Leibniz==>eqA==>eqA) f. + + Lemma fold_init : + forall m i i', eqA i i' -> eqA (fold f m i) (fold f m i'). + Proof. + intros. apply fold_rel with (R:=eqA); auto. + intros. apply Comp; auto. + Qed. + + Lemma fold_Empty : + forall m i, Empty m -> eqA (fold f m i) i. + Proof. + intros. apply fold_rec_nodep with (P:=fun a => eqA a i). + reflexivity. + intros. elim (H k e); auto. Qed. - Lemma fold_Equal : forall m1 m2 (A:Type)(eqA:A->A->Prop)(st:Setoid_Theory A eqA) - (f:key->elt->A->A)(i:A), - compat_op eqke eqA (fun y =>f (fst y) (snd y)) -> - transpose eqA (fun y => f (fst y) (snd y)) -> - Equal m1 m2 -> + (** As noticed by P. Casteran, asking for the general [SetoidList.transpose] + here is too restrictive. Think for instance of [f] being [M.add] : + in general, [M.add k e (M.add k e' m)] is not equivalent to + [M.add k e' (M.add k e m)]. Fortunately, we will never encounter this + situation during a real [fold], since the keys received by this [fold] + are unique. Hence we can ask the transposition property to hold only + for non-equal keys. + + This idea could be push slightly further, by asking the transposition + property to hold only for (non-equal) keys living in the map given to + [fold]. Please contact us if you need such a version. + + FSets could also benefit from a restricted [transpose], but for this + case the gain is unclear. *) + + Definition transpose_neqkey := + forall k k' e e' a, ~E.eq k k' -> + eqA (f k e (f k' e' a)) (f k' e' (f k e a)). + + Hypothesis Tra : transpose_neqkey. + + Lemma fold_commutes : forall i m k e, ~In k m -> + eqA (fold f m (f k e i)) (f k e (fold f m i)). + Proof. + intros i m k e Hnotin. + apply fold_rel with (R:= fun a b => eqA a (f k e b)); auto. + reflexivity. + intros. + transitivity (f k0 e0 (f k e b)). + apply Comp; auto. + apply Tra; auto. + contradict Hnotin; rewrite <- Hnotin; exists e0; auto. + Qed. + + Lemma fold_Equal : forall m1 m2 i, Equal m1 m2 -> eqA (fold f m1 i) (fold f m2 i). Proof. assert (eqke_refl : forall p, eqke p p). @@ -826,22 +1097,26 @@ Module WProperties (E:DecidableType)(M:WSfun E). intros (x1,x2) (y1,y2) (z1,z2); unfold eq_key_elt; simpl. intuition; eauto; congruence. intros; do 2 rewrite fold_1; do 2 rewrite <- fold_left_rev_right. - apply fold_right_equivlistA with (eqA:=eqke) (eqB:=eqA); auto. + apply fold_right_equivlistA_restr with + (R:=fun p p' => ~eqk p p') (eqA:=eqke) (eqB:=eqA); auto. + intros (k1,e1) (k2,e2) a1 a2 (Hk,He) Ha; simpl in *; apply Comp; auto. + unfold eq_key; auto. + intros (k1,e1) (k2,e2) (k3,e3). unfold eq_key_elt, eq_key; simpl. + intuition eauto. + intros (k,e) (k',e'); unfold eq_key; simpl; auto. apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3w. apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3w. + apply ForallList2_equiv1 with (eqA:=eqk); try red; eauto. + apply NoDupA_rev; try red; eauto. apply elements_3w. red; intros. do 2 rewrite InA_rev. destruct x; do 2 rewrite <- elements_mapsto_iff. do 2 rewrite find_mapsto_iff. - rewrite H1; split; auto. + rewrite H; split; auto. Qed. - Lemma fold_Add : forall m1 m2 x e (A:Type)(eqA:A->A->Prop)(st:Setoid_Theory A eqA) - (f:key->elt->A->A)(i:A), - compat_op eqke eqA (fun y =>f (fst y) (snd y)) -> - transpose eqA (fun y =>f (fst y) (snd y)) -> - ~In x m1 -> Add x e m1 m2 -> - eqA (fold f m2 i) (f x e (fold f m1 i)). + 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. assert (eqke_refl : forall p, eqke p p). red; auto. @@ -852,52 +1127,68 @@ Module WProperties (E:DecidableType)(M:WSfun E). intuition; eauto; congruence. 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 *. - change (f x e (fold_right f' i (rev (elements m1)))) - with (f' (x,e) (fold_right f' i (rev (elements m1)))). - apply fold_right_add with (eqA:=eqke)(eqB:=eqA); auto. + change (f k e (fold_right f' i (rev (elements m1)))) + with (f' (k,e) (fold_right f' i (rev (elements m1)))). + apply fold_right_add_restr with + (R:=fun p p'=>~eqk p p')(eqA:=eqke)(eqB:=eqA); auto. + intros (k1,e1) (k2,e2) a1 a2 (Hk,He) Ha; unfold f'; simpl in *. apply Comp; auto. + + unfold eq_key; auto. + intros (k1,e1) (k2,e2) (k3,e3). unfold eq_key_elt, eq_key; simpl. + intuition eauto. + unfold f'; intros (k1,e1) (k2,e2); unfold eq_key; simpl; auto. apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3w. apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3w. + apply ForallList2_equiv1 with (eqA:=eqk); try red; eauto. + apply NoDupA_rev; try red; eauto. apply elements_3w. rewrite InA_rev. - contradict H1. + contradict H. exists e. rewrite elements_mapsto_iff; auto. intros a. - rewrite InA_cons; do 2 rewrite InA_rev; + rewrite InA_cons; do 2 rewrite InA_rev; destruct a as (a,b); do 2 rewrite <- elements_mapsto_iff. do 2 rewrite find_mapsto_iff; unfold eq_key_elt; simpl. - rewrite H2. + rewrite H0. rewrite add_o. - destruct (eq_dec x a); intuition. - inversion H3; auto. + destruct (eq_dec k a); intuition. + inversion H1; auto. f_equal; auto. - elim H1. + elim H. exists b; apply MapsTo_1 with a; auto with map. elim n; auto. Qed. - Lemma cardinal_fold : forall m : t elt, + Lemma fold_add : forall m k e i, ~In k m -> + eqA (fold f (add k e m) i) (f k e (fold f m i)). + Proof. + intros. apply fold_Add; try red; auto. + Qed. + + End Fold_More. + + (** * Cardinal *) + + Lemma cardinal_fold : forall m : t elt, cardinal m = fold (fun _ _ => S) m 0. Proof. intros; rewrite cardinal_1, fold_1. symmetry; apply fold_left_length; auto. Qed. - Lemma cardinal_Empty : forall m : t elt, + Lemma cardinal_Empty : forall m : t elt, Empty m <-> cardinal m = 0. Proof. intros. rewrite cardinal_1, elements_Empty. destruct (elements m); intuition; discriminate. Qed. - - Lemma Equal_cardinal : forall m m' : t elt, + + Lemma Equal_cardinal : forall m m' : t elt, Equal m m' -> cardinal m = cardinal m'. Proof. intros; do 2 rewrite cardinal_fold. - apply fold_Equal with (eqA:=@eq _); auto. - constructor; auto; congruence. - red; auto. - red; auto. + apply fold_Equal with (eqA:=Leibniz); compute; auto. Qed. Lemma cardinal_1 : forall m : t elt, Empty m -> cardinal m = 0. @@ -910,10 +1201,7 @@ Module WProperties (E:DecidableType)(M:WSfun E). Proof. intros; do 2 rewrite cardinal_fold. change S with ((fun _ _ => S) x e). - apply fold_Add; auto. - constructor; intros; auto; congruence. - red; simpl; auto. - red; simpl; auto. + apply fold_Add with (eqA:=Leibniz); compute; auto. Qed. Lemma cardinal_inv_1 : forall m : t elt, @@ -943,27 +1231,16 @@ Module WProperties (E:DecidableType)(M:WSfun E). eauto. Qed. - Lemma map_induction : - forall P : t elt -> Type, - (forall m, Empty m -> P m) -> - (forall m m', P m -> forall x e, ~In x m -> Add x e m m' -> P m') -> - forall m, P m. - Proof. - intros; remember (cardinal m) as n; revert m Heqn; induction n; intros. - apply X; apply cardinal_inv_1; auto. + (** * Additional notions over maps *) - destruct (cardinal_inv_2 (sym_eq Heqn)) as ((x,e),H0); simpl in *. - assert (Add x e (remove x m) m). - red; intros. - rewrite add_o; rewrite remove_o; destruct (eq_dec x y); eauto with map. - apply X0 with (remove x m) x e; auto with map. - apply IHn; auto with map. - assert (S n = S (cardinal (remove x m))). - rewrite Heqn; eapply cardinal_2; eauto with map. - inversion H1; auto with map. - Qed. + Definition Disjoint (m m' : t elt) := + forall k, ~(In k m /\ In k m'). + + Definition Partition (m m1 m2 : t elt) := + Disjoint m1 m2 /\ + (forall k e, MapsTo k e m <-> MapsTo k e m1 \/ MapsTo k e m2). - (** * Let's emulate some functions not present in the interface *) + (** * Emulation of some functions lacking in the interface *) Definition filter (f : key -> elt -> bool)(m : t elt) := fold (fun k e m => if f k e then add k e m else m) m (empty _). @@ -977,122 +1254,411 @@ Module WProperties (E:DecidableType)(M:WSfun E). Definition partition (f : key -> elt -> bool)(m : t elt) := (filter f m, filter (fun k e => negb (f k e)) m). + (** [update] adds to [m1] all the bindings of [m2]. It can be seen as + an [union] operator which gives priority to its 2nd argument + in case of binding conflit. *) + + Definition update (m1 m2 : t elt) := fold (@add _) m2 m1. + + (** [restrict] keeps from [m1] only the bindings whose key is in [m2]. + It can be seen as an [inter] operator, with priority to its 1st argument + in case of binding conflit. *) + + Definition restrict (m1 m2 : t elt) := filter (fun k _ => mem k m2) m1. + + (** [diff] erases from [m1] all bindings whose key is in [m2]. *) + + Definition diff (m1 m2 : t elt) := filter (fun k _ => negb (mem k m2)) m1. + Section Specs. Variable f : key -> elt -> bool. - Hypothesis Hf : forall e, compat_bool E.eq (fun k => f k e). + Hypothesis Hf : Morphism (E.eq==>Leibniz==>Leibniz) f. - Lemma filter_iff : forall m k e, + Lemma filter_iff : forall m k e, MapsTo k e (filter f m) <-> MapsTo k e m /\ f k e = true. Proof. - unfold filter; intros. - rewrite fold_1. - rewrite <- fold_left_rev_right. - rewrite (elements_mapsto_iff m). - rewrite <- (InA_rev eqke (k,e) (elements m)). - assert (NoDupA eqk (rev (elements m))). - apply NoDupA_rev; auto; try apply elements_3w; auto. - intros (k1,e1); compute; auto. - intros (k1,e1)(k2,e2); compute; auto. - intros (k1,e1)(k2,e2)(k3,e3); compute; eauto. - induction (rev (elements m)); simpl; auto. - - rewrite empty_mapsto_iff. - intuition. - inversion H1. - - destruct a as (k',e'); simpl. - inversion_clear H. - case_eq (f k' e'); intros; simpl; - try rewrite add_mapsto_iff; rewrite IHl; clear IHl; intuition. - constructor; red; auto. - rewrite (Hf e' H2),H4 in H; auto. - inversion_clear H3. - compute in H2; destruct H2; auto. - destruct (E.eq_dec k' k); auto. - elim H0. - rewrite InA_alt in *; destruct H2 as (w,Hw); exists w; intuition. - red in H2; red; simpl in *; intuition. - rewrite e0; auto. - inversion_clear H3; auto. - compute in H2; destruct H2. - rewrite (Hf e H2),H3,H in H4; discriminate. + unfold filter. + set (f':=fun k e m => if f k e then add k e m else m). + intro m. pattern m, (fold f' m (empty _)). apply fold_rec. + + intros m' Hm' k e. rewrite empty_mapsto_iff. intuition. + elim (Hm' k e); auto. + + intros k e acc m1 m2 Hke Hn Hadd IH k' e'. + change (Equal m2 (add k e m1)) in Hadd; rewrite Hadd. + unfold f'; simpl. + case_eq (f k e); intros Hfke; simpl; + rewrite !add_mapsto_iff, IH; clear IH; intuition. + rewrite <- Hfke; apply Hf; auto. + destruct (eq_dec k k') as [Hk|Hk]; [left|right]; auto. + elim Hn; exists e'; rewrite Hk; auto. + assert (f k e = f k' e') by (apply Hf; auto). congruence. Qed. - + Lemma for_all_iff : forall m, for_all f m = true <-> (forall k e, MapsTo k e m -> f k e = true). Proof. - cut (forall m : t elt, - for_all f m = true <-> - (forall k e, InA eqke (k,e) (rev (elements m)) -> f k e = true)). - intros; rewrite H; split; intros. - apply H0; rewrite InA_rev, <- elements_mapsto_iff; auto. - apply H0; rewrite InA_rev, <- elements_mapsto_iff in H1; auto. - - unfold for_all; intros. - rewrite fold_1. - rewrite <- fold_left_rev_right. - assert (NoDupA eqk (rev (elements m))). - apply NoDupA_rev; auto; try apply elements_3w; auto. - intros (k1,e1); compute; auto. - intros (k1,e1)(k2,e2); compute; auto. - intros (k1,e1)(k2,e2)(k3,e3); compute; eauto. - induction (rev (elements m)); simpl; auto. - - intuition. - inversion H1. - - destruct a as (k,e); simpl. - inversion_clear H. - case_eq (f k e); intros; simpl; - try rewrite IHl; clear IHl; intuition. - inversion_clear H3; auto. - compute in H4; destruct H4. - rewrite (Hf e0 H3), H4; auto. - rewrite <-H, <-(H2 k e); auto. - constructor; red; auto. + unfold for_all. + set (f':=fun k e b => if f k e then b else false). + intro m. pattern m, (fold f' m true). apply fold_rec. + + intros m' Hm'. split; auto. intros _ k e Hke. elim (Hm' k e); auto. + + intros k e b m1 m2 _ Hn Hadd IH. clear m. + change (Equal m2 (add k e m1)) in Hadd. + unfold f'; simpl. case_eq (f k e); intros Hfke. + (* f k e = true *) + rewrite IH. clear IH. split; intros Hmapsto k' e' Hke'. + rewrite Hadd, add_mapsto_iff in Hke'. + destruct Hke' as [(?,?)|(?,?)]; auto. + rewrite <- Hfke; apply Hf; auto. + apply Hmapsto. rewrite Hadd, add_mapsto_iff; right; split; auto. + contradict Hn; exists e'; rewrite Hn; auto. + (* f k e = false *) + split; intros H; try discriminate. + rewrite <- Hfke. apply H. + rewrite Hadd, add_mapsto_iff; auto. Qed. - + Lemma exists_iff : forall m, - exists_ f m = true <-> + exists_ f m = true <-> (exists p, MapsTo (fst p) (snd p) m /\ f (fst p) (snd p) = true). Proof. - cut (forall m : t elt, - exists_ f m = true <-> - (exists p, InA eqke p (rev (elements m)) - /\ f (fst p) (snd p) = true)). - intros; rewrite H; split; intros. - destruct H0 as ((k,e),Hke); exists (k,e). - rewrite InA_rev, <-elements_mapsto_iff in Hke; auto. - destruct H0 as ((k,e),Hke); exists (k,e). - rewrite InA_rev, <-elements_mapsto_iff; auto. - unfold exists_; intros. - rewrite fold_1. - rewrite <- fold_left_rev_right. - assert (NoDupA eqk (rev (elements m))). - apply NoDupA_rev; auto; try apply elements_3w; auto. - intros (k1,e1); compute; auto. - intros (k1,e1)(k2,e2); compute; auto. - intros (k1,e1)(k2,e2)(k3,e3); compute; eauto. - induction (rev (elements m)); simpl; auto. - - intuition; try discriminate. - destruct H0 as ((k,e),(Hke,_)); inversion Hke. - - destruct a as (k,e); simpl. - inversion_clear H. - case_eq (f k e); intros; simpl; - try rewrite IHl; clear IHl; intuition. + unfold exists_. + set (f':=fun k e b => if f k e then true else b). + intro m. pattern m, (fold f' m false). apply fold_rec. + + intros m' Hm'. split; try (intros; discriminate). + intros ((k,e),(Hke,_)); simpl in *. elim (Hm' k e); auto. + + intros k e b m1 m2 _ Hn Hadd IH. clear m. + change (Equal m2 (add k e m1)) in Hadd. + unfold f'; simpl. case_eq (f k e); intros Hfke. + (* f k e = true *) + split; [intros _|auto]. exists (k,e); simpl; split; auto. - constructor; red; auto. - destruct H2 as ((k',e'),(Hke',Hf')); exists (k',e'); simpl; auto. - destruct H2 as ((k',e'),(Hke',Hf')); simpl in *. - inversion_clear Hke'. - compute in H2; destruct H2. - rewrite (Hf e' H2), H3,H in Hf'; discriminate. + rewrite Hadd, add_mapsto_iff; auto. + (* f k e = false *) + rewrite IH. clear IH. split; intros ((k',e'),(Hke1,Hke2)); simpl in *. + exists (k',e'); simpl; split; auto. + rewrite Hadd, add_mapsto_iff; right; split; auto. + contradict Hn. exists e'; rewrite Hn; auto. + rewrite Hadd, add_mapsto_iff in Hke1. destruct Hke1 as [(?,?)|(?,?)]. + assert (f k' e' = f k e) by (apply Hf; auto). congruence. exists (k',e'); auto. Qed. + End Specs. + Lemma Disjoint_alt : forall m m', + Disjoint m m' <-> + (forall k e e', MapsTo k e m -> MapsTo k e' m' -> False). + Proof. + unfold Disjoint; split. + intros H k v v' H1 H2. + apply H with k; split. + exists v; trivial. + exists v'; trivial. + intros H k ((v,Hv),(v',Hv')). + eapply H; eauto. + Qed. + + Section Partition. + Variable f : key -> elt -> bool. + Hypothesis Hf : Morphism (E.eq==>Leibniz==>Leibniz) f. + + Lemma partition_iff_1 : forall m m1 k e, + m1 = fst (partition f m) -> + (MapsTo k e m1 <-> MapsTo k e m /\ f k e = true). + Proof. + unfold partition; simpl; intros. subst m1. + apply filter_iff; auto. + Qed. + + Lemma partition_iff_2 : forall m m2 k e, + m2 = snd (partition f m) -> + (MapsTo k e m2 <-> MapsTo k e m /\ f k e = false). + Proof. + unfold partition; simpl; intros. subst m2. + rewrite filter_iff. + split; intros (H,H'); split; auto. + destruct (f k e); simpl in *; auto. + rewrite H'; auto. + repeat red; intros. f_equal. apply Hf; auto. + Qed. + + Lemma partition_Partition : forall m m1 m2, + partition f m = (m1,m2) -> Partition m m1 m2. + Proof. + intros. split. + rewrite Disjoint_alt. intros k e e'. + rewrite (@partition_iff_1 m m1), (@partition_iff_2 m m2) + by (rewrite H; auto). + intros (U,V) (W,Z). rewrite <- (MapsTo_fun U W) in Z; congruence. + intros k e. + rewrite (@partition_iff_1 m m1), (@partition_iff_2 m m2) + by (rewrite H; auto). + destruct (f k e); intuition. + Qed. + + End Partition. + + Lemma Partition_In : forall m m1 m2 k, + Partition m m1 m2 -> In k m -> {In k m1}+{In k m2}. + Proof. + intros m m1 m2 k Hm Hk. + destruct (In_dec m1 k) as [H|H]; [left|right]; auto. + destruct Hm as (Hm,Hm'). + destruct Hk as (e,He); rewrite Hm' in He; destruct He. + elim H; exists e; auto. + exists e; auto. + Defined. + + Lemma Disjoint_sym : forall m1 m2, Disjoint m1 m2 -> Disjoint m2 m1. + Proof. + intros m1 m2 H k (H1,H2). elim (H k); auto. + Qed. + + Lemma Partition_sym : forall m m1 m2, + Partition m m1 m2 -> Partition m m2 m1. + Proof. + intros m m1 m2 (H,H'); split. + apply Disjoint_sym; auto. + intros; rewrite H'; intuition. + Qed. + + Lemma Partition_Empty : forall m m1 m2, Partition m m1 m2 -> + (Empty m <-> (Empty m1 /\ Empty m2)). + Proof. + intros m m1 m2 (Hdisj,Heq). split. + intro He. + split; intros k e Hke; elim (He k e); rewrite Heq; auto. + intros (He1,He2) k e Hke. rewrite Heq in Hke. destruct Hke. + elim (He1 k e); auto. + elim (He2 k e); auto. + Qed. + + Lemma Partition_Add : + forall m m' x e , ~In x m -> Add x e m m' -> + forall m1 m2, Partition m' m1 m2 -> + exists m3, (Add x e m3 m1 /\ Partition m m3 m2 \/ + Add x e m3 m2 /\ Partition m m1 m3). + Proof. + unfold Partition. intros m m' x e Hn Hadd m1 m2 (Hdisj,Hor). + assert (Heq : Equal m (remove x m')). + change (Equal m' (add x e m)) in Hadd. rewrite Hadd. + intro k. rewrite remove_o, add_o. + destruct eq_dec as [He|Hne]; auto. + rewrite <- He, <- not_find_in_iff; auto. + assert (H : MapsTo x e m'). + change (Equal m' (add x e m)) in Hadd; rewrite Hadd. + apply add_1; auto. + rewrite Hor in H; destruct H. + + (* first case : x in m1 *) + exists (remove x m1); left. split; [|split]. + (* add *) + change (Equal m1 (add x e (remove x m1))). + intro k. + rewrite add_o, remove_o. + destruct eq_dec as [He|Hne]; auto. + rewrite <- He; apply find_1; auto. + (* disjoint *) + intros k (H1,H2). elim (Hdisj k). split; auto. + rewrite remove_in_iff in H1; destruct H1; auto. + (* mapsto *) + intros k' e'. + rewrite Heq, 2 remove_mapsto_iff, Hor. + intuition. + elim (Hdisj x); split; [exists e|exists e']; auto. + apply MapsTo_1 with k'; auto. + + (* second case : x in m2 *) + exists (remove x m2); right. split; [|split]. + (* add *) + change (Equal m2 (add x e (remove x m2))). + intro k. + rewrite add_o, remove_o. + destruct eq_dec as [He|Hne]; auto. + rewrite <- He; apply find_1; auto. + (* disjoint *) + intros k (H1,H2). elim (Hdisj k). split; auto. + rewrite remove_in_iff in H2; destruct H2; auto. + (* mapsto *) + intros k' e'. + rewrite Heq, 2 remove_mapsto_iff, Hor. + intuition. + elim (Hdisj x); split; [exists e'|exists e]; auto. + apply MapsTo_1 with k'; auto. + Qed. + + Lemma Partition_fold : + forall (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA)(f:key->elt->A->A), + Morphism (E.eq==>Leibniz==>eqA==>eqA) f -> + transpose_neqkey eqA f -> + forall m m1 m2 i, + Partition m m1 m2 -> + eqA (fold f m i) (fold f m1 (fold f m2 i)). + Proof. + intros A eqA st f Comp Tra. + induction m as [m Hm|m m' IH k e Hn Hadd] using map_induction. + + intros m1 m2 i Hp. rewrite (fold_Empty (eqA:=eqA)); auto. + rewrite (Partition_Empty Hp) in Hm. destruct Hm. + rewrite 2 (fold_Empty (eqA:=eqA)); auto. reflexivity. + + intros m1 m2 i Hp. + destruct (Partition_Add Hn Hadd Hp) as (m3,[(Hadd',Hp')|(Hadd',Hp')]). + (* fst case: m3 is (k,e)::m1 *) + assert (~In k m3). + contradict Hn. destruct Hn as (e',He'). + destruct Hp' as (Hp1,Hp2). exists e'. rewrite Hp2; auto. + transitivity (f k e (fold f m i)). + apply fold_Add with (eqA:=eqA); auto. + symmetry. + transitivity (f k e (fold f m3 (fold f m2 i))). + apply fold_Add with (eqA:=eqA); auto. + apply Comp; auto. + symmetry; apply IH; auto. + (* snd case: m3 is (k,e)::m2 *) + assert (~In k m3). + contradict Hn. destruct Hn as (e',He'). + destruct Hp' as (Hp1,Hp2). exists e'. rewrite Hp2; auto. + assert (~In k m1). + contradict Hn. destruct Hn as (e',He'). + destruct Hp' as (Hp1,Hp2). exists e'. rewrite Hp2; auto. + transitivity (f k e (fold f m i)). + apply fold_Add with (eqA:=eqA); auto. + transitivity (f k e (fold f m1 (fold f m3 i))). + apply Comp; auto using IH. + transitivity (fold f m1 (f k e (fold f m3 i))). + symmetry. + apply fold_commutes with (eqA:=eqA); auto. + apply fold_init with (eqA:=eqA); auto. + symmetry. + apply fold_Add with (eqA:=eqA); auto. + Qed. + + Lemma Partition_cardinal : forall m m1 m2, Partition m m1 m2 -> + cardinal m = cardinal m1 + cardinal m2. + Proof. + intros. + rewrite (cardinal_fold m), (cardinal_fold m1). + set (f:=fun (_:key)(_:elt)=>S). + setoid_replace (fold f m 0) with (fold f m1 (fold f m2 0)). + rewrite <- cardinal_fold. + intros. apply fold_rel with (R:=fun u v => u = v + cardinal m2); simpl; auto. + apply Partition_fold with (eqA:=@Logic.eq _); try red; auto. + compute; auto. + Qed. + + Lemma Partition_partition : forall m m1 m2, Partition m m1 m2 -> + let f := fun k (_:elt) => mem k m1 in + Equal m1 (fst (partition f m)) /\ Equal m2 (snd (partition f m)). + Proof. + intros m m1 m2 Hm f. + assert (Hf : Morphism (E.eq==>Leibniz==>Leibniz) f). + intros k k' Hk e e' _; unfold f; rewrite Hk; auto. + set (m1':= fst (partition f m)). + set (m2':= snd (partition f m)). + split; rewrite Equal_mapsto_iff; intros k e. + rewrite (@partition_iff_1 f Hf m m1') by auto. + unfold f. + rewrite <- mem_in_iff. + destruct Hm as (Hm,Hm'). + rewrite Hm'. + intuition. + exists e; auto. + elim (Hm k); split; auto; exists e; auto. + rewrite (@partition_iff_2 f Hf m m2') by auto. + unfold f. + rewrite <- not_mem_in_iff. + destruct Hm as (Hm,Hm'). + rewrite Hm'. + intuition. + elim (Hm k); split; auto; exists e; auto. + elim H1; exists e; auto. + Qed. + + Lemma update_mapsto_iff : forall m m' k e, + MapsTo k e (update m m') <-> + (MapsTo k e m' \/ (MapsTo k e m /\ ~In k m')). + Proof. + unfold update. + intros m m'. + pattern m', (fold (@add _) m' m). apply fold_rec. + + intros m0 Hm0 k e. + assert (~In k m0) by (intros (e0,He0); apply (Hm0 k e0); auto). + intuition. + elim (Hm0 k e); auto. + + intros k e m0 m1 m2 _ Hn Hadd IH k' e'. + change (Equal m2 (add k e m1)) in Hadd. + rewrite Hadd, 2 add_mapsto_iff, IH, add_in_iff. clear IH. intuition. + Qed. + + Lemma update_dec : forall m m' k e, MapsTo k e (update m m') -> + { MapsTo k e m' } + { MapsTo k e m /\ ~In k m'}. + Proof. + intros m m' k e H. rewrite update_mapsto_iff in H. + destruct (In_dec m' k) as [H'|H']; [left|right]; intuition. + elim H'; exists e; auto. + Defined. + + Lemma update_in_iff : forall m m' k, + In k (update m m') <-> In k m \/ In k m'. + Proof. + intros m m' k. split. + intros (e,H); rewrite update_mapsto_iff in H. + destruct H; [right|left]; exists e; intuition. + destruct (In_dec m' k) as [H|H]. + destruct H as (e,H). intros _; exists e. + rewrite update_mapsto_iff; left; auto. + destruct 1 as [H'|H']; [|elim H; auto]. + destruct H' as (e,H'). exists e. + rewrite update_mapsto_iff; right; auto. + Qed. + + Lemma diff_mapsto_iff : forall m m' k e, + MapsTo k e (diff m m') <-> MapsTo k e m /\ ~In k m'. + Proof. + intros m m' k e. + unfold diff. + rewrite filter_iff. + intuition. + rewrite mem_1 in *; auto; discriminate. + intros ? ? Hk _ _ _; rewrite Hk; auto. + Qed. + + Lemma diff_in_iff : forall m m' k, + In k (diff m m') <-> In k m /\ ~In k m'. + Proof. + intros m m' k. split. + intros (e,H); rewrite diff_mapsto_iff in H. + destruct H; split; auto. exists e; auto. + intros ((e,H),H'); exists e; rewrite diff_mapsto_iff; auto. + Qed. + + Lemma restrict_mapsto_iff : forall m m' k e, + MapsTo k e (restrict m m') <-> MapsTo k e m /\ In k m'. + Proof. + intros m m' k e. + unfold restrict. + rewrite filter_iff. + intuition. + intros ? ? Hk _ _ _; rewrite Hk; auto. + Qed. + + Lemma restrict_in_iff : forall m m' k, + In k (restrict m m') <-> In k m /\ In k m'. + Proof. + intros m m' k. split. + intros (e,H); rewrite restrict_mapsto_iff in H. + destruct H; split; auto. exists e; auto. + intros ((e,H),H'); exists e; rewrite restrict_mapsto_iff; auto. + Qed. + (** specialized versions analyzing only keys (resp. elements) *) Definition filter_dom (f : key -> bool) := filter (fun k _ => f k). @@ -1106,17 +1672,85 @@ Module WProperties (E:DecidableType)(M:WSfun E). End Elt. - Add Parametric Morphism elt : (@cardinal elt) with signature Equal ==> @Logic.eq _ as cardinal_m. + Add Parametric Morphism elt : (@cardinal elt) + with signature Equal ==> Leibniz as cardinal_m. Proof. intros; apply Equal_cardinal; auto. Qed. -End WProperties. - -(** * Same Properties for full maps *) - -Module Properties (M:S). - Module D := OT_as_DT M.E. - Include WProperties D M. -End Properties. + Add Parametric Morphism elt : (@Disjoint elt) + with signature Equal ==> Equal ==> iff as Disjoint_m. + Proof. + intros m1 m1' Hm1 m2 m2' Hm2. unfold Disjoint. split; intros. + rewrite <- Hm1, <- Hm2; auto. + rewrite Hm1, Hm2; auto. + Qed. + + Add Parametric Morphism elt : (@Partition elt) + with signature Equal ==> Equal ==> Equal ==> iff as Partition_m. + Proof. + intros m1 m1' Hm1 m2 m2' Hm2 m3 m3' Hm3. unfold Partition. + rewrite <- Hm2, <- Hm3. + split; intros (H,H'); split; auto; intros. + rewrite <- Hm1, <- Hm2, <- Hm3; auto. + rewrite Hm1, Hm2, Hm3; auto. + Qed. + + Add Parametric Morphism elt : (@update elt) + with signature Equal ==> Equal ==> Equal as update_m. + Proof. + intros m1 m1' Hm1 m2 m2' Hm2. + setoid_replace (update m1 m2) with (update m1' m2); unfold update. + apply fold_Equal with (eqA:=Equal); auto. + intros k k' Hk e e' He m m' Hm; rewrite Hk,He,Hm; red; auto. + intros k k' e e' i Hneq x. + rewrite !add_o; do 2 destruct eq_dec; auto. elim Hneq; eauto. + apply fold_init with (eqA:=Equal); auto. + intros k k' Hk e e' He m m' Hm; rewrite Hk,He,Hm; red; auto. + Qed. + + Add Parametric Morphism elt : (@restrict elt) + with signature Equal ==> Equal ==> Equal as restrict_m. + Proof. + intros m1 m1' Hm1 m2 m2' Hm2. + setoid_replace (restrict m1 m2) with (restrict m1' m2); + unfold restrict, filter. + apply fold_rel with (R:=Equal); try red; auto. + intros k e i i' H Hii' x. + pattern (mem k m2); rewrite Hm2. (* UGLY, see with Matthieu *) + destruct mem; rewrite Hii'; auto. + apply fold_Equal with (eqA:=Equal); auto. + intros k k' Hk e e' He m m' Hm; simpl in *. + pattern (mem k m2); rewrite Hk. (* idem *) + destruct mem; rewrite ?Hk,?He,Hm; red; auto. + intros k k' e e' i Hneq x. + case_eq (mem k m2); case_eq (mem k' m2); intros; auto. + rewrite !add_o; do 2 destruct eq_dec; auto. elim Hneq; eauto. + Qed. + + Add Parametric Morphism elt : (@diff elt) + with signature Equal ==> Equal ==> Equal as diff_m. + Proof. + intros m1 m1' Hm1 m2 m2' Hm2. + setoid_replace (diff m1 m2) with (diff m1' m2); + unfold diff, filter. + apply fold_rel with (R:=Equal); try red; auto. + intros k e i i' H Hii' x. + pattern (mem k m2); rewrite Hm2. (* idem *) + destruct mem; simpl; rewrite Hii'; auto. + apply fold_Equal with (eqA:=Equal); auto. + intros k k' Hk e e' He m m' Hm; simpl in *. + pattern (mem k m2); rewrite Hk. (* idem *) + destruct mem; simpl; rewrite ?Hk,?He,Hm; red; auto. + intros k k' e e' i Hneq x. + case_eq (mem k m2); case_eq (mem k' m2); intros; simpl; auto. + rewrite !add_o; do 2 destruct eq_dec; auto. elim Hneq; eauto. + Qed. + +End WProperties_fun. + +(** * Same Properties for self-contained weak maps and for full maps *) + +Module WProperties (M:WS) := WProperties_fun M.E M. +Module Properties := WProperties. (** * Properties specific to maps with ordered keys *) @@ -1151,7 +1785,8 @@ Module OrdProperties (M:S). Ltac clean_eauto := unfold O.eqke, O.ltk; simpl; intuition; eauto. - Definition gtb (p p':key*elt) := match E.compare (fst p) (fst p') with GT _ => true | _ => false end. + Definition gtb (p p':key*elt) := + match E.compare (fst p) (fst p') with GT _ => true | _ => false end. Definition leb p := fun p' => negb (gtb p p'). Definition elements_lt p m := List.filter (gtb p) (elements m). @@ -1275,7 +1910,7 @@ Module OrdProperties (M:S). rewrite find_mapsto_iff; rewrite (H0 t0); rewrite <- find_mapsto_iff. rewrite add_mapsto_iff; unfold O.eqke; simpl. intuition. - destruct (ME.eq_dec x t0); auto. + destruct (E.eq_dec x t0); auto. elimtype False. assert (In t0 m). exists e0; auto. @@ -1305,7 +1940,7 @@ Module OrdProperties (M:S). rewrite find_mapsto_iff; rewrite (H0 t0); rewrite <- find_mapsto_iff. rewrite add_mapsto_iff; unfold O.eqke; simpl. intuition. - destruct (ME.eq_dec x t0); auto. + destruct (E.eq_dec x t0); auto. elimtype False. assert (In t0 m). exists e0; auto. @@ -1361,7 +1996,7 @@ Module OrdProperties (M:S). inversion_clear H1; [ | inversion_clear H2; eauto ]. red in H3; simpl in H3; destruct H3. destruct p as (p1,p2). - destruct (ME.eq_dec p1 x). + destruct (E.eq_dec p1 x). apply ME.lt_eq with p1; auto. inversion_clear H2. inversion_clear H5. @@ -1513,74 +2148,53 @@ Module OrdProperties (M:S). (** The following lemma has already been proved on Weak Maps, but with one additionnal hypothesis (some [transpose] fact). *) - Lemma fold_Equal : forall s1 s2 (A:Type)(eqA:A->A->Prop)(st:Setoid_Theory A eqA) - (f:key->elt->A->A)(i:A), - compat_op eqke eqA (fun y =>f (fst y) (snd y)) -> - Equal s1 s2 -> - eqA (fold f s1 i) (fold f s2 i). + Lemma fold_Equal : forall m1 m2 (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA) + (f:key->elt->A->A)(i:A), + Morphism (E.eq==>Leibniz==>eqA==>eqA) f -> + Equal m1 m2 -> + eqA (fold f m1 i) (fold f m2 i). Proof. - intros. + intros m1 m2 A eqA st f i Hf Heq. do 2 rewrite fold_1. do 2 rewrite <- fold_left_rev_right. apply fold_right_eqlistA with (eqA:=eqke) (eqB:=eqA); auto. - apply eqlistA_rev. - apply elements_Equal_eqlistA; auto. + intros (k,e) (k',e') a a' (Hk,He) Ha; simpl in *; apply Hf; auto. + apply eqlistA_rev. apply elements_Equal_eqlistA. auto. Qed. - Lemma fold_Add : forall s1 s2 x e (A:Type)(eqA:A->A->Prop)(st:Setoid_Theory A eqA) - (f:key->elt->A->A)(i:A), - compat_op eqke eqA (fun y =>f (fst y) (snd y)) -> - transpose eqA (fun y =>f (fst y) (snd y)) -> - ~In x s1 -> Add x e s1 s2 -> - eqA (fold f s2 i) (f x e (fold f s1 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 *. - change (f x e (fold_right f' i (rev (elements s1)))) - with (f' (x,e) (fold_right f' i (rev (elements s1)))). - trans_st (fold_right f' i - (rev (elements_lt (x, e) s1 ++ (x,e) :: elements_ge (x, e) s1))). - apply fold_right_eqlistA with (eqA:=eqke) (eqB:=eqA); auto. - apply eqlistA_rev. - apply elements_Add; auto. - rewrite distr_rev; simpl. - rewrite app_ass; simpl. - rewrite (elements_split (x,e) s1). - rewrite distr_rev; simpl. - apply fold_right_commutes with (eqA:=eqke) (eqB:=eqA); auto. - Qed. - - Lemma fold_Add_Above : forall s1 s2 x e (A:Type)(eqA:A->A->Prop)(st:Setoid_Theory A eqA) - (f:key->elt->A->A)(i:A), - compat_op eqke eqA (fun y =>f (fst y) (snd y)) -> - Above x s1 -> Add x e s1 s2 -> - eqA (fold f s2 i) (f x e (fold f s1 i)). + Lemma fold_Add_Above : forall m1 m2 x e (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA) + (f:key->elt->A->A)(i:A), + Morphism (E.eq==>Leibniz==>eqA==>eqA) f -> + 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 *. - trans_st (fold_right f' i (rev (elements s1 ++ (x,e)::nil))). + 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) a1 a2 (Hk,He) Ha; unfold f'; simpl in *; apply H; auto. apply eqlistA_rev. apply elements_Add_Above; auto. rewrite distr_rev; simpl. - refl_st. + reflexivity. Qed. - Lemma fold_Add_Below : forall s1 s2 x e (A:Type)(eqA:A->A->Prop)(st:Setoid_Theory A eqA) - (f:key->elt->A->A)(i:A), - compat_op eqke eqA (fun y =>f (fst y) (snd y)) -> - Below x s1 -> Add x e s1 s2 -> - eqA (fold f s2 i) (fold f s1 (f x e i)). + Lemma fold_Add_Below : forall m1 m2 x e (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA) + (f:key->elt->A->A)(i:A), + Morphism (E.eq==>Leibniz==>eqA==>eqA) f -> + 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 *. - trans_st (fold_right f' i (rev (((x,e)::nil)++elements s1))). + 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) a1 a2 (Hk,He) Ha; unfold f'; simpl in *; apply H; auto. apply eqlistA_rev. simpl; apply elements_Add_Below; auto. rewrite distr_rev; simpl. rewrite fold_right_app. - refl_st. + reflexivity. Qed. End Fold_properties. @@ -1589,7 +2203,3 @@ Module OrdProperties (M:S). End OrdProperties. - - - - |