update to the current set of axioms

core_lang.v

@@ -40,6 +40,8 @@ Module Type CORE_LANG.
                        K1 [[ e ]] = K2 [[ e ]] -> K1 = K2.
   Axiom fill_inj2  : forall K e1 e2,
                        K [[ e1 ]] = K [[ e2 ]] -> e1 = e2.
+  Axiom fill_noinv: forall K1 K2, (* Interestingly, it seems impossible to derive this *)
+                       K1 ∘ K2 = ε -> K1 = ε /\ K2 = ε.
   Axiom fill_value : forall K e,
                        is_value (K [[ e ]]) ->
                        K = ε.
@@ -56,10 +58,14 @@ Module Type CORE_LANG.
   (** The primitive atomic stepping relation **)
   Parameter prim_step : prim_cfg -> prim_cfg -> Prop.
 
+
+  Definition reducible e: Prop :=
+    exists sigma cfg', prim_step (e, sigma) cfg'.
+
   Definition stuck (e : expr) : Prop :=
-    forall σ c K e',
+    forall K e',
       e = K [[ e' ]] ->
-      ~prim_step (e', σ) c.
+      ~reducible e'.
 
   Axiom fork_stuck :
     forall K e, stuck (K [[ fork e ]]).
@@ -71,9 +77,9 @@ Module Type CORE_LANG.
      sub-context of K' - in other words, e also contains the reducible
      expression *)
   Axiom step_by_value :
-    forall K K' e e' sigma cfg,
+    forall K K' e e',
       K [[ e ]] = K' [[ e' ]] ->
-      prim_step (e', sigma) cfg ->
+      reducible e' ->
       ~ is_value e ->
       exists K'', K' = K ∘ K''.
   (* Similar to above, buth with a fork instead of a reducible
@@ -87,13 +93,13 @@ Module Type CORE_LANG.
   (** Atomic expressions **)
   Parameter atomic : expr -> Prop.
 
-  Axiom atomic_not_stuck :
-    forall e, atomic e -> ~stuck e.
+  Axiom atomic_reducible :
+    forall e, atomic e -> reducible e.
+
 
-  Axiom atomic_step : forall eR K e e' σ σ',
-                        atomic eR ->
-                        eR = K [[ e ]] ->
-                        prim_step (e, σ) (e', σ') ->
-                        K = ε /\ is_value e'.
+  Axiom atomic_step: forall e σ e' σ',
+                       atomic e ->
+                       prim_step (e, σ) (e', σ') ->
+                       is_value e'.
 
 End CORE_LANG.

iris.v

@@ -589,7 +589,7 @@ Module Iris (RL : PCM_T) (C : CORE_LANG).
       - intros w n r; apply Hp; exact I.
     Qed.
 
-    Lemma vsFalse m1 m2 :
+    Lemma vsFalse m1 m2 : (* TODO move to derived rules *)
       valid (vs m1 m2 ⊥ ⊥).
     Proof.
       rewrite valid_iff, box_top.
@@ -745,7 +745,7 @@ Qed.
 
 
 
-    (* XXX missing statements: GhostUpd, VSTimeless *)
+    (* XXX missing statements: VSTimeless *)
 
   End ViewShiftProps.
 
@@ -1163,7 +1163,7 @@ Qed.
     Qed.
 
     (** Framing **)
-
+    (* TODO: mask framing *)
     Lemma htFrame m P R e φ :
       ht m P e φ ⊑ ht m (P * R) e (lift_bin sc φ (umconst R)).
     Proof.
@@ -1270,8 +1270,6 @@ Qed.
           eapply fork_not_value; eassumption.
     Qed.
 
-    (** Not stated: the Shift (timeless) rule *)
-
   End HoareTripleProperties.
 
 End Iris.

lang.v

@@ -89,7 +89,48 @@ Module Lang (C : CORE_LANG).
     apply comp_ctx_inj1 in HEq; congruence.
   Qed.
 
-  (* atomic expressions *)
+  (* Lemmas about expressions *)
+  Lemma reducible_not_value e:
+    reducible e -> ~is_value e.
+  Proof.
+    intros H_red H_val.
+    eapply values_stuck; try eassumption.
+    now erewrite fill_empty.
+  Qed.
+
+  Lemma step_same_ctx: forall K K' e e',
+                         fill K e = fill K' e' ->
+                         reducible e  ->
+                         reducible e' ->
+                         K = K'.
+  Proof.
+    intros K K' e e' H_fill H_red H_red'.
+    edestruct (step_by_value K K' e e') as [K'' H_K''].
+    - assumption.
+    - assumption.
+    - now apply reducible_not_value.
+    - edestruct (step_by_value K' K e' e) as [K''' H_K'''].
+      + now symmetry.
+      + assumption.
+      + now apply reducible_not_value.
+      + subst K.
+        rewrite comp_ctx_assoc in H_K''.
+        assert (H_emp := comp_ctx_neut_emp_r _ _ H_K'').
+        apply fill_noinv in H_emp.
+        destruct H_emp as[H_K'''_emp H_K''_emp].
+        subst K'' K'''.
+        now rewrite comp_ctx_emp_r.
+  Qed.
+
+  Lemma atomic_not_stuck e:
+    atomic e -> ~stuck e.
+  Proof.
+    intros H_atomic H_stuck.
+    eapply H_stuck.
+    - now erewrite fill_empty.
+    - now eapply atomic_reducible.
+  Qed.
+
   Lemma fork_not_atomic K e :
     ~atomic (K [[ fork e ]]).
   Proof.