From d0bd6f449cc166ae1348d5106fcf5ea6caa2a115 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Thu, 25 May 2017 11:14:45 +0200 Subject: [PATCH] More properties about the order on finite maps. --- theories/fin_maps.v | 107 ++++++++++++++++++++++++++++++++------------ 1 file changed, 79 insertions(+), 28 deletions(-) diff --git a/theories/fin_maps.v b/theories/fin_maps.v index 1c92db6..ecb3ef7 100644 --- a/theories/fin_maps.v +++ b/theories/fin_maps.v @@ -205,14 +205,15 @@ Proof. unfold subseteq, map_subseteq, map_relation. split; intros Hm i; specialize (Hm i); destruct (m1 !! i), (m2 !! i); naive_solver. Qed. -Global Instance: ∀ {A} (R : relation A), PreOrder R → PreOrder (map_included R). +Global Instance map_included_preorder {A} (R : relation A) : + PreOrder R → PreOrder (map_included R). Proof. split; [intros m i; by destruct (m !! i); simpl|]. intros m1 m2 m3 Hm12 Hm23 i; specialize (Hm12 i); specialize (Hm23 i). destruct (m1 !! i), (m2 !! i), (m3 !! i); simplify_eq/=; done || etrans; eauto. Qed. -Global Instance: PartialOrder ((⊆) : relation (M A)). +Global Instance map_subseteq_po : PartialOrder ((⊆) : relation (M A)). Proof. split; [apply _|]. intros m1 m2; rewrite !map_subseteq_spec. @@ -248,6 +249,22 @@ Qed. Lemma map_fmap_empty {A B} (f : A → B) : f <\$> (∅ : M A) = ∅. Proof. by apply map_eq; intros i; rewrite lookup_fmap, !lookup_empty. Qed. +Lemma map_subset_alt {A} (m1 m2 : M A) : + m1 ⊂ m2 ↔ m1 ⊆ m2 ∧ ∃ i, m1 !! i = None ∧ is_Some (m2 !! i). +Proof. + rewrite strict_spec_alt. split. + - intros [? Heq]; split; [done|]. + destruct (decide (Exists (λ '(i,_), m1 !! i = None) (map_to_list m2))) + as [[[i x] [?%elem_of_map_to_list ?]]%Exists_exists + |Hm%(not_Exists_Forall _)]; [eauto|]. + destruct Heq; apply (anti_symm _), map_subseteq_spec; [done|intros i x Hi]. + assert (is_Some (m1 !! i)) as [x' ?]. + { by apply not_eq_None_Some, + (proj1 (Forall_forall _ _) Hm (i,x)), elem_of_map_to_list. } + by rewrite <-(lookup_weaken_inv m1 m2 i x' x). + - intros [? (i&?&x&?)]; split; [done|]. congruence. +Qed. + (** ** Properties of the [partial_alter] operation *) Lemma partial_alter_ext {A} (f g : option A → option A) (m : M A) i : (∀ x, m !! i = x → f x = g x) → partial_alter f i m = partial_alter g i m. @@ -290,20 +307,18 @@ Qed. Lemma partial_alter_subset {A} f (m : M A) i : m !! i = None → is_Some (f (m !! i)) → m ⊂ partial_alter f i m. Proof. - intros Hi Hfi. split; [by apply partial_alter_subseteq|]. - rewrite !map_subseteq_spec. inversion Hfi as [x Hx]. intros Hm. - apply (Some_ne_None x). rewrite <-(Hm i x); [done|]. - by rewrite lookup_partial_alter. + intros Hi Hfi. apply map_subset_alt; split; [by apply partial_alter_subseteq|]. + exists i. by rewrite lookup_partial_alter. Qed. (** ** Properties of the [alter] operation *) -Lemma alter_ext {A} (f g : A → A) (m : M A) i : - (∀ x, m !! i = Some x → f x = g x) → alter f i m = alter g i m. -Proof. intro. apply partial_alter_ext. intros [x|] ?; f_equal/=; auto. Qed. Lemma lookup_alter {A} (f : A → A) m i : alter f i m !! i = f <\$> m !! i. Proof. unfold alter. apply lookup_partial_alter. Qed. Lemma lookup_alter_ne {A} (f : A → A) m i j : i ≠ j → alter f i m !! j = m !! j. Proof. unfold alter. apply lookup_partial_alter_ne. Qed. +Lemma alter_ext {A} (f g : A → A) (m : M A) i : + (∀ x, m !! i = Some x → f x = g x) → alter f i m = alter g i m. +Proof. intro. apply partial_alter_ext. intros [x|] ?; f_equal/=; auto. Qed. Lemma alter_compose {A} (f g : A → A) (m : M A) i: alter (f ∘ g) i m = alter f i (alter g i m). Proof. @@ -327,6 +342,9 @@ Proof. by destruct (decide (i = j)) as [->|?]; rewrite ?lookup_alter, ?fmap_None, ?lookup_alter_ne. Qed. +Lemma lookup_alter_is_Some {A} (f : A → A) m i j : + is_Some (alter f i m !! j) ↔ is_Some (m !! j). +Proof. by rewrite <-!not_eq_None_Some, lookup_alter_None. Qed. Lemma alter_id {A} (f : A → A) m i : (∀ x, m !! i = Some x → f x = x) → alter f i m = m. Proof. @@ -334,6 +352,18 @@ Proof. { rewrite lookup_alter; destruct (m !! j); f_equal/=; auto. } by rewrite lookup_alter_ne by done. Qed. +Lemma alter_mono {A} f (m1 m2 : M A) i : m1 ⊆ m2 → alter f i m1 ⊆ alter f i m2. +Proof. + rewrite !map_subseteq_spec. intros ? j x. + rewrite !lookup_alter_Some. naive_solver. +Qed. +Lemma alter_strict_mono {A} f (m1 m2 : M A) i : + m1 ⊂ m2 → alter f i m1 ⊂ alter f i m2. +Proof. + rewrite !map_subset_alt. + intros [? (j&?&?)]; split; auto using alter_mono. + exists j. by rewrite lookup_alter_None, lookup_alter_is_Some. +Qed. (** ** Properties of the [delete] operation *) Lemma lookup_delete {A} (m : M A) i : delete i m !! i = None. @@ -387,20 +417,16 @@ Lemma delete_subseteq {A} (m : M A) i : delete i m ⊆ m. Proof. rewrite !map_subseteq_spec. intros j x. rewrite lookup_delete_Some. tauto. Qed. -Lemma delete_subseteq_compat {A} (m1 m2 : M A) i : - m1 ⊆ m2 → delete i m1 ⊆ delete i m2. +Lemma delete_subset {A} (m : M A) i : is_Some (m !! i) → delete i m ⊂ m. Proof. - rewrite !map_subseteq_spec. intros ? j x. - rewrite !lookup_delete_Some. intuition eauto. + intros [x ?]; apply map_subset_alt; split; [apply delete_subseteq|]. + exists i. rewrite lookup_delete; eauto. Qed. -Lemma delete_subset_alt {A} (m : M A) i x : m !! i = Some x → delete i m ⊂ m. +Lemma delete_mono {A} (m1 m2 : M A) i : m1 ⊆ m2 → delete i m1 ⊆ delete i m2. Proof. - split; [apply delete_subseteq|]. - rewrite !map_subseteq_spec. intros Hi. apply (None_ne_Some x). - by rewrite <-(lookup_delete m i), (Hi i x). + rewrite !map_subseteq_spec. intros ? j x. + rewrite !lookup_delete_Some. intuition eauto. Qed. -Lemma delete_subset {A} (m : M A) i : is_Some (m !! i) → delete i m ⊂ m. -Proof. inversion 1. eauto using delete_subset_alt. Qed. (** ** Properties of the [insert] operation *) Lemma lookup_insert {A} (m : M A) i x : <[i:=x]>m !! i = Some x. @@ -447,17 +473,28 @@ Proof. - rewrite lookup_insert. destruct (m !! j); simpl; eauto. - rewrite lookup_insert_ne by done. by destruct (m !! j); simpl. Qed. +Lemma insert_empty {A} i (x : A) : <[i:=x]>∅ = {[i := x]}. +Proof. done. Qed. +Lemma insert_non_empty {A} (m : M A) i x : <[i:=x]>m ≠ ∅. +Proof. + intros Hi%(f_equal (!! i)). by rewrite lookup_insert, lookup_empty in Hi. +Qed. + Lemma insert_subseteq {A} (m : M A) i x : m !! i = None → m ⊆ <[i:=x]>m. Proof. apply partial_alter_subseteq. Qed. Lemma insert_subset {A} (m : M A) i x : m !! i = None → m ⊂ <[i:=x]>m. Proof. intro. apply partial_alter_subset; eauto. Qed. +Lemma insert_mono {A} (m1 m2 : M A) i x : m1 ⊆ m2 → <[i:=x]> m1 ⊆ <[i:=x]>m2. +Proof. + rewrite !map_subseteq_spec. + intros Hm j y. rewrite !lookup_insert_Some. naive_solver. +Qed. Lemma insert_subseteq_r {A} (m1 m2 : M A) i x : m1 !! i = None → m1 ⊆ m2 → m1 ⊆ <[i:=x]>m2. Proof. - rewrite !map_subseteq_spec. intros ?? j ?. - destruct (decide (j = i)) as [->|?]; [congruence|]. - rewrite lookup_insert_ne; auto. + intros. trans (<[i:=x]> m1); eauto using insert_subseteq, insert_mono. Qed. + Lemma insert_delete_subseteq {A} (m1 m2 : M A) i x : m1 !! i = None → <[i:=x]> m1 ⊆ m2 → m1 ⊆ delete i m2. Proof. @@ -491,12 +528,6 @@ Proof. - eauto using insert_delete_subset. - by rewrite lookup_delete. Qed. -Lemma insert_empty {A} i (x : A) : <[i:=x]>∅ = {[i := x]}. -Proof. done. Qed. -Lemma insert_non_empty {A} (m : M A) i x : <[i:=x]>m ≠ ∅. -Proof. - intros Hi%(f_equal (!! i)). by rewrite lookup_insert, lookup_empty in Hi. -Qed. (** ** Properties of the singleton maps *) Lemma lookup_singleton_Some {A} i j (x y : A) : @@ -593,6 +624,26 @@ Proof. by destruct (m !! i) eqn:?; simpl; erewrite ?Hi by eauto. Qed. +Lemma map_fmap_mono {A B} (f : A → B) (m1 m2 : M A) : + m1 ⊆ m2 → f <\$> m1 ⊆ f <\$> m2. +Proof. + rewrite !map_subseteq_spec; intros Hm i x. + rewrite !lookup_fmap, !fmap_Some. naive_solver. +Qed. +Lemma map_fmap_strict_mono {A B} (f : A → B) (m1 m2 : M A) : + m1 ⊂ m2 → f <\$> m1 ⊂ f <\$> m2. +Proof. + rewrite !map_subset_alt. + intros [? (j&?&?)]; split; auto using map_fmap_mono. + exists j. by rewrite !lookup_fmap, fmap_None, fmap_is_Some. +Qed. +Lemma map_omap_mono {A B} (f : A → option B) (m1 m2 : M A) : + m1 ⊆ m2 → omap f m1 ⊆ omap f m2. +Proof. + rewrite !map_subseteq_spec; intros Hm i x. + rewrite !lookup_omap, !bind_Some. naive_solver. +Qed. + (** ** Properties of conversion to lists *) Lemma elem_of_map_to_list' {A} (m : M A) ix : ix ∈ map_to_list m ↔ m !! ix.1 = Some (ix.2). -- GitLab