Commit bd1e14de by Simon Friis Vindum

### State big_sepM_impl_strong slightly differently

parent ba03110d
Pipeline #51295 passed with stage
in 17 minutes and 31 seconds
 ... ... @@ -1501,32 +1501,20 @@ Lemma big_sepM_sep_zip `{Countable K} {A B} ([∗ map] k↦x ∈ m1, Φ1 k x) ∗ ([∗ map] k↦y ∈ m2, Φ2 k y). Proof. apply big_opM_sep_zip. Qed. Lemma map_filter_true_id `{Countable K} {A} (P : (K * A → Prop)) `{∀ (x : (K * A)), Decision (P x)} (m : gmap K A) : (∀ k x, m !! k = Some x → P (k, x)) → filter P m = m. Proof. intros Hi. induction m as [|i y m ? IH] using map_ind; [done|]. rewrite map_filter_insert. - rewrite IH; [done|]. intros j ??. apply Hi. destruct (decide (i = j)); [naive_solver|]. apply lookup_insert_Some. naive_solver. - apply Hi. by rewrite lookup_insert. Qed. Lemma big_sepM_impl_strong `{Countable K} {A B} Φ (Ψ : K → B → PROP) m1 (m2 : gmap K B) : Lemma big_sepM_impl_strong `{Countable K} {A B} Φ (Ψ : K → B → PROP) (m1 : gmap K A) (m2 : gmap K B) : ([∗ map] k↦x ∈ m1, Φ k x) -∗ □ (∀ (k : K) (y : B), (if m1 !! k is Some x then Φ k x else emp) -∗ ⌜m2 !! k = Some y⌝ → ((∃ (x : A), ⌜m1 !! k = Some x⌝ ∧ Φ k x) ∨ ⌜m1 !! k = None⌝) -∗ Ψ k y) -∗ ([∗ map] k↦y ∈ m2, Ψ k y) ∗ ([∗ map] k↦x ∈ (filter (λ '(k, _), m2 !! k = None) m1), Φ k x). ([∗ map] k↦x ∈ (filter (λ '(k, hi), m2 !! k = None) m1), Φ k x). Proof. 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_true_id; done. rewrite map_filter_id; done. - apply wand_intro_r. rewrite big_sepM_insert; last done. rewrite intuitionistically_sep_dup. ... ... @@ -1534,47 +1522,44 @@ Proof. 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 -or_intro_l -(exist_intro x). rewrite pure_True // left_id. rewrite big_sepM_delete; last apply 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. 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 impl_intro_l, pure_elim_l=> ?. 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 //. * simpl. intros j x'. destruct (decide (i = j)). 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 -or_intro_r. rewrite impl_wand_2. rewrite pure_True // left_id -assoc. + rewrite left_id -assoc. apply sep_mono_r. specialize (IH m1). apply wand_elim_l' in IH. erewrite map_filter_strong_ext. 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 //. 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. Qed. Lemma big_sepM_impl_dom_subseteq `{Countable K} {A B} Φ (Ψ : K → B → PROP) (m1 : gmap K A) (m2 : gmap K B) : Φ (Ψ : K → B → PROP) (m1 : gmap K A) (m2 : gmap K B) : dom (gset _) m2 ⊆ dom _ m1 → ([∗ map] k↦x ∈ m1, Φ k x) -∗ □ (∀ (k : K) (x : A) (y : B), ... ... @@ -1586,15 +1571,12 @@ Proof. apply wand_mono; last done. apply intuitionistically_intro'. rewrite intuitionistically_elim. apply forall_intro=> k. apply forall_intro=> y. apply impl_intro_l, pure_elim_l=> look. apply wand_intro_r. apply wand_elim_r'. apply or_elim. - apply exist_elim=> x. apply pure_elim_l=> ?. rewrite (forall_elim k) (forall_elim x) (forall_elim y). do 2 rewrite pure_True // left_id. apply wand_intro_l. apply wand_elim_l. - rewrite -not_elem_of_dom. apply pure_elim'=> ?. apply elem_of_dom_2 in look. set_solver. 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). 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. Qed. Section and_map. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!