Commit ee76981d authored by Robbert's avatar Robbert

Merge branch 'robbert/dom_filter' into 'master'

Remove `map` infix in lemmas about `dom` and `filter`.

See merge request !176
parents ef460edd 5710f90e
Pipeline #31613 passed with stage
in 10 minutes and 57 seconds
This file lists "large-ish" changes to the std++ Coq library, but not every This file lists "large-ish" changes to the std++ Coq library, but not every
API-breaking change is listed. 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) ## 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. Coq 8.12 is newly supported by this release, and Coq 8.7 is no longer supported.
......
...@@ -21,14 +21,14 @@ Lemma lookup_lookup_total_dom `{!Inhabited A} (m : M A) i : ...@@ -21,14 +21,14 @@ Lemma lookup_lookup_total_dom `{!Inhabited A} (m : M A) i :
i dom D m m !! i = Some (m !!! i). i dom D m m !! i = Some (m !!! i).
Proof. rewrite elem_of_dom. apply lookup_lookup_total. Qed. 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)) ( i, i X x, m !! i = Some x P (i, x))
dom D (filter P m) X. dom D (filter P m) X.
Proof. Proof.
intros HX i. rewrite elem_of_dom, HX. intros HX i. rewrite elem_of_dom, HX.
unfold is_Some. by setoid_rewrite map_filter_lookup_Some. unfold is_Some. by setoid_rewrite map_filter_lookup_Some.
Qed. 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. dom D (filter P m) dom D m.
Proof. Proof.
intros ?. rewrite 2!elem_of_dom. intros ?. rewrite 2!elem_of_dom.
...@@ -156,10 +156,10 @@ Proof. intros ???. unfold_leibniz. by apply dom_proper. Qed. ...@@ -156,10 +156,10 @@ Proof. intros ???. unfold_leibniz. by apply dom_proper. Qed.
Section leibniz. Section leibniz.
Context `{!LeibnizEquiv D}. 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)) ( i, i X x, m !! i = Some x P (i, x))
dom D (filter P m) = 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) _) = . Lemma dom_empty_L {A} : dom D (@empty (M A) _) = .
Proof. unfold_leibniz; apply dom_empty. Qed. Proof. unfold_leibniz; apply dom_empty. Qed.
Lemma dom_empty_inv_L {A} (m : M A) : dom D m = m = . Lemma dom_empty_inv_L {A} (m : M A) : dom D m = m = .
......
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