From e11f52aa26ac3ef86456151877ae2b683c4ac63d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 5 Jun 2015 10:17:36 +0200
Subject: [PATCH] show that owning a ghost-unit can be boxed
---
iris_core.v | 10 ++++++++++
1 file changed, 10 insertions(+)
diff --git a/iris_core.v b/iris_core.v
index 89aa27784..60bde6705 100644
--- a/iris_core.v
+++ b/iris_core.v
@@ -950,6 +950,16 @@ Module Type IRIS_CORE (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
rewrite ->Hg1, Hg2. apply pordR. exact Heq.
Qed.
+ Lemma ownL_box (g: RL.res) :
+ ownL (1 g) == â–¡ownL (1 g).
+ Proof.
+ apply pord_antisym; last exact:box_elim.
+ move=>w n. destruct n; first (intro; exact:bpred).
+ case=>[gr Heq]. simpl. destruct (ra_unit_mono (1 g) gr) as [g' Heq'].
+ simpl in Heq. rewrite -Heq. exists g'.
+ rewrite (comm gr) Heq' ra_unit_idem comm. reflexivity.
+ Qed.
+
Lemma ownL_something:
valid(xist ownL).
Proof.
--
GitLab