oO we can have a general bind rule... with very few assumptions about filling

iris_ht_rules.v

@@ -93,6 +93,45 @@ Module Type IRIS_HT_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP:
     { assumption. }
     Qed.
 
+    (** 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 φ :=
+        n[(fun v : value => wp safe m (fill 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 φ e safe m :
+        wp safe m e (plug_bind safe m φ) ⊑ wp safe m (fill e) φ.
+      Proof.
+        intros w n He.
+        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. }
+          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.
+          destruct (HS _ _ _ HStep) as (wret & wfk & Hret & Hfk & HE).
+          exists wret wfk. split; last tauto.
+          clear Hfk HE. eapply IH; assumption.
+      Qed.
+    End Bind.
+
     (** Mask weakening **)
     Lemma wpWeakenMask safe m1 m2 e φ (HD : m1 ⊑ m2) :
       wp safe m1 e φ ⊑ wp safe m2 e φ.