From b5a8204a4ef324534398c66ab6e5e9475aa33093 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 21 Sep 2020 00:10:02 +0200
Subject: [PATCH] Environment subtyping rules for copy.
---
theories/logrel/environments.v | 23 +++++++++++++++++++++--
1 file changed, 21 insertions(+), 2 deletions(-)
diff --git a/theories/logrel/environments.v b/theories/logrel/environments.v
index 39cc3a5..4ea545f 100644
--- a/theories/logrel/environments.v
+++ b/theories/logrel/environments.v
@@ -10,9 +10,10 @@ relations on environments are defined:
In addition, some lemmas/rules about these definitions are proved, corresponding
to the syntactic typing rules that are typically found in substructural type
systems. *)
-From actris.logrel Require Export term_types subtyping.
-From iris.proofmode Require Import tactics.
From iris.algebra Require Export list.
+From iris.bi.lib Require Import core.
+From actris.logrel Require Export term_types subtyping_rules.
+From iris.proofmode Require Import tactics.
Inductive env_item Σ := EnvItem {
env_item_name : string;
@@ -205,4 +206,22 @@ Section env.
iDestruct (env_ltyped_app with "Hvs") as "[Hvs1 Hvs2]".
iApply env_ltyped_app. iSplitL "Hvs1"; [by iApply "H"|by iApply "H'"].
Qed.
+ Lemma env_le_copy x A :
+ ⊢ env_le [EnvItem x A] [EnvItem x A; EnvItem x (copy- A)].
+ Proof.
+ iIntros "!>" (vs) "Hvs".
+ iDestruct (env_ltyped_cons with "Hvs") as (v ?) "[HA _]".
+ iAssert (ltty_car (copy- A) v)%lty as "#HAm"; [by iApply coreP_intro|].
+ iApply env_ltyped_cons. iExists _; iSplit; [done|]. iFrame "HA".
+ iApply env_ltyped_cons. iExists _; iSplit; [done|]. iFrame "HAm".
+ iApply env_ltyped_nil.
+ Qed.
+ Lemma env_le_copyable x A :
+ lty_copyable A -∗
+ env_le [EnvItem x A] [EnvItem x A; EnvItem x A].
+ Proof.
+ iIntros "#H". iApply env_le_trans; [iApply env_le_copy|].
+ iApply env_le_cons; [iApply lty_le_refl|].
+ iApply env_le_cons; [by iApply lty_le_copy_inv_elim_copyable|iApply env_le_nil].
+ Qed.
End env.
--
GitLab