Commit 41306b35 by Dan Frumin

### Simplify `big_sepM2_union_inv_l` proof significantly.

`Thank you, Robbert.`
parent 6c3226cc
 ... ... @@ -1926,58 +1926,33 @@ Section map2. [∗ map] k↦y1;y2 ∈ m1;m2, Φ1 k y1 ∗ Φ2 k y2. Proof. intros. apply wand_intro_r. by rewrite big_sepM2_sepM. Qed. Lemma big_sepM2_union_inv_l (Φ : K → A → B → PROP) (m1 m2 : gmap K A) (n : gmap K B): m1 ##ₘ m2 → ([∗ map] k↦x;y ∈ (m1 ∪ m2);n, Φ k x y) ⊢ ∃ n1 n2, ⌜n = n1 ∪ n2⌝ ∧ ([∗ map] k↦x;y ∈ m1;n1, Φ k x y) ∗ ([∗ map] k↦x;y ∈ m2;n2, Φ k x y). Proof. pose (P := λ m1, ∀ (m2 : gmap K A) (n : gmap K B), m1 ##ₘ m2 → ([∗ map] k↦x;y ∈ (m1 ∪ m2);n, Φ k x y) -∗ ∃ n1 n2 : gmap K B, ⌜n = n1 ∪ n2⌝ ∧ ([∗ map] k↦x;y ∈ m1;n1, Φ k x y) ∗ ([∗ map] k↦x;y ∈ m2;n2, Φ k x y)). revert m1 m2 n. eapply (map_ind P); unfold P; clear P. { intros m2 n ?. rewrite left_id. rewrite -(exist_intro ∅) -(exist_intro n) left_id pure_True // left_id. rewrite big_sepM2_empty left_id //. } intros i x m1 Hm1 IH m2 n [Hm2i Hmm]%map_disjoint_insert_l. eapply (pure_elim (dom (gset K) n = {[i]} ∪ dom (gset K) m1 ∪ dom (gset K) m2)). { rewrite big_sepM2_dom dom_union_L dom_insert_L. eapply pure_mono. naive_solver. } intros Hdomn. destruct (n !! i) as [y|] eqn:Hni; last first. { exfalso. eapply (not_elem_of_dom n i); eauto; set_solver. } assert (n = <[i:=y]>(delete i n)) as ->. { by rewrite insert_delete insert_id//. } assert ((m1 ∪ m2) !! i = None) as Hm1m2i. { eapply lookup_union_None; naive_solver. } assert (delete i n !! i = None) by eapply lookup_delete. rewrite -insert_union_l big_sepM2_insert//. rewrite (IH m2 (delete i n)) //. rewrite sep_exist_l. eapply exist_elim=>n1. rewrite sep_exist_l. eapply exist_elim=>n2. rewrite comm. eapply wand_elim_l'. eapply pure_elim_l=>Hn1n2. rewrite -(exist_intro (<[i:=y]>n1)) -(exist_intro n2). rewrite pure_True; last first. { rewrite Hn1n2. by rewrite insert_union_l. } eapply (pure_elim (n1 !! i = None)). { rewrite big_sepM2_dom. rewrite sep_elim_l. eapply pure_mono. intros Hfoo. eapply not_elem_of_dom. rewrite -Hfoo. by eapply not_elem_of_dom. } intros Hn1. rewrite big_sepM2_insert // left_id. eapply wand_intro_l. by rewrite assoc. Lemma big_sepM2_union_inv_l (Φ : K → A → B → PROP) m1 m2 m' : m1 ##ₘ m2 → ([∗ map] k↦x;y ∈ (m1 ∪ m2);m', Φ k x y) ⊢ ∃ m1' m2', ⌜m' = m1' ∪ m2'⌝ ∧ ⌜ m1' ##ₘ m2' ⌝ ∧ ([∗ map] k↦x;y ∈ m1;m1', Φ k x y) ∗ ([∗ map] k↦x;y ∈ m2;m2', Φ k x y). Proof. revert m'. induction m1 as [|i x m1 ? IH] using map_ind; intros m' ?; decompose_map_disjoint. { rewrite -(exist_intro ∅) -(exist_intro m') !left_id_L. rewrite !pure_True //; last by apply map_disjoint_empty_l. rewrite big_sepM2_empty !left_id //. } rewrite -insert_union_l big_sepM2_delete_l; last by apply lookup_insert. apply exist_elim=> y. apply pure_elim_l=> ?. rewrite delete_insert; last by apply lookup_union_None. rewrite IH //. rewrite sep_exist_l. eapply exist_elim=> m1'. rewrite sep_exist_l. eapply exist_elim=> m2'. rewrite comm. apply wand_elim_l', pure_elim_l=> Hm'. apply pure_elim_l=> ?. assert ((m1' ∪ m2') !! i = None) as [??]%lookup_union_None. { by rewrite -Hm' lookup_delete. } apply wand_intro_l. rewrite -(exist_intro (<[i:=y]> m1')) -(exist_intro m2'). apply and_intro. { apply pure_intro. by rewrite -insert_union_l -Hm' insert_delete insert_id. } apply and_intro. { apply pure_intro. by apply map_disjoint_insert_l. } by rewrite big_sepM2_insert // -assoc. Qed. Global Instance big_sepM2_empty_persistent Φ : ... ... @@ -2006,12 +1981,12 @@ Section map2. End map2. Lemma big_sepM2_union_inv_r `{Countable K} {A B} (Φ : K → A → B → PROP) (m1 m2 : gmap K B) (n : gmap K A) : (Φ : K → A → B → PROP) (m1 m2 : gmap K B) (m' : gmap K A) : m1 ##ₘ m2 → ([∗ map] k↦x;y ∈ n;(m1 ∪ m2), Φ k x y) ⊢ ∃ n1 n2, ⌜n = n1 ∪ n2⌝ ∧ ([∗ map] k↦x;y ∈ n1;m1, Φ k x y) ∗ ([∗ map] k↦x;y ∈ n2;m2, Φ k x y). ([∗ map] k↦x;y ∈ m';(m1 ∪ m2), Φ k x y) ⊢ ∃ m1' m2', ⌜ m' = m1' ∪ m2' ⌝ ∧ ⌜ m1' ##ₘ m2' ⌝ ∧ ([∗ map] k↦x;y ∈ m1';m1, Φ k x y) ∗ ([∗ map] k↦x;y ∈ m2';m2, Φ k x y). Proof. intros Hm. rewrite -(big_sepM2_flip Φ). rewrite (big_sepM2_union_inv_l (λ k (x : B) y, Φ k y x)) //. ... ...
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!