From 99c799ee98016ee9baf9f8034aabf93b1586721f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 30 Oct 2015 18:02:01 +0100
Subject: [PATCH] also show htBind in ectx_lang
---
ectx_lang.v | 18 ++++++++++++++++--
1 file changed, 16 insertions(+), 2 deletions(-)
diff --git a/ectx_lang.v b/ectx_lang.v
index 7389b74ff..aee1d5322 100644
--- a/ectx_lang.v
+++ b/ectx_lang.v
@@ -1,5 +1,5 @@
Require Import Arith Ssreflect.ssreflect Ssreflect.ssrfun.
-Require Import world_prop world_prop_recdom core_lang lang iris_core iris_plog iris_ht_rules.
+Require Import world_prop world_prop_recdom core_lang lang iris_core iris_plog iris_ht_rules iris_vs_rules iris_derived_rules.
Require Import ModuRes.RA ModuRes.SPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap ModuRes.RAConstr ModuRes.CMRA.
Set Bullet Behavior "Strict Subproofs".
@@ -168,6 +168,13 @@ Module ECTX_IRIS (RL : VIRA_T) (E : ECTX_LANG) (R: ECTX_RES RL E) (WP: WORLD_PRO
Module Import Core := IrisCore RL Lang Res World.
Module Import Plog := IrisPlog RL Lang Res World Core.
Module Import HTRules := IrisHTRules RL Lang Res World Core Plog.
+ Module Import VSRules := IrisVSRules RL Lang Res World Core Plog.
+ Module Import DerivedRules := IrisDerivedRules RL Lang Res World Core Plog VSRules HTRules.
+
+ Local Open Scope ra_scope.
+ Local Open Scope de_scope.
+ Local Open Scope bi_scope.
+ Local Open Scope iris_scope.
(** We can hae bind with evaluation contexts **)
Lemma fill_is_fill K: IsFill (E.fill K).
@@ -193,9 +200,16 @@ Module ECTX_IRIS (RL : VIRA_T) (E : ECTX_LANG) (R: ECTX_RES RL E) (WP: WORLD_PRO
Qed.
Lemma wpBind φ K e safe m :
- wp safe m e (plug_bind (E.fill K) safe m φ) ⊑ wp safe m (E.fill K e) φ.
+ wp safe m e (HTRules.plug_bind (E.fill K) safe m φ) ⊑ wp safe m (E.fill K e) φ.
Proof.
apply wpBind. apply fill_is_fill.
Qed.
+ Lemma htBind K P Q R e safe m :
+ ht safe m P e Q ∧ all (plug_bind (E.fill K) safe m Q R) ⊑ ht safe m P (E.fill K e) R.
+ Proof.
+ apply htBind. apply fill_is_fill.
+ Qed.
+
+
End ECTX_IRIS.
--
GitLab