From 4605684ccc60890d4ca0a49becdea314fafe4056 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jjourdan@mpi-sws.org>
Date: Tue, 25 Oct 2016 16:58:01 +0200
Subject: [PATCH] Make lft_extract monotone, so that own_uniq_borrowing can be
proved.
---
lifetime.v | 3 ++-
perm_incl.v | 6 ++----
2 files changed, 4 insertions(+), 5 deletions(-)
diff --git a/lifetime.v b/lifetime.v
index a4b579ef..ae6e905a 100644
--- a/lifetime.v
+++ b/lifetime.v
@@ -61,7 +61,8 @@ Section lft.
Global Existing Instance lft_incl_persistent.
Axiom lft_extract_proper : ∀ κ, Proper ((⊣⊢) ==> (⊣⊢)) (lft_extract κ).
- Global Existing Instance lft_extract_proper.
+ Axiom lft_extract_mono : ∀ κ, Proper ((⊢) ==> (⊢)) (lft_extract κ).
+ Global Existing Instances lft_extract_proper lft_extract_mono.
Axiom lft_borrow_proper : ∀ κ, Proper ((⊣⊢) ==> (⊣⊢)) (lft_borrow κ).
Global Existing Instance lft_borrow_proper.
diff --git a/perm_incl.v b/perm_incl.v
index 83e7be59..3f46d966 100644
--- a/perm_incl.v
+++ b/perm_incl.v
@@ -238,10 +238,8 @@ Section props.
- iExists _. eauto. }
iVs (lft_borrow_create with "Hκ Hf") as "[_ Hf]". done.
iVs (lft_extract_combine with "[-]"). done. by iFrame.
- (* FIXME : extraction needs to be monotone in some sense to
- remove the later. *)
- admit.
- Admitted.
+ iVsIntro. iApply lft_extract_mono; last done. by iDestruct 1 as "[$$]".
+ Qed.
Lemma reborrow_uniq_borrowing κ κ' v ty :
borrowing κ (κ ⊑ κ') (v ◁ &uniq{κ'}ty) (v ◁ &uniq{κ}ty).
--
GitLab