From 41306b352ebe0bd1e083503ee49cced970d9655b Mon Sep 17 00:00:00 2001
From: Dan Frumin <dan@groupoid.moe>
Date: Wed, 26 May 2021 13:45:41 +0200
Subject: [PATCH] Simplify `big_sepM2_union_inv_l` proof significantly.

Thank you, Robbert.
---
 iris/bi/big_op.v | 89 +++++++++++++++++-------------------------------
 1 file changed, 32 insertions(+), 57 deletions(-)

diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index 460f3a7a3..aac677b83 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -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)) //.
-- 
GitLab