From c7b1b95440c2d149d9ef305b122a79d4cc89b024 Mon Sep 17 00:00:00 2001
From: Filip Sieczkowski <filips@cs.au.dk>
Date: Sun, 6 Jul 2014 19:13:00 +0200
Subject: [PATCH] Finished with the formalisation.

---
 core_lang.v |  4 ----
 iris.v      |  8 ++++++--
 lang.v      | 12 ++++++++++++
 3 files changed, 18 insertions(+), 6 deletions(-)

diff --git a/core_lang.v b/core_lang.v
index 8131a74d4..d1d427d95 100644
--- a/core_lang.v
+++ b/core_lang.v
@@ -96,10 +96,6 @@ Module Type CORE_LANG.
   Axiom atomic_reducible :
     forall e, atomic e -> reducible e.
 
-  Axiom atomic_fill :
-    forall e K (HAt : atomic (K [[e ]])),
-      K = empty_ctx.
-
   Axiom atomic_step: forall e σ e' σ',
                        atomic e ->
                        prim_step (e, σ) (e', σ') ->
diff --git a/iris.v b/iris.v
index 06cd6abd9..95f3c00c4 100644
--- a/iris.v
+++ b/iris.v
@@ -1358,7 +1358,9 @@ Qed.
         [reflexivity | apply le_n | rewrite HSub; eassumption | eassumption |].
       edestruct HS as [w [r'' [s'' [HSw [He' HE] ] ] ] ]; try eassumption; clear He HS HE'.
       destruct k as [| k]; [exists w' r' s'; split; [reflexivity | split; [apply wpO | exact I] ] |].
-      subst e; assert (HT := atomic_fill _ _ HAt); subst K.
+      assert (HNV : ~ is_value ei)
+        by (intros HV; eapply (values_stuck _ HV); [symmetry; apply fill_empty | repeat eexists; eassumption]).
+      subst e; assert (HT := atomic_fill _ _ HAt HNV); subst K; clear HNV.
       rewrite fill_empty in *; rename ei into e.
       setoid_rewrite HSw'; setoid_rewrite HSw.
       assert (HVal := atomic_step _ _ _ _ HAt HStep).
@@ -1467,7 +1469,9 @@ Qed.
           [| eapply erasure_not_empty in HE';
              [contradiction | now erewrite !pcm_op_zero by apply _] ].
         do 3 eexists; split; [eassumption | split; [| eassumption] ].
-        subst e; assert (HT := atomic_fill _ _ HAt); subst K.
+        assert (HNV : ~ is_value ei)
+          by (intros HV; eapply (values_stuck _ HV); [symmetry; apply fill_empty | repeat eexists; eassumption]).
+        subst e; assert (HT := atomic_fill _ _ HAt HNV); subst K; clear HNV.
         rewrite fill_empty in *.
         unfold lt in HLt; rewrite <- HLt, HSw, HSw' in HLR; simpl in HLR.
         assert (HVal := atomic_step _ _ _ _ HAt HStep).
diff --git a/lang.v b/lang.v
index f7cce2388..5f09ade32 100644
--- a/lang.v
+++ b/lang.v
@@ -147,4 +147,16 @@ Module Lang (C : CORE_LANG).
     tauto.
   Qed.
 
+  Lemma atomic_fill e K
+        (HAt : atomic (K [[ e ]]))
+        (HNV : ~ is_value e) :
+    K = empty_ctx.
+  Proof.
+    destruct (step_by_value K ε e (K [[ e ]])) as [K' EQK].
+    - now rewrite fill_empty.
+    - now apply atomic_reducible.
+    - assumption.
+    - symmetry in EQK; now apply fill_noinv in EQK.
+  Qed.
+
 End Lang.
-- 
GitLab