From 547bf068fba2ac2376a600210f59c625e4221382 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 30 Nov 2016 12:24:00 +0100
Subject: [PATCH] Tweak proofs.

---
 opam.pins                   |  2 +-
 theories/typing/perm_incl.v | 11 +++----
 theories/typing/type.v      | 58 +++++++++++++++++++------------------
 theories/typing/type_incl.v | 28 +++++++++---------
 theories/typing/typing.v    | 30 +++++++------------
 5 files changed, 60 insertions(+), 69 deletions(-)

diff --git a/opam.pins b/opam.pins
index 1aed0164..0f3ece52 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq#f49a7f18c4afc34b9d2766f2b18e45e1a3cd38e7
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq#4417beb8bfa43f89c09a027e8dd55550bf8f7a63
diff --git a/theories/typing/perm_incl.v b/theories/typing/perm_incl.v
index d83416a3..4e58a261 100644
--- a/theories/typing/perm_incl.v
+++ b/theories/typing/perm_incl.v
@@ -37,8 +37,8 @@ Section props.
   Proof.
     split.
     - iIntros (? tid) "H". eauto.
-    - iIntros (??? H12 H23 tid) "#LFT H".
-      iMod (H12 with "LFT H") as "H". by iApply (H23 with "LFT").
+    - iIntros (??? H12 H23 tid) "#LFT H". iApply (H23 with "LFT >").
+      by iApply (H12 with "LFT").
   Qed.
 
   Global Instance perm_equiv_equiv : Equivalence (⇔).
@@ -277,10 +277,7 @@ Section props.
     iApply (fupd_mask_mono (↑lftN)). done.
     iMod (bor_create with "LFT Hown") as "[Hbor Hext]". done.
     iSplitL "Hbor". by simpl; eauto.
-    iMod (bor_create with "LFT Hf") as "[_ Hf]". done.
-    iIntros "!>#H†".
-    iMod ("Hext" with "H†") as "Hext". iMod ("Hf" with "H†") as "Hf". iIntros "!>/=".
-    iExists _. iFrame. auto.
+    iIntros "!>#H†". iExists _. iMod ("Hext" with "H†") as "$". by iFrame.
   Qed.
 
   Lemma rebor_uniq_borrowing κ κ' ν ty :
@@ -293,7 +290,7 @@ Section props.
     iApply (fupd_mask_mono (↑lftN)). done.
     iMod (rebor with "LFT Hord H") as "[H Hextr]". done.
     iModIntro. iSplitL "H". iExists _. by eauto.
-    iIntros "H†". iMod ("Hextr" with "H†"). simpl. auto.
+    iIntros "H†". iExists _. by iMod ("Hextr" with "H†") as "$".
   Qed.
 
   Lemma lftincl_borrowing κ κ' q : borrowing κ ⊤ q.[κ'] (κ ⊑ κ').
diff --git a/theories/typing/type.v b/theories/typing/type.v
index e9b99373..506470f9 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -157,7 +157,8 @@ Section types.
          (∃ l:loc, ⌜vl = [ #l ]⌝ ∗ ▷ l ↦∗: ty.(ty_own) tid ∗ ▷ †{q}l…ty.(ty_size))%I;
        ty_shr κ tid E l :=
          (∃ l':loc, &frac{κ}(λ q', l ↦{q'} #l') ∗
-            ∀ q', □ (q'.[κ] ={mgmtE ∪ E, mgmtE}▷=∗ ty.(ty_shr) κ tid E l' ∗ q'.[κ]))%I
+            □ (∀ q' F, ⌜E ∪ mgmtE ⊆ F⌝ →
+                 q'.[κ] ={F,F∖E}▷=∗ ty.(ty_shr) κ tid E l' ∗ q'.[κ]))%I
     |}.
   Next Obligation. done. Qed.
   Next Obligation.
@@ -176,25 +177,26 @@ Section types.
     rewrite bor_unfold_idx. iDestruct "Hb2" as (i) "(#Hpb&Hpbown)".
     iMod (inv_alloc N _ (idx_bor_own 1 i ∨ ty_shr ty κ tid (↑N) l')%I
          with "[Hpbown]") as "#Hinv"; first by eauto.
-    iExists l'. iIntros "!>{$Hbf}".  iIntros (q'') "!#Htok".
+    iExists l'. iIntros "!>{$Hbf}!#". iIntros (q'' F) "% Htok".
     iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
-    replace ((mgmtE ∪ ↑N) ∖ ↑N) with mgmtE by set_solver.
     iDestruct "INV" as "[>Hbtok|#Hshr]".
-    - iMod (bor_later_tok with "LFT [Hbtok] Htok") as "[Hb Htok]". set_solver.
-      { rewrite bor_unfold_idx. iExists i. eauto. }
-      iMod (ty.(ty_share) with "LFT Hb Htok") as "[#$ $]"; try done.
-      iApply "Hclose". eauto.
-    - iIntros "!>". iNext. iMod ("Hclose" with "[]") as "_"; by eauto.
+    - iMod (bor_later_tok with "LFT [Hbtok] Htok") as "H". set_solver.
+      { rewrite bor_unfold_idx. eauto. }
+      iModIntro. iNext. iMod "H" as "[Hb Htok]".
+      iMod (ty.(ty_share) with "LFT Hb Htok") as "[#$ $]". done. set_solver.
+      iApply "Hclose". auto.
+    - iModIntro. iNext. iMod ("Hclose" with "[]") as "_"; by eauto.
   Qed.
   Next Obligation.
     intros _ ty κ κ' tid E E' l ?. iIntros "#LFT #Hκ #H".
-    iDestruct "H" as (l') "[Hfb Hvs]".
-    iExists l'. iSplit. by iApply (frac_bor_shorten with "[]").
-    iIntros (q') "!#Htok".
-    iApply step_fupd_mask_mono. reflexivity. apply union_preserving_l. eassumption.
+    iDestruct "H" as (l') "[Hfb #Hvs]".
+    iExists l'. iSplit. by iApply (frac_bor_shorten with "[]"). iIntros "!#".
+    iIntros (q' F) "% Htok".
+    iApply (step_fupd_mask_mono F _ _ (F∖E)). set_solver. set_solver.
     iMod (lft_incl_acc with "Hκ Htok") as (q'') "[Htok Hclose]". set_solver.
-    iMod ("Hvs" $! q'' with "Htok") as "[Hshr Htok]".
-    iMod ("Hclose" with "Htok") as "$". by iApply (ty.(ty_shr_mono) with "LFT Hκ").
+    iMod ("Hvs" with "* [%] Htok") as "Hvs'". set_solver. iModIntro. iNext.
+    iMod "Hvs'" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
+      by iApply (ty.(ty_shr_mono) with "LFT Hκ").
   Qed.
   Next Obligation. done. Qed.
 
@@ -204,8 +206,8 @@ Section types.
          (∃ l:loc, ⌜vl = [ #l ]⌝ ∗ &{κ} l ↦∗: ty.(ty_own) tid)%I;
        ty_shr κ' tid E l :=
          (∃ l':loc, &frac{κ'}(λ q', l ↦{q'} #l') ∗
-            ∀ q', □ (q'.[κ∪κ']
-               ={mgmtE ∪ E, ↑tlN}▷=∗ ty.(ty_shr) (κ∪κ') tid E l' ∗ q'.[κ∪κ']))%I
+            □ ∀ q' F, ⌜E ∪ mgmtE ⊆ F⌝ → q'.[κ∪κ']
+               ={F, F∖E∖↑lftN}▷=∗ ty.(ty_shr) (κ∪κ') tid E l' ∗ q'.[κ∪κ'])%I
     |}.
   Next Obligation. done. Qed.
   Next Obligation.
@@ -223,16 +225,14 @@ Section types.
     rewrite {1}bor_unfold_idx. iDestruct "Hb2" as (i) "[#Hpb Hpbown]".
     iMod (inv_alloc N _ (idx_bor_own 1 i ∨ ty_shr ty (κ∪κ') tid (↑N) l')%I
          with "[Hpbown]") as "#Hinv"; first by eauto.
-    iExists l'. iIntros "!>{$Hbf}". iIntros (q'') "!#Htok".
-    iApply (step_fupd_mask_mono (mgmtE ∪ ↑N) _ _ ((mgmtE ∪ ↑N) ∖ ↑N ∖ ↑lftN)).
-    { assert (nclose lftN ⊥ ↑tlN) by solve_ndisj. set_solver. } set_solver.
+    iExists l'. iIntros "!>{$Hbf}!#". iIntros (q'' F) "% Htok".
     iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
     iDestruct "INV" as "[>Hbtok|#Hshr]".
-    - iAssert (&{κ'}&{κ} l' ↦∗: ty_own ty tid)%I with "[Hbtok]" as "Hb".
-      { rewrite (bor_unfold_idx κ'). eauto. }
-      iMod (bor_unnest with "LFT Hb") as "Hb". set_solver.
-      iMod (ty.(ty_share) with "LFT Hb Htok") as "[#Hshr Htok]"; try done. set_solver.
-      iMod ("Hclose" with "[]") as "_". eauto. by iFrame.
+    - iMod (bor_unnest _ _ _ (l' ↦∗: ty_own ty tid)%I with "LFT [Hbtok]") as "Hb".
+      { set_solver. } { iApply bor_unfold_idx. eauto. }
+      iModIntro. iNext. iMod "Hb".
+      iMod (ty.(ty_share) with "LFT Hb Htok") as "[#$ $]"; try done. set_solver.
+      iApply "Hclose". eauto.
     - iMod ("Hclose" with "[]") as "_". by eauto.
       iApply step_fupd_mask_mono; last by eauto. done. set_solver.
   Qed.
@@ -243,11 +243,13 @@ Section types.
       - iApply lft_le_incl. apply gmultiset_union_subseteq_l.
       - iApply (lft_incl_trans with "[] Hκ").
         iApply lft_le_incl. apply gmultiset_union_subseteq_r. }
-    iExists l'. iSplit. by iApply (frac_bor_shorten with "[]"). iIntros (q) "!#Htok".
-    iApply step_fupd_mask_mono. reflexivity. apply union_preserving_l. eassumption.
+    iExists l'. iSplit. by iApply (frac_bor_shorten with "[]").
+    iIntros "!#". iIntros (q F) "% Htok".
+    iApply (step_fupd_mask_mono F _ _ (F∖E∖ ↑lftN)). set_solver. set_solver.
     iMod (lft_incl_acc with "Hκ0 Htok") as (q') "[Htok Hclose]". set_solver.
-    iMod ("Hvs" $! q' with "Htok") as "[#Hshr Htok]".
-    iMod ("Hclose" with "Htok") as "$". by iApply (ty_shr_mono with "LFT Hκ0").
+    iMod ("Hvs" with "* [%] Htok") as "Hvs'". set_solver. iModIntro. iNext.
+    iMod "Hvs'" as "[#Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
+      by iApply (ty_shr_mono with "LFT Hκ0").
   Qed.
   Next Obligation. done. Qed.
 
diff --git a/theories/typing/type_incl.v b/theories/typing/type_incl.v
index 163cf82d..8fa5349e 100644
--- a/theories/typing/type_incl.v
+++ b/theories/typing/type_incl.v
@@ -38,8 +38,7 @@ Section ty_incl.
   Lemma ty_incl_weaken ρ θ ty1 ty2 :
     ρ ⇒ θ → ty_incl θ ty1 ty2 → ty_incl ρ ty1 ty2.
   Proof.
-    iIntros (Hρθ Hρ' tid) "#LFT H". iMod (Hρθ with "LFT H").
-    by iApply (Hρ' with "LFT").
+    iIntros (Hρθ Hρ' tid) "#LFT H". iApply (Hρ' with "LFT>"). iApply (Hρθ with "LFT H").
   Qed.
 
   Global Instance ty_incl_preorder ρ: Duplicable ρ → PreOrder (ty_incl ρ).
@@ -63,8 +62,9 @@ Section ty_incl.
       iDestruct (ty_size_eq with "Hown") as %<-. iFrame.
       iExists _. by iFrame.
     - iDestruct "H" as (l') "[Hfb #Hvs]". iSplit; last done. iExists l'. iFrame.
-      iIntros (q') "!#Hκ". iMod ("Hvs" $! _ with "Hκ") as "[Hshr $]".
-      by iDestruct ("Hshri" $! _ _ _ with "Hshr") as "[$ _]".
+      iIntros "!#". iIntros (q' F) "% Hκ".
+      iMod ("Hvs" with "* [%] Hκ") as "Hvs'". done. iModIntro. iNext.
+      iMod "Hvs'" as "[Hshr $]". by iDestruct ("Hshri" with "* Hshr") as "[$ _]".
   Qed.
 
   Lemma lft_incl_ty_incl_uniq_bor ty κ1 κ2 :
@@ -79,9 +79,10 @@ Section ty_incl.
             apply gmultiset_union_subseteq_l.
         - iApply lft_le_incl. apply gmultiset_union_subseteq_r. }
       iSplitL; last done. iDestruct "H" as (l') "[Hbor #Hupd]". iExists l'.
-      iFrame. iIntros (q') "!#Htok".
+      iFrame. iIntros "!#". iIntros (q' F) "% Htok".
       iMod (lft_incl_acc with "Hincl' Htok") as (q'') "[Htok Hclose]". set_solver.
-      iMod ("Hupd" with "*Htok") as "[H Htok]". iMod ("Hclose" with "Htok") as "$".
+      iMod ("Hupd" with "* [%] Htok") as "Hupd'"; try done. iModIntro. iNext.
+      iMod "Hupd'" as "[H Htok]". iMod ("Hclose" with "Htok") as "$".
       by iApply (ty_shr_mono with "LFT Hincl' H").
   Qed.
 
@@ -194,7 +195,7 @@ Section ty_incl.
                   → (nth i tyl2 ∅%T).(ty_own) tid vl)).
       { clear -FA DUP. induction FA as [|ty1 ty2 tyl1 tyl2 Hincl _ IH].
         - iIntros "_ _!>*!#". eauto.
-        - iIntros "#LFT #Hρ".  iMod (IH with "LFT Hρ") as "#IH".
+        - iIntros "#LFT #Hρ". iMod (IH with "LFT Hρ") as "#IH".
           iMod (Hincl with "LFT Hρ") as "[#Hh _]".
           iIntros "!>*!#*Hown". destruct i as [|i]. by iApply "Hh". by iApply "IH". }
       iMod (Hincl with "LFT Hρ") as "#Hincl". iIntros "!>!#*H".
@@ -219,8 +220,8 @@ Section ty_incl.
   Proof.
     iIntros (? Hρ1ρ2 tid) "#LFT #Hρ!>". iSplit; iIntros "!#*H"; last by auto.
     iDestruct "H" as (f) "[% Hwp]". subst. iExists _. iSplit. done.
-    iIntros (vl) "Hρ2 Htl". iMod (Hρ1ρ2 with "LFT [$Hρ2 $Hρ]").
-    by iApply ("Hwp" with "[-Htl] Htl").
+    iIntros (vl) "Hρ2 Htl". iApply ("Hwp" with ">[-Htl] Htl").
+    iApply (Hρ1ρ2 with "LFT"). by iFrame.
   Qed.
 
   Lemma ty_incl_fn {A n} ρ ρ1 ρ2 :
@@ -229,13 +230,12 @@ Section ty_incl.
   Proof.
     iIntros (? Hρ1ρ2 tid) "#LFT #Hρ!>". iSplit; iIntros "!#*#H".
     - iDestruct "H" as (f) "[% Hwp]". subst. iExists _. iSplit. done.
-      iIntros (x vl) "!#[Hρ2 Htl]". iMod (Hρ1ρ2 with "LFT [$Hρ2 $Hρ]").
-      iApply "Hwp". by iFrame.
+      iIntros (x vl) "!#[Hρ2 Htl]". iApply ("Hwp" with ">").
+      iFrame. iApply (Hρ1ρ2 with "LFT"). by iFrame.
     - iSplit; last done. simpl. iDestruct "H" as (vl0) "[? Hvl]".
       iExists vl0. iFrame "#". iNext. iDestruct "Hvl" as (f) "[% Hwp]".
-      iExists f. iSplit. done.
-      iIntros (x vl) "!#[Hρ2 Htl]". iMod (Hρ1ρ2 with "LFT [$Hρ2 $Hρ]").
-      iApply "Hwp". by iFrame.
+      iExists f. iSplit. done. iIntros (x vl) "!#[Hρ2 Htl]".
+      iApply ("Hwp" with ">"). iFrame. iApply (Hρ1ρ2 with "LFT >"). by iFrame.
   Qed.
 
   Lemma ty_incl_fn_cont {A n} ρ ρf (x : A) :
diff --git a/theories/typing/typing.v b/theories/typing/typing.v
index d2681f49..ae621f46 100644
--- a/theories/typing/typing.v
+++ b/theories/typing/typing.v
@@ -292,17 +292,13 @@ Section typing.
     iApply (has_type_wp with "H◁"). iIntros (v) "Hνv H◁!>". iDestruct "Hνv" as %Hνv.
     rewrite has_type_value. iDestruct "H◁" as (l) "[Heq #H↦]". iDestruct "Heq" as %[=->].
     iMod (lft_incl_acc with "H⊑ Htok") as (q'') "[[Htok1 Htok2] Hclose]". done.
-    iDestruct "H↦" as (vl) "[H↦b Hown]".
+    iDestruct "H↦" as (vl) "[H↦b #Hown]".
     iMod (frac_bor_acc with "LFT H↦b Htok1") as (q''') "[>H↦ Hclose']". done.
-    iApply (wp_fupd_step _ (↑heapN) with "[Hown Htok2]"); try done.
-    - rewrite -(left_id (R:=eq) ∅ (∪) (↑heapN)). assert (⊤ = ⊤∖↑heapN ∪ ↑heapN) as ->.
-      { by rewrite (comm (R:=eq)) -union_difference_L. }
-      iApply step_fupd_mask_frame_r; try set_solver.
-      iApply step_fupd_mask_mono; last by iApply ("Hown" with "* Htok2").
-        set_solver. repeat apply union_least; solve_ndisj.
+    iApply (wp_fupd_step _ (⊤∖↑lrustN) with "[Hown Htok2]"); try done.
+    - iApply ("Hown" with "* [%] Htok2"). set_solver.
     - wp_read. iIntros "!>[Hshr ?]". iFrame "H⊑".
-      iSplitL "Hshr"; first by iExists _; auto.
-      iMod ("Hclose'" with "[$H↦]") as "?". iApply "Hclose". iFrame.
+      iSplitL "Hshr"; first by iExists _; auto. iApply ("Hclose" with ">").
+      iFrame. iApply "Hclose'". auto.
   Qed.
 
   Lemma typed_deref_uniq_bor_bor ty ν κ κ' κ'' q:
@@ -326,7 +322,7 @@ Section typing.
     wp_read. iIntros "!> Hbor". iFrame "#". iSplitL "Hbor".
     - iExists _. iSplitR; first by auto. iApply (bor_shorten with "[] Hbor").
       iApply (lft_incl_glb with "H⊑2"). iApply lft_incl_refl.
-    - iMod ("Hclose'" with "[$H↦]") as "[_ ?]". by iApply "Hclose".
+    - iApply ("Hclose" with ">"). by iMod ("Hclose'" with "[$H↦]") as "[_ $]".
   Qed.
 
   Lemma typed_deref_shr_bor_bor ty ν κ κ' κ'' q:
@@ -343,16 +339,12 @@ Section typing.
     iAssert (κ' ⊑ κ'' ∪ κ')%I as "#H⊑3".
     { iApply (lft_incl_glb with "H⊑2 []"). iApply lft_incl_refl. }
     iMod (lft_incl_acc with "H⊑3 Htok2") as (q''') "[Htok Hclose'']". done.
-    iApply (wp_fupd_step _ (↑heapN) with "[Hown Htok]"); try done.
-    - rewrite -(left_id (R:=eq) ∅ (∪) (↑heapN)). assert (⊤ = ⊤∖↑heapN ∪ ↑heapN) as ->.
-      { by rewrite (comm (R:=eq)) -union_difference_L. }
-      iApply step_fupd_mask_frame_r; try set_solver.
-      iApply step_fupd_mask_mono; last by iApply ("Hown" with "* Htok").
-        set_solver. repeat apply union_least; solve_ndisj.
+    iApply (wp_fupd_step _ (_∖_) with "[Hown Htok]"); try done.
+    - iApply ("Hown" with "* [%] Htok"). set_solver.
     - wp_read. iIntros "!>[Hshr Htok]". iFrame "H⊑1". iSplitL "Hshr".
       + iExists _. iSplitR. done. by iApply (ty_shr_mono with "LFT H⊑3 Hshr").
-      + iMod ("Hclose''" with "Htok"). iMod ("Hclose'" with "[$H↦]").
-        iApply "Hclose". iFrame.
+      + iApply ("Hclose" with ">"). iMod ("Hclose'" with "[$H↦]") as "$".
+        by iMod ("Hclose''" with "Htok") as "$".
   Qed.
 
   Definition update (ty : type) (ρ1 ρ2 : expr → perm) : Prop :=
@@ -421,7 +413,7 @@ Section typing.
     typed_program ρ2 e → (ρ1 ⇒ ρ2) → typed_program ρ1 e.
   Proof.
     iIntros (Hρ2 Hρ12 tid) "!#(#HEAP & #LFT & Hρ1 & Htl)".
-    iMod (Hρ12 with "LFT Hρ1"). iApply Hρ2. iFrame "∗#".
+    iApply (Hρ2 with ">"). iFrame "∗#". iApply (Hρ12 with "LFT Hρ1").
   Qed.
 
   Lemma typed_program_exists {A} ρ θ e:
-- 
GitLab