Commit 7413fc76 authored by Robbert Krebbers's avatar Robbert Krebbers Committed by Simon Friis Vindum
Browse files

Apply 4 suggestion(s) to 1 file(s)

parent d4423268
Pipeline #51499 failed with stage
in 3 minutes and 53 seconds
......@@ -1501,79 +1501,62 @@ Lemma big_sepM_sep_zip `{Countable K} {A B}
([ map] kx m1, Φ1 k x) ([ map] ky m2, Φ2 k y).
Proof. apply big_opM_sep_zip. Qed.
Lemma big_sepM_impl_strong `{Countable K} {A B} Φ (Ψ : K B PROP) (m1 : gmap K A) (m2 : gmap K B) :
Lemma big_sepM_impl_strong `{Countable K} {A B}
(Φ : K A PROP) (Ψ : K B PROP) (m1 : gmap K A) (m2 : gmap K B) :
([ map] kx m1, Φ k x) -
( (k : K) (y : B),
(if m1 !! k is Some x then Φ k x else emp) -
m2 !! k = Some y
Ψ k y) -
([ map] ky m2, Ψ k y)
([ map] kx (filter (λ '(k, hi), m2 !! k = None) m1), Φ k x).
([ map] kx filter (λ '(k, _), m2 !! k = None) m1, Φ k x).
Proof.
apply wand_intro_r.
revert m1. induction m2 as [|i y m ? IH] using map_ind=> m1.
- apply wand_intro_r.
rewrite big_sepM_empty left_id.
rewrite intuitionistically_elim_emp right_id.
rewrite map_filter_id; done.
- apply wand_intro_r.
rewrite big_sepM_insert; last done.
rewrite intuitionistically_sep_dup.
rewrite assoc. rewrite (comm _ _ ( _))%I.
rewrite {1}intuitionistically_elim {1}(forall_elim i) {1}(forall_elim y).
rewrite lookup_insert pure_True // left_id.
destruct (m1 !! i) as [x|] eqn:Hl.
+ rewrite big_sepM_delete; last apply Hl.
rewrite assoc assoc wand_elim_l -assoc -assoc.
apply sep_mono_r.
specialize (IH (delete i m1)). apply wand_elim_l' in IH.
erewrite map_filter_strong_ext_1.
* erewrite <- IH.
apply sep_mono_r.
apply intuitionistically_intro'. rewrite intuitionistically_elim.
apply forall_intro=> k. apply forall_intro=> b.
rewrite (forall_elim k) (forall_elim b).
apply wand_intro_r.
apply impl_intro_l, pure_elim_l=> Hi.
assert (i k) by congruence.
rewrite lookup_insert_ne // pure_True // left_id.
rewrite lookup_delete_ne // wand_elim_l //.
* intros j x'. destruct (decide (i = j)).
{ simplify_eq. rewrite lookup_delete lookup_insert. naive_solver. }
rewrite lookup_delete_ne // lookup_insert_ne //.
+ rewrite left_id -assoc.
apply sep_mono_r.
specialize (IH m1). apply wand_elim_l' in IH.
erewrite map_filter_strong_ext_1.
* erewrite <- IH.
apply sep_mono_r.
apply intuitionistically_intro'. rewrite intuitionistically_elim.
apply forall_intro=> k. apply forall_intro=> b.
rewrite (forall_elim k) (forall_elim b).
apply wand_intro_r.
apply impl_intro_l, pure_elim_l=> ?.
rewrite lookup_insert_ne; last congruence.
rewrite pure_True // left_id // wand_elim_l //.
* intros i' x'. simpl.
destruct (decide (i = i')) as [?|neq]; first naive_solver.
by rewrite lookup_insert_ne.
{ rewrite big_sepM_empty left_id sep_elim_l.
rewrite map_filter_id //. }
rewrite big_sepM_insert; last done.
rewrite intuitionistically_sep_dup.
rewrite assoc. rewrite (comm _ _ ( _))%I.
rewrite {1}intuitionistically_elim {1}(forall_elim i) {1}(forall_elim y).
rewrite lookup_insert pure_True // left_id.
destruct (m1 !! i) as [x|] eqn:Hx.
- rewrite big_sepM_delete; last done.
rewrite assoc assoc wand_elim_l -2!assoc. apply sep_mono_r.
assert (filter (λ '(k, _), <[i:=y]> m !! k = None) m1
= filter (λ '(k, _), m !! k = None) (delete i m1)) as ->.
{ apply map_filter_strong_ext_1=> k z.
rewrite lookup_insert_None lookup_delete_Some. naive_solver. }
rewrite -IH. do 2 f_equiv. f_equiv=> k. f_equiv=> z.
apply wand_intro_r. apply impl_intro_l, pure_elim_l=> ?.
assert (i k) by congruence.
rewrite lookup_insert_ne // pure_True // left_id.
rewrite lookup_delete_ne // wand_elim_l //.
- rewrite left_id -assoc. apply sep_mono_r.
assert (filter (λ '(k, _), <[i:=y]> m !! k = None) m1
= filter (λ '(k, _), m !! k = None) m1) as ->.
{ apply map_filter_strong_ext_1=> k z.
rewrite lookup_insert_None. naive_solver. }
rewrite -IH. do 2 f_equiv. f_equiv=> k. f_equiv=> z.
apply wand_intro_r. apply impl_intro_l, pure_elim_l=> ?.
rewrite lookup_insert_ne; last congruence.
rewrite pure_True // left_id // wand_elim_l //.
Qed.
Lemma big_sepM_impl_dom_subseteq `{Countable K} {A B}
Φ (Ψ : K B PROP) (m1 : gmap K A) (m2 : gmap K B) :
(Φ : K A PROP) (Ψ : K B PROP) (m1 : gmap K A) (m2 : gmap K B) :
dom (gset _) m2 dom _ m1
([ map] kx m1, Φ k x) -
( (k : K) (x : A) (y : B),
m1 !! k = Some x m2 !! k = Some y Φ k x - Ψ k y) -
m1 !! k = Some x m2 !! k = Some y
Φ k x - Ψ k y) -
([ map] ky m2, Ψ k y)
([ map] kx (filter (λ '(k, _), m2 !! k = None) m1), Φ k x).
([ map] kx filter (λ '(k, _), m2 !! k = None) m1, Φ k x).
Proof.
intros Hsub. rewrite big_sepM_impl_strong.
apply wand_mono; last done.
apply intuitionistically_intro'. rewrite intuitionistically_elim.
apply forall_intro=> k. apply forall_intro=> y.
intros. rewrite big_sepM_impl_strong.
apply wand_mono; last done. f_equiv. f_equiv=> k. apply forall_intro=> y.
apply wand_intro_r, impl_intro_l, pure_elim_l=> Hlm2.
destruct (m1 !! k) as [x|] eqn:Hlm1.
- rewrite (forall_elim k) (forall_elim x) (forall_elim y).
- rewrite (forall_elim x) (forall_elim y).
do 2 rewrite pure_True // left_id //. apply wand_elim_l.
- apply elem_of_dom_2 in Hlm2. apply not_elem_of_dom in Hlm1.
set_solver.
......
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