Merge branch 'master' of gitlab.mpi-sws.org:FP/LambdaRust-coq

theories/lifetime/frac_borrow.v

@@ -26,11 +26,12 @@ Section frac_bor.
   Global Instance frac_bor_proper κ :
     Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (frac_bor κ).
   Proof. solve_proper. Qed.
-  Lemma frac_bor_iff_proper κ φ' :
+
+  Lemma frac_bor_iff κ φ' :
     ▷ □ (∀ q, φ q ↔ φ' q) -∗ &frac{κ} φ -∗ &frac{κ} φ'.
   Proof.
     iIntros "#Hφφ' H". iDestruct "H" as (γ κ') "[? Hφ]". iExists γ, κ'. iFrame.
-    iApply (shr_bor_iff_proper with "[Hφφ'] Hφ"). iNext. iAlways.
+    iApply (shr_bor_iff with "[Hφφ'] Hφ"). iNext. iAlways.
     iSplit; iIntros "H"; iDestruct "H" as (q) "[H ?]"; iExists q; iFrame; by iApply "Hφφ'".
   Qed.
 

theories/lifetime/lifetime_sig.v

@@ -67,11 +67,9 @@ Module Type lifetime_sig.
   Global Declare Instance bor_ne κ n : Proper (dist n ==> dist n) (bor κ).
   Global Declare Instance bor_contractive κ : Contractive (bor κ).
   Global Declare Instance bor_proper κ : Proper ((≡) ==> (≡)) (bor κ).
-  Parameter bor_iff_proper : ∀ κ P P', ▷ □ (P ↔ P') -∗ &{κ}P -∗ &{κ}P'.
   Global Declare Instance idx_bor_ne κ i n : Proper (dist n ==> dist n) (idx_bor κ i).
   Global Declare Instance idx_bor_contractive κ i : Contractive (idx_bor κ i).
   Global Declare Instance idx_bor_proper κ i : Proper ((≡) ==> (≡)) (idx_bor κ i).
-  Parameter idx_bor_iff_proper : ∀ κ i P P', ▷ □ (P ↔ P') -∗ &{κ,i}P -∗ &{κ,i}P'.
 
   Global Declare Instance lft_tok_fractional κ : Fractional (λ q, q.[κ])%I.
   Global Declare Instance lft_tok_as_fractional κ q :
@@ -94,20 +92,24 @@ Module Type lifetime_sig.
   Parameter bor_fake : ∀ E κ P,
     ↑lftN ⊆ E → lft_ctx -∗ [†κ] ={E}=∗ &{κ}P.
 
+  Parameter bor_iff : ∀ κ P P', ▷ □ (P ↔ P') -∗ &{κ}P -∗ &{κ}P'.
+  Parameter bor_shorten : ∀ κ κ' P, κ ⊑ κ' -∗ &{κ'}P -∗ &{κ}P.
+
   Parameter bor_sep : ∀ E κ P Q,
     ↑lftN ⊆ E → lft_ctx -∗ &{κ} (P ∗ Q) ={E}=∗ &{κ} P ∗ &{κ} Q.
   Parameter bor_combine : ∀ E κ P Q,
     ↑lftN ⊆ E → lft_ctx -∗ &{κ} P -∗ &{κ} Q ={E}=∗ &{κ} (P ∗ Q).
 
-  Parameter bor_unfold_idx : ∀ κ P, &{κ}P ⊣⊢ ∃ i, &{κ,i}P ∗ idx_bor_own 1 i.
-  Parameter bor_shorten : ∀ κ κ' P, κ ⊑ κ' -∗ &{κ'}P -∗ &{κ}P.
-  Parameter idx_bor_shorten : ∀ κ κ' i P, κ ⊑ κ' -∗ &{κ',i} P -∗ &{κ,i} P.
-
   Parameter rebor : ∀ E κ κ' P,
     ↑lftN ⊆ E → lft_ctx -∗ κ' ⊑ κ -∗ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗ &{κ}P).
   Parameter bor_unnest : ∀ E κ κ' P,
     ↑lftN ⊆ E → lft_ctx -∗ &{κ'} &{κ} P ={E, E∖↑lftN}▷=∗ &{κ ∪ κ'} P.
 
+  Parameter bor_unfold_idx : ∀ κ P, &{κ}P ⊣⊢ ∃ i, &{κ,i}P ∗ idx_bor_own 1 i.
+
+  Parameter idx_bor_shorten : ∀ κ κ' i P, κ ⊑ κ' -∗ &{κ',i} P -∗ &{κ,i} P.
+  Parameter idx_bor_iff : ∀ κ i P P', ▷ □ (P ↔ P') -∗ &{κ,i}P -∗ &{κ,i}P'.
+
   Parameter idx_bor_acc : ∀ E q κ i P, ↑lftN ⊆ E →
     lft_ctx -∗ &{κ,i}P -∗ idx_bor_own 1 i -∗ q.[κ] ={E}=∗
       ▷ P ∗ (▷ P ={E}=∗ idx_bor_own 1 i ∗ q.[κ]).

theories/lifetime/model/primitive.v

@@ -380,7 +380,7 @@ Proof.
 Qed.
 
 (** Basic rules about borrows *)
-Lemma raw_bor_iff_proper i P P' : ▷ □ (P ↔ P') -∗ raw_bor i P -∗ raw_bor i P'.
+Lemma raw_bor_iff i P P' : ▷ □ (P ↔ P') -∗ raw_bor i P -∗ raw_bor i P'.
 Proof.
   iIntros "#HPP' HP". unfold raw_bor. iDestruct "HP" as (s) "[HiP HP]".
   iExists s. iFrame. iDestruct "HP" as (P0) "[#Hiff ?]". iExists P0. iFrame.
@@ -388,7 +388,7 @@ Proof.
   by iApply "HPP'"; iApply "Hiff". by iApply "Hiff"; iApply "HPP'".
 Qed.
 
-Lemma idx_bor_iff_proper κ i P P' : ▷ □ (P ↔ P') -∗ &{κ,i}P -∗ &{κ,i}P'.
+Lemma idx_bor_iff κ i P P' : ▷ □ (P ↔ P') -∗ &{κ,i}P -∗ &{κ,i}P'.
 Proof.
   unfold idx_bor. iIntros "#HPP' [$ HP]". iDestruct "HP" as (P0) "[#HP0P Hs]".
   iExists P0. iFrame. iNext. iAlways. iSplit; iIntros.
@@ -404,10 +404,10 @@ Proof.
     iExists κ'. iFrame. iExists s. by iFrame.
 Qed.
 
-Lemma bor_iff_proper κ P P' : ▷ □ (P ↔ P') -∗ &{κ}P -∗ &{κ}P'.
+Lemma bor_iff κ P P' : ▷ □ (P ↔ P') -∗ &{κ}P -∗ &{κ}P'.
 Proof.
   rewrite !bor_unfold_idx. iIntros "#HPP' HP". iDestruct "HP" as (i) "[??]".
-  iExists i. iFrame. by iApply (idx_bor_iff_proper with "HPP'").
+  iExists i. iFrame. by iApply (idx_bor_iff with "HPP'").
 Qed.
 
 Lemma bor_shorten κ κ' P : κ ⊑ κ' -∗ &{κ'}P -∗ &{κ}P.

theories/lifetime/model/raw_reborrow.v

@@ -133,7 +133,7 @@ Proof.
     iIntros "[$ [>? $]]". iModIntro. iNext. rewrite /raw_bor.
     iExists i. iFrame. iExists _. iFrame "#". }
   iExists Pb'. iModIntro. iFrame. iSplitL "Hclose Hκ". by iApply "Hclose".
-  by iApply (raw_bor_iff_proper with "HPP'").
+  by iApply (raw_bor_iff with "HPP'").
 Qed.
 
 Lemma raw_rebor E κ κ' P :
@@ -171,7 +171,7 @@ Proof.
     with "[$HI $Hκ] Hi Hislice Hbor [Hvs]")
     as (Pb') "([HI Hκ] & HP' & Halive & Hvs)"; [solve_ndisj|done|done|..].
   { iNext. by iApply lft_vs_frame. }
-  iDestruct (raw_bor_iff_proper with "HPP' HP'") as "$".
+  iDestruct (raw_bor_iff with "HPP' HP'") as "$".
   iDestruct ("Hκclose" with "Hκ") as "Hinv".
   iMod ("Hclose" with "[HA HI Hinv Halive Hinh Hvs]") as "_".
   { iNext. rewrite {2}/lfts_inv. iExists A, I. iFrame "HA HI".

theories/lifetime/na_borrow.v

@@ -20,11 +20,12 @@ Section na_bor.
   Proof. solve_contractive. Qed.
   Global Instance na_bor_proper κ : Proper ((⊣⊢) ==> (⊣⊢)) (na_bor κ tid N).
   Proof. solve_proper. Qed.
-  Lemma na_bor_iff_proper κ P' :
+
+  Lemma na_bor_iff κ P' :
     ▷ □ (P ↔ P') -∗ &na{κ, tid, N} P -∗ &na{κ, tid, N} P'.
   Proof.
     iIntros "HPP' H". iDestruct "H" as (i) "[HP ?]". iExists i. iFrame.
-    iApply (idx_bor_iff_proper with "HPP' HP").
+    iApply (idx_bor_iff with "HPP' HP").
   Qed.
 
   Global Instance na_bor_persistent κ : PersistentP (&na{κ,tid,N} P) := _.

theories/lifetime/shr_borrow.v

@@ -18,10 +18,11 @@ Section shared_bors.
   Proof. solve_contractive. Qed.
   Global Instance shr_bor_proper : Proper ((⊣⊢) ==> (⊣⊢)) (shr_bor κ).
   Proof. solve_proper. Qed.
-  Lemma shr_bor_iff_proper κ P' : ▷ □ (P ↔ P') -∗ &shr{κ} P -∗ &shr{κ} P'.
+
+  Lemma shr_bor_iff κ P' : ▷ □ (P ↔ P') -∗ &shr{κ} P -∗ &shr{κ} P'.
   Proof.
     iIntros "HPP' H". iDestruct "H" as (i) "[HP ?]". iExists i. iFrame.
-    iApply (idx_bor_iff_proper with "HPP' HP").
+    iApply (idx_bor_iff with "HPP' HP").
   Qed.
 
   Global Instance shr_bor_persistent : PersistentP (&shr{κ} P) := _.

theories/typing/uniq_bor.v

@@ -64,7 +64,7 @@ Section uniq_bor.
     iDestruct (Hty with "[] [] []") as "(_ & #Ho & #Hs)"; [done..|clear Hty].
     iDestruct (Hκ with "[] []") as "#Hκ"; [done..|]. iSplit; iAlways.
     - iIntros (? [|[[]|][]]) "H"; try iDestruct "H" as "[]".
-      iApply (bor_shorten with "Hκ"). iApply bor_iff_proper; last done.
+      iApply (bor_shorten with "Hκ"). iApply bor_iff; last done.
       iSplit; iIntros "!>!# H"; iDestruct "H" as (vl) "[??]";
       iExists vl; iFrame; by iApply "Ho".
     - iIntros (κ ??) "H". iAssert (κ2 ∪ κ ⊑ κ1 ∪ κ)%I as "#Hincl'".
@@ -96,7 +96,7 @@ Section uniq_bor.
     Send ty → Send (uniq_bor κ ty).
   Proof.
     iIntros (Hsend tid1 tid2 [|[[]|][]]) "H"; try iDestruct "H" as "[]".
-    iApply bor_iff_proper; last done. iNext. iAlways. iApply uPred.equiv_iff.
+    iApply bor_iff; last done. iNext. iAlways. iApply uPred.equiv_iff.
     do 3 f_equiv. iSplit; iIntros "."; by iApply Hsend.
   Qed.
 

theories/typing/unsafe/cell.v

@@ -34,7 +34,7 @@ Section cell.
     iDestruct (EQ with "LFT HE HL") as "(% & #Hown & #Hshr)".
     iSplit; [done|iSplit; iIntros "!# * H"].
     - iApply ("Hown" with "H").
-    - iApply na_bor_iff_proper; last done. iSplit; iIntros "!>!# H";
+    - iApply na_bor_iff; last done. iSplit; iIntros "!>!# H";
       iDestruct "H" as (vl) "[??]"; iExists vl; iFrame; by iApply "Hown".
   Qed.
   Lemma cell_mono' E L ty1 ty2 : eqtype E L ty1 ty2 → subtype E L (cell ty1) (cell ty2).

theories/typing/unsafe/refcell.v

@@ -21,7 +21,7 @@ Definition reading_st (q : frac) (κ : lft) : refcell_stR :=
   Some (Cinr (to_agree (κ : leibnizC lft), q, xH)).
 Definition writing_st : refcell_stR := Some (Cinl (Excl ())).
 
-Definition refcellN := nroot .@ "refcell".
+Definition refcellN := lrustN .@ "refcell".
 Definition refcell_invN := refcellN .@ "inv".
 
 Section refcell_inv.
@@ -56,7 +56,7 @@ Section refcell_inv.
     iDestruct (Hty with "LFT HE HL") as "(% & Hown & Hshr)".
     iAssert (□ (&{α} shift_loc l 1 ↦∗: ty_own ty1 tid -∗
                 &{α} shift_loc l 1 ↦∗: ty_own ty2 tid))%I with "[]" as "#Hb".
-    { iIntros "!# H". iApply bor_iff_proper; last done.
+    { iIntros "!# H". iApply bor_iff; last done.
       iSplit; iIntros "!>!#H"; iDestruct "H" as (vl) "[Hf H]"; iExists vl;
       iFrame; by iApply "Hown". }
     iDestruct "H" as (st) "H"; iExists st;
@@ -82,7 +82,7 @@ Section refcell.
          (∃ α γ, κ ⊑ α ∗ &na{α, tid, refcell_invN}(refcell_inv tid l γ α ty))%I |}.
   Next Obligation.
     iIntros (??[|[[]|]]); try iIntros "[]". rewrite ty_size_eq.
-    iIntros "[_ %]!%/=". congruence.
+    iIntros "[_ %] !% /=". congruence.
   Qed.
   Next Obligation.
     iIntros (ty E κ l tid q ?) "#LFT Hb Htok".
@@ -147,7 +147,7 @@ Section refcell.
     - iPureIntro. simpl. congruence.
     - destruct vl as [|[[]|]]; try done. iDestruct "H" as "[$ H]". by iApply "Hown".
     - iDestruct "H" as (a γ) "[Ha H]". iExists a, γ. iFrame.
-      iApply na_bor_iff_proper; last done.
+      iApply na_bor_iff; last done.
       iSplit; iIntros "!>!# H"; by iApply refcell_inv_proper.
   Qed.
   Lemma refcell_mono' E L ty1 ty2 :

theories/typing/unsafe/refmut.v

@@ -89,7 +89,7 @@ Section refmut.
     - iIntros (tid [|[[]|][|[[]|][]]]); try iIntros "[]". iIntros "H".
       iDestruct "H" as (γ β ty') "(Hb & #H⊑ & #Hinv & Hown)".
       iExists γ, β, ty'. iFrame "∗#". iSplit.
-      + iApply bor_iff_proper; last done.
+      + iApply bor_iff; last done.
         iSplit; iIntros "!>!# H"; iDestruct "H" as (vl) "[??]";
           iExists vl; iFrame; by iApply "Ho".
       + by iApply lft_incl_trans.