From 16da535d1e2bdd34503de427d5c23640d1a78739 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 11 Sep 2019 22:09:57 +0200
Subject: [PATCH] Equality lemma for `dom D (filter P m)`.

---
 CHANGELOG.md           |  6 ++++++
 theories/fin_map_dom.v | 13 ++++++++++++-
 2 files changed, 18 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 0e0de459..210ae54b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,6 +1,12 @@
 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` into `dom_map_filter_subseteq` and repurpose
+  `dom_map_filter` for the version with the equality. This follows the naming
+  convention for similar lemmas.
+
 ## std++ 1.2.1 (released 2019-08-29)
 
 This release of std++ received contributions by Dan Frumin, Michael Sammler,
diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index f4c4fb86..6fc4c394 100644
--- a/theories/fin_map_dom.v
+++ b/theories/fin_map_dom.v
@@ -19,7 +19,14 @@ Class FinMapDom K M D `{∀ A, Dom (M A) D, FMap M,
 Section fin_map_dom.
 Context `{FinMapDom K M D}.
 
-Lemma dom_map_filter {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A):
+Lemma dom_map_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):
   dom D (filter P m) ⊆ dom D m.
 Proof.
   intros ?. rewrite 2!elem_of_dom.
@@ -132,6 +139,10 @@ Global Instance dom_proper_L `{!Equiv A, !LeibnizEquiv D} :
 Proof. intros ???. unfold_leibniz. by apply dom_proper. Qed.
 
 Context `{!LeibnizEquiv D}.
+Lemma dom_map_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.
 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