From 042fdf1ab349bd745e99a0ebcdf9ae49bff044ef Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Mon, 18 Mar 2019 18:37:15 +0100
Subject: [PATCH] Add the `refines_store` compatibility rule.

---
 theories/logic/compatibility.v | 19 +++++++++++++++++++
 theories/typing/fundamental.v  | 14 +++-----------
 2 files changed, 22 insertions(+), 11 deletions(-)

diff --git a/theories/logic/compatibility.v b/theories/logic/compatibility.v
index 8e075e5..96ad668 100644
--- a/theories/logic/compatibility.v
+++ b/theories/logic/compatibility.v
@@ -89,5 +89,24 @@ Section compatibility.
     rel_rec_l. rel_rec_r. iApply "H".
   Qed.
 
+  Lemma refines_store e1 e2 e1' e2' A :
+    (REL e1 << e1' : ref A) -∗
+    (REL e2 << e2' : A) -∗
+    REL e1 <- e2 << e1' <- e2' : ().
+  Proof.
+    iIntros "IH1 IH2".
+    rel_bind_ap e2 e2' "IH2" w w' "IH2".
+    rel_bind_ap e1 e1' "IH1" v v' "IH1".
+    iDestruct "IH1" as (l l') "(% & % & Hinv)"; simplify_eq/=.
+    rel_store_l_atomic.
+    iInv (relocN .@ "ref" .@ (l,l')) as (v v') "[Hv1 [>Hv2 #Hv]]" "Hclose".
+    iModIntro. iExists _; iFrame "Hv1".
+    iNext. iIntros "Hw1".
+    rel_store_r.
+    iMod ("Hclose" with "[Hw1 Hv2 IH2]").
+    { iNext; iExists _, _; simpl; iFrame. }
+    value_case.
+  Qed.
+
 End compatibility.
 
diff --git a/theories/typing/fundamental.v b/theories/typing/fundamental.v
index 4aee02c..9d49a03 100644
--- a/theories/typing/fundamental.v
+++ b/theories/typing/fundamental.v
@@ -278,17 +278,9 @@ Section fundamental.
   Proof.
     iIntros "IH1 IH2".
     intro_clause.
-    rel_bind_ap e2 e2' "IH2" w w' "IH2".
-    rel_bind_ap e1 e1' "IH1" v v' "IH1".
-    iDestruct "IH1" as (l l') "(% & % & Hinv)"; simplify_eq/=.
-    rel_store_l_atomic.
-    iInv (relocN .@ "ref" .@ (l,l')) as (v v') "[Hv1 [>Hv2 #Hv]]" "Hclose".
-    iModIntro. iExists _; iFrame "Hv1".
-    iNext. iIntros "Hw1".
-    rel_store_r.
-    iMod ("Hclose" with "[Hw1 Hv2 IH2]").
-    { iNext; iExists _, _; simpl; iFrame. }
-    value_case.
+    iApply (refines_store with "[IH1] [IH2]").
+    - by iApply "IH1".
+    - by iApply "IH2".
   Qed.
 
   Lemma bin_log_related_CAS Δ Γ e1 e2 e3 e1' e2' e3' τ
-- 
GitLab