From e6cb690acf97529d93da465b7bb8544142b1c800 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 22 Mar 2017 14:39:20 +0100
Subject: [PATCH] WIP.

---
 theories/typing/borrow.v        | 16 +++++++--------
 theories/typing/fixpoint.v      |  2 +-
 theories/typing/product_split.v | 35 ++++++++++++++++-----------------
 theories/typing/shr_bor.v       | 17 ++++++++--------
 theories/typing/uniq_bor.v      | 21 ++++++++++----------
 5 files changed, 43 insertions(+), 48 deletions(-)

diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index 4d075647..e97f2447 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -15,7 +15,7 @@ Section borrow.
   Lemma tctx_borrow E L p n ty κ :
     tctx_incl E L [p ◁ own_ptr n ty] [p ◁ &uniq{κ}ty; p ◁{κ} own_ptr n ty].
   Proof.
-    iIntros (tid ??) "#LFT $ $ H".
+    iIntros (tid ?)  "#LFT _ $ H".
     rewrite /tctx_interp big_sepL_singleton big_sepL_cons big_sepL_singleton.
     iDestruct "H" as ([[]|]) "[% Hown]"; try done. iDestruct "Hown" as "[Hmt ?]".
     iMod (bor_create with "LFT Hmt") as "[Hbor Hext]". done.
@@ -47,7 +47,7 @@ Section borrow.
     lctx_lft_alive E L κ →
     typed_instruction_ty E L [p ◁ &uniq{κ} own_ptr n ty] (!p) (&uniq{κ} ty).
   Proof.
-    iIntros (Hκ tid qE) "#LFT $ HE HL Hp".
+    iIntros (Hκ tid) "#LFT HE $ HL Hp".
     rewrite tctx_interp_singleton.
     iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; first set_solver.
     wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown"; try done.
@@ -77,7 +77,7 @@ Section borrow.
     lctx_lft_alive E L κ →
     typed_instruction_ty E L [p ◁ &shr{κ} own_ptr n ty] (!p) (&shr{κ} ty).
   Proof.
-    iIntros (Hκ tid qE) "#LFT $ HE HL Hp".
+    iIntros (Hκ tid) "#LFT HE $ HL Hp".
     rewrite tctx_interp_singleton.
     iMod (Hκ with "HE HL") as (q) "[[Htok1 Htok2] Hclose]"; first set_solver.
     wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown"; try done.
@@ -103,10 +103,9 @@ Section borrow.
     lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
     typed_instruction_ty E L [p ◁ &uniq{κ} &uniq{κ'} ty] (!p) (&uniq{κ} ty).
   Proof.
-    iIntros (Hκ Hincl tid qE) "#LFT $ HE HL Hp".
+    iIntros (Hκ Hincl tid) "#LFT #HE $ HL Hp".
     rewrite tctx_interp_singleton.
-    iPoseProof (Hincl with "[#] [#]") as "Hincl".
-    { by iApply elctx_interp_persist. } { by iApply llctx_interp_persist. }
+    iDestruct (Hincl with "HL HE") as "#Hincl".
     iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; first set_solver.
     wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown"; try done.
     iMod (bor_exists with "LFT Hown") as (vl) "Hbor". done.
@@ -137,9 +136,8 @@ Section borrow.
     lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
     typed_instruction_ty E L [p ◁ &shr{κ} &uniq{κ'} ty] (!p) (&shr{κ} ty).
   Proof.
-    iIntros (Hκ Hincl tid qE) "#LFT $ HE HL Hp". rewrite tctx_interp_singleton.
-    iPoseProof (Hincl with "[#] [#]") as "Hincl".
-    { by iApply elctx_interp_persist. } { by iApply llctx_interp_persist. }
+    iIntros (Hκ Hincl tid) "#LFT HE $ HL Hp". rewrite tctx_interp_singleton.
+    iDestruct (Hincl with "HL HE") as "#Hincl".
     iMod (Hκ with "HE HL") as (q) "[[Htok1 Htok2] Hclose]"; first set_solver.
     wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hshr"; try done.
     iDestruct "Hshr" as (l') "[H↦ Hown]".
diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index 59bb90bf..a3bd0cc2 100644
--- a/theories/typing/fixpoint.v
+++ b/theories/typing/fixpoint.v
@@ -74,7 +74,7 @@ Section fixpoint.
   Proof.
     unfold eqtype, subtype, type_incl.
     setoid_rewrite <-fixpointK_unfold; [| by apply type_contractive_ne, _..].
-    split; iIntros "_ _"; (iSplit; first done); iSplit; iIntros "!#*$".
+    split; iIntros (qL) "_ !# _"; (iSplit; first done); iSplit; iIntros "!#*$".
   Qed.
 End fixpoint.
 
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index 47a6b6fa..68d42dba 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -37,16 +37,16 @@ Section product_split.
     (∀ tid ty vl, (ptr ty).(ty_own) tid vl -∗ ⌜∃ l : loc, vl = [(#l) : val]⌝) →
     ∀ p, tctx_incl E L [p ◁ ptr $ product tyl] (hasty_ptr_offsets p ptr tyl 0).
   Proof.
-    iIntros (Hsplit Hloc p tid q1 q2) "#LFT HE HL H".
+    iIntros (Hsplit Hloc p tid q) "#LFT #HE HL H".
     iInduction tyl as [|ty tyl IH] "IH" forall (p).
-    { iFrame "HE HL". rewrite tctx_interp_nil. done. }
-    rewrite product_cons. iMod (Hsplit with "LFT HE HL H") as "(HE & HL & H)".
+    { rewrite tctx_interp_nil. auto. }
+    rewrite product_cons. iMod (Hsplit with "LFT HE HL H") as "(HL & H)".
     cbn -[tctx_elt_interp]. rewrite tctx_interp_cons tctx_interp_singleton tctx_interp_cons.
     iDestruct "H" as "[Hty Htyl]". iDestruct "Hty" as (v) "[Hp Hty]". iDestruct "Hp" as %Hp. 
     iDestruct (Hloc with "Hty") as %[l [=->]].
     iAssert (tctx_elt_interp tid (p +ₗ #0 ◁ ptr ty)) with "[Hty]" as "$".
     { iExists #l. iSplit; last done. simpl; by rewrite Hp shift_loc_0. }
-    iMod ("IH" with "HE HL [Htyl]") as "($ & $ & Htyl)".
+    iMod ("IH" with "HL [Htyl]") as "($ & Htyl)".
     { rewrite tctx_interp_singleton //. }
     iClear "IH". rewrite (hasty_ptr_offsets_offset l) // -plus_n_O //.
   Qed.
@@ -59,7 +59,7 @@ Section product_split.
     (∀ tid ty vl, (ptr ty).(ty_own) tid vl -∗ ⌜∃ l : loc, vl = [(#l) : val]⌝) →
     ∀ p, tctx_incl E L (hasty_ptr_offsets p ptr tyl 0) [p ◁ ptr $ product tyl].
   Proof.
-    iIntros (Hptr Htyl Hmerge Hloc p tid q1 q2) "#LFT HE HL H".
+    iIntros (Hptr Htyl Hmerge Hloc p tid q) "#LFT #HE HL H".
     iInduction tyl as [|ty tyl IH] "IH" forall (p Htyl); first done.
     rewrite product_cons. rewrite /= tctx_interp_singleton tctx_interp_cons.
     iDestruct "H" as "[Hty Htyl]". iDestruct "Hty" as (v) "[Hp Hty]".
@@ -68,16 +68,15 @@ Section product_split.
     { move:Hp. simpl. clear. destruct (eval_path p); last done.
       destruct v; try done. destruct l0; try done. rewrite shift_loc_0. done. }
     clear Hp. destruct tyl.
-    { iDestruct (elctx_interp_persist with "HE") as "#HE'".
-      iDestruct (llctx_interp_persist with "HL") as "#HL'". iFrame "HE HL". 
-      iClear "IH Htyl". iExists #l. rewrite product_nil. iSplitR; first done.
-      assert (eqtype E L (ptr ty) (ptr (product2 ty unit))) as [Hincl _].
+    { assert (eqtype E L (ptr ty) (ptr (product2 ty unit))) as [Hincl _].
       { rewrite right_id. done. }
-      iDestruct (Hincl with "HE' HL'") as "#(_ & #Heq & _)". by iApply "Heq". }
-    iMod ("IH" with "[] HE HL [Htyl]") as "(HE & HL & Htyl)"; first done.
+      iDestruct (Hincl with "HL HE") as "#(_ & #Heq & _)".
+      iFrame. iClear "IH Htyl". iExists #l. rewrite product_nil. iSplitR; first done.
+      by iApply "Heq". }
+    iMod ("IH" with "[] HL [Htyl]") as "(HL & Htyl)"; first done.
     { change (ty_size ty) with (0+ty_size ty)%nat at 1.
       rewrite plus_comm -hasty_ptr_offsets_offset //. }
-    iClear "IH". iMod (Hmerge with "LFT HE HL [Hty Htyl]") as "($ & $ & ?)";
+    iClear "IH". iMod (Hmerge with "LFT HE HL [Hty Htyl]") as "($ & ?)";
                    last by rewrite tctx_interp_singleton.
     rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton. iFrame.
     iExists #l. iSplit; done.
@@ -88,7 +87,7 @@ Section product_split.
     tctx_incl E L [p ◁ own_ptr n $ product2 ty1 ty2]
                   [p ◁ own_ptr n ty1; p +ₗ #ty1.(ty_size) ◁ own_ptr n ty2].
   Proof.
-    iIntros (tid q1 q2) "#LFT $ $ H".
+    iIntros (tid q) "#LFT _ $ H".
     rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
     iDestruct "H" as ([[]|]) "[#Hp H]"; try done.
     iDestruct "H" as "[H >H†]". iDestruct "H" as (vl) "[>H↦ H]".
@@ -106,7 +105,7 @@ Section product_split.
     tctx_incl E L [p ◁ own_ptr n ty1; p +ₗ #ty1.(ty_size) ◁ own_ptr n ty2]
                   [p ◁ own_ptr n $ product2 ty1 ty2].
   Proof.
-    iIntros (tid q1 q2) "#LFT $ $ H".
+    iIntros (tid q) "#LFT _ $ H".
     rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
     iDestruct "H" as "[H1 H2]". iDestruct "H1" as ([[]|]) "(Hp1 & H1)"; try done.
     iDestruct "H1" as "(H↦1 & H†1)".
@@ -143,7 +142,7 @@ Section product_split.
     tctx_incl E L [p ◁ &uniq{κ} product2 ty1 ty2]
                   [p ◁ &uniq{κ} ty1; p +ₗ #ty1.(ty_size) ◁ &uniq{κ} ty2].
   Proof.
-    iIntros (tid q1 q2) "#LFT $ $ H".
+    iIntros (tid q) "#LFT _ $ H".
     rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
     iDestruct "H" as ([[]|]) "[Hp H]"; try done. iDestruct "Hp" as %Hp.
     rewrite /= split_prod_mt. iMod (bor_sep with "LFT H") as "[H1 H2]".
@@ -155,7 +154,7 @@ Section product_split.
     tctx_incl E L [p ◁ &uniq{κ} ty1; p +ₗ #ty1.(ty_size) ◁ &uniq{κ} ty2]
                   [p ◁ &uniq{κ} product2 ty1 ty2].
   Proof.
-    iIntros (tid q1 q2) "#LFT $ $ H".
+    iIntros (tid q) "#LFT _ $ H".
     rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
     iDestruct "H" as "[H1 H2]". iDestruct "H1" as ([[]|]) "[Hp1 H1]"; try done.
     iDestruct "Hp1" as %Hp1. iDestruct "H2" as (v2) "(Hp2 & H2)". rewrite /= Hp1.
@@ -192,7 +191,7 @@ Section product_split.
     tctx_incl E L [p ◁ &shr{κ} product2 ty1 ty2]
                   [p ◁ &shr{κ} ty1; p +ₗ #ty1.(ty_size) ◁ &shr{κ} ty2].
   Proof.
-    iIntros (tid q1 q2) "#LFT $ $ H".
+    iIntros (tid q) "#LFT _ $ H".
     rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
     iDestruct "H" as ([[]|]) "[Hp H]"; try iDestruct "H" as "[]".
     iDestruct "H" as "[H1 H2]". iDestruct "Hp" as %Hp.
@@ -203,7 +202,7 @@ Section product_split.
     tctx_incl E L [p ◁ &shr{κ} ty1; p +ₗ #ty1.(ty_size) ◁ &shr{κ} ty2]
                   [p ◁ &shr{κ} product2 ty1 ty2].
   Proof.
-    iIntros (tid q1 q2) "#LFT $ $ H".
+    iIntros (tid q) "#LFT _ $ H".
     rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
     iDestruct "H" as "[H1 H2]". iDestruct "H1" as ([[]|]) "[Hp1 Hown1]"; try done.
     iDestruct "Hp1" as %Hp1. iDestruct "H2" as ([[]|]) "[Hp2 Hown2]"; try done.
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index 2a1abdb4..311dad58 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -20,9 +20,11 @@ Section shr_bor.
     Proper (flip (lctx_lft_incl E L) ==> subtype E L ==> subtype E L) shr_bor.
   Proof.
     intros κ1 κ2 Hκ ty1 ty2 Hty. apply subtype_simple_type.
-    iIntros (? [|[[]|][]]) "#HE #HL H"; try done.
-    iDestruct (Hκ with "HE HL") as "#Hκ". iApply (ty2.(ty_shr_mono) with "Hκ").
-    iDestruct (Hty with "[] []") as "(_ & _ & #Hs1)"; [done..|clear Hty].
+    iIntros (?) "/= HL". iDestruct (Hκ with "HL") as "#Hincl".
+    iDestruct (Hty with "HL") as "#Hty". iIntros "!# #HE".
+    iIntros (? [|[[]|][]]) "H"; try done. iDestruct ("Hincl" with "HE") as "#Hκ".
+    iApply (ty2.(ty_shr_mono) with "Hκ").
+    iDestruct ("Hty" with "HE") as "(_ & _ & #Hs1)"; [done..|clear Hty].
     by iApply "Hs1".
   Qed.
   Global Instance shr_mono_flip E L :
@@ -64,11 +66,8 @@ Section typing.
     lctx_lft_incl E L κ' κ →
     tctx_incl E L [p ◁ &shr{κ}ty] [p ◁ &shr{κ'}ty; p ◁{κ} &shr{κ}ty].
   Proof.
-    iIntros (Hκκ' tid ??) "#LFT HE HL H".
-    iDestruct (elctx_interp_persist with "HE") as "#HE'".
-    iDestruct (llctx_interp_persist with "HL") as "#HL'". iFrame "HE HL".
-    iDestruct (Hκκ' with "HE' HL'") as "Hκκ'".
-    rewrite /tctx_interp big_sepL_singleton big_sepL_cons big_sepL_singleton.
+    iIntros (Hκκ' tid ?) "#LFT #HE HL H". iDestruct (Hκκ' with "HL HE") as "#Hκκ'".
+    iFrame. rewrite /tctx_interp big_sepL_singleton big_sepL_cons big_sepL_singleton.
     iDestruct "H" as ([[]|]) "[% #Hshr]"; try done. iModIntro. iSplit.
     - iExists _. iSplit. done. by iApply (ty_shr_mono with "Hκκ' Hshr").
     - iExists _. auto.
@@ -78,7 +77,7 @@ Section typing.
     Copy ty → lctx_lft_alive E L κ → typed_read E L (&shr{κ}ty) ty (&shr{κ}ty).
   Proof.
     iIntros (Hcopy Halive) "!#".
-    iIntros ([[]|] tid F qE qL ?) "#LFT Htl HE HL #Hshr"; try done.
+    iIntros ([[]|] tid F qL ?) "#LFT #HE Htl HL #Hshr"; try done.
     iMod (Halive with "HE HL") as (q) "[Hκ Hclose]"; first set_solver.
     assert (↑shrN ⊆ (↑lrustN : coPset)) by solve_ndisj. (* set_solver needs some help. *)
     iMod (copy_shr_acc with "LFT Hshr Htl Hκ") as (q') "(Htl & H↦ & Hcl)".
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index d39e3a47..722c74e2 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -46,9 +46,11 @@ Section uniq_bor.
   Global Instance uniq_mono E L :
     Proper (flip (lctx_lft_incl E L) ==> eqtype E L ==> subtype E L) uniq_bor.
   Proof.
-    intros κ1 κ2 Hκ ty1 ty2 Hty%eqtype_unfold. iIntros. iSplit; first done.
-    iDestruct (Hty with "[] []") as "(_ & #Ho & #Hs)"; [done..|clear Hty].
-    iDestruct (Hκ with "[] []") as "#Hκ"; [done..|]. iSplit; iAlways.
+    intros κ1 κ2 Hκ ty1 ty2. rewrite eqtype_unfold=>Hty. iIntros (?) "HL".
+    iDestruct (Hty with "HL") as "#Hty". iDestruct (Hκ with "HL") as "#Hκ".
+    iIntros "!# #HE". iSplit; first done.
+    iDestruct ("Hty" with "HE") as "(_ & #Ho & #Hs)"; [done..|clear Hty].
+    iSpecialize ("Hκ" with "HE"). iSplit; iAlways.
     - iIntros (? [|[[]|][]]) "H"; try done.
       iApply (bor_shorten with "Hκ"). iApply bor_iff; last done.
       iSplit; iIntros "!>!# H"; iDestruct "H" as (vl) "[??]";
@@ -109,7 +111,7 @@ Section typing.
   Lemma tctx_share E L p κ ty :
     lctx_lft_alive E L κ → tctx_incl E L [p ◁ &uniq{κ}ty] [p ◁ &shr{κ}ty].
   Proof.
-    iIntros (Hκ ???) "#LFT HE HL Huniq".
+    iIntros (Hκ ??) "#LFT #HE HL Huniq".
     iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; [try done..|].
     rewrite !tctx_interp_singleton /=.
     iDestruct "Huniq" as ([[]|]) "[% Huniq]"; try done.
@@ -121,11 +123,8 @@ Section typing.
     lctx_lft_incl E L κ' κ →
     tctx_incl E L [p ◁ &uniq{κ}ty] [p ◁ &uniq{κ'}ty; p ◁{κ'} &uniq{κ}ty].
   Proof.
-    iIntros (Hκκ' tid ??) "#LFT HE HL H".
-    iDestruct (elctx_interp_persist with "HE") as "#HE'".
-    iDestruct (llctx_interp_persist with "HL") as "#HL'". iFrame "HE HL".
-    iDestruct (Hκκ' with "HE' HL'") as "Hκκ'".
-    rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
+    iIntros (Hκκ' tid ?) "#LFT HE HL H". iDestruct (Hκκ' with "HL HE") as "#Hκκ'".
+    iFrame. rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
     iDestruct "H" as ([[]|]) "[% Hb]"; try done.
     iMod (rebor with "LFT Hκκ' Hb") as "[Hb Hext]". done. iModIntro.
     iSplitL "Hb"; iExists _; auto.
@@ -174,7 +173,7 @@ Section typing.
     Copy ty → lctx_lft_alive E L κ → typed_read E L (&uniq{κ}ty) ty (&uniq{κ}ty).
   Proof.
     iIntros (Hcopy Halive) "!#".
-    iIntros ([[]|] tid F qE qL ?) "#LFT Htl HE HL Hown"; try done.
+    iIntros ([[]|] tid F qL ?) "#LFT #HE Htl HL Hown"; try done.
     iMod (Halive with "HE HL") as (q) "[Hκ Hclose]"; first set_solver.
     iMod (bor_acc with "LFT Hown Hκ") as "[H↦ Hclose']"; first set_solver.
     iDestruct "H↦" as (vl) "[>H↦ #Hown]".
@@ -188,7 +187,7 @@ Section typing.
     lctx_lft_alive E L κ → typed_write E L (&uniq{κ}ty) ty (&uniq{κ}ty).
   Proof.
     iIntros (Halive) "!#".
-    iIntros ([[]|] tid F qE qL ?) "#LFT HE HL Hown"; try done.
+    iIntros ([[]|] tid F qL ?) "#LFT HE HL Hown"; try done.
     iMod (Halive with "HE HL") as (q) "[Htok Hclose]"; first set_solver.
     iMod (bor_acc with "LFT Hown Htok") as "[H↦ Hclose']". set_solver.
     iDestruct "H↦" as (vl) "[>H↦ Hown]". rewrite ty.(ty_size_eq).
-- 
GitLab