From a7490068ec0106989d36d9df269fd21c567f99af Mon Sep 17 00:00:00 2001 From: Alix Trieu Date: Tue, 14 Jul 2020 15:49:22 +0200 Subject: [PATCH 1/3] Extra lemmas about map_imap --- theories/fin_maps.v | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/theories/fin_maps.v b/theories/fin_maps.v index fc357d44..6a2d3ca3 100644 --- a/theories/fin_maps.v +++ b/theories/fin_maps.v @@ -944,6 +944,16 @@ Proof. by rewrite map_lookup_imap. Qed. +Lemma map_imap_delete {A B} (f : K → A → option B) (i : K) (v : A) (m : M A) : + map_imap f (delete i m) = delete i (map_imap f m). +Proof. + apply map_eq. intros k. rewrite map_lookup_imap. + destruct (decide (k = i)) as [->|Hk_not_i]. + - by rewrite !lookup_delete. + - rewrite !lookup_delete_ne by done. + by rewrite map_lookup_imap. +Qed. + Lemma map_imap_ext {A1 A2 B} (f1 : K → A1 → option B) (f2 : K → A2 → option B) (m1 : M A1) (m2 : M A2) : (∀ k, f1 k <\$> (m1 !! k) = f2 k <\$> (m2 !! k)) → @@ -953,6 +963,17 @@ Proof. specialize (HExt i). destruct (m1 !! i), (m2 !! i); naive_solver. Qed. +Lemma map_imap_compose {A1 A2 B} (f1 : K → A1 → option B) + (f2 : K → A2 → option A1) (m : M A2) : + map_imap f1 (map_imap f2 m) = map_imap (fun k v => f2 k v ≫= f1 k) m. +Proof. + apply map_eq. intros i. rewrite !map_lookup_imap. by destruct (m !! i). +Qed. + +Lemma map_imap_empty {A B} (f : K → A → option B) : + map_imap f (∅ : M A) = ∅. +Proof. unfold map_imap. by rewrite map_to_list_empty. Qed. + (** ** Properties of the size operation *) Lemma map_size_empty {A} : size (∅ : M A) = 0. Proof. unfold size, map_size. by rewrite map_to_list_empty. Qed. -- GitLab From ec17969475076b7baba0fe6695fdd7cafebd6073 Mon Sep 17 00:00:00 2001 From: Alix Trieu Date: Tue, 14 Jul 2020 16:50:32 +0200 Subject: [PATCH 2/3] Additional lemmas about dom and map_imap --- theories/fin_map_dom.v | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v index 243b1644..338911a5 100644 --- a/theories/fin_map_dom.v +++ b/theories/fin_map_dom.v @@ -35,6 +35,22 @@ Proof. destruct 1 as [?[Eq _]%map_filter_lookup_Some]. by eexists. Qed. +Lemma dom_map_imap_subseteq {A B} (f: K -> A -> option B) (m: M A) : + dom D (map_imap f m) ⊆ dom D m. +Proof. + intros k. rewrite 2!elem_of_dom, map_lookup_imap. + destruct (m !! k) as [a|] eqn:Heq; simpl; [by eexists|by inversion 1]. +Qed. +Lemma dom_map_imap {A B} (f: K -> A -> option B) (m: M A) X : + (∀ i, i ∈ X ↔ ∃ x, m !! i = Some x ∧ is_Some (f i x)) -> + dom D (map_imap f m) ≡ X. +Proof. + intros HX k. rewrite elem_of_dom, HX, map_lookup_imap. + unfold is_Some. destruct (m !! k) as [a|] eqn:Heq; simpl. + - split; eauto. destruct 1 as [x [HA HB]]. by inversion HA. + - split; [by destruct 1|]. by destruct 1 as [? [? _]]. +Qed. + Lemma elem_of_dom_2 {A} (m : M A) i x : m !! i = Some x → i ∈ dom D m. Proof. rewrite elem_of_dom; eauto. Qed. Lemma not_elem_of_dom {A} (m : M A) i : i ∉ dom D m ↔ m !! i = None. @@ -167,6 +183,10 @@ Section leibniz. Proof. unfold_leibniz; apply dom_difference. Qed. Lemma dom_fmap_L {A B} (f : A → B) (m : M A) : dom D (f <\$> m) = dom D m. Proof. unfold_leibniz; apply dom_fmap. Qed. + Lemma dom_map_imap_L {A B} (f: K -> A -> option B) (m: M A) X : + (∀ i, i ∈ X ↔ ∃ x, m !! i = Some x ∧ is_Some (f i x)) -> + dom D (map_imap f m) = X. + Proof. unfold_leibniz; apply dom_map_imap. Qed. End leibniz. (** * Set solver instances *) -- GitLab From a76c295a09873684279a708e7de335f492db4519 Mon Sep 17 00:00:00 2001 From: Alix Trieu Date: Thu, 16 Jul 2020 11:02:39 +0200 Subject: [PATCH 3/3] Apply Robbert's suggestions --- theories/fin_map_dom.v | 18 ++++++++---------- theories/fin_maps.v | 8 ++++---- 2 files changed, 12 insertions(+), 14 deletions(-) diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v index 338911a5..ed3c554e 100644 --- a/theories/fin_map_dom.v +++ b/theories/fin_map_dom.v @@ -35,20 +35,18 @@ Proof. destruct 1 as [?[Eq _]%map_filter_lookup_Some]. by eexists. Qed. -Lemma dom_map_imap_subseteq {A B} (f: K -> A -> option B) (m: M A) : +Lemma dom_imap_subseteq {A B} (f: K → A → option B) (m: M A) : dom D (map_imap f m) ⊆ dom D m. Proof. intros k. rewrite 2!elem_of_dom, map_lookup_imap. - destruct (m !! k) as [a|] eqn:Heq; simpl; [by eexists|by inversion 1]. + destruct 1 as [?[?[Eq _]]%bind_Some]. by eexists. Qed. -Lemma dom_map_imap {A B} (f: K -> A -> option B) (m: M A) X : - (∀ i, i ∈ X ↔ ∃ x, m !! i = Some x ∧ is_Some (f i x)) -> +Lemma dom_imap {A B} (f: K → A → option B) (m: M A) X : + (∀ i, i ∈ X ↔ ∃ x, m !! i = Some x ∧ is_Some (f i x)) → dom D (map_imap f m) ≡ X. Proof. intros HX k. rewrite elem_of_dom, HX, map_lookup_imap. - unfold is_Some. destruct (m !! k) as [a|] eqn:Heq; simpl. - - split; eauto. destruct 1 as [x [HA HB]]. by inversion HA. - - split; [by destruct 1|]. by destruct 1 as [? [? _]]. + unfold is_Some. setoid_rewrite bind_Some. naive_solver. Qed. Lemma elem_of_dom_2 {A} (m : M A) i x : m !! i = Some x → i ∈ dom D m. @@ -183,10 +181,10 @@ Section leibniz. Proof. unfold_leibniz; apply dom_difference. Qed. Lemma dom_fmap_L {A B} (f : A → B) (m : M A) : dom D (f <\$> m) = dom D m. Proof. unfold_leibniz; apply dom_fmap. Qed. - Lemma dom_map_imap_L {A B} (f: K -> A -> option B) (m: M A) X : - (∀ i, i ∈ X ↔ ∃ x, m !! i = Some x ∧ is_Some (f i x)) -> + Lemma dom_imap_L {A B} (f: K → A → option B) (m: M A) X : + (∀ i, i ∈ X ↔ ∃ x, m !! i = Some x ∧ is_Some (f i x)) → dom D (map_imap f m) = X. - Proof. unfold_leibniz; apply dom_map_imap. Qed. + Proof. unfold_leibniz; apply dom_imap. Qed. End leibniz. (** * Set solver instances *) diff --git a/theories/fin_maps.v b/theories/fin_maps.v index 6a2d3ca3..fefb1e3d 100644 --- a/theories/fin_maps.v +++ b/theories/fin_maps.v @@ -944,7 +944,7 @@ Proof. by rewrite map_lookup_imap. Qed. -Lemma map_imap_delete {A B} (f : K → A → option B) (i : K) (v : A) (m : M A) : +Lemma map_imap_delete {A B} (f : K → A → option B) (m : M A) (i : K) : map_imap f (delete i m) = delete i (map_imap f m). Proof. apply map_eq. intros k. rewrite map_lookup_imap. @@ -964,14 +964,14 @@ Proof. Qed. Lemma map_imap_compose {A1 A2 B} (f1 : K → A1 → option B) - (f2 : K → A2 → option A1) (m : M A2) : - map_imap f1 (map_imap f2 m) = map_imap (fun k v => f2 k v ≫= f1 k) m. + (f2 : K → A2 → option A1) (m : M A2) : + map_imap f1 (map_imap f2 m) = map_imap (λ k x, f2 k x ≫= f1 k) m. Proof. apply map_eq. intros i. rewrite !map_lookup_imap. by destruct (m !! i). Qed. Lemma map_imap_empty {A B} (f : K → A → option B) : - map_imap f (∅ : M A) = ∅. + map_imap f ∅ =@{M B} ∅. Proof. unfold map_imap. by rewrite map_to_list_empty. Qed. (** ** Properties of the size operation *) -- GitLab