tune the filling axioms to make more sense

ectx_lang.v

@@ -179,24 +179,18 @@ Module ECTX_IRIS (RL : VIRA_T) (E : ECTX_LANG) (R: ECTX_RES RL E) (WP: WORLD_PRO
   (** We can hae bind with evaluation contexts **)
   Lemma fill_is_fill K: IsFill (E.fill K).
   Proof.
-    split; intros; last (split; intros; first split).
-    - eapply E.fill_value. eassumption.
-    - intros (K' & e1' & e2' & Heq1 & Heq2 & Hstep).
+    split; last split.
+    - intros ? Hval. eapply E.fill_value. eassumption.
+    - intros ? ? ? ? ? (K' & e1' & e2' & Heq1 & Heq2 & Hstep).
       exists (E.comp_ctx K K') e1' e2'. rewrite -!E.fill_comp Heq1 Heq2.
       split; last split; reflexivity || assumption.
-    - intros (K' & e1' & e2' & Heq1 & Heq2 & Hstep).
+    - intros ? ? ? ? ? Hnval (K' & e1' & e2' & Heq1 & Heq2 & Hstep).
       destruct (E.step_by_value _ _ _ _ Heq1) as [K'' HeqK].
       + do 3 eexists. eassumption.
       + assumption.
-      + exists K''. subst K'. rewrite -!E.fill_comp in Heq1, Heq2.
-        apply E.fill_inj_r in Heq1. apply E.fill_inj_r in Heq2.
-        do 2 eexists. split; last split; eassumption.
-    - destruct H0 as (K' & e1' & e2' & Heq1 & Heq2 & Hstep).
-      destruct (E.step_by_value _ _ _ _ Heq1) as [K'' HeqK].
-      + do 3 eexists. eassumption.
-      + assumption.
-      + subst K'. rewrite -E.fill_comp in Heq2.
-        eexists. eassumption.
+      + subst e2 K'. rewrite -E.fill_comp in Heq1. apply E.fill_inj_r in Heq1. subst e1.
+        exists (E.fill K'' e2'). split; first by rewrite -E.fill_comp.
+        do 3 eexists. split; last split; eassumption || reflexivity.
   Qed.
         
   Lemma wpBind φ K e safe m :
@@ -211,5 +205,4 @@ Module ECTX_IRIS (RL : VIRA_T) (E : ECTX_LANG) (R: ECTX_RES RL E) (WP: WORLD_PRO
     apply htBind. apply fill_is_fill.
   Qed.
   
-
 End ECTX_IRIS.

iris_check.v

@@ -89,7 +89,7 @@ Proof.
   split; last split.
   - by firstorder.
   - by firstorder.
-  - intros. eexists. reflexivity.
+  - intros. eexists. split; reflexivity || eassumption.
 Qed.
 
 (* And now we check for axioms *)

iris_ht_rules.v

@@ -97,9 +97,9 @@ Module Type IRIS_HT_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP:
     Section Bind.
       Definition IsFill (fill: expr -> expr): Prop :=
         (forall e, is_value (fill e) -> is_value e) /\
-        forall e1 σ1 e2 σ2 ef, ~is_value e1 ->
-          (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').
+        (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) φ )].
@@ -112,21 +112,19 @@ Module Type IRIS_HT_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP:
       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. destruct HFill as [HFillValue HFillStep].
+        intros w n He. destruct HFill as (HFval & HFstep & HFfstep).
         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, HFillValue, HV. }
+          { exfalso. apply HNVal, HFval, 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. edestruct HFillStep as [HFillStepEq _]; last erewrite <-HFillStepEq; first assumption. eapply Hstep. }
-          intros. edestruct (HFillStep e σ e' σ' ef) as [_ HFillStepEx]; first done.
-          destruct (HFillStepEx HStep) as [e'' Heq]. subst e'.
-          edestruct HFillStep as [HFillStepEq _]; last erewrite <-HFillStepEq in HStep; first done.
-          destruct (HS _ _ _ HStep) as (wret & wfk & Hret & Hfk & HE).
+            right. do 3 eexists. eapply HFstep. eassumption. }
+          intros. edestruct (HFfstep 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.
       Qed.