From b27416cb4299c5b2e1d1507d5e1a1102847efec5 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Fri, 16 Sep 2016 23:55:20 +0200
Subject: [PATCH] Prove [reborrow_shr_perm_incl].
---
perm_incl.v | 11 +++++++++++
1 file changed, 11 insertions(+)
diff --git a/perm_incl.v b/perm_incl.v
index 01824cbd..b30251d4 100644
--- a/perm_incl.v
+++ b/perm_incl.v
@@ -261,6 +261,17 @@ Section props.
- iExists _. eauto.
Qed.
+ Lemma reborrow_shr_perm_incl κ κ' v ty :
+ κ ⊑ κ' ★ v ◁ &shr{κ'}ty ⇒ v ◁ &shr{κ}ty.
+ Proof.
+ iIntros (tid) "[#Hord #Hκ']".
+ destruct v as [[[|l|]|]|];
+ try by (iDestruct "Hκ'" as "[]" || iDestruct "Hκ'" as (l) "[% _]").
+ iDestruct "Hκ'" as (l') "[EQ Hκ']". iDestruct "EQ" as %[=]. subst l'.
+ iVsIntro. iExists _. iSplit. done.
+ by iApply (ty_shr_mono with "Hord Hκ'").
+ Qed.
+
Lemma lftincl_borrowing κ κ' q : borrowing κ ⊤ [κ']{q} (κ ⊑ κ').
Proof.
iIntros (tid) "#Hκ #Hord [Htok #Hκ']".
--
GitLab