From cc70f824dff9f40ed05e6cbc1b58e2121072d474 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 8 Jun 2021 00:28:55 +0200
Subject: [PATCH] =?UTF-8?q?Rename=20`map=5Fdisjoint=5Ffilter`=20=E2=86=92?=
 =?UTF-8?q?=20`map=5Fdisjoint=5Ffilter=5Fcomplement`=20and=20`map=5Funion?=
 =?UTF-8?q?=5Ffilter`=20=E2=86=92=20`map=5Ffilter=5Funion=5Fcomplement`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/fin_map_dom.v | 2 +-
 theories/fin_maps.v    | 9 ++++++---
 2 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index c955877e..d46161ad 100644
--- a/theories/fin_map_dom.v
+++ b/theories/fin_map_dom.v
@@ -182,7 +182,7 @@ Proof.
   intros.
   exists (filter (λ '(k,x), k ∈ X1) m), (filter (λ '(k,x), k ∉ X1) m).
   assert (filter (λ '(k, _), k ∈ X1) m ##ₘ filter (λ '(k, _), k ∉ X1) m).
-  { apply map_disjoint_filter. }
+  { apply map_disjoint_filter_complement. }
   split_and!; [|done| |].
   - apply map_eq; intros i. apply option_eq; intros x.
     rewrite lookup_union_Some, !map_filter_lookup_Some by done.
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 2b568bfc..4bfbcdaf 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1868,7 +1868,9 @@ Proof.
 Qed.
 Lemma map_disjoint_delete_r {A} (m1 m2 : M A) i : m1 ##ₘ m2 → m1 ##ₘ delete i m2.
 Proof. symmetry. by apply map_disjoint_delete_l. Qed.
-Lemma map_disjoint_filter {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A) :
+
+Lemma map_disjoint_filter_complement {A} (P : K * A → Prop)
+    `{!∀ x, Decision (P x)} (m : M A) :
   filter P m ##ₘ filter (λ v, ¬ P v) m.
 Proof.
   apply map_disjoint_spec. intros i x y.
@@ -2184,11 +2186,12 @@ Proof.
   naive_solver eauto using map_Forall_union_1_1,
     map_Forall_union_1_2, map_Forall_union_2.
 Qed.
-Lemma map_union_filter {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A) :
+Lemma map_filter_union_complement {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A) :
   filter P m ∪ filter (λ v, ¬ P v) m = m.
 Proof.
   apply map_eq; intros i. apply option_eq; intros x.
-  rewrite lookup_union_Some, !map_filter_lookup_Some by apply map_disjoint_filter.
+  rewrite lookup_union_Some, !map_filter_lookup_Some
+    by auto using map_disjoint_filter_complement.
   destruct (decide (P (i,x))); naive_solver.
 Qed.
 Lemma map_fmap_union {A B} (f : A → B) (m1 m2 : M A) :
-- 
GitLab