From 5710f90e52dbe0409b856fadeba3e5665de4d1b5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 16 Jul 2020 14:00:42 +0200
Subject: [PATCH] =?UTF-8?q?Rename=20`dom=5Fmap=20filter`=20=E2=86=92=20`do?=
 =?UTF-8?q?m=5Ffilter`,=20`dom=5Fmap=5Ffilter=5FL`=20=E2=86=92=20`dom=5Ffi?=
 =?UTF-8?q?lter=5FL`,=20and=20`dom=5Fmap=5Ffilter=5Fsubseteq`=20=E2=86=92?=
 =?UTF-8?q?=20`dom=5Ffilter=5Fsubseteq`=20for=20consistency's=20sake.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This was pointed out by @atrieu in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/175#note_53746
---
 CHANGELOG.md           | 5 +++++
 theories/fin_map_dom.v | 8 ++++----
 2 files changed, 9 insertions(+), 4 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index aca01da6..81d013d3 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,6 +1,11 @@
 This file lists "large-ish" changes to the std++ Coq library, but not every
 API-breaking change is listed.
 
+## std++ master
+
+- Rename `dom_map filter` → `dom_filter`, `dom_map_filter_L` → `dom_filter_L`,
+  and `dom_map_filter_subseteq` → `dom_filter_subseteq` for consistency's sake.
+
 ## std++ 1.4.0 (released 2020-07-15)
 
 Coq 8.12 is newly supported by this release, and Coq 8.7 is no longer supported.
diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index ed3c554e..886daae1 100644
--- a/theories/fin_map_dom.v
+++ b/theories/fin_map_dom.v
@@ -21,14 +21,14 @@ Lemma lookup_lookup_total_dom `{!Inhabited A} (m : M A) i :
   i ∈ dom D m → m !! i = Some (m !!! i).
 Proof. rewrite elem_of_dom. apply lookup_lookup_total. Qed.
 
-Lemma dom_map_filter {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A) X :
+Lemma dom_filter {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A) X :
   (∀ i, i ∈ X ↔ ∃ x, m !! i = Some x ∧ P (i, x)) →
   dom D (filter P m) ≡ X.
 Proof.
   intros HX i. rewrite elem_of_dom, HX.
   unfold is_Some. by setoid_rewrite map_filter_lookup_Some.
 Qed.
-Lemma dom_map_filter_subseteq {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A):
+Lemma dom_filter_subseteq {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A):
   dom D (filter P m) ⊆ dom D m.
 Proof.
   intros ?. rewrite 2!elem_of_dom.
@@ -156,10 +156,10 @@ Proof. intros ???. unfold_leibniz. by apply dom_proper. Qed.
 
 Section leibniz.
   Context `{!LeibnizEquiv D}.
-  Lemma dom_map_filter_L {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A) X :
+  Lemma dom_filter_L {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A) X :
     (∀ i, i ∈ X ↔ ∃ x, m !! i = Some x ∧ P (i, x)) →
     dom D (filter P m) = X.
-  Proof. unfold_leibniz. apply dom_map_filter. Qed.
+  Proof. unfold_leibniz. apply dom_filter. Qed.
   Lemma dom_empty_L {A} : dom D (@empty (M A) _) = ∅.
   Proof. unfold_leibniz; apply dom_empty. Qed.
   Lemma dom_empty_inv_L {A} (m : M A) : dom D m = ∅ → m = ∅.
-- 
GitLab