From a57aae68f78cb3a4b5f8be8ea0554fa0c778b4c8 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 12 Mar 2020 14:18:00 +0100
Subject: [PATCH] derive bor_iff from idx_bor_iff

---
 theories/lifetime/lifetime.v     | 7 +++++++
 theories/lifetime/lifetime_sig.v | 1 -
 2 files changed, 7 insertions(+), 1 deletion(-)

diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index 4a2eb931..9d9c54da 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -93,6 +93,13 @@ Proof.
   iMod (bor_exists (A:=bool) with "LFT H") as ([]) "H"; auto.
 Qed.
 
+Lemma bor_iff κ P P' : ▷ □ (P ↔ P') -∗ &{κ}P -∗ &{κ}P'.
+Proof.
+  rewrite !bor_unfold_idx. iIntros "#HP Hbor".
+  iDestruct "Hbor" as (i) "[Hbor Htok]". iExists i. iFrame "Htok".
+  iApply idx_bor_iff; done.
+Qed.
+
 Lemma bor_iff_proper κ P P': ▷ □ (P ↔ P') -∗ □ (&{κ}P ↔ &{κ}P').
 Proof.
   iIntros "#HP !#". iSplit; iIntros "?"; iApply bor_iff; try done.
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 10a29398..72b263c8 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -99,7 +99,6 @@ 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,
-- 
GitLab