Commit 86e53498 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'map_filter_strong_ext' into 'master'

Strengthen `map_filter_strong_ext` and `map_filter_ext`.

See merge request iris/stdpp!269
parents 29af30c2 4100164d
......@@ -42,6 +42,7 @@ API-breaking change is listed.
- Add function `kmap` to transform the keys of finite maps.
- Set `Hint Mode` for the classes `PartialOrder`, `TotalOrder`, `MRet`, `MBind`,
`MJoin`, `FMap`, `OMap`, `MGuard`, `SemiSet`, `Set_`, `TopSet`, and `Infinite`.
- Make `map_filter_strong_ext` and `map_filter_ext` bidirectional.
The following `sed` script should perform most of the renaming
(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
......
......@@ -1326,16 +1326,24 @@ Section map_filter_ext.
Context {A} (P Q : K * A Prop) `{! x, Decision (P x), ! x, Decision (Q x)}.
Lemma map_filter_strong_ext (m1 m2 : M A) :
( i x, (P (i, x) m1 !! i = Some x) (Q (i, x) m2 !! i = Some x))
filter P m1 = filter Q m2.
filter P m1 = filter Q m2
( i x, (P (i, x) m1 !! i = Some x) (Q (i, x) m2 !! i = Some x)).
Proof.
intros HPiff. apply map_eq. intros i. apply option_eq; intros x.
rewrite !map_filter_lookup_Some. naive_solver.
intros. rewrite map_eq_iff. setoid_rewrite option_eq.
setoid_rewrite map_filter_lookup_Some. naive_solver.
Qed.
Lemma map_filter_strong_ext_1 (m1 m2 : M A) :
( i x, (P (i, x) m1 !! i = Some x) (Q (i, x) m2 !! i = Some x))
filter P m1 = filter Q m2.
Proof. by rewrite map_filter_strong_ext. Qed.
Lemma map_filter_strong_ext_2 (m1 m2 : M A) i x :
filter P m1 = filter Q m2
(P (i, x) m1 !! i = Some x) (Q (i, x) m2 !! i = Some x).
Proof. by rewrite map_filter_strong_ext. Qed.
Lemma map_filter_ext (m : M A) :
( i x, m !! i = Some x P (i, x) Q (i, x))
( i x, m !! i = Some x P (i, x) Q (i, x))
filter P m = filter Q m.
Proof. intro. apply map_filter_strong_ext. naive_solver. Qed.
Proof. rewrite map_filter_strong_ext. naive_solver. Qed.
End map_filter_ext.
Section map_filter_insert_and_delete.
......
Supports Markdown
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