Commit 10636f91 authored by Paulo Emílio de Vilhena's avatar Paulo Emílio de Vilhena
Browse files

Add context to section [map_filter_misc] and shorten some proofs.

parent 388382c4
......@@ -1316,10 +1316,9 @@ Section map_filter_insert_and_delete.
P (i, x) filter P (<[i:=x]> m) = <[i:=x]> (filter P m).
Proof.
intros HP. apply map_eq. intros j. apply option_eq; intros y.
destruct (decide (j = i)) as [->|?].
- rewrite map_filter_lookup_Some, !lookup_insert. naive_solver.
- rewrite lookup_insert_ne, !map_filter_lookup_Some, lookup_insert_ne by done.
naive_solver.
rewrite map_filter_lookup_Some. destruct (decide (i = j)) as [->|?].
- rewrite !lookup_insert. naive_solver.
- rewrite !lookup_insert_ne by done. symmetry. apply map_filter_lookup_Some.
Qed.
Lemma map_filter_insert_not' m i x :
......@@ -1353,22 +1352,20 @@ Section map_filter_insert_and_delete.
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_strong_ext. intros j y.
split; intros [? Hlkup].
- rewrite lookup_delete_ne in Hlkup; [done|].
intros ->. by rewrite lookup_delete in Hlkup.
- by rewrite lookup_delete_ne by naive_solver.
intros ?. case (m !! i) as [x|] eqn:?.
- by rewrite <-(map_filter_insert_not_delete _ _ x), insert_id by done.
- by rewrite delete_notin.
Qed.
End map_filter_insert_and_delete.
Section map_filter_misc.
Context {A} (P : K * A Prop) `{! x, Decision (P x)}.
Implicit Types m : M A.
Lemma map_filter_empty {A} (P : K * A Prop) `{! x, Decision (P x)} :
filter P ( : M A) = .
Lemma map_filter_empty : filter P ( : M A) = .
Proof. apply map_fold_empty. Qed.
Lemma map_filter_alt {A} (P : K * A Prop) `{! x, Decision (P x)} (m : M A) :
filter P m = list_to_map (filter P (map_to_list m)).
Lemma map_filter_alt m : filter P m = list_to_map (filter P (map_to_list m)).
Proof.
apply list_to_map_flip. induction m as [|k x m ? IH] using map_ind.
{ by rewrite map_to_list_empty, map_filter_empty, map_to_list_empty. }
......@@ -1378,8 +1375,7 @@ Section map_filter_misc.
- by rewrite map_filter_insert_not' by naive_solver.
Qed.
Lemma map_filter_fmap {A B} (P : K * A Prop) `{! x, Decision (P x)}
(f : B A) (m : M B) :
Lemma map_filter_fmap {B} (f : B A) (m : M B) :
filter P (f <$> m) = f <$> filter (λ '(i, x), P (i, (f x))) m.
Proof.
apply map_eq. intros i. apply option_eq; intros x.
......@@ -1387,29 +1383,20 @@ Section map_filter_misc.
naive_solver.
Qed.
Lemma map_filter_filter {A} (P Q : K * A Prop)
`{! x, Decision (P x), ! x, Decision (Q x)} (m : M A) :
Lemma map_filter_filter Q `{! x, Decision (Q x)} m :
filter P (filter Q m) = filter (λ '(i, x), P (i, x) Q (i, x)) m.
Proof.
apply map_filter_strong_ext. intros k v.
apply map_filter_strong_ext. intros ??.
rewrite map_filter_lookup_Some. naive_solver.
Qed.
Lemma map_filter_filter_l {A} (P Q : K * A Prop)
`{! x, Decision (P x), ! x, Decision (Q x)} (m : M A) :
Lemma map_filter_filter_l Q `{! x, Decision (Q x)} m :
( i x, m !! i = Some x P (i, x) Q (i, x))
filter P (filter Q m) = filter P m.
Proof.
intros HPimp. rewrite map_filter_filter.
apply map_filter_strong_ext. naive_solver.
Qed.
Lemma map_filter_filter_r {A} (P Q : K * A Prop)
`{! x, Decision (P x), ! x, Decision (Q x)} (m : M A) :
Proof. intros ?. rewrite map_filter_filter. apply map_filter_ext. naive_solver. Qed.
Lemma map_filter_filter_r Q `{! x, Decision (Q x)} m :
( i x, m !! i = Some x Q (i, x) P (i, x))
filter P (filter Q m) = filter Q m.
Proof.
intros HPimp. rewrite map_filter_filter.
apply map_filter_strong_ext. naive_solver.
Qed.
Proof. intros ?. rewrite map_filter_filter. apply map_filter_ext. naive_solver. Qed.
End map_filter_misc.
(** ** Properties of the [map_Forall] predicate *)
......
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