From bd38fde217e4a3ea27f114821d39beb328cff090 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Fri, 25 Nov 2016 23:31:42 +0100
Subject: [PATCH] Ported shared borrows.

---
 _CoqProject                     |  1 +
 theories/lifetime/creation.v    |  2 +-
 theories/lifetime/definitions.v |  5 +--
 theories/lifetime/derived.v     | 12 -------
 theories/lifetime/primitive.v   | 41 +++++++++++++++---------
 theories/lifetime/rebor.v       | 14 +++++++-
 theories/lifetime/shr_borrow.v  | 56 ++++++++++++++++++++++++++++++++
 theories/shr_borrow.v           | 57 ---------------------------------
 8 files changed, 99 insertions(+), 89 deletions(-)
 create mode 100644 theories/lifetime/shr_borrow.v
 delete mode 100644 theories/shr_borrow.v

diff --git a/_CoqProject b/_CoqProject
index c6465301..7c8c4d67 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -6,3 +6,4 @@ theories/lifetime/creation.v
 theories/lifetime/primitive.v
 theories/lifetime/todo.v
 theories/lifetime/borrow.v
+theories/lifetime/shr_borrow.v
diff --git a/theories/lifetime/creation.v b/theories/lifetime/creation.v
index 8ea552ff..0b9e20bf 100644
--- a/theories/lifetime/creation.v
+++ b/theories/lifetime/creation.v
@@ -117,7 +117,7 @@ Proof.
   { iIntros (i s HBI).
     iDestruct (big_sepM_lookup _ B with "HB") as "HB"=> //.
     destruct s as [|q|κ']; rewrite /bor_cnt //.
-    { iDestruct (lft_tok_dead_own with "HB Hκ") as "[]". }
+    { iDestruct (lft_tok_dead with "HB Hκ") as "[]". }
     iDestruct "HB" as "[% Hcnt]".
     iDestruct (own_cnt_auth with "HI Hcnt") as %?.
     iDestruct (@big_sepS_elem_of with "Hdead") as "Hdead"; first by eauto.
diff --git a/theories/lifetime/definitions.v b/theories/lifetime/definitions.v
index e8bc268b..fb3a87dc 100644
--- a/theories/lifetime/definitions.v
+++ b/theories/lifetime/definitions.v
@@ -285,9 +285,10 @@ Proof. solve_proper. Qed.
 Global Instance bor_proper κ : Proper ((≡) ==> (≡)) (bor κ).
 Proof. apply (ne_proper _). Qed.
 
-(*** PersistentP and TimelessP instances  *)
+(*** PersistentP and TimelessP and instances  *)
 Global Instance lft_tok_timeless q κ : TimelessP q.[κ].
 Proof. rewrite /lft_tok. apply _. Qed.
+
 Global Instance lft_dead_persistent κ : PersistentP [†κ].
 Proof. rewrite /lft_dead. apply _. Qed.
 Global Instance lft_dead_timeless κ : PersistentP [†κ].
@@ -298,7 +299,7 @@ Proof. rewrite /lft_incl. apply _. Qed.
 
 Global Instance idx_bor_persistent κ i P : PersistentP (&{κ,i} P).
 Proof. rewrite /idx_bor. apply _. Qed.
-Global Instance idx_borrow_own_timeless q i : TimelessP (idx_bor_own q i).
+Global Instance idx_bor_own_timeless q i : TimelessP (idx_bor_own q i).
 Proof. rewrite /idx_bor_own. apply _. Qed.
 
 Global Instance lft_ctx_persistent : PersistentP lft_ctx.
diff --git a/theories/lifetime/derived.v b/theories/lifetime/derived.v
index 9e34bc60..251884ae 100644
--- a/theories/lifetime/derived.v
+++ b/theories/lifetime/derived.v
@@ -66,16 +66,4 @@ Proof.
   - iIntros "Hst". by iDestruct (lft_dead_static with "Hst") as "[]".
 Qed.
 
-Lemma reborrow E P κ κ' :
-  ↑lftN ⊆ E →
-  lft_ctx -∗ κ' ⊑ κ -∗ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗  &{κ}P).
-Proof.
-  iIntros (?) "#LFT #H⊑ HP". (* iMod (bor_rebor' with "LFT HP") as "[Hκ' H∋]".
-    done. by exists κ'.
-  iDestruct (borrow_shorten with "[H⊑] Hκ'") as "$".
-  { iApply lft_incl_lb. iSplit. done. iApply lft_incl_refl. }
-  iIntros "!>Hκ'". iApply ("H∋" with "[Hκ']"). iApply lft_dead_or. auto.
-Qed.
-*)
-Admitted.
 End derived.
diff --git a/theories/lifetime/primitive.v b/theories/lifetime/primitive.v
index ec30c544..33e0e6f3 100644
--- a/theories/lifetime/primitive.v
+++ b/theories/lifetime/primitive.v
@@ -1,7 +1,7 @@
 From lrust.lifetime Require Export definitions.
 From iris.algebra Require Import csum auth frac gmap dec_agree gset.
 From iris.base_logic Require Import big_op.
-From iris.base_logic.lib Require Import boxes.
+From iris.base_logic.lib Require Import boxes fractional.
 From iris.proofmode Require Import tactics.
 Import uPred.
 
@@ -217,16 +217,7 @@ Proof.
   rewrite -sep_or_r -pure_or. do 2 f_equiv. set_solver.
 Qed.
 
-Lemma lft_tok_frac_op κ q q' : (q + q').[κ] ⊣⊢ q.[κ] ∗ q'.[κ].
-Proof.
-  rewrite /lft_tok -big_sepMS_sepMS. apply big_sepMS_proper=> Λ _.
-  by rewrite -own_op -auth_frag_op op_singleton.
-Qed.
-
-Lemma lft_tok_split κ q : q.[κ] ⊣⊢ (q/2).[κ] ∗ (q/2).[κ].
-Proof. by rewrite -lft_tok_frac_op Qp_div_2. Qed.
-
-Lemma lft_tok_dead_own q κ : q.[κ] -∗ [† κ] -∗ False.
+Lemma lft_tok_dead q κ : q.[κ] -∗ [† κ] -∗ False.
 Proof.
   rewrite /lft_tok /lft_dead. iIntros "H"; iDestruct 1 as (Λ') "[% H']".
   iDestruct (big_sepMS_elem_of _ _ Λ' with "H") as "H"=> //.
@@ -240,6 +231,24 @@ Proof. by rewrite /lft_tok big_sepMS_empty. Qed.
 Lemma lft_dead_static : [† static] -∗ False.
 Proof. rewrite /lft_dead. iDestruct 1 as (Λ) "[% H']". set_solver. Qed.
 
+(* Fractional and AsFractional instances *)
+Global Instance lft_tok_fractional κ : Fractional (λ q, q.[κ])%I.
+Proof.
+  intros p q. rewrite /lft_tok -big_sepMS_sepMS. apply big_sepMS_proper.
+  intros Λ ?. rewrite -Cinl_op -op_singleton auth_frag_op own_op //.
+Qed.
+Global Instance lft_tok_as_fractional κ q :
+  AsFractional q.[κ] (λ q, q.[κ])%I q.
+Proof. done. Qed.
+Global Instance idx_bor_own_fractional i : Fractional (λ q, idx_bor_own q i)%I.
+Proof.
+  intros p q. rewrite /idx_bor_own -own_bor_op /own_bor. f_equiv=>?.
+  by rewrite -auth_frag_op op_singleton.
+Qed.
+Global Instance idx_bor_own_as_fractional i q :
+  AsFractional (idx_bor_own q i) (λ q, idx_bor_own q i)%I q.
+Proof. done. Qed.
+
 (** Lifetime inclusion *)
 Lemma lft_le_incl κ κ' : κ' ⊆ κ → (κ ⊑ κ')%I.
 Proof.
@@ -264,18 +273,18 @@ Proof.
 Qed.
 
 Lemma lft_incl_glb κ κ' κ'' : κ ⊑ κ' -∗ κ ⊑ κ'' -∗ κ ⊑ κ' ∪ κ''.
-Proof. (*
-  iIntros "[#[H1 H1†] #[H2 H2†]]!#". iSplitR.
+Proof.
+  unfold lft_incl. iIntros "#[H1 H1†] #[H2 H2†]!#". iSplitR.
   - iIntros (q) "[Hκ'1 Hκ'2]".
     iMod ("H1" with "*Hκ'1") as (q') "[Hκ' Hclose']".
     iMod ("H2" with "*Hκ'2") as (q'') "[Hκ'' Hclose'']".
     destruct (Qp_lower_bound q' q'') as (qq & q'0 & q''0 & -> & ->).
-    iExists qq. rewrite -lft_tok_op !lft_tok_frac_op.
+    iExists qq. rewrite -lft_tok_op.
     iDestruct "Hκ'" as "[$ Hκ']". iDestruct "Hκ''" as "[$ Hκ'']".
     iIntros "!>[Hκ'0 Hκ''0]".
     iMod ("Hclose'" with "[$Hκ' $Hκ'0]") as "$".
-    by iMod ("Hclose''" with "[$Hκ'' $Hκ''0]") as "$".
+    iApply "Hclose''". iFrame.
   - rewrite -lft_dead_or. iIntros "[H†|H†]". by iApply "H1†". by iApply "H2†".
-Qed. *) Admitted.
+Qed.
 
 End primitive.
diff --git a/theories/lifetime/rebor.v b/theories/lifetime/rebor.v
index c9199c15..7fe8f7e7 100644
--- a/theories/lifetime/rebor.v
+++ b/theories/lifetime/rebor.v
@@ -119,8 +119,20 @@ Lemma bor_rebor' E κ κ' P :
   ↑lftN ⊆ E → κ ⊆ κ' →
   lft_ctx -∗ &{κ} P ={E}=∗ &{κ'} P ∗ ([†κ'] ={E}=∗ &{κ} P).
 Proof. Admitted.
+Lemma rebor E P κ κ' :
+  ↑lftN ⊆ E →
+  lft_ctx -∗ κ' ⊑ κ -∗ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗  &{κ}P).
+Proof.
+  iIntros (?) "#LFT #H⊑ HP". (* iMod (bor_rebor' with "LFT HP") as "[Hκ' H∋]".
+    done. by exists κ'.
+  iDestruct (borrow_shorten with "[H⊑] Hκ'") as "$".
+  { iApply lft_incl_lb. iSplit. done. iApply lft_incl_refl. }
+  iIntros "!>Hκ'". iApply ("H∋" with "[Hκ']"). iApply lft_dead_or. auto.
+Qed.
+*)
+Admitted.
 Lemma bor_unnest E κ κ' P :
   ↑lftN ⊆ E →
-  lft_ctx -∗ &{κ'} &{κ} P ={E}▷=∗ &{κ ∪ κ'} P.
+  lft_ctx -∗ &{κ'} &{κ} P ={E, E∖↑lftN}▷=∗ &{κ ∪ κ'} P.
 Proof. Admitted.
 End rebor.
diff --git a/theories/lifetime/shr_borrow.v b/theories/lifetime/shr_borrow.v
new file mode 100644
index 00000000..2db70d36
--- /dev/null
+++ b/theories/lifetime/shr_borrow.v
@@ -0,0 +1,56 @@
+From iris.algebra Require Import gmap auth frac.
+From iris.proofmode Require Import tactics.
+From lrust.lifetime Require Export derived.
+
+(** Shared bors  *)
+Definition shr_bor `{invG Σ, lftG Σ} κ (P : iProp Σ) :=
+  (∃ i, idx_bor κ i P ∗ inv lftN (∃ q, idx_bor_own q i))%I.
+Notation "&shr{ κ } P" := (shr_bor κ P)
+  (format "&shr{ κ } P", at level 20, right associativity) : uPred_scope.
+
+Section shared_bors.
+  Context `{invG Σ, lftG Σ} (P : iProp Σ).
+
+  Global Instance shr_bor_proper :
+    Proper ((⊣⊢) ==> (⊣⊢)) (shr_bor κ).
+  Proof. solve_proper. Qed.
+  Global Instance shr_bor_persistent : PersistentP (&shr{κ} P) := _.
+
+  Lemma bor_share E κ : ↑lftN ⊆ E → &{κ}P ={E}=∗ &shr{κ}P.
+  Proof.
+    iIntros (?) "HP". rewrite bor_unfold_idx. iDestruct "HP" as (i) "(#?&Hown)".
+    iExists i. iFrame "#". iApply inv_alloc. auto.
+  Qed.
+
+  Lemma shr_bor_acc E κ :
+    ↑lftN ⊆ E →
+    lft_ctx -∗ &shr{κ}P ={E,E∖↑lftN}=∗ ▷P ∗ (▷P ={E∖↑lftN,E}=∗ True) ∨
+               [†κ] ∗ |={E∖↑lftN,E}=> True.
+  Proof.
+    iIntros (?) "#LFT #HP". iDestruct "HP" as (i) "(#Hidx&#Hinv)".
+    iInv lftN as (q') ">[Hq'0 Hq'1]" "Hclose".
+    iMod ("Hclose" with "[Hq'1]") as "_". by eauto.
+    iMod (idx_bor_atomic_acc with "LFT Hidx Hq'0") as "[[HP Hclose]|[H† Hclose]]". done.
+    - iLeft. iFrame. iIntros "!>HP". by iMod ("Hclose" with "HP").
+    - iRight. iFrame. iIntros "!>". by iMod "Hclose".
+  Qed.
+
+  Lemma shr_bor_acc_tok E q κ :
+    ↑lftN ⊆ E →
+    lft_ctx -∗ &shr{κ}P -∗ q.[κ] ={E,E∖↑lftN}=∗ ▷P ∗ (▷P ={E∖↑lftN,E}=∗ q.[κ]).
+  Proof.
+    iIntros (?) "#LFT #Hshr Hκ".
+    iMod (shr_bor_acc with "LFT Hshr") as "[[$ Hclose]|[H† _]]". done.
+    - iIntros "!>HP". by iMod ("Hclose" with "HP").
+    - iDestruct (lft_tok_dead with "Hκ H†") as "[]".
+  Qed.
+
+  Lemma shr_bor_shorten κ κ': κ ⊑ κ' -∗ &shr{κ'}P -∗ &shr{κ}P.
+  Proof.
+    iIntros "#H⊑ H". iDestruct "H" as (i) "[??]". iExists i. iFrame.
+      by iApply (idx_bor_shorten with "H⊑").
+  Qed.
+
+End shared_bors.
+
+Typeclasses Opaque shr_bor.
diff --git a/theories/shr_borrow.v b/theories/shr_borrow.v
deleted file mode 100644
index 5987de8d..00000000
--- a/theories/shr_borrow.v
+++ /dev/null
@@ -1,57 +0,0 @@
-From iris.algebra Require Import gmap auth frac.
-From iris.proofmode Require Import tactics.
-From lrust Require Export lifetime.
-
-(** Shared borrows  *)
-Definition shr_borrow `{invG Σ, lifetimeG Σ} κ (P : iProp Σ) :=
-  (∃ i, idx_borrow κ i P ∗ inv lftN (∃ q, idx_borrow_own q i))%I.
-Notation "&shr{ κ } P" := (shr_borrow κ P)
-  (format "&shr{ κ } P", at level 20, right associativity) : uPred_scope.
-
-Section shared_borrows.
-  Context `{invG Σ, lifetimeG Σ} (P : iProp Σ).
-
-  Global Instance shr_borrow_proper :
-    Proper ((⊣⊢) ==> (⊣⊢)) (shr_borrow κ).
-  Proof. solve_proper. Qed.
-  Global Instance shr_borrow_persistent : PersistentP (&shr{κ} P) := _.
-
-  Lemma borrow_share E κ : ↑lftN ⊆ E → &{κ}P ={E}=∗ &shr{κ}P.
-  Proof.
-    iIntros (?) "HP". unfold borrow. iDestruct "HP" as (i) "(#?&Hown)".
-    iExists i. iFrame "#". iApply inv_alloc. auto.
-  Qed.
-
-  Lemma shr_borrow_acc E κ :
-    ↑lftN ⊆ E →
-    lft_ctx -∗ &shr{κ}P ={E,E∖↑lftN}=∗ ▷P ∗ (▷P ={E∖↑lftN,E}=∗ True) ∨
-               [†κ] ∗ |={E∖↑lftN,E}=> True.
-  Proof.
-    iIntros (?) "#LFT #HP". iDestruct "HP" as (i) "(#Hidx&#Hinv)".
-    iInv lftN as (q') ">Hq'" "Hclose".
-    rewrite -(Qp_div_2 q') /idx_borrow_own -op_singleton auth_frag_op own_op.
-    iDestruct "Hq'" as "[Hq'0 Hq'1]". iMod ("Hclose" with "[Hq'1]") as "_". by eauto.
-    iMod (idx_borrow_atomic_acc with "LFT Hidx Hq'0") as "[[HP Hclose]|[H† Hclose]]". done.
-    - iLeft. iFrame. iIntros "!>HP". by iMod ("Hclose" with "HP").
-    - iRight. iFrame. iIntros "!>". by iMod "Hclose".
-  Qed.
-
-  Lemma shr_borrow_acc_tok E q κ :
-    ↑lftN ⊆ E →
-    lft_ctx -∗ &shr{κ}P -∗ q.[κ] ={E,E∖↑lftN}=∗ ▷P ∗ (▷P ={E∖↑lftN,E}=∗ q.[κ]).
-  Proof.
-    iIntros (?) "#LFT #Hshr Hκ".
-    iMod (shr_borrow_acc with "LFT Hshr") as "[[$ Hclose]|[H† _]]". done.
-    - iIntros "!>HP". by iMod ("Hclose" with "HP").
-    - iDestruct (lft_own_dead with "Hκ H†") as "[]".
-  Qed.
-
-  Lemma shr_borrow_shorten κ κ': κ ⊑ κ' -∗ &shr{κ'}P -∗ &shr{κ}P.
-  Proof.
-    iIntros "#H⊑ H". iDestruct "H" as (i) "[??]". iExists i. iFrame.
-      by iApply (idx_borrow_shorten with "H⊑").
-  Qed.
-
-End shared_borrows.
-
-Typeclasses Opaque shr_borrow.
-- 
GitLab