Commit f53dfb6d authored by Robbert's avatar Robbert

Merge branch 'robbert/map_filter' into 'master'

More lemmas for `filter` w.r.t. maps

See merge request !96
parents 07d34651 16da535d
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,
......
......@@ -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 = .
......
......@@ -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) :
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment