Misc.

theories/lifetime/creation.v

@@ -63,7 +63,8 @@ Proof.
       rewrite /lft_inh. iExists ∅. rewrite to_gmap_empty.
       iSplitL; [|iApply box_alloc]. rewrite /own_inh. iExists γs. by iSplit.
     - rewrite lft_inv_alive_unfold. iExists True%I, True%I. iSplitL "Hbor".
-      { rewrite /lft_bor_alive. iExists ∅. rewrite !fmap_empty big_sepM_empty.
+      { rewrite /lft_bor_alive. iExists ∅.
+        rewrite /to_borUR !fmap_empty big_sepM_empty.
         iSplitR; [iApply box_alloc|]. iSplit=>//.
         rewrite /own_bor. iExists γs. by iFrame. }
       rewrite lft_vs_unfold. iSplitR "Hinh".
@@ -79,8 +80,8 @@ Proof.
       by rewrite lookup_fmap HAΛ. }
     iModIntro. iExists (<[Λ:=false]>A), (<[κ:=γs]> I).
     iSplit; first rewrite lookup_insert; eauto.
-    rewrite /own_ilft_auth /own_alft_auth !fmap_insert. iFrame "HA HI".
-    rewrite dom_insert_L big_sepS_insert ?not_elem_of_dom //.
+    rewrite /own_ilft_auth /own_alft_auth /to_ilftUR /to_alftUR !fmap_insert.
+    iFrame "HA HI". rewrite dom_insert_L big_sepS_insert ?not_elem_of_dom //.
     iSplitR "HA'".
     { rewrite /lft_inv. iNext. iRight. iSplit.
       { by iDestruct "Hdeadandalive" as "[? _]". }
@@ -92,7 +93,7 @@ Proof.
     + iRight. iFrame "HA". iPureIntro. by apply lft_dead_in_insert.
   - iModIntro. iExists A, (<[κ:=γs]> I).
     iSplit; first rewrite lookup_insert; eauto.
-    iSplitL "HI"; first by rewrite /own_ilft_auth fmap_insert.
+    iSplitL "HI"; first by rewrite /own_ilft_auth /to_ilftUR fmap_insert.
     rewrite dom_insert_L big_sepS_insert ?not_elem_of_dom //.
     iFrame "HA HA'". iNext. rewrite /lft_inv. destruct Haliveordead.
     + iLeft. by iDestruct "Hdeadandalive" as "[_ $]".
@@ -230,7 +231,7 @@ Proof.
     by rewrite lookup_fmap HΛ. }
   iMod ("Hclose" with "[HA HI Hinv]") as "_".
   { iNext. rewrite /lfts_inv /own_alft_auth.
-    iExists (<[Λ:=true]>A), I; rewrite fmap_insert; iFrame.
+    iExists (<[Λ:=true]>A), I. rewrite /to_alftUR fmap_insert; iFrame.
     iApply (@big_sepS_impl with "[$Hinv]").
     iAlways. rewrite /lft_inv. iIntros (κ ?) "[[Hκ %]|[Hκ %]]".
     - iLeft. iFrame "Hκ". iPureIntro. by apply lft_alive_in_insert.
@@ -268,7 +269,7 @@ Proof.
   { iModIntro. rewrite /lft_dead. iExists Λ.
     rewrite elem_of_singleton. auto. }
   iNext. iExists (<[Λ:=false]>A), I.
-  rewrite /own_alft_auth fmap_insert. iFrame "HA HI".
+  rewrite /own_alft_auth /to_alftUR fmap_insert. iFrame "HA HI".
   rewrite HI !big_sepS_union //.
   iSplitL "HinvK HinvD"; first iSplitL "HinvK".
   - iApply (@big_sepS_impl with "[$HinvK]"); iIntros "!#".

theories/lifetime/definitions.v

@@ -28,9 +28,6 @@ Definition lft_stateR := csumR fracR unitR.
 Definition to_lft_stateR (b : bool) : lft_stateR :=
   if b then Cinl 1%Qp else Cinr ().
 
-Instance to_lft_stateR_inj : Inj eq eq to_lft_stateR.
-Proof. by intros [] []. Qed.
-
 Record lft_names := LftNames {
   bor_name : gname;
   cnt_name : gname;
@@ -39,16 +36,26 @@ Record lft_names := LftNames {
 Instance lft_names_eq_dec : EqDecision lft_names.
 Proof. solve_decision. Defined.
 
+Definition alftUR := gmapUR atomic_lft lft_stateR.
+Definition to_alftUR : gmap atomic_lft bool → alftUR := fmap to_lft_stateR. 
+
+Definition ilftUR := gmapUR lft (dec_agreeR lft_names).
+Definition to_ilftUR : gmap lft lft_names → ilftUR := fmap DecAgree.
+
+Definition borUR := gmapUR slice_name (prodR fracR (dec_agreeR bor_state)).
+Definition to_borUR : gmap slice_name bor_state → borUR := fmap ((1%Qp,) ∘ DecAgree).
+
+Definition inhUR := gset_disjUR slice_name.
+
 Class lftG Σ := LftG {
   lft_box :> boxG Σ;
-  alft_inG :> inG Σ (authR (gmapUR atomic_lft lft_stateR));
+  alft_inG :> inG Σ (authR alftUR);
   alft_name : gname;
-  ilft_inG :> inG Σ (authR (gmapUR lft (dec_agreeR lft_names)));
+  ilft_inG :> inG Σ (authR ilftUR);
   ilft_name : gname;
-  lft_bor_box :>
-    inG Σ (authR (gmapUR slice_name (prodR fracR (dec_agreeR bor_state))));
+  lft_bor_box :> inG Σ (authR borUR);
   lft_cnt_inG :> inG Σ (authR natUR);
-  lft_inh_box :> inG Σ (authR (gset_disjUR slice_name));
+  lft_inh_box :> inG Σ (authR inhUR);
 }.
 
 Section defs.
@@ -61,9 +68,9 @@ Section defs.
     (∃ Λ, ⌜Λ ∈ κ⌝ ∗ own alft_name (◯ {[ Λ := Cinr () ]}))%I.
 
   Definition own_alft_auth (A : gmap atomic_lft bool) : iProp Σ :=
-    own alft_name (● (to_lft_stateR <$> A)).
+    own alft_name (● to_alftUR A).
   Definition own_ilft_auth (I : gmap lft lft_names) : iProp Σ :=
-    own ilft_name (● (DecAgree <$> I)).
+    own ilft_name (● to_ilftUR I).
 
   Definition own_bor (κ : lft)
       (x : auth (gmap slice_name (frac * dec_agree bor_state))) : iProp Σ :=
@@ -91,7 +98,7 @@ Section defs.
   Definition lft_bor_alive (κ : lft) (Pi : iProp Σ) : iProp Σ :=
     (∃ B : gmap slice_name bor_state,
       box borN (bor_filled <$> B) Pi ∗
-      own_bor κ (● ((1%Qp,) ∘ DecAgree <$> B)) ∗
+      own_bor κ (● to_borUR B) ∗
       [∗ map] s ∈ B, bor_cnt κ s)%I.
 
   Definition lft_bor_dead (κ : lft) : iProp Σ :=
@@ -140,9 +147,9 @@ Section defs.
       lft_inh κ true Pi)%I.
 
   Definition lft_alive_in (A : gmap atomic_lft bool) (κ : lft) : Prop :=
-    ∀ Λ:atomic_lft, Λ ∈ κ → A !! Λ = Some true.
+    ∀ Λ : atomic_lft, Λ ∈ κ → A !! Λ = Some true.
   Definition lft_dead_in (A : gmap atomic_lft bool) (κ : lft) : Prop :=
-    ∃ Λ:atomic_lft, Λ ∈ κ ∧ A !! Λ = Some false.
+    ∃ Λ : atomic_lft, Λ ∈ κ ∧ A !! Λ = Some false.
 
   Definition lft_inv (A : gmap atomic_lft bool) (κ : lft) : iProp Σ :=
     (lft_inv_alive κ ∗ ⌜lft_alive_in A κ⌝ ∨

theories/lifetime/derived.v

@@ -93,8 +93,8 @@ Lemma reborrow E P κ κ' :
   ↑lftN ⊆ E →
   lft_ctx ⊢ κ' ⊑ κ -∗ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗  &{κ}P).
 Proof.
-  iIntros (?) "#LFT #H⊑ HP". iMod (bor_reborrow' with "LFT HP") as "[Hκ' H∋]".
-    done. (* by exists κ'.
+  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.

theories/lifetime/primitive.v

 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.proofmode Require Import tactics.
 Import uPred.
 
@@ -8,6 +9,14 @@ Section primitive.
 Context `{invG Σ, lftG Σ}.
 Implicit Types κ : lft.
 
+Lemma to_borUR_included (B : gmap slice_name bor_state) i s :
+  {[i := (1%Qp, DecAgree s)]} ≼ to_borUR B → B !! i = Some s.
+Proof.
+  rewrite singleton_included=> -[qs [/leibniz_equiv_iff]].
+  rewrite lookup_fmap fmap_Some=> -[s' [? ->]].
+  by move=> /Some_pair_included [_] /Some_included_total /DecAgree_included=>->.
+Qed.
+
 (** Ownership *)
 Lemma own_ilft_auth_agree (I : gmap lft lft_names) κ γs :
   own_ilft_auth I ⊢
@@ -15,19 +24,18 @@ Lemma own_ilft_auth_agree (I : gmap lft lft_names) κ γs :
 Proof.
   iIntros "HI Hκ". iDestruct (own_valid_2 with "HI Hκ")
     as %[[? [??]]%singleton_included _]%auth_valid_discrete_2.
-  simplify_map_eq; simplify_option_eq; eauto.
+  unfold to_ilftUR in *. simplify_map_eq; simplify_option_eq; eauto.
 Qed.
 
 Lemma own_alft_auth_agree (A : gmap atomic_lft bool) Λ b :
   own_alft_auth A ⊢
     own alft_name (◯ {[Λ := to_lft_stateR b]}) -∗ ⌜A !! Λ = Some b⌝.
 Proof.
-  iIntros "HA HΛ". iDestruct (own_valid_2 with "HA HΛ")
-    as %[[? [Heq Hle]]%singleton_included _]%auth_valid_discrete_2.
-  simplify_map_eq. destruct (A!!Λ) as [b'|]; last done. inversion Heq. subst x.
-  apply Some_included in Hle. destruct Hle as [->%leibniz_equiv%(inj _)|Hle]. done.
-  apply csum_included in Hle.
-  destruct Hle as [Hle|[(?&?&?&?&?)|(?&?&?&?&?)]], b, b'; try done.
+  iIntros "HA HΛ".
+  iDestruct (own_valid_2 with "HA HΛ") as %[HA _]%auth_valid_discrete_2.
+  iPureIntro. move: HA=> /singleton_included [qs [/leibniz_equiv_iff]].
+  rewrite lookup_fmap fmap_Some=> -[b' [? ->]] /Some_included.
+  move=> [/leibniz_equiv_iff|/csum_included]; destruct b, b'; naive_solver.
 Qed.
 
 Lemma own_bor_auth I κ x : own_ilft_auth I ⊢ own_bor κ x -∗ ⌜is_Some (I !! κ)⌝.
@@ -222,6 +230,7 @@ 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.
 
+(** Lifetime inclusion *)
 Lemma lft_le_incl κ κ' : κ' ⊆ κ → True ⊢ κ ⊑ κ'.
 Proof.
   iIntros (->%gmultiset_union_difference) "!#". iSplitR.
@@ -243,5 +252,4 @@ Proof.
     iMod ("Hclose'" with "Hκ''") as "Hκ'". by iApply "Hclose".
   - iIntros "H†". iMod ("H2†" with "H†"). by iApply "H1†".
 Qed.
-
 End primitive.

theories/lifetime/rebor.v

@@ -43,15 +43,10 @@ Proof.
   rewrite lft_inv_alive_unfold;
     iDestruct "HAκ" as (Pb' Pi') "(Hbor'&Hvs'&Hinh')".
   rewrite {2}/lft_bor_alive; iDestruct "Hbor'" as (B) "(Hbox & >HκB & HB)".
-  iDestruct (own_bor_valid_2 with "HκB Hraw") as %[HB _]%auth_valid_discrete_2.
-  move: HB=> /singleton_included=> -[qs].
-  rewrite leibniz_equiv_iff lookup_fmap fmap_Some=> -[[s [? ->]] /Some_pair_included [??]].
-SearchAbout Some included.
-  apply singleton_included in HB as (?&?&?).
-SearchAbout 
-simpl in *.
+  iDestruct (own_bor_valid_2 with "HκB Hraw")
+    as %[HB%to_borUR_included _]%auth_valid_discrete_2.
   
-  Check big_sepS_delete.
+
 Admitted.
 
 Lemma bor_rebor' E κ κ' P :
@@ -61,4 +56,5 @@ Proof. Admitted.
 Lemma bor_unnest E κ κ' P :
   ↑lftN ⊆ E →
   lft_ctx ⊢ &{κ'} &{κ} P ={E}▷=∗ &{κ ∪ κ'} P.
-Proof. Admitted.
+Proof. Admitted.
\ No newline at end of file
+End rebor.
\ No newline at end of file