diff options
Diffstat (limited to 'theories/MMaps/MMapFacts.v')
| -rw-r--r-- | theories/MMaps/MMapFacts.v | 2434 |
1 files changed, 2434 insertions, 0 deletions
diff --git a/theories/MMaps/MMapFacts.v b/theories/MMaps/MMapFacts.v new file mode 100644 index 00000000..69066a7b --- /dev/null +++ b/theories/MMaps/MMapFacts.v @@ -0,0 +1,2434 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(** * Finite maps library *) + +(** This functor derives additional facts from [MMapInterface.S]. These + facts are mainly the specifications of [MMapInterface.S] written using + different styles: equivalence and boolean equalities. +*) + +Require Import Bool Equalities Orders OrdersFacts OrdersLists. +Require Import Morphisms Permutation SetoidPermutation. +Require Export MMapInterface. +Set Implicit Arguments. +Unset Strict Implicit. + +Lemma eq_bool_alt b b' : b=b' <-> (b=true <-> b'=true). +Proof. + destruct b, b'; intuition. +Qed. + +Lemma eq_option_alt {elt}(o o':option elt) : + o=o' <-> (forall e, o=Some e <-> o'=Some e). +Proof. +split; intros. +- now subst. +- destruct o, o'; rewrite ?H; auto. + symmetry; now apply H. +Qed. + +Lemma option_map_some {A B}(f:A->B) o : + option_map f o <> None <-> o <> None. +Proof. + destruct o; simpl. now split. split; now destruct 1. +Qed. + +(** * Properties about weak maps *) + +Module WProperties_fun (E:DecidableType)(Import M:WSfun E). + +Definition Empty {elt}(m : t elt) := forall x e, ~MapsTo x e m. + +(** A few things about E.eq *) + +Lemma eq_refl x : E.eq x x. Proof. apply E.eq_equiv. Qed. +Lemma eq_sym x y : E.eq x y -> E.eq y x. Proof. apply E.eq_equiv. Qed. +Lemma eq_trans x y z : E.eq x y -> E.eq y z -> E.eq x z. +Proof. apply E.eq_equiv. Qed. +Hint Immediate eq_refl eq_sym : map. +Hint Resolve eq_trans eq_equivalence E.eq_equiv : map. + +Definition eqb x y := if E.eq_dec x y then true else false. + +Lemma eqb_eq x y : eqb x y = true <-> E.eq x y. +Proof. + unfold eqb; case E.eq_dec; now intuition. +Qed. + +Lemma eqb_sym x y : eqb x y = eqb y x. +Proof. + apply eq_bool_alt. rewrite !eqb_eq. split; apply E.eq_equiv. +Qed. + +(** Initial results about MapsTo and In *) + +Lemma mapsto_fun {elt} m x (e e':elt) : + MapsTo x e m -> MapsTo x e' m -> e=e'. +Proof. +rewrite <- !find_spec. congruence. +Qed. + +Lemma in_find {elt} (m : t elt) x : In x m <-> find x m <> None. +Proof. + unfold In. split. + - intros (e,H). rewrite <-find_spec in H. congruence. + - destruct (find x m) as [e|] eqn:H. + + exists e. now apply find_spec. + + now destruct 1. +Qed. + +Lemma not_in_find {elt} (m : t elt) x : ~In x m <-> find x m = None. +Proof. + rewrite in_find. split; auto. + intros; destruct (find x m); trivial. now destruct H. +Qed. + +Notation in_find_iff := in_find (only parsing). +Notation not_find_in_iff := not_in_find (only parsing). + +(** * [Equal] is a setoid equality. *) + +Infix "==" := Equal (at level 30). + +Lemma Equal_refl {elt} (m : t elt) : m == m. +Proof. red; reflexivity. Qed. + +Lemma Equal_sym {elt} (m m' : t elt) : m == m' -> m' == m. +Proof. unfold Equal; auto. Qed. + +Lemma Equal_trans {elt} (m m' m'' : t elt) : + m == m' -> m' == m'' -> m == m''. +Proof. unfold Equal; congruence. Qed. + +Instance Equal_equiv {elt} : Equivalence (@Equal elt). +Proof. +constructor; [exact Equal_refl | exact Equal_sym | exact Equal_trans]. +Qed. + +Arguments Equal {elt} m m'. + +Instance MapsTo_m {elt} : + Proper (E.eq==>Logic.eq==>Equal==>iff) (@MapsTo elt). +Proof. +intros k k' Hk e e' <- m m' Hm. rewrite <- Hk. +now rewrite <- !find_spec, Hm. +Qed. + +Instance In_m {elt} : + Proper (E.eq==>Equal==>iff) (@In elt). +Proof. +intros k k' Hk m m' Hm. unfold In. +split; intros (e,H); exists e; revert H; + now rewrite Hk, <- !find_spec, Hm. +Qed. + +Instance find_m {elt} : Proper (E.eq==>Equal==>Logic.eq) (@find elt). +Proof. +intros k k' Hk m m' <-. +rewrite eq_option_alt. intros. now rewrite !find_spec, Hk. +Qed. + +Instance mem_m {elt} : Proper (E.eq==>Equal==>Logic.eq) (@mem elt). +Proof. +intros k k' Hk m m' Hm. now rewrite eq_bool_alt, !mem_spec, Hk, Hm. +Qed. + +Instance Empty_m {elt} : Proper (Equal==>iff) (@Empty elt). +Proof. +intros m m' Hm. unfold Empty. now setoid_rewrite Hm. +Qed. + +Instance is_empty_m {elt} : Proper (Equal ==> Logic.eq) (@is_empty elt). +Proof. +intros m m' Hm. rewrite eq_bool_alt, !is_empty_spec. + now setoid_rewrite Hm. +Qed. + +Instance add_m {elt} : Proper (E.eq==>Logic.eq==>Equal==>Equal) (@add elt). +Proof. +intros k k' Hk e e' <- m m' Hm y. +destruct (E.eq_dec k y) as [H|H]. +- rewrite <-H, add_spec1. now rewrite Hk, add_spec1. +- rewrite !add_spec2; trivial. now rewrite <- Hk. +Qed. + +Instance remove_m {elt} : Proper (E.eq==>Equal==>Equal) (@remove elt). +Proof. +intros k k' Hk m m' Hm y. +destruct (E.eq_dec k y) as [H|H]. +- rewrite <-H, remove_spec1. now rewrite Hk, remove_spec1. +- rewrite !remove_spec2; trivial. now rewrite <- Hk. +Qed. + +Instance map_m {elt elt'} : + Proper ((Logic.eq==>Logic.eq)==>Equal==>Equal) (@map elt elt'). +Proof. +intros f f' Hf m m' Hm y. rewrite !map_spec, Hm. +destruct (find y m'); simpl; trivial. f_equal. now apply Hf. +Qed. + +Instance mapi_m {elt elt'} : + Proper ((E.eq==>Logic.eq==>Logic.eq)==>Equal==>Equal) (@mapi elt elt'). +Proof. +intros f f' Hf m m' Hm y. +destruct (mapi_spec f m y) as (x,(Hx,->)). +destruct (mapi_spec f' m' y) as (x',(Hx',->)). +rewrite <- Hm. destruct (find y m); trivial. simpl. +f_equal. apply Hf; trivial. now rewrite Hx, Hx'. +Qed. + +Instance merge_m {elt elt' elt''} : + Proper ((E.eq==>Logic.eq==>Logic.eq==>Logic.eq)==>Equal==>Equal==>Equal) + (@merge elt elt' elt''). +Proof. +intros f f' Hf m1 m1' Hm1 m2 m2' Hm2 y. +destruct (find y m1) as [e1|] eqn:H1. +- apply find_spec in H1. + assert (H : In y m1 \/ In y m2) by (left; now exists e1). + destruct (merge_spec1 f H) as (y1,(Hy1,->)). + rewrite Hm1,Hm2 in H. + destruct (merge_spec1 f' H) as (y2,(Hy2,->)). + rewrite <- Hm1, <- Hm2. apply Hf; trivial. now transitivity y. +- destruct (find y m2) as [e2|] eqn:H2. + + apply find_spec in H2. + assert (H : In y m1 \/ In y m2) by (right; now exists e2). + destruct (merge_spec1 f H) as (y1,(Hy1,->)). + rewrite Hm1,Hm2 in H. + destruct (merge_spec1 f' H) as (y2,(Hy2,->)). + rewrite <- Hm1, <- Hm2. apply Hf; trivial. now transitivity y. + + apply not_in_find in H1. apply not_in_find in H2. + assert (H : ~In y (merge f m1 m2)). + { intro H. apply merge_spec2 in H. intuition. } + apply not_in_find in H. rewrite H. + symmetry. apply not_in_find. intro H'. + apply merge_spec2 in H'. rewrite <- Hm1, <- Hm2 in H'. + intuition. +Qed. + +(* Later: compatibility for cardinal, fold, ... *) + +(** ** Earlier specifications (cf. FMaps) *) + +Section OldSpecs. +Variable elt: Type. +Implicit Type m: t elt. +Implicit Type x y z: key. +Implicit Type e: elt. + +Lemma MapsTo_1 m x y e : E.eq x y -> MapsTo x e m -> MapsTo y e m. +Proof. + now intros ->. +Qed. + +Lemma find_1 m x e : MapsTo x e m -> find x m = Some e. +Proof. apply find_spec. Qed. + +Lemma find_2 m x e : find x m = Some e -> MapsTo x e m. +Proof. apply find_spec. Qed. + +Lemma mem_1 m x : In x m -> mem x m = true. +Proof. apply mem_spec. Qed. + +Lemma mem_2 m x : mem x m = true -> In x m. +Proof. apply mem_spec. Qed. + +Lemma empty_1 : Empty (@empty elt). +Proof. + intros x e. now rewrite <- find_spec, empty_spec. +Qed. + +Lemma is_empty_1 m : Empty m -> is_empty m = true. +Proof. + unfold Empty; rewrite is_empty_spec. setoid_rewrite <- find_spec. + intros H x. specialize (H x). + destruct (find x m) as [e|]; trivial. + now destruct (H e). +Qed. + +Lemma is_empty_2 m : is_empty m = true -> Empty m. +Proof. + rewrite is_empty_spec. intros H x e. now rewrite <- find_spec, H. +Qed. + +Lemma add_1 m x y e : E.eq x y -> MapsTo y e (add x e m). +Proof. + intros <-. rewrite <-find_spec. apply add_spec1. +Qed. + +Lemma add_2 m x y e e' : + ~ E.eq x y -> MapsTo y e m -> MapsTo y e (add x e' m). +Proof. + intro. now rewrite <- !find_spec, add_spec2. +Qed. + +Lemma add_3 m x y e e' : + ~ E.eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m. +Proof. + intro. rewrite <- !find_spec, add_spec2; trivial. +Qed. + +Lemma remove_1 m x y : E.eq x y -> ~ In y (remove x m). +Proof. + intros <-. apply not_in_find. apply remove_spec1. +Qed. + +Lemma remove_2 m x y e : + ~ E.eq x y -> MapsTo y e m -> MapsTo y e (remove x m). +Proof. + intro. now rewrite <- !find_spec, remove_spec2. +Qed. + +Lemma remove_3bis m x y e : + find y (remove x m) = Some e -> find y m = Some e. +Proof. + destruct (E.eq_dec x y) as [<-|H]. + - now rewrite remove_spec1. + - now rewrite remove_spec2. +Qed. + +Lemma remove_3 m x y e : MapsTo y e (remove x m) -> MapsTo y e m. +Proof. + rewrite <-!find_spec. apply remove_3bis. +Qed. + +Lemma bindings_1 m x e : + MapsTo x e m -> InA eq_key_elt (x,e) (bindings m). +Proof. apply bindings_spec1. Qed. + +Lemma bindings_2 m x e : + InA eq_key_elt (x,e) (bindings m) -> MapsTo x e m. +Proof. apply bindings_spec1. Qed. + +Lemma bindings_3w m : NoDupA eq_key (bindings m). +Proof. apply bindings_spec2w. Qed. + +Lemma cardinal_1 m : cardinal m = length (bindings m). +Proof. apply cardinal_spec. Qed. + +Lemma fold_1 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) (bindings m) i. +Proof. apply fold_spec. Qed. + +Lemma equal_1 m m' cmp : Equivb cmp m m' -> equal cmp m m' = true. +Proof. apply equal_spec. Qed. + +Lemma equal_2 m m' cmp : equal cmp m m' = true -> Equivb cmp m m'. +Proof. apply equal_spec. Qed. + +End OldSpecs. + +Lemma map_1 {elt elt'}(m: t elt)(x:key)(e:elt)(f:elt->elt') : + MapsTo x e m -> MapsTo x (f e) (map f m). +Proof. + rewrite <- !find_spec, map_spec. now intros ->. +Qed. + +Lemma map_2 {elt elt'}(m: t elt)(x:key)(f:elt->elt') : + In x (map f m) -> In x m. +Proof. + rewrite !in_find, map_spec. apply option_map_some. +Qed. + +Lemma mapi_1 {elt elt'}(m: t elt)(x:key)(e:elt)(f:key->elt->elt') : + MapsTo x e m -> + exists y, E.eq y x /\ MapsTo x (f y e) (mapi f m). +Proof. + destruct (mapi_spec f m x) as (y,(Hy,Eq)). + intro H. exists y; split; trivial. + rewrite <-find_spec in *. now rewrite Eq, H. +Qed. + +Lemma mapi_2 {elt elt'}(m: t elt)(x:key)(f:key->elt->elt') : + In x (mapi f m) -> In x m. +Proof. + destruct (mapi_spec f m x) as (y,(Hy,Eq)). + rewrite !in_find. intro H; contradict H. now rewrite Eq, H. +Qed. + +(** The ancestor [map2] of the current [merge] was dealing with functions + on datas only, not on keys. *) + +Definition map2 {elt elt' elt''} (f:option elt->option elt'->option elt'') + := merge (fun _ => f). + +Lemma map2_1 {elt elt' elt''}(m: t elt)(m': t elt') + (x:key)(f:option elt->option elt'->option elt'') : + In x m \/ In x m' -> + find x (map2 f m m') = f (find x m) (find x m'). +Proof. + intros. unfold map2. + now destruct (merge_spec1 (fun _ => f) H) as (y,(_,->)). +Qed. + +Lemma map2_2 {elt elt' elt''}(m: t elt)(m': t elt') + (x:key)(f:option elt->option elt'->option elt'') : + In x (map2 f m m') -> In x m \/ In x m'. +Proof. apply merge_spec2. Qed. + +Hint Immediate MapsTo_1 mem_2 is_empty_2 + map_2 mapi_2 add_3 remove_3 find_2 : map. +Hint Resolve mem_1 is_empty_1 is_empty_2 add_1 add_2 remove_1 + remove_2 find_1 fold_1 map_1 mapi_1 mapi_2 : map. + +(** ** Specifications written using equivalences *) + +Section IffSpec. +Variable elt: Type. +Implicit Type m: t elt. +Implicit Type x y z: key. +Implicit Type e: elt. + +Lemma in_iff m x y : E.eq x y -> (In x m <-> In y m). +Proof. now intros ->. Qed. + +Lemma mapsto_iff m x y e : E.eq x y -> (MapsTo x e m <-> MapsTo y e m). +Proof. now intros ->. Qed. + +Lemma mem_in_iff m x : In x m <-> mem x m = true. +Proof. symmetry. apply mem_spec. Qed. + +Lemma not_mem_in_iff m x : ~In x m <-> mem x m = false. +Proof. +rewrite mem_in_iff; destruct (mem x m); intuition. +Qed. + +Lemma mem_find m x : mem x m = true <-> find x m <> None. +Proof. + rewrite <- mem_in_iff. apply in_find. +Qed. + +Lemma not_mem_find m x : mem x m = false <-> find x m = None. +Proof. + rewrite <- not_mem_in_iff. apply not_in_find. +Qed. + +Lemma In_dec m x : { In x m } + { ~ In x m }. +Proof. + generalize (mem_in_iff m x). + destruct (mem x m); [left|right]; intuition. +Qed. + +Lemma find_mapsto_iff m x e : MapsTo x e m <-> find x m = Some e. +Proof. symmetry. apply find_spec. Qed. + +Lemma equal_iff m m' cmp : Equivb cmp m m' <-> equal cmp m m' = true. +Proof. symmetry. apply equal_spec. Qed. + +Lemma empty_mapsto_iff x e : MapsTo x e empty <-> False. +Proof. +rewrite <- find_spec, empty_spec. now split. +Qed. + +Lemma not_in_empty x : ~In x (@empty elt). +Proof. +intros (e,H). revert H. apply empty_mapsto_iff. +Qed. + +Lemma empty_in_iff x : In x (@empty elt) <-> False. +Proof. +split; [ apply not_in_empty | destruct 1 ]. +Qed. + +Lemma is_empty_iff m : Empty m <-> is_empty m = true. +Proof. split; [apply is_empty_1 | apply is_empty_2 ]. Qed. + +Lemma add_mapsto_iff m x y e e' : + MapsTo y e' (add x e m) <-> + (E.eq x y /\ e=e') \/ + (~E.eq x y /\ MapsTo y e' m). +Proof. +split. +- intros H. destruct (E.eq_dec x y); [left|right]; split; trivial. + + symmetry. apply (mapsto_fun H); auto with map. + + now apply add_3 with x e. +- destruct 1 as [(H,H')|(H,H')]; subst; auto with map. +Qed. + +Lemma add_mapsto_new m x y e e' : ~In x m -> + MapsTo y e' (add x e m) <-> (E.eq x y /\ e=e') \/ MapsTo y e' m. +Proof. + intros. + rewrite add_mapsto_iff. intuition. + right; split; trivial. contradict H. exists e'. now rewrite H. +Qed. + +Lemma in_add m x y e : In y m -> In y (add x e m). +Proof. + destruct (E.eq_dec x y) as [<-|H']. + - now rewrite !in_find, add_spec1. + - now rewrite !in_find, add_spec2. +Qed. + +Lemma add_in_iff m x y e : In y (add x e m) <-> E.eq x y \/ In y m. +Proof. +split. +- intros H. destruct (E.eq_dec x y); [now left|right]. + rewrite in_find, add_spec2 in H; trivial. now apply in_find. +- intros [<-|H]. + + exists e. now apply add_1. + + now apply in_add. +Qed. + +Lemma add_neq_mapsto_iff m x y e e' : + ~ E.eq x y -> (MapsTo y e' (add x e m) <-> MapsTo y e' m). +Proof. +split; [apply add_3|apply add_2]; auto. +Qed. + +Lemma add_neq_in_iff m x y e : + ~ E.eq x y -> (In y (add x e m) <-> In y m). +Proof. +split; intros (e',H0); exists e'. +- now apply add_3 with x e. +- now apply add_2. +Qed. + +Lemma remove_mapsto_iff m x y e : + MapsTo y e (remove x m) <-> ~E.eq x y /\ MapsTo y e m. +Proof. +split; [split|destruct 1]. +- intro E. revert H. now rewrite <-E, <- find_spec, remove_spec1. +- now apply remove_3 with x. +- now apply remove_2. +Qed. + +Lemma remove_in_iff m x y : In y (remove x m) <-> ~E.eq x y /\ In y m. +Proof. +unfold In; split; [ intros (e,H) | intros (E,(e,H)) ]. +- apply remove_mapsto_iff in H. destruct H; split; trivial. + now exists e. +- exists e. now apply remove_2. +Qed. + +Lemma remove_neq_mapsto_iff : forall m x y e, + ~ E.eq x y -> (MapsTo y e (remove x m) <-> MapsTo y e m). +Proof. +split; [apply remove_3|apply remove_2]; auto. +Qed. + +Lemma remove_neq_in_iff : forall m x y, + ~ E.eq x y -> (In y (remove x m) <-> In y m). +Proof. +split; intros (e',H0); exists e'. +- now apply remove_3 with x. +- now apply remove_2. +Qed. + +Lemma bindings_mapsto_iff m x e : + MapsTo x e m <-> InA eq_key_elt (x,e) (bindings m). +Proof. symmetry. apply bindings_spec1. Qed. + +Lemma bindings_in_iff m x : + In x m <-> exists e, InA eq_key_elt (x,e) (bindings m). +Proof. +unfold In; split; intros (e,H); exists e; now apply bindings_spec1. +Qed. + +End IffSpec. + +Lemma map_mapsto_iff {elt elt'} m x b (f : elt -> elt') : + MapsTo x b (map f m) <-> exists a, b = f a /\ MapsTo x a m. +Proof. +rewrite <-find_spec, map_spec. setoid_rewrite <- find_spec. +destruct (find x m); simpl; split. +- injection 1. now exists e. +- intros (a,(->,H)). now injection H as ->. +- discriminate. +- intros (a,(_,H)); discriminate. +Qed. + +Lemma map_in_iff {elt elt'} m x (f : elt -> elt') : + In x (map f m) <-> In x m. +Proof. +rewrite !in_find, map_spec. apply option_map_some. +Qed. + +Lemma mapi_in_iff {elt elt'} m x (f:key->elt->elt') : + In x (mapi f m) <-> In x m. +Proof. +rewrite !in_find. destruct (mapi_spec f m x) as (y,(_,->)). +apply option_map_some. +Qed. + +(** Unfortunately, we don't have simple equivalences for [mapi] + and [MapsTo]. The only correct one needs compatibility of [f]. *) + +Lemma mapi_inv {elt elt'} m x b (f : key -> elt -> elt') : + MapsTo x b (mapi f m) -> + exists a y, E.eq y x /\ b = f y a /\ MapsTo x a m. +Proof. +rewrite <- find_spec. setoid_rewrite <- find_spec. +destruct (mapi_spec f m x) as (y,(E,->)). +destruct (find x m); simpl. +- injection 1 as <-. now exists e, y. +- discriminate. +Qed. + +Lemma mapi_spec' {elt elt'} (f:key->elt->elt') : + Proper (E.eq==>Logic.eq==>Logic.eq) f -> + forall m x, + find x (mapi f m) = option_map (f x) (find x m). +Proof. + intros. destruct (mapi_spec f m x) as (y,(Hy,->)). + destruct (find x m); simpl; trivial. + now rewrite Hy. +Qed. + +Lemma mapi_1bis {elt elt'} m x e (f:key->elt->elt') : + Proper (E.eq==>Logic.eq==>Logic.eq) f -> + MapsTo x e m -> MapsTo x (f x e) (mapi f m). +Proof. +intros. destruct (mapi_1 f H0) as (y,(->,H2)). trivial. +Qed. + +Lemma mapi_mapsto_iff {elt elt'} m x b (f:key->elt->elt') : + Proper (E.eq==>Logic.eq==>Logic.eq) f -> + (MapsTo x b (mapi f m) <-> exists a, b = f x a /\ MapsTo x a m). +Proof. +rewrite <-find_spec. setoid_rewrite <-find_spec. +intros Pr. rewrite mapi_spec' by trivial. +destruct (find x m); simpl; split. +- injection 1 as <-. now exists e. +- intros (a,(->,H)). now injection H as <-. +- discriminate. +- intros (a,(_,H)). discriminate. +Qed. + +(** Things are even worse for [merge] : we don't try to state any + equivalence, see instead boolean results below. *) + +(** Useful tactic for simplifying expressions like + [In y (add x e (remove z m))] *) + +Ltac map_iff := + repeat (progress ( + rewrite add_mapsto_iff || rewrite add_in_iff || + rewrite remove_mapsto_iff || rewrite remove_in_iff || + rewrite empty_mapsto_iff || rewrite empty_in_iff || + rewrite map_mapsto_iff || rewrite map_in_iff || + rewrite mapi_in_iff)). + +(** ** Specifications written using boolean predicates *) + +Section BoolSpec. + +Lemma mem_find_b {elt}(m:t elt)(x:key) : + mem x m = if find x m then true else false. +Proof. +apply eq_bool_alt. rewrite mem_find. destruct (find x m). +- now split. +- split; (discriminate || now destruct 1). +Qed. + +Variable elt elt' elt'' : Type. +Implicit Types m : t elt. +Implicit Types x y z : key. +Implicit Types e : elt. + +Lemma mem_b m x y : E.eq x y -> mem x m = mem y m. +Proof. now intros ->. Qed. + +Lemma find_o m x y : E.eq x y -> find x m = find y m. +Proof. now intros ->. Qed. + +Lemma empty_o x : find x (@empty elt) = None. +Proof. apply empty_spec. Qed. + +Lemma empty_a x : mem x (@empty elt) = false. +Proof. apply not_mem_find. apply empty_spec. Qed. + +Lemma add_eq_o m x y e : + E.eq x y -> find y (add x e m) = Some e. +Proof. + intros <-. apply add_spec1. +Qed. + +Lemma add_neq_o m x y e : + ~ E.eq x y -> find y (add x e m) = find y m. +Proof. apply add_spec2. Qed. +Hint Resolve add_neq_o : map. + +Lemma add_o m x y e : + find y (add x e m) = if E.eq_dec x y then Some e else find y m. +Proof. +destruct (E.eq_dec x y); auto with map. +Qed. + +Lemma add_eq_b m x y e : + E.eq x y -> mem y (add x e m) = true. +Proof. +intros <-. apply mem_spec, add_in_iff. now left. +Qed. + +Lemma add_neq_b m x y e : + ~E.eq x y -> mem y (add x e m) = mem y m. +Proof. +intros. now rewrite !mem_find_b, add_neq_o. +Qed. + +Lemma add_b m x y e : + mem y (add x e m) = eqb x y || mem y m. +Proof. +rewrite !mem_find_b, add_o. unfold eqb. +now destruct (E.eq_dec x y). +Qed. + +Lemma remove_eq_o m x y : + E.eq x y -> find y (remove x m) = None. +Proof. intros ->. apply remove_spec1. Qed. + +Lemma remove_neq_o m x y : + ~ E.eq x y -> find y (remove x m) = find y m. +Proof. apply remove_spec2. Qed. + +Hint Resolve remove_eq_o remove_neq_o : map. + +Lemma remove_o m x y : + find y (remove x m) = if E.eq_dec x y then None else find y m. +Proof. +destruct (E.eq_dec x y); auto with map. +Qed. + +Lemma remove_eq_b m x y : + E.eq x y -> mem y (remove x m) = false. +Proof. +intros <-. now rewrite mem_find_b, remove_eq_o. +Qed. + +Lemma remove_neq_b m x y : + ~ E.eq x y -> mem y (remove x m) = mem y m. +Proof. +intros. now rewrite !mem_find_b, remove_neq_o. +Qed. + +Lemma remove_b m x y : + mem y (remove x m) = negb (eqb x y) && mem y m. +Proof. +rewrite !mem_find_b, remove_o; unfold eqb. +now destruct (E.eq_dec x y). +Qed. + +Lemma map_o m x (f:elt->elt') : + find x (map f m) = option_map f (find x m). +Proof. apply map_spec. Qed. + +Lemma map_b m x (f:elt->elt') : + mem x (map f m) = mem x m. +Proof. +rewrite !mem_find_b, map_o. now destruct (find x m). +Qed. + +Lemma mapi_b m x (f:key->elt->elt') : + mem x (mapi f m) = mem x m. +Proof. +apply eq_bool_alt; rewrite !mem_spec. apply mapi_in_iff. +Qed. + +Lemma mapi_o m x (f:key->elt->elt') : + Proper (E.eq==>Logic.eq==>Logic.eq) f -> + find x (mapi f m) = option_map (f x) (find x m). +Proof. intros; now apply mapi_spec'. Qed. + +Lemma merge_spec1' (f:key->option elt->option elt'->option elt'') : + Proper (E.eq==>Logic.eq==>Logic.eq==>Logic.eq) f -> + forall (m:t elt)(m':t elt') x, + In x m \/ In x m' -> + find x (merge f m m') = f x (find x m) (find x m'). +Proof. + intros Hf m m' x H. + now destruct (merge_spec1 f H) as (y,(->,->)). +Qed. + +Lemma merge_spec1_none (f:key->option elt->option elt'->option elt'') : + (forall x, f x None None = None) -> + forall (m: t elt)(m': t elt') x, + exists y, E.eq y x /\ find x (merge f m m') = f y (find x m) (find x m'). +Proof. +intros Hf m m' x. +destruct (find x m) as [e|] eqn:Hm. +- assert (H : In x m \/ In x m') by (left; exists e; now apply find_spec). + destruct (merge_spec1 f H) as (y,(Hy,->)). + exists y; split; trivial. now rewrite Hm. +- destruct (find x m') as [e|] eqn:Hm'. + + assert (H : In x m \/ In x m') by (right; exists e; now apply find_spec). + destruct (merge_spec1 f H) as (y,(Hy,->)). + exists y; split; trivial. now rewrite Hm, Hm'. + + exists x. split. reflexivity. rewrite Hf. + apply not_in_find. intro H. + apply merge_spec2 in H. apply not_in_find in Hm. apply not_in_find in Hm'. + intuition. +Qed. + +Lemma merge_spec1'_none (f:key->option elt->option elt'->option elt'') : + Proper (E.eq==>Logic.eq==>Logic.eq==>Logic.eq) f -> + (forall x, f x None None = None) -> + forall (m: t elt)(m': t elt') x, + find x (merge f m m') = f x (find x m) (find x m'). +Proof. + intros Hf Hf' m m' x. + now destruct (merge_spec1_none Hf' m m' x) as (y,(->,->)). +Qed. + +Lemma bindings_o : forall m x, + find x m = findA (eqb x) (bindings m). +Proof. +intros. rewrite eq_option_alt. intro e. +rewrite <- find_mapsto_iff, bindings_mapsto_iff. +unfold eqb. +rewrite <- findA_NoDupA; dintuition; try apply bindings_3w; eauto. +Qed. + +Lemma bindings_b : forall m x, + mem x m = existsb (fun p => eqb x (fst p)) (bindings m). +Proof. +intros. +apply eq_bool_alt. +rewrite mem_spec, bindings_in_iff, existsb_exists. +split. +- intros (e,H). + rewrite InA_alt in H. + destruct H as ((k,e'),((H1,H2),H')); simpl in *; subst e'. + exists (k, e); split; trivial. simpl. now apply eqb_eq. +- intros ((k,e),(H,H')); simpl in *. apply eqb_eq in H'. + exists e. rewrite InA_alt. exists (k,e). now repeat split. +Qed. + +End BoolSpec. + +Section Equalities. +Variable elt:Type. + +(** A few basic equalities *) + +Lemma eq_empty (m: t elt) : m == empty <-> is_empty m = true. +Proof. + unfold Equal. rewrite is_empty_spec. now setoid_rewrite empty_spec. +Qed. + +Lemma add_id (m: t elt) x e : add x e m == m <-> find x m = Some e. +Proof. + split. + - intros H. rewrite <- (H x). apply add_spec1. + - intros H y. rewrite !add_o. now destruct E.eq_dec as [<-|E]. +Qed. + +Lemma add_add_1 (m: t elt) x e : + add x e (add x e m) == add x e m. +Proof. + intros y. rewrite !add_o. destruct E.eq_dec; auto. +Qed. + +Lemma add_add_2 (m: t elt) x x' e e' : + ~E.eq x x' -> add x e (add x' e' m) == add x' e' (add x e m). +Proof. + intros H y. rewrite !add_o. + do 2 destruct E.eq_dec; auto. + elim H. now transitivity y. +Qed. + +Lemma remove_id (m: t elt) x : remove x m == m <-> ~In x m. +Proof. + rewrite not_in_find. split. + - intros H. rewrite <- (H x). apply remove_spec1. + - intros H y. rewrite !remove_o. now destruct E.eq_dec as [<-|E]. +Qed. + +Lemma remove_remove_1 (m: t elt) x : + remove x (remove x m) == remove x m. +Proof. + intros y. rewrite !remove_o. destruct E.eq_dec; auto. +Qed. + +Lemma remove_remove_2 (m: t elt) x x' : + remove x (remove x' m) == remove x' (remove x m). +Proof. + intros y. rewrite !remove_o. do 2 destruct E.eq_dec; auto. +Qed. + +Lemma remove_add_1 (m: t elt) x e : + remove x (add x e m) == remove x m. +Proof. + intro y. rewrite !remove_o, !add_o. now destruct E.eq_dec. +Qed. + +Lemma remove_add_2 (m: t elt) x x' e : + ~E.eq x x' -> remove x' (add x e m) == add x e (remove x' m). +Proof. + intros H y. rewrite !remove_o, !add_o. + do 2 destruct E.eq_dec; auto. + - elim H; now transitivity y. + - symmetry. now apply remove_eq_o. + - symmetry. now apply remove_neq_o. +Qed. + +Lemma add_remove_1 (m: t elt) x e : + add x e (remove x m) == add x e m. +Proof. + intro y. rewrite !add_o, !remove_o. now destruct E.eq_dec. +Qed. + +(** Another characterisation of [Equal] *) + +Lemma Equal_mapsto_iff : forall m1 m2 : t elt, + 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), + m == m' <-> Equiv Logic.eq m m'. +Proof. +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] + are related. *) + +Section Cmp. +Variable eq_elt : elt->elt->Prop. +Variable cmp : elt->elt->bool. + +Definition compat_cmp := + forall e e', cmp e e' = true <-> eq_elt e e'. + +Lemma Equiv_Equivb : compat_cmp -> + forall m m', Equiv eq_elt m m' <-> Equivb cmp m m'. +Proof. + unfold Equivb, Equiv, Cmp; intuition. + red in H; rewrite H; eauto. + red in H; rewrite <-H; eauto. +Qed. +End Cmp. + +(** Composition of the two last results: relation between [Equal] + and [Equivb]. *) + +Lemma Equal_Equivb : forall cmp, + (forall e e', cmp e e' = true <-> e = e') -> + forall (m m':t elt), m == m' <-> Equivb cmp m m'. +Proof. + intros; rewrite Equal_Equiv. + apply Equiv_Equivb; auto. +Qed. + +Lemma Equal_Equivb_eqdec : + forall eq_elt_dec : (forall e e', { e = e' } + { e <> e' }), + let cmp := fun e e' => if eq_elt_dec e e' then true else false in + forall (m m':t elt), m == m' <-> Equivb cmp m m'. +Proof. +intros; apply Equal_Equivb. +unfold cmp; clear cmp; intros. +destruct eq_elt_dec; now intuition. +Qed. + +End Equalities. + +(** * Results about [fold], [bindings], induction principles... *) + +Section Elt. + Variable elt:Type. + + Definition Add x (e:elt) m m' := m' == (add x e m). + + Notation eqke := (@eq_key_elt elt). + Notation eqk := (@eq_key elt). + + Instance eqk_equiv : Equivalence eqk. + Proof. unfold eq_key. destruct E.eq_equiv. constructor; eauto. Qed. + + Instance eqke_equiv : Equivalence eqke. + Proof. + unfold eq_key_elt; split; repeat red; intuition; simpl in *; + etransitivity; eauto. + Qed. + + (** Complements about InA, NoDupA and findA *) + + Lemma InA_eqke_eqk k k' e e' l : + E.eq k k' -> InA eqke (k,e) l -> InA eqk (k',e') l. + Proof. + intros Hk. rewrite 2 InA_alt. + intros ((k'',e'') & (Hk'',He'') & H); simpl in *; subst e''. + exists (k'',e); split; auto. red; simpl. now transitivity k. + Qed. + + Lemma NoDupA_incl {A} (R R':relation A) : + (forall x y, R x y -> R' x y) -> + forall l, NoDupA R' l -> NoDupA R l. + Proof. + intros Incl. + induction 1 as [ | a l E _ IH ]; constructor; auto. + contradict E. revert E. rewrite 2 InA_alt. firstorder. + Qed. + + Lemma NoDupA_eqk_eqke l : NoDupA eqk l -> NoDupA eqke l. + Proof. + apply NoDupA_incl. now destruct 1. + Qed. + + Lemma findA_rev l k : NoDupA eqk l -> + findA (eqb k) l = findA (eqb k) (rev l). + Proof. + intros H. apply eq_option_alt. intros e. unfold eqb. + rewrite <- !findA_NoDupA, InA_rev; eauto with map. reflexivity. + change (NoDupA eqk (rev l)). apply NoDupA_rev; auto using eqk_equiv. + Qed. + + (** * Bindings *) + + Lemma bindings_Empty (m:t elt) : Empty m <-> bindings m = nil. + Proof. + unfold Empty. split; intros H. + - assert (H' : forall a, ~ List.In a (bindings m)). + { intros (k,e) H'. apply (H k e). + rewrite bindings_mapsto_iff, InA_alt. + exists (k,e); repeat split; auto with map. } + destruct (bindings m) as [|p l]; trivial. + destruct (H' p); simpl; auto. + - intros x e. rewrite bindings_mapsto_iff, InA_alt. + rewrite H. now intros (y,(E,H')). + Qed. + + Lemma bindings_empty : bindings (@empty elt) = nil. + Proof. + rewrite <-bindings_Empty; apply empty_1. + Qed. + + (** * 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 := + List.fold_right (uncurry (@add _)) (@empty elt). + + Definition to_list := bindings. + + 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. + - unfold uncurry; simpl. + 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 (E.eq_dec k k'); [left|right]; split; auto with map. + 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. + unfold uncurry; simpl. + inversion_clear Hnodup as [| ? ? Hnotin Hnodup']. + specialize (IH k Hnodup'); clear Hnodup'. + rewrite add_o, IH, eqb_sym. unfold eqb; now destruct E.eq_dec. + 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 <- bindings_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, bindings_o; auto. + apply bindings_3w. + Qed. + + (** * 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 (bindings 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 + 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_spec_right. + set (F:=uncurry f). + set (l:=rev (bindings 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, bindings_mapsto_iff; auto with *. } + assert (Hdup : NoDupA eqk l). + { unfold l. apply NoDupA_rev; try red; unfold eq_key ; eauto with *. + apply bindings_3w. } + assert (Hsame : forall k, find k m = findA (eqb k) l). + { intros k. unfold l. rewrite bindings_o, findA_rev; auto. + apply bindings_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 with map. + + inversion_clear Hdup. contradict H. destruct H as (e',He'). + apply InA_eqke_eqk with k e'; auto with map. + rewrite <- of_list_1; auto. + + intro k'. rewrite Hsame, add_o, of_list_1b. simpl. + rewrite eqb_sym. unfold eqb. now destruct E.eq_dec. + inversion_clear Hdup; auto with map. + + 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. + rewrite 2 fold_spec_right. set (l:=rev (bindings 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)). + { intros; apply Rstep; auto. + rewrite bindings_mapsto_iff, <- InA_rev; auto with map. } + clearbody l; clear Rstep m. + induction l; simpl; auto. + apply Rstep'; auto. + destruct a; simpl; rewrite InA_cons; left; red; auto with map. + 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. + apply (@fold_rec_bis _ (fun s _ => P s) (fun _ _ _ => tt) tt m); eauto. + Qed. + + (** [fold] can be used to reconstruct the same initial set. *) + + Lemma fold_identity : forall m : t elt, Equal (fold (@add _) m empty) m. + Proof. + 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'. + red in Heq. 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). + + Lemma fold_Empty (f:key->elt->A->A) : + 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_init (f:key->elt->A->A) : + Proper (E.eq==>eq==>eqA==>eqA) f -> + forall m i i', eqA i i' -> eqA (fold f m i) (fold f m i'). + Proof. + intros Hf m i i' Hi. apply fold_rel with (R:=eqA); auto. + intros. now apply Hf. + Qed. + + (** Transpositions of f (a.k.a diamond property). + Could we swap two sequential calls to f, i.e. do we have: + + f k e (f k' e' a) == f k' e' (f k e a) + + First, we do no need this equation for all keys, but only + when k and k' aren't equal, as suggested by Pierre Castéran. + Think for instance of [f] being [M.add] : in general, we don't have + [M.add k e (M.add k e' m) == 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. + NB: without this condition, this condition would be + [SetoidList.transpose2]. + + Secondly, instead of the equation above, we now use a statement + with more basic equalities, allowing to prove [fold_commutes] even + when [f] isn't a morphism. + NB: When [f] is a morphism, [Diamond f] gives back the equation above. +*) + + Definition Diamond (f:key->elt->A->A) := + forall k k' e e' a b b', ~E.eq k k' -> + eqA (f k e a) b -> eqA (f k' e' a) b' -> eqA (f k e b') (f k' e' b). + + Lemma fold_commutes (f:key->elt->A->A) : + Diamond f -> + 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 Hf i m k e H. + apply fold_rel with (R:= fun a b => eqA a (f k e b)); auto. + - reflexivity. + - intros k' e' b a Hm E. + apply Hf with a; try easy. + contradict H; rewrite <- H. now exists e'. + Qed. + + Hint Resolve NoDupA_eqk_eqke NoDupA_rev bindings_3w : map. + + Lemma fold_Proper (f:key->elt->A->A) : + Proper (E.eq==>eq==>eqA==>eqA) f -> + Diamond f -> + Proper (Equal==>eqA==>eqA) (fold f). + Proof. + intros Hf Hf' m1 m2 Hm i j Hi. + rewrite 2 fold_spec_right. + assert (NoDupA eqk (rev (bindings m1))) by (auto with * ). + assert (NoDupA eqk (rev (bindings m2))) by (auto with * ). + apply fold_right_equivlistA_restr2 with (R:=complement eqk)(eqA:=eqke) + ; auto with *. + - intros (k1,e1) (k2,e2) (Hk,He) a1 a2 Ha; simpl in *. now apply Hf. + - unfold complement, eq_key, eq_key_elt; repeat red. intuition eauto with map. + - intros (k,e) (k',e') z z' h h'; unfold eq_key, uncurry;simpl; auto. + rewrite h'. eapply Hf'; now eauto. + - rewrite <- NoDupA_altdef; auto. + - intros (k,e). + rewrite 2 InA_rev, <- 2 bindings_mapsto_iff, 2 find_mapsto_iff, Hm; + auto with *. + Qed. + + Lemma fold_Equal (f:key->elt->A->A) : + Proper (E.eq==>eq==>eqA==>eqA) f -> + Diamond f -> + forall m1 m2 i, + Equal m1 m2 -> + eqA (fold f m1 i) (fold f m2 i). + Proof. + intros. now apply fold_Proper. + Qed. + + Lemma fold_Add (f:key->elt->A->A) : + Proper (E.eq==>eq==>eqA==>eqA) f -> + Diamond f -> + 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 Hf Hf' m1 m2 k e i Hm1 Hm2. + rewrite 2 fold_spec_right. + set (f':=uncurry f). + change (f k e (fold_right f' i (rev (bindings m1)))) + with (f' (k,e) (fold_right f' i (rev (bindings m1)))). + assert (NoDupA eqk (rev (bindings m1))) by (auto with * ). + assert (NoDupA eqk (rev (bindings m2))) by (auto with * ). + apply fold_right_add_restr with + (R:=complement eqk)(eqA:=eqke); auto with *. + - intros (k1,e1) (k2,e2) (Hk,He) a a' Ha; unfold f'; simpl in *. now apply Hf. + - unfold complement, eq_key_elt, eq_key; repeat red; intuition eauto with map. + - intros (k1,e1) (k2,e2) z1 z2; unfold eq_key, f', uncurry; simpl. + eapply Hf'; now eauto. + - rewrite <- NoDupA_altdef; auto. + - rewrite InA_rev, <- bindings_mapsto_iff by (auto with * ). firstorder. + - intros (a,b). + rewrite InA_cons, 2 InA_rev, <- 2 bindings_mapsto_iff, + 2 find_mapsto_iff by (auto with * ). + unfold eq_key_elt; simpl. + rewrite Hm2, !find_spec, add_mapsto_new; intuition. + Qed. + + Lemma fold_add (f:key->elt->A->A) : + Proper (E.eq==>eq==>eqA==>eqA) f -> + Diamond f -> + 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. now apply fold_Add. + Qed. + + End Fold_More. + + (** * Cardinal *) + + Lemma cardinal_fold (m : t elt) : + cardinal m = fold (fun _ _ => S) m 0. + Proof. + rewrite cardinal_1, fold_1. + symmetry; apply fold_left_length; auto. + Qed. + + Lemma cardinal_Empty : forall m : t elt, + Empty m <-> cardinal m = 0. + Proof. + intros. + rewrite cardinal_1, bindings_Empty. + destruct (bindings m); intuition; discriminate. + Qed. + + Lemma Equal_cardinal (m m' : t elt) : + Equal m m' -> cardinal m = cardinal m'. + Proof. + intro. rewrite 2 cardinal_fold. + apply fold_Equal with (eqA:=eq); try congruence; auto with map. + Qed. + + Lemma cardinal_0 (m : t elt) : Empty m -> cardinal m = 0. + Proof. + intros; rewrite <- cardinal_Empty; auto. + Qed. + + Lemma cardinal_S m m' x e : + ~ In x m -> Add x e m m' -> cardinal m' = S (cardinal m). + Proof. + intros. rewrite 2 cardinal_fold. + change S with ((fun _ _ => S) x e). + apply fold_Add with (eqA:=eq); try congruence; auto with map. + Qed. + + Lemma cardinal_inv_1 : forall m : t elt, + cardinal m = 0 -> Empty m. + Proof. + intros; rewrite cardinal_Empty; auto. + Qed. + Hint Resolve cardinal_inv_1 : map. + + Lemma cardinal_inv_2 : + forall m n, cardinal m = S n -> { p : key*elt | MapsTo (fst p) (snd p) m }. + Proof. + intros; rewrite M.cardinal_spec in *. + generalize (bindings_mapsto_iff m). + destruct (bindings m); try discriminate. + exists p; auto. + rewrite H0; destruct p; simpl; auto. + constructor; red; auto with map. + Qed. + + Lemma cardinal_inv_2b : + forall m, cardinal m <> 0 -> { p : key*elt | MapsTo (fst p) (snd p) m }. + Proof. + intros. + generalize (@cardinal_inv_2 m); destruct cardinal. + elim H;auto. + eauto. + Qed. + + Lemma not_empty_mapsto (m : t elt) : + ~Empty m -> exists k e, MapsTo k e m. + Proof. + intro. + destruct (@cardinal_inv_2b m) as ((k,e),H'). + contradict H. now apply cardinal_inv_1. + exists k; now exists e. + Qed. + + Lemma not_empty_in (m:t elt) : + ~Empty m -> exists k, In k m. + Proof. + intro. destruct (not_empty_mapsto H) as (k,Hk). + now exists k. + Qed. + + (** * Additional notions over maps *) + + 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). + + (** * 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. + + Definition for_all (f : key -> elt -> bool)(m : t elt) := + fold (fun k e b => if f k e then b else false) m true. + + Definition exists_ (f : key -> elt -> bool)(m : t elt) := + fold (fun k e b => if f k e then true else b) m false. + + 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. + + (** Properties of these abbreviations *) + + Lemma filter_iff (f : key -> elt -> bool) : + Proper (E.eq==>eq==>eq) f -> + forall m k e, + MapsTo k e (filter f m) <-> MapsTo k e m /\ f k e = true. + Proof. + unfold filter. + set (f':=fun k e m => if f k e then add k e m else m). + intros Hf 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. + rewrite add_mapsto_new by trivial. + case_eq (f k e); intros Hfke; simpl; + rewrite ?add_mapsto_iff, IH; clear IH; intuition. + + rewrite <- Hfke; apply Hf; auto with map. + + right. repeat split; trivial. contradict Hn. rewrite Hn. now exists e'. + + assert (f k e = f k' e') by (apply Hf; auto). congruence. + Qed. + + Lemma for_all_filter f m : + for_all f m = is_empty (filter (fun k e => negb (f k e)) m). + Proof. + unfold for_all, filter. + eapply fold_rel with (R:=fun x y => x = is_empty y). + - symmetry. apply is_empty_iff. apply empty_1. + - intros; subst. destruct (f k e); simpl; trivial. + symmetry. apply not_true_is_false. rewrite is_empty_spec. + intros H'. specialize (H' k). now rewrite add_spec1 in H'. + Qed. + + Lemma exists_filter f m : + exists_ f m = negb (is_empty (filter f m)). + Proof. + unfold for_all, filter. + eapply fold_rel with (R:=fun x y => x = negb (is_empty y)). + - symmetry. rewrite negb_false_iff. apply is_empty_iff. apply empty_1. + - intros; subst. destruct (f k e); simpl; trivial. + symmetry. rewrite negb_true_iff. apply not_true_is_false. + rewrite is_empty_spec. + intros H'. specialize (H' k). now rewrite add_spec1 in H'. + Qed. + + Lemma for_all_iff f m : + Proper (E.eq==>eq==>eq) f -> + (for_all f m = true <-> (forall k e, MapsTo k e m -> f k e = true)). + Proof. + intros Hf. + rewrite for_all_filter. + rewrite <- is_empty_iff. unfold Empty. + split; intros H k e; specialize (H k e); + rewrite filter_iff in * by solve_proper; intuition. + - destruct (f k e); auto. + - now rewrite H0 in H2. + Qed. + + Lemma exists_iff f m : + Proper (E.eq==>eq==>eq) f -> + (exists_ f m = true <-> + (exists k e, MapsTo k e m /\ f k e = true)). + Proof. + intros Hf. + rewrite exists_filter. rewrite negb_true_iff. + rewrite <- not_true_iff_false, <- is_empty_iff. + split. + - intros H. apply not_empty_mapsto in H. now setoid_rewrite filter_iff in H. + - unfold Empty. setoid_rewrite filter_iff; trivial. firstorder. + Qed. + + 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 : Proper (E.eq==>eq==>eq) 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 E.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 with map. } + 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 E.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 with map. + + - (* 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 E.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 with map. + Qed. + + Lemma Partition_fold : + forall (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA)(f:key->elt->A->A), + Proper (E.eq==>eq==>eqA==>eqA) f -> + Diamond 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 with map. + 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 with map. + 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. + apply fold_rel with (R:=fun u v => u = v + cardinal m2); simpl; auto. + apply Partition_fold with (eqA:=eq); compute; auto with map. congruence. + 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 : Proper (E.eq==>eq==>eq) 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. bindings) *) + + Definition filter_dom (f : key -> bool) := filter (fun k _ => f k). + Definition filter_range (f : elt -> bool) := filter (fun _ => f). + Definition for_all_dom (f : key -> bool) := for_all (fun k _ => f k). + Definition for_all_range (f : elt -> bool) := for_all (fun _ => f). + Definition exists_dom (f : key -> bool) := exists_ (fun k _ => f k). + Definition exists_range (f : elt -> bool) := exists_ (fun _ => f). + Definition partition_dom (f : key -> bool) := partition (fun k _ => f k). + Definition partition_range (f : elt -> bool) := partition (fun _ => f). + + End Elt. + + Instance cardinal_m {elt} : Proper (Equal ==> Logic.eq) (@cardinal elt). + Proof. intros m m'. apply Equal_cardinal. Qed. + + Instance Disjoint_m {elt} : Proper (Equal ==> Equal ==> iff) (@Disjoint elt). + Proof. + intros m1 m1' Hm1 m2 m2' Hm2. unfold Disjoint. split; intros. + rewrite <- Hm1, <- Hm2; auto. + rewrite Hm1, Hm2; auto. + Qed. + + Instance Partition_m {elt} : + Proper (Equal ==> Equal ==> Equal ==> iff) (@Partition elt). + 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. + +(* + Instance filter_m0 {elt} (f:key->elt->bool) : + Proper (E.eq==>Logic.eq==>Logic.eq) f -> + Proper (Equal==>Equal) (filter f). + Proof. + intros Hf m m' Hm. apply Equal_mapsto_iff. intros. + now rewrite !filter_iff, Hm. + Qed. +*) + + Instance filter_m {elt} : + Proper ((E.eq==>Logic.eq==>Logic.eq)==>Equal==>Equal) (@filter elt). + Proof. + intros f f' Hf m m' Hm. unfold filter. + rewrite 2 fold_spec_right. + set (l := rev (bindings m)). + set (l' := rev (bindings m')). + set (op := fun (f:key->elt->bool) => + uncurry (fun k e acc => if f k e then add k e acc else acc)). + change (Equal (fold_right (op f) empty l) (fold_right (op f') empty l')). + assert (Hl : NoDupA eq_key l). + { apply NoDupA_rev. apply eqk_equiv. apply bindings_spec2w. } + assert (Hl' : NoDupA eq_key l'). + { apply NoDupA_rev. apply eqk_equiv. apply bindings_spec2w. } + assert (H : PermutationA eq_key_elt l l'). + { apply NoDupA_equivlistA_PermutationA. + - apply eqke_equiv. + - now apply NoDupA_eqk_eqke. + - now apply NoDupA_eqk_eqke. + - intros (k,e); unfold l, l'. rewrite 2 InA_rev, 2 bindings_spec1. + rewrite Equal_mapsto_iff in Hm. apply Hm. } + destruct (PermutationA_decompose (eqke_equiv _) H) as (l0,(P,E)). + transitivity (fold_right (op f) empty l0). + - apply fold_right_equivlistA_restr2 + with (eqA:=Logic.eq)(R:=complement eq_key); auto with *. + + intros p p' <- acc acc' Hacc. + destruct p as (k,e); unfold op, uncurry; simpl. + destruct (f k e); now rewrite Hacc. + + intros (k,e) (k',e') z z'. + unfold op, complement, uncurry, eq_key; simpl. + intros Hk Hz. + destruct (f k e), (f k' e'); rewrite <- Hz; try reflexivity. + now apply add_add_2. + + apply NoDupA_incl with eq_key; trivial. intros; subst; now red. + + apply PermutationA_preserves_NoDupA with l; auto with *. + apply Permutation_PermutationA; auto with *. + apply NoDupA_incl with eq_key; trivial. intros; subst; now red. + + apply NoDupA_altdef. apply NoDupA_rev. apply eqk_equiv. + apply bindings_spec2w. + + apply PermutationA_equivlistA; auto with *. + apply Permutation_PermutationA; auto with *. + - clearbody l'. clear l Hl Hl' H P m m' Hm. + induction E. + + reflexivity. + + simpl. destruct x as (k,e), x' as (k',e'). + unfold op, uncurry at 1 3; simpl. + destruct H; simpl in *. rewrite <- (Hf _ _ H _ _ H0). + destruct (f k e); trivial. now f_equiv. + Qed. + + Instance for_all_m {elt} : + Proper ((E.eq==>Logic.eq==>Logic.eq)==>Equal==>Logic.eq) (@for_all elt). + Proof. + intros f f' Hf m m' Hm. rewrite 2 for_all_filter. + (* Strange: we cannot rewrite Hm here... *) + f_equiv. f_equiv; trivial. + intros k k' Hk e e' He. f_equal. now apply Hf. + Qed. + + Instance exists_m {elt} : + Proper ((E.eq==>Logic.eq==>Logic.eq)==>Equal==>Logic.eq) (@exists_ elt). + Proof. + intros f f' Hf m m' Hm. rewrite 2 exists_filter. + f_equal. now apply is_empty_m, filter_m. + Qed. + + Fact diamond_add {elt} : Diamond Equal (@add elt). + Proof. + intros k k' e e' a b b' Hk <- <-. now apply add_add_2. + Qed. + + Instance update_m {elt} : Proper (Equal ==> Equal ==> Equal) (@update elt). + Proof. + intros m1 m1' Hm1 m2 m2' Hm2. + unfold update. + apply fold_Proper; auto using diamond_add with *. + Qed. + + Instance restrict_m {elt} : Proper (Equal==>Equal==>Equal) (@restrict elt). + Proof. + intros m1 m1' Hm1 m2 m2' Hm2 y. + unfold restrict. + apply eq_option_alt. intros e. + rewrite !find_spec, !filter_iff, Hm1, Hm2. reflexivity. + clear. intros x x' Hx e e' He. now rewrite Hx. + clear. intros x x' Hx e e' He. now rewrite Hx. + Qed. + + Instance diff_m {elt} : Proper (Equal==>Equal==>Equal) (@diff elt). + Proof. + intros m1 m1' Hm1 m2 m2' Hm2 y. + unfold diff. + apply eq_option_alt. intros e. + rewrite !find_spec, !filter_iff, Hm1, Hm2. reflexivity. + clear. intros x x' Hx e e' He. now rewrite Hx. + clear. intros x x' Hx e e' He. now rewrite Hx. + 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 *) + +Module OrdProperties (M:S). + Module Import ME := OrderedTypeFacts M.E. + Module Import O:=KeyOrderedType M.E. + Module Import P:=Properties M. + Import M. + + Section Elt. + Variable elt:Type. + + Definition Above x (m:t elt) := forall y, In y m -> E.lt y x. + Definition Below x (m:t elt) := forall y, In y m -> E.lt x y. + + Section Bindings. + + Lemma sort_equivlistA_eqlistA : forall l l' : list (key*elt), + sort ltk l -> sort ltk l' -> equivlistA eqke l l' -> eqlistA eqke l l'. + Proof. + apply SortA_equivlistA_eqlistA; eauto with *. + Qed. + + Ltac klean := unfold O.eqke, O.ltk, RelCompFun in *; simpl in *. + Ltac keauto := klean; intuition; eauto. + + 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 bindings_lt p m := List.filter (gtb p) (bindings m). + Definition bindings_ge p m := List.filter (leb p) (bindings m). + + Lemma gtb_1 : forall p p', gtb p p' = true <-> ltk p' p. + Proof. + intros (x,e) (y,e'); unfold gtb; klean. + case E.compare_spec; intuition; try discriminate; ME.order. + Qed. + + Lemma leb_1 : forall p p', leb p p' = true <-> ~ltk p' p. + Proof. + intros (x,e) (y,e'); unfold leb, gtb; klean. + case E.compare_spec; intuition; try discriminate; ME.order. + Qed. + + Instance gtb_compat : forall p, Proper (eqke==>eq) (gtb p). + Proof. + red; intros (x,e) (a,e') (b,e'') H; red in H; simpl in *; destruct H. + generalize (gtb_1 (x,e) (a,e'))(gtb_1 (x,e) (b,e'')); + destruct (gtb (x,e) (a,e')); destruct (gtb (x,e) (b,e'')); klean; auto. + - intros. symmetry; rewrite H2. rewrite <-H, <-H1; auto. + - intros. rewrite H1. rewrite H, <- H2; auto. + Qed. + + Instance leb_compat : forall p, Proper (eqke==>eq) (leb p). + Proof. + intros x a b H. unfold leb; f_equal; apply gtb_compat; auto. + Qed. + + Hint Resolve gtb_compat leb_compat bindings_spec2 : map. + + Lemma bindings_split : forall p m, + bindings m = bindings_lt p m ++ bindings_ge p m. + Proof. + unfold bindings_lt, bindings_ge, leb; intros. + apply filter_split with (eqA:=eqk) (ltA:=ltk); eauto with *. + intros; destruct x; destruct y; destruct p. + rewrite gtb_1 in H; klean. + apply not_true_iff_false in H0. rewrite gtb_1 in H0. klean. ME.order. + Qed. + + Lemma bindings_Add : forall m m' x e, ~In x m -> Add x e m m' -> + eqlistA eqke (bindings m') + (bindings_lt (x,e) m ++ (x,e):: bindings_ge (x,e) m). + Proof. + intros; unfold bindings_lt, bindings_ge. + apply sort_equivlistA_eqlistA; auto with *. + - apply (@SortA_app _ eqke); auto with *. + + apply (@filter_sort _ eqke); auto with *; keauto. + + constructor; auto with map. + * apply (@filter_sort _ eqke); auto with *; keauto. + * rewrite (@InfA_alt _ eqke); auto with *; try (keauto; fail). + { intros. + rewrite filter_InA in H1; auto with *; destruct H1. + rewrite leb_1 in H2. + destruct y; klean. + rewrite <- bindings_mapsto_iff in H1. + assert (~E.eq x t0). + { contradict H. + exists e0; apply MapsTo_1 with t0; auto. + ME.order. } + ME.order. } + { apply (@filter_sort _ eqke); auto with *; keauto. } + + intros. + rewrite filter_InA in H1; auto with *; destruct H1. + rewrite gtb_1 in H3. + destruct y; destruct x0; klean. + inversion_clear H2. + * red in H4; klean; destruct H4; simpl in *. ME.order. + * rewrite filter_InA in H4; auto with *; destruct H4. + rewrite leb_1 in H4. klean; ME.order. + - intros (k,e'). + rewrite InA_app_iff, InA_cons, 2 filter_InA, + <-2 bindings_mapsto_iff, leb_1, gtb_1, + find_mapsto_iff, (H0 k), <- find_mapsto_iff, + add_mapsto_iff by (auto with * ). + change (eqke (k,e') (x,e)) with (E.eq k x /\ e' = e). + klean. + split. + + intros [(->,->)|(Hk,Hm)]. + * right; now left. + * destruct (lt_dec k x); intuition. + + intros [(Hm,LT)|[(->,->)|(Hm,EQ)]]. + * right; split; trivial; ME.order. + * now left. + * destruct (eq_dec x k) as [Hk|Hk]. + elim H. exists e'. now rewrite Hk. + right; auto. + Qed. + + Lemma bindings_Add_Above : forall m m' x e, + Above x m -> Add x e m m' -> + eqlistA eqke (bindings m') (bindings m ++ (x,e)::nil). + Proof. + intros. + apply sort_equivlistA_eqlistA; auto with *. + apply (@SortA_app _ eqke); auto with *. + intros. + inversion_clear H2. + destruct x0; destruct y. + rewrite <- bindings_mapsto_iff in H1. + destruct H3; klean. + rewrite H2. + apply H; firstorder. + inversion H3. + red; intros a; destruct a. + rewrite InA_app_iff, InA_cons, InA_nil, <- 2 bindings_mapsto_iff, + find_mapsto_iff, (H0 t0), <- find_mapsto_iff, + add_mapsto_iff by (auto with *). + change (eqke (t0,e0) (x,e)) with (E.eq t0 x /\ e0 = e). + intuition. + destruct (E.eq_dec x t0) as [Heq|Hneq]; auto. + exfalso. + assert (In t0 m) by (exists e0; auto). + generalize (H t0 H1). + ME.order. + Qed. + + Lemma bindings_Add_Below : forall m m' x e, + Below x m -> Add x e m m' -> + eqlistA eqke (bindings m') ((x,e)::bindings m). + Proof. + intros. + apply sort_equivlistA_eqlistA; auto with *. + change (sort ltk (((x,e)::nil) ++ bindings m)). + apply (@SortA_app _ eqke); auto with *. + intros. + inversion_clear H1. + destruct y; destruct x0. + rewrite <- bindings_mapsto_iff in H2. + destruct H3; klean. + rewrite H1. + apply H; firstorder. + inversion H3. + red; intros a; destruct a. + rewrite InA_cons, <- 2 bindings_mapsto_iff, + find_mapsto_iff, (H0 t0), <- find_mapsto_iff, + add_mapsto_iff by (auto with * ). + change (eqke (t0,e0) (x,e)) with (E.eq t0 x /\ e0 = e). + intuition. + destruct (E.eq_dec x t0) as [Heq|Hneq]; auto. + exfalso. + assert (In t0 m) by (exists e0; auto). + generalize (H t0 H1). + ME.order. + Qed. + + Lemma bindings_Equal_eqlistA : forall (m m': t elt), + Equal m m' -> eqlistA eqke (bindings m) (bindings m'). + Proof. + intros. + apply sort_equivlistA_eqlistA; auto with *. + red; intros. + destruct x; do 2 rewrite <- bindings_mapsto_iff. + do 2 rewrite find_mapsto_iff; rewrite H; split; auto. + Qed. + + End Bindings. + + Section Min_Max_Elt. + + (** We emulate two [max_elt] and [min_elt] functions. *) + + Fixpoint max_elt_aux (l:list (key*elt)) := match l with + | nil => None + | (x,e)::nil => Some (x,e) + | (x,e)::l => max_elt_aux l + end. + Definition max_elt m := max_elt_aux (bindings m). + + Lemma max_elt_Above : + forall m x e, max_elt m = Some (x,e) -> Above x (remove x m). + Proof. + red; intros. + rewrite remove_in_iff in H0. + destruct H0. + rewrite bindings_in_iff in H1. + destruct H1. + unfold max_elt in *. + generalize (bindings_spec2 m). + revert x e H y x0 H0 H1. + induction (bindings m). + simpl; intros; try discriminate. + intros. + destruct a; destruct l; simpl in *. + injection H; clear H; intros; subst. + inversion_clear H1. + red in H; simpl in *; intuition. + now elim H0. + inversion H. + change (max_elt_aux (p::l) = Some (x,e)) in H. + generalize (IHl x e H); clear IHl; intros IHl. + inversion_clear H1; [ | inversion_clear H2; eauto ]. + red in H3; simpl in H3; destruct H3. + destruct p as (p1,p2). + destruct (E.eq_dec p1 x) as [Heq|Hneq]. + rewrite <- Heq; auto. + inversion_clear H2. + inversion_clear H5. + red in H2; simpl in H2; ME.order. + transitivity p1; auto. + inversion_clear H2. + inversion_clear H5. + red in H2; simpl in H2; ME.order. + eapply IHl; eauto with *. + econstructor; eauto. + red; eauto with *. + inversion H2; auto. + Qed. + + Lemma max_elt_MapsTo : + forall m x e, max_elt m = Some (x,e) -> MapsTo x e m. + Proof. + intros. + unfold max_elt in *. + rewrite bindings_mapsto_iff. + induction (bindings m). + simpl; try discriminate. + destruct a; destruct l; simpl in *. + injection H; intros; subst; constructor; red; auto with *. + constructor 2; auto. + Qed. + + Lemma max_elt_Empty : + forall m, max_elt m = None -> Empty m. + Proof. + intros. + unfold max_elt in *. + rewrite bindings_Empty. + induction (bindings m); auto. + destruct a; destruct l; simpl in *; try discriminate. + assert (H':=IHl H); discriminate. + Qed. + + Definition min_elt m : option (key*elt) := match bindings m with + | nil => None + | (x,e)::_ => Some (x,e) + end. + + Lemma min_elt_Below : + forall m x e, min_elt m = Some (x,e) -> Below x (remove x m). + Proof. + unfold min_elt, Below; intros. + rewrite remove_in_iff in H0; destruct H0. + rewrite bindings_in_iff in H1. + destruct H1. + generalize (bindings_spec2 m). + destruct (bindings m). + try discriminate. + destruct p; injection H; intros; subst. + inversion_clear H1. + red in H2; destruct H2; simpl in *; ME.order. + inversion_clear H4. + rewrite (@InfA_alt _ eqke) in H3; eauto with *. + apply (H3 (y,x0)); auto. + Qed. + + Lemma min_elt_MapsTo : + forall m x e, min_elt m = Some (x,e) -> MapsTo x e m. + Proof. + intros. + unfold min_elt in *. + rewrite bindings_mapsto_iff. + destruct (bindings m). + simpl; try discriminate. + destruct p; simpl in *. + injection H; intros; subst; constructor; red; auto with *. + Qed. + + Lemma min_elt_Empty : + forall m, min_elt m = None -> Empty m. + Proof. + intros. + unfold min_elt in *. + rewrite bindings_Empty. + destruct (bindings m); auto. + destruct p; simpl in *; discriminate. + Qed. + + End Min_Max_Elt. + + Section Induction_Principles. + + Lemma map_induction_max : + forall P : t elt -> Type, + (forall m, Empty m -> P m) -> + (forall m m', P m -> forall x e, Above 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. + + case_eq (max_elt m); intros. + destruct p. + assert (Add k e (remove k m) m). + { apply max_elt_MapsTo, find_spec, add_id in H. + unfold Add. symmetry. now rewrite add_remove_1. } + apply X0 with (remove k m) k e; auto with map. + apply IHn. + assert (S n = S (cardinal (remove k m))). + { rewrite Heqn. + eapply cardinal_S; eauto with map. } + inversion H1; auto. + eapply max_elt_Above; eauto. + + apply X; apply max_elt_Empty; auto. + Qed. + + Lemma map_induction_min : + forall P : t elt -> Type, + (forall m, Empty m -> P m) -> + (forall m m', P m -> forall x e, Below 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. + + case_eq (min_elt m); intros. + destruct p. + assert (Add k e (remove k m) m). + { apply min_elt_MapsTo, find_spec, add_id in H. + unfold Add. symmetry. now rewrite add_remove_1. } + apply X0 with (remove k m) k e; auto. + apply IHn. + assert (S n = S (cardinal (remove k m))). + { rewrite Heqn. + eapply cardinal_S; eauto with map. } + inversion H1; auto. + eapply min_elt_Below; eauto. + + apply X; apply min_elt_Empty; auto. + Qed. + + End Induction_Principles. + + Section Fold_properties. + + (** The following lemma has already been proved on Weak Maps, + but with one additionnal hypothesis (some [transpose] fact). *) + + Lemma fold_Equal : forall m1 m2 (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA) + (f:key->elt->A->A)(i:A), + Proper (E.eq==>eq==>eqA==>eqA) f -> + Equal m1 m2 -> + eqA (fold f m1 i) (fold f m2 i). + Proof. + intros m1 m2 A eqA st f i Hf Heq. + 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 bindings_Equal_eqlistA. auto. + Qed. + + 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) (P:Proper (E.eq==>eq==>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. rewrite 2 fold_spec_right. set (f':=uncurry f). + transitivity (fold_right f' i (rev (bindings 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. + apply eqlistA_rev. + apply bindings_Add_Above; auto. + rewrite distr_rev; simpl. + reflexivity. + Qed. + + 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) (P:Proper (E.eq==>eq==>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. rewrite 2 fold_spec_right. set (f':=uncurry f). + transitivity (fold_right f' i (rev (((x,e)::nil)++bindings 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. + apply eqlistA_rev. + simpl; apply bindings_Add_Below; auto. + rewrite distr_rev; simpl. + rewrite fold_right_app. + reflexivity. + Qed. + + End Fold_properties. + + End Elt. + +End OrdProperties. |