From 6058134f80b3e1c2deb4d46e9c509738c6179c1d Mon Sep 17 00:00:00 2001 From: Dan Frumin Date: Sat, 29 May 2021 16:04:59 +0200 Subject: [PATCH 1/3] Add `map_filter_strong_ext_2`. --- theories/fin_maps.v | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/theories/fin_maps.v b/theories/fin_maps.v index 473196e0..b3cc8794 100644 --- a/theories/fin_maps.v +++ b/theories/fin_maps.v @@ -1332,6 +1332,13 @@ Section map_filter_ext. intros HPiff. apply map_eq. intros i. apply option_eq; intros x. rewrite !map_filter_lookup_Some. naive_solver. Qed. + Lemma map_filter_strong_ext_2 (m1 m2 : M A) i x : + filter P m1 = filter Q m2 → + (P (i, x) ∧ m1 !! i = Some x) ↔ (Q (i, x) ∧ m2 !! i = Some x). + Proof. + intros Hfilt. rewrite (comm _ (P (i, x))), (comm _ (Q (i, x))). + rewrite <- !map_filter_lookup_Some. by repeat f_equiv. + Qed. Lemma map_filter_ext (m : M A) : (∀ i x, m !! i = Some x → P (i, x) ↔ Q (i, x)) → filter P m = filter Q m. -- GitLab From 8396f122de5930c83a106631edaeaac97116a776 Mon Sep 17 00:00:00 2001 From: Dan Frumin Date: Mon, 31 May 2021 18:05:43 +0200 Subject: [PATCH 2/3] Better naming --- theories/fin_maps.v | 21 +++++++++++---------- 1 file changed, 11 insertions(+), 10 deletions(-) diff --git a/theories/fin_maps.v b/theories/fin_maps.v index b3cc8794..2b568bfc 100644 --- a/theories/fin_maps.v +++ b/theories/fin_maps.v @@ -1326,23 +1326,24 @@ Section map_filter_ext. Context {A} (P Q : K * A → Prop) `{!∀ x, Decision (P x), !∀ x, Decision (Q x)}. Lemma map_filter_strong_ext (m1 m2 : M A) : - (∀ i x, (P (i, x) ∧ m1 !! i = Some x) ↔ (Q (i, x) ∧ m2 !! i = Some x)) → - filter P m1 = filter Q m2. + filter P m1 = filter Q m2 ↔ + (∀ i x, (P (i, x) ∧ m1 !! i = Some x) ↔ (Q (i, x) ∧ m2 !! i = Some x)). Proof. - intros HPiff. apply map_eq. intros i. apply option_eq; intros x. - rewrite !map_filter_lookup_Some. naive_solver. + intros. rewrite map_eq_iff. setoid_rewrite option_eq. + setoid_rewrite map_filter_lookup_Some. naive_solver. Qed. + Lemma map_filter_strong_ext_1 (m1 m2 : M A) : + (∀ i x, (P (i, x) ∧ m1 !! i = Some x) ↔ (Q (i, x) ∧ m2 !! i = Some x)) → + filter P m1 = filter Q m2. + Proof. by rewrite map_filter_strong_ext. Qed. Lemma map_filter_strong_ext_2 (m1 m2 : M A) i x : filter P m1 = filter Q m2 → (P (i, x) ∧ m1 !! i = Some x) ↔ (Q (i, x) ∧ m2 !! i = Some x). - Proof. - intros Hfilt. rewrite (comm _ (P (i, x))), (comm _ (Q (i, x))). - rewrite <- !map_filter_lookup_Some. by repeat f_equiv. - Qed. + Proof. by rewrite map_filter_strong_ext. Qed. Lemma map_filter_ext (m : M A) : - (∀ i x, m !! i = Some x → P (i, x) ↔ Q (i, x)) → + (∀ i x, m !! i = Some x → P (i, x) ↔ Q (i, x)) ↔ filter P m = filter Q m. - Proof. intro. apply map_filter_strong_ext. naive_solver. Qed. + Proof. rewrite map_filter_strong_ext. naive_solver. Qed. End map_filter_ext. Section map_filter_insert_and_delete. -- GitLab From 4100164d346e76a498ec202dc540652870847aae Mon Sep 17 00:00:00 2001 From: Dan Frumin Date: Sat, 5 Jun 2021 15:13:56 +0200 Subject: [PATCH 3/3] Update changelog --- CHANGELOG.md | 1 + 1 file changed, 1 insertion(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 5a18b345..deec3e67 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -42,6 +42,7 @@ API-breaking change is listed. - Add function `kmap` to transform the keys of finite maps. - Set `Hint Mode` for the classes `PartialOrder`, `TotalOrder`, `MRet`, `MBind`, `MJoin`, `FMap`, `OMap`, `MGuard`, `SemiSet`, `Set_`, `TopSet`, and `Infinite`. +- Make `map_filter_strong_ext` and `map_filter_ext` bidirectional. The following `sed` script should perform most of the renaming (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`): -- GitLab