From 6e850e1ee6484e264e395b6404b4a643e7d282b9 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 30 Oct 2015 16:15:16 +0100
Subject: [PATCH] show again the general bind rule
---
iris_check.v | 11 +++++++++++
iris_derived_rules.v | 44 ++++++++++++++++++++++++++++++++++++++++++--
iris_ht_rules.v | 30 +++++++++++++++---------------
3 files changed, 68 insertions(+), 17 deletions(-)
diff --git a/iris_check.v b/iris_check.v
index 21affbdb1..eeb257d8c 100644
--- a/iris_check.v
+++ b/iris_check.v
@@ -83,6 +83,15 @@ Module Import VSRules := IrisVSRules TrivialRA StupidLang Res World Core Plog.
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).
+Proof.
+ split; last split.
+ - by firstorder.
+ - by firstorder.
+ - intros. eexists. reflexivity.
+Qed.
+
(* And now we check for axioms *)
Print Assumptions adequacy_obs.
Print Assumptions adequacy_safe.
@@ -94,9 +103,11 @@ Print Assumptions lift_pure_det_step.
(including the base logic) would take too long. *)
Print Assumptions pvsOpen.
Print Assumptions pvsClose.
+Print Assumptions pvsTrans.
Print Assumptions pvsGhostUpd.
Print Assumptions wpPreVS.
Print Assumptions wpACons.
Print Assumptions wpFrameRes.
+Print Assumptions wpBind.
diff --git a/iris_derived_rules.v b/iris_derived_rules.v
index 50ae332dd..178fc6f32 100644
--- a/iris_derived_rules.v
+++ b/iris_derived_rules.v
@@ -235,6 +235,13 @@ Module Type IRIS_DERIVED_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C)
apply box_equiv. apply all_equiv=>v. reflexivity.
Qed.
+ Lemma wpPreVS' m safe e φ:
+ pvs m m (wp safe m e (pvs m m <M< φ)) ⊑ wp safe m e (pvs m m <M< φ).
+ Proof.
+ etransitivity; first eapply wpPreVS. eapply wpMon=>v. simpl morph. eapply pvsTrans.
+ de_auto_eq.
+ Qed.
+
(* pvs before and after the hoare triple can be collapsed into it *)
Lemma htMCons m m' safe e P P' Q Q':
□((P → (pvs m m') P')
@@ -263,8 +270,8 @@ Module Type IRIS_DERIVED_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C)
vs m m P P' ∧ ht safe m P' e Q' ∧ all (vsLift m m Q' Q) ⊑ ht safe m P e Q.
Proof.
rewrite /vs {1}/ht -vsLiftBox -!box_conj. apply htIntro.
- etransitivity; first by eapply htMCons. etransitivity; first by eapply wpPreVS.
- eapply wpMon. intros v. eapply pvsTrans. de_auto_eq.
+ etransitivity; first by eapply htMCons. etransitivity; first by eapply wpPreVS'.
+ reflexivity.
Qed.
Lemma htACons safe m m' e P P' Q Q'
@@ -277,6 +284,39 @@ Module Type IRIS_DERIVED_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C)
eapply htMCons.
Qed.
+
+ Section Bind.
+ (** 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' )].
+ Next Obligation.
+ intros v1 v2 EQv; unfold ht; eapply box_dist.
+ eapply impl_dist.
+ - apply Q; assumption.
+ - destruct n as [| n]; [apply dist_bound | hnf in EQv].
+ 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.
+ 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.
+ 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.
+ etransitivity; last eapply wpImpl with (φ:=pvs m m <M< Q). apply and_R; split.
+ - rewrite ->and_projL. apply box_intro. rewrite ->box_elim, ->and_projR.
+ apply all_pord=>v. simpl morph. rewrite /ht. rewrite ->box_elim. reflexivity.
+ - eapply modus_ponens; first by apply and_projR.
+ rewrite ->and_projL, ->box_elim, and_projL. reflexivity.
+ Qed.
+ End Bind.
+
+
Lemma htWeakenMask safe m m' P e Q (HD: m ⊑ m'):
ht safe m P e Q ⊑ ht safe m' P e Q.
Proof.
diff --git a/iris_ht_rules.v b/iris_ht_rules.v
index f629e8923..2eaa340c6 100644
--- a/iris_ht_rules.v
+++ b/iris_ht_rules.v
@@ -95,14 +95,13 @@ Module Type IRIS_HT_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP:
(** Bind - in general **)
Section Bind.
- Parameter fill: expr -> expr.
- Axiom fill_step: forall e1 σ1 e2 σ2 ef,
- prim_step (e1, σ1) (e2, σ2) ef <-> prim_step (fill e1, σ1) (fill e2, σ2) ef.
- Axiom fill_step_all: forall e1 σ1 e2 σ2 ef,
- prim_step (fill e1, σ1) (e2, σ2) ef -> exists e2', e2 = fill e2'.
- Axiom fill_val: forall e, is_value (fill e) -> is_value e.
-
- Program Definition plug_bind safe m φ :=
+ 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) /\
+ (prim_step (fill e1, σ1) (e2, σ2) ef -> exists e2', e2 = fill e2').
+
+ Program Definition plug_bind (fill: expr -> expr) safe m φ :=
n[(fun v : value => wp safe m (fill v) φ )].
Next Obligation.
intros v1 v2 EQv.
@@ -110,22 +109,23 @@ Module Type IRIS_HT_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP:
hnf in EQv. now rewrite EQv.
Qed.
- Lemma wpBind φ e safe m :
- wp safe m e (plug_bind safe m φ) ⊑ wp safe m (fill e) φ.
+ 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) φ.
Proof.
- intros w n He.
+ intros w n He. destruct HFill as [HFillValue HFillStep].
revert e w He; induction n using wf_nat_ind; intros; rename H into IH.
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, fill_val, HV. }
+ { exfalso. apply HNVal, HFillValue, 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. erewrite <-fill_step. eapply Hstep. }
- intros. destruct (fill_step_all _ _ _ _ _ HStep) as [e'' Heq]. subst e'.
- rewrite <-fill_step in HStep.
+ right. do 3 eexists. edestruct HFillStep as [HFillStepEq _]. erewrite <-HFillStepEq. eapply Hstep. }
+ intros. edestruct (HFillStep e σ e' σ' ef) as [_ HFillStepEx].
+ destruct (HFillStepEx HStep) as [e'' Heq]. subst e'.
+ edestruct HFillStep as [HFillStepEq _]. erewrite <-HFillStepEq in HStep.
destruct (HS _ _ _ HStep) as (wret & wfk & Hret & Hfk & HE).
exists wret wfk. split; last tauto.
clear Hfk HE. eapply IH; assumption.
--
GitLab