From 9331a3716bf288a1d01d9d0c11a7c03978fef41c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 19 Jan 2016 18:59:20 +0100
Subject: [PATCH] Introduce notion of reducible, as in the appendix.

---
 iris/hoare_lifting.v | 8 ++++----
 iris/language.v      | 5 +++++
 iris/lifting.v       | 4 ++--
 iris/weakestpre.v    | 2 +-
 4 files changed, 12 insertions(+), 7 deletions(-)

diff --git a/iris/hoare_lifting.v b/iris/hoare_lifting.v
index dac04e964..53886aab2 100644
--- a/iris/hoare_lifting.v
+++ b/iris/hoare_lifting.v
@@ -15,7 +15,7 @@ Import uPred.
 Lemma ht_lift_step E1 E2
     (Ï† : iexpr Î£ â†’ istate Î£ â†’ option (iexpr Î£) â†’ Prop) P P' Q1 Q2 R e1 Ïƒ1 :
   E1 âŠ† E2 â†’ to_val e1 = None â†’
-  (âˆƒ e2 Ïƒ2 ef, prim_step e1 Ïƒ1 e2 Ïƒ2 ef) â†’
+  reducible e1 Ïƒ1 â†’
   (âˆ€ e2 Ïƒ2 ef, prim_step e1 Ïƒ1 e2 Ïƒ2 ef â†’ Ï† e2 Ïƒ2 ef) â†’
   (P >{E2,E1}> (ownP Ïƒ1 â˜… â–· P') âˆ§ âˆ€ e2 Ïƒ2 ef,
     (â–  Ï† e2 Ïƒ2 ef â˜… ownP Ïƒ2 â˜… P') >{E1,E2}> (Q1 e2 Ïƒ2 ef â˜… Q2 e2 Ïƒ2 ef) âˆ§
@@ -45,7 +45,7 @@ Qed.
 Lemma ht_lift_atomic E
     (Ï† : iexpr Î£ â†’ istate Î£ â†’ option (iexpr Î£) â†’ Prop) P e1 Ïƒ1 :
   atomic e1 â†’
-  (âˆƒ e2 Ïƒ2 ef, prim_step e1 Ïƒ1 e2 Ïƒ2 ef) â†’
+  reducible e1 Ïƒ1 â†’
   (âˆ€ e2 Ïƒ2 ef, prim_step e1 Ïƒ1 e2 Ïƒ2 ef â†’ Ï† e2 Ïƒ2 ef) â†’
   (âˆ€ e2 Ïƒ2 ef, {{ â–  Ï† e2 Ïƒ2 ef â˜… P }} ef ?@ coPset_all {{ Î» _, True }}) âŠ‘
   {{ ownP Ïƒ1 â˜… â–· P }} e1 @ E {{ Î» v, âˆƒ Ïƒ2 ef, ownP Ïƒ2 â˜… â–  Ï† (of_val v) Ïƒ2 ef }}.
@@ -71,7 +71,7 @@ Proof.
 Qed.
 Lemma ht_lift_pure_step E (Ï† : iexpr Î£ â†’ option (iexpr Î£) â†’ Prop) P P' Q e1 :
   to_val e1 = None â†’
-  (âˆ€ Ïƒ1, âˆƒ e2 Ïƒ2 ef, prim_step e1 Ïƒ1 e2 Ïƒ2 ef) â†’
+  (âˆ€ Ïƒ1, reducible e1 Ïƒ1) â†’
   (âˆ€ Ïƒ1 e2 Ïƒ2 ef, prim_step e1 Ïƒ1 e2 Ïƒ2 ef â†’ Ïƒ1 = Ïƒ2 âˆ§ Ï† e2 ef) â†’
   (âˆ€ e2 ef,
     {{ â–  Ï† e2 ef â˜… P }} e2 @ E {{ Q }} âˆ§
@@ -97,7 +97,7 @@ Qed.
 Lemma ht_lift_pure_determistic_step E
     (Ï† : iexpr Î£ â†’ option (iexpr Î£) â†’ Prop) P P' Q e1 e2 ef :
   to_val e1 = None â†’
-  (âˆ€ Ïƒ1, prim_step e1 Ïƒ1 e2 Ïƒ1 ef) â†’
+  (âˆ€ Ïƒ1, reducible e1 Ïƒ1) â†’
   (âˆ€ Ïƒ1 e2' Ïƒ2 ef', prim_step e1 Ïƒ1 e2' Ïƒ2 ef' â†’ Ïƒ1 = Ïƒ2 âˆ§ e2 = e2' âˆ§ ef = ef')â†’
   ({{ P }} e2 @ E {{ Q }} âˆ§ {{ P' }} ef ?@ coPset_all {{ Î» _, True }})
   âŠ‘ {{ â–·(P â˜… P') }} e1 @ E {{ Q }}.
diff --git a/iris/language.v b/iris/language.v
index 443340947..c92a7ebb9 100644
--- a/iris/language.v
+++ b/iris/language.v
@@ -18,6 +18,11 @@ Class Language (E V St : Type) := {
 Section language.
   Context `{Language E V St}.
 
+  Definition reducible (e : E) (Ïƒ : St) :=
+    âˆƒ e' Ïƒ' ef, prim_step e Ïƒ e' Ïƒ' ef.
+  Lemma reducible_not_val e Ïƒ : reducible e Ïƒ â†’ to_val e = None.
+  Proof. intros (?&?&?&?); eauto using values_stuck. Qed.
+
   Lemma atomic_of_val v : Â¬atomic (of_val v).
   Proof.
     by intros Hat; apply atomic_not_value in Hat; rewrite to_of_val in Hat.
diff --git a/iris/lifting.v b/iris/lifting.v
index 8526f16e4..c94eda289 100644
--- a/iris/lifting.v
+++ b/iris/lifting.v
@@ -16,7 +16,7 @@ Transparent uPred_holds.
 Lemma wp_lift_step E1 E2
     (Ï† : iexpr Î£ â†’ istate Î£ â†’ option (iexpr Î£) â†’ Prop) Q e1 Ïƒ1 :
   E1 âŠ† E2 â†’ to_val e1 = None â†’
-  (âˆƒ e2 Ïƒ2 ef, prim_step e1 Ïƒ1 e2 Ïƒ2 ef) â†’
+  reducible e1 Ïƒ1 â†’
   (âˆ€ e2 Ïƒ2 ef, prim_step e1 Ïƒ1 e2 Ïƒ2 ef â†’ Ï† e2 Ïƒ2 ef) â†’
   pvs E2 E1 (ownP Ïƒ1 â˜… â–· âˆ€ e2 Ïƒ2 ef, (â–  Ï† e2 Ïƒ2 ef âˆ§ ownP Ïƒ2) -â˜…
     pvs E1 E2 (wp E2 e2 Q â˜… default True ef (flip (wp coPset_all) (Î» _, True))))
@@ -37,7 +37,7 @@ Proof.
 Qed.
 Lemma wp_lift_pure_step E (Ï† : iexpr Î£ â†’ option (iexpr Î£) â†’ Prop) Q e1 :
   to_val e1 = None â†’
-  (âˆ€ Ïƒ1, âˆƒ e2 Ïƒ2 ef, prim_step e1 Ïƒ1 e2 Ïƒ2 ef) â†’
+  (âˆ€ Ïƒ1, reducible e1 Ïƒ1) â†’
   (âˆ€ Ïƒ1 e2 Ïƒ2 ef, prim_step e1 Ïƒ1 e2 Ïƒ2 ef â†’ Ïƒ1 = Ïƒ2 âˆ§ Ï† e2 ef) â†’
   (â–· âˆ€ e2 ef, â–  Ï† e2 ef â†’
     wp E e2 Q â˜… default True ef (flip (wp coPset_all) (Î» _, True)))
diff --git a/iris/weakestpre.v b/iris/weakestpre.v
index 3e34864fa..c4383ab18 100644
--- a/iris/weakestpre.v
+++ b/iris/weakestpre.v
@@ -9,7 +9,7 @@ Local Hint Extern 10 (âœ“{_} _) =>
 
 Record wp_go {Î£} (E : coPset) (Q Qfork : iexpr Î£ â†’ nat â†’ res' Î£ â†’ Prop)
     (k : nat) (rf : res' Î£) (e1 : iexpr Î£) (Ïƒ1 : istate Î£) := {
-  wf_safe : âˆƒ e2 Ïƒ2 ef, prim_step e1 Ïƒ1 e2 Ïƒ2 ef;
+  wf_safe : reducible e1 Ïƒ1;
   wp_step e2 Ïƒ2 ef :
     prim_step e1 Ïƒ1 e2 Ïƒ2 ef â†’
     âˆƒ r2 r2',
-- 
GitLab