From eced4fb8f45cb4529d29b3d299e813e1133bfed2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Dani=C3=ABl=20Louwrink?= <daniel.louwrink@gmail.com>
Date: Thu, 23 Apr 2020 21:25:51 +0200
Subject: [PATCH] extract minimal coreP example
---
theories/logrel/copying.v | 12 +++++++++++-
1 file changed, 11 insertions(+), 1 deletion(-)
diff --git a/theories/logrel/copying.v b/theories/logrel/copying.v
index a7655fd..83e0e18 100644
--- a/theories/logrel/copying.v
+++ b/theories/logrel/copying.v
@@ -23,11 +23,21 @@ Section copying.
⊢ copy A <: A.
Proof. by iIntros (v) "!> #H". Qed.
+ Lemma coreP_desired_lemma (P : iProp Σ) :
+ □ (P -∗ □ P) -∗ coreP P -∗ P.
+ Proof.
+ iIntros "HP Hcore".
+ Admitted.
+
Lemma lty_le_copy_minus A :
copyable A -∗ copy- A <: A.
Proof.
iIntros "#HA". iIntros (v) "!> #Hv".
- Admitted.
+ iSpecialize ("HA" $! v).
+ iApply coreP_desired_lemma.
+ - iModIntro. iApply "HA".
+ - iApply "Hv".
+ Qed.
(* Copyability of types *)
Lemma lty_unit_copyable :
--
GitLab