Commit 1516b839 authored by Robbert's avatar Robbert

Merge branch 'map_filter_lemmata' into 'master'

Add results about deleting and inserting filtered out elements

See merge request !46
parents 020f31f4 24676fe2
Pipeline #13427 passed with stage
in 7 minutes and 35 seconds
......@@ -1074,6 +1074,13 @@ Section map_filter.
naive_solver.
Qed.
Lemma map_filter_insert_not m i x :
( y, ¬ P (i, y)) filter P (<[i:=x]> m) = filter P m.
Proof.
intros HP. apply map_filter_lookup_eq. intros j y Hy.
by rewrite lookup_insert_ne by naive_solver.
Qed.
Lemma map_filter_delete m i : filter P (delete i m) = delete i (filter P m).
Proof.
apply map_eq. intros j. apply option_eq; intros y.
......@@ -1083,6 +1090,13 @@ Section map_filter.
naive_solver.
Qed.
Lemma map_filter_delete_not m i:
( y, ¬ P (i, y)) filter P (delete i m) = filter P m.
Proof.
intros HP. apply map_filter_lookup_eq; intros j y Hy.
by rewrite lookup_delete_ne by naive_solver.
Qed.
Lemma map_filter_empty : filter P ( : M A) = .
Proof. apply map_fold_empty. Qed.
End map_filter.
......
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