From 95c7a3f3201af655dfd4501a4f5cfae1a418fceb Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 16 Oct 2015 10:52:40 +0200
Subject: [PATCH] Show the relationship between safe expressions and thread
 pool reduction

---
 iris_check.v |  2 +-
 iris_meta.v  | 32 ++++++++++++++++++++++++++++----
 2 files changed, 29 insertions(+), 5 deletions(-)

diff --git a/iris_check.v b/iris_check.v
index 0fba71722..236ec9d00 100644
--- a/iris_check.v
+++ b/iris_check.v
@@ -192,7 +192,7 @@ Module Import HTRules := IrisHTRules TrivialRA StupidLang Res World Core Plog.
 
 (* And now we check for axioms *)
 Print Assumptions adequacy_obs.
-(* TODO enable this once it is proven Print Assumptions adequacy_safe. *)
+Print Assumptions adequacy_safe.
 
 Print Assumptions lift_atomic_det_step.
 Print Assumptions lift_pure_det_step.
diff --git a/iris_meta.v b/iris_meta.v
index 68e0b9c4d..ca9ff12e8 100644
--- a/iris_meta.v
+++ b/iris_meta.v
@@ -209,7 +209,7 @@ Module Type IRIS_META (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
     Qed.
 
     (* Adequacy for safe triples *)
-    Theorem adequacy_safe_expr m e (Q : vPred) tp' σ σ' e'
+    Lemma adequacy_safe_expr m e (Q : vPred) tp' σ σ' e'
             (HT  : valid (ht true m (ownS σ) e Q))
             (HSN : steps ([e], σ) (tp', σ'))
             (HE  : e' ∈ tp'):
@@ -227,13 +227,37 @@ Module Type IRIS_META (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
       - apply HSafe. reflexivity.
     Qed.
 
-    Theorem adequacy_safe m e (Q : vPred) tp' σ σ' e'
+    Theorem adequacy_safe m e (Q : vPred) tp' σ σ'
             (HT  : valid (ht true m (ownS σ) e Q))
             (HSN : steps ([e], σ) (tp', σ')):
       (forall e', e' ∈ tp' -> is_value e') \/ exists tp'' σ'', step (tp', σ') (tp'', σ'').
     Proof.
-      (* TODO: Prove this. *)
-    Abort.
+      assert (Hsafe: forall e', e' ∈ tp' -> safeExpr e' σ').
+      { move=>e' HE. eapply adequacy_safe_expr; eassumption. }
+      clear -Hsafe. induction tp' as [|e tp' IH].
+      - left. move=>? [].
+      - move:IH. case/(_ _)/Wrap.
+        { move=>e' Hin. apply Hsafe. right. assumption. }
+        case=>IH; last first.
+        { destruct IH as [tp'' [σ'' Hstep]]. right.
+          destruct Hstep.
+          - inversion H0=>{H0}; inversion H1=>{H1}; subst.
+            do 2 eexists. eapply step_atomic; first eassumption; last reflexivity.
+            rewrite app_comm_cons. reflexivity.
+          - inversion H=>{H}; inversion H0=>{H0}; subst.
+            do 2 eexists. eapply step_fork; last reflexivity.
+            rewrite app_comm_cons. reflexivity.
+        }
+        move:(Hsafe e)=>{Hsafe}. case/(_ _)/Wrap; first by left.
+        case=>[Hsafe|[[σ'' [ei [ei' [K [Hfill Hstep]]]]]|[e' [K Hfill]]]].
+        + left. move=>e'. case.
+          * by move =><-.
+          * by auto.
+        + right. do 2 eexists. eapply step_atomic with (t1:=[]); first eassumption; last reflexivity.
+          rewrite Hfill. reflexivity.
+        + right. do 2 eexists. eapply step_fork with (t1:=[]); last reflexivity.
+          rewrite Hfill. reflexivity.
+    Qed.
 
   End Adequacy.
 
-- 
GitLab