Commit d523141d authored by Ralf Jung's avatar Ralf Jung

rename: filling function -> context function

parent 5cca350d
......@@ -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.
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment