diff --git a/CHANGELOG.md b/CHANGELOG.md index 0e0de45930e20bc262d067a85f531493f46af77c..210ae54badd1596da1f9ef7dbbc566f04e2adb76 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 f4c4fb867c5a4dea2ca4d705632e70a05d24e8e2..6fc4c39434f74ce3664e3601919e1f6dfb4a9599 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 = ∅. diff --git a/theories/fin_maps.v b/theories/fin_maps.v index d279c4e7d65e48bd141450ab1b312a16b7a68b15..f22e042198d8875e5433ba519f1330cf1ed98484 100644 --- a/theories/fin_maps.v +++ b/theories/fin_maps.v @@ -1507,6 +1507,12 @@ 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) : + filter P m ##ₘ filter (λ v, ¬ P v) m. +Proof. + apply map_disjoint_spec. intros i x y. + rewrite !map_filter_lookup_Some. naive_solver. +Qed. (** ** Properties of the [union_with] operation *) Section union_with. @@ -1783,6 +1789,13 @@ Proof. naive_solver eauto using map_Forall_union_11, map_Forall_union_12, map_Forall_union_2. Qed. +Lemma map_union_filter {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. + destruct (decide (P (i,x))); naive_solver. +Qed. (** ** Properties of the [union_list] operation *) Lemma map_disjoint_union_list_l {A} (ms : list (M A)) (m : M A) :