diff --git a/ectx_lang.v b/ectx_lang.v
index 9a2c056820eebdb129f8a78134f0a66e7f5afc44..88778e90d04efa15564d11ce0918512861177bc6 100644
--- a/ectx_lang.v
+++ b/ectx_lang.v
@@ -177,7 +177,7 @@ Module ECTX_IRIS (RL : VIRA_T) (E : ECTX_LANG) (R: ECTX_RES RL E) (WP: WORLD_PRO
Local Open Scope iris_scope.
(** We can hae bind with evaluation contexts **)
- Lemma fill_is_fill K: IsFill (E.fill K).
+ Lemma fill_is_ctx K: IsCtx (E.fill K).
Proof.
split; last split.
- intros ? Hval. eapply E.fill_value. eassumption.
@@ -196,13 +196,13 @@ Module ECTX_IRIS (RL : VIRA_T) (E : ECTX_LANG) (R: ECTX_RES RL E) (WP: WORLD_PRO
Lemma wpBind φ K e safe m :
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.
+ apply wpBind. apply fill_is_ctx.
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.
+ apply htBind. apply fill_is_ctx.
Qed.
End ECTX_IRIS.
diff --git a/iris_check.v b/iris_check.v
index cf2a853c48c28671915e1bfa606b539601bc3319..c4abd386840086e67ef3b9ede1054064b88e6f1e 100644
--- a/iris_check.v
+++ b/iris_check.v
@@ -84,7 +84,7 @@ Module Import HTRules := IrisHTRules TrivialRA StupidLang Res World Core Plog.
Module Import Meta := IrisMeta TrivialRA StupidLang Res World Core Plog HTRules.
(* Make sure the precondition of Bind can actually be met. *)
-Lemma id_is_fill: IsFill (fun e => e).
+Lemma id_is_ctx: IsCtx (fun e => e).
Proof.
split; last split.
- by firstorder.
diff --git a/iris_derived_rules.v b/iris_derived_rules.v
index 178fc6f32ee60402368c849373160195447a3e14..c21caf945bc8e26c4b05967b46e44fcc88d9d4a5 100644
--- a/iris_derived_rules.v
+++ b/iris_derived_rules.v
@@ -289,8 +289,8 @@ Module Type IRIS_DERIVED_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C)
(** Quantification in the logic works over nonexpansive maps, so
we need to show that plugging the value into the postcondition
and context is nonexpansive. *)
- Program Definition plug_bind (fill: expr -> expr) safe m Q Q' :=
- n[(fun v : value => ht safe m (Q v) (fill v) Q' )].
+ Program Definition plug_bind (ctx: expr -> expr) safe m Q Q' :=
+ n[(fun v : value => ht safe m (Q v) (ctx v) Q' )].
Next Obligation.
intros v1 v2 EQv; unfold ht; eapply box_dist.
eapply impl_dist.
@@ -299,12 +299,12 @@ Module Type IRIS_DERIVED_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C)
rewrite EQv; reflexivity.
Qed.
- Lemma htBind fill P Q R e safe m (HFill: IsFill fill) :
- ht safe m P e Q ∧ all (plug_bind fill safe m Q R) ⊑ ht safe m P (fill e) R.
+ Lemma htBind ctx P Q R e safe m (HCtx: IsCtx ctx) :
+ ht safe m P e Q ∧ all (plug_bind ctx safe m Q R) ⊑ ht safe m P (ctx e) R.
Proof.
rewrite /plug_bind {1 2}/ht. etransitivity; last eapply htIntro.
{ erewrite box_conj. apply and_pord; first reflexivity.
- erewrite (box_all (plug_bind fill safe m (pvs m m <M< Q) R)). apply all_pord=>v. simpl morph.
+ erewrite (box_all (plug_bind ctx safe m (pvs m m <M< Q) R)). apply all_pord=>v. simpl morph.
rewrite /ht. apply box_intro, box_intro. apply and_impl.
etransitivity; last eapply wpPreVS'. etransitivity; first by eapply pvsImpl. reflexivity. }
etransitivity; last by eapply wpBind.
diff --git a/iris_ht_rules.v b/iris_ht_rules.v
index 8a0c0304947af6c1d7793194cc68b0e1b952fab0..dc83650160071e6b3630d050a3fdf2f27c3267b5 100644
--- a/iris_ht_rules.v
+++ b/iris_ht_rules.v
@@ -95,37 +95,37 @@ Module Type IRIS_HT_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP:
(** Bind - in general **)
Section Bind.
- Definition IsFill (fill: expr -> expr): Prop :=
- (forall e, is_value (fill e) -> is_value e) /\
- (forall e1 σ1 e2 σ2 ef, prim_step (e1, σ1) (e2, σ2) ef -> prim_step (fill e1, σ1) (fill e2, σ2) ef) /\
- (forall e1 σ1 e2 σ2 ef, ~is_value e1 -> prim_step (fill e1, σ1) (e2, σ2) ef ->
- exists e2', e2 = fill e2' /\ prim_step (e1, σ1) (e2', σ2) ef).
-
- Program Definition plug_bind (fill: expr -> expr) safe m φ :=
- n[(fun v : value => wp safe m (fill v) φ )].
+ Definition IsCtx (ctx: expr -> expr): Prop :=
+ (forall e, is_value (ctx e) -> is_value e) /\
+ (forall e1 σ1 e2 σ2 ef, prim_step (e1, σ1) (e2, σ2) ef -> prim_step (ctx e1, σ1) (ctx e2, σ2) ef) /\
+ (forall e1 σ1 e2 σ2 ef, ~is_value e1 -> prim_step (ctx e1, σ1) (e2, σ2) ef ->
+ exists e2', e2 = ctx e2' /\ prim_step (e1, σ1) (e2', σ2) ef).
+
+ Program Definition plug_bind (ctx: expr -> expr) safe m φ :=
+ n[(fun v : value => wp safe m (ctx v) φ )].
Next Obligation.
intros v1 v2 EQv.
destruct n as [|n]; first by apply: dist_bound.
hnf in EQv. now rewrite EQv.
Qed.
- Lemma wpBind (fill: expr -> expr) φ e safe m (HFill: IsFill fill):
- wp safe m e (plug_bind fill safe m φ) ⊑ wp safe m (fill e) φ.
+ Lemma wpBind ctx φ e safe m (HCtx: IsCtx ctx):
+ wp safe m e (plug_bind ctx safe m φ) ⊑ wp safe m (ctx e) φ.
Proof.
- intros w n He. destruct HFill as (HFval & HFstep & HFfstep).
+ intros w n He. destruct HCtx as (HCval & HCstep & HCfstep).
revert e w He; induction n using wf_nat_ind; intros; rename H into IH.
(* We need to actually decide whether e is a value, to establish safety in the case that
it is not. *)
destruct (is_value_dec e) as [HVal | HNVal]; [clear IH |].
- eapply (wpValue _ HVal) in He. exact:He.
- rewrite ->unfold_wp in He; rewrite unfold_wp. split; intros.
- { exfalso. apply HNVal, HFval, HV. }
+ { exfalso. apply HNVal, HCval, HV. }
edestruct He as [_ He']; try eassumption; []; clear He.
edestruct He' as [HS HSf]; try eassumption; []; clear He' HE HD.
split; last first.
{ intros Heq. destruct (HSf Heq) as [?|[σ' [e' [ef Hstep]]]]; first contradiction.
- right. do 3 eexists. eapply HFstep. eassumption. }
- intros. edestruct (HFfstep e σ e' σ' ef) as (e'' & Heq' & Hstep'); first done; first done.
+ right. do 3 eexists. eapply HCstep. eassumption. }
+ intros. edestruct (HCfstep e σ e' σ' ef) as (e'' & Heq' & Hstep'); first done; first done.
destruct (HS _ _ _ Hstep') as (wret & wfk & Hret & Hfk & HE). subst e'.
exists wret wfk. split; last tauto.
clear Hfk HE. eapply IH; assumption.