From f01e18b3ec657d59e74c4b5db7d8023d8b57fc04 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Fri, 10 May 2019 16:35:54 +0200
Subject: [PATCH] Add `refines_load`.

---
 theories/logic/compatibility.v | 17 +++++++++++++++++
 theories/typing/fundamental.v  | 12 ++----------
 2 files changed, 19 insertions(+), 10 deletions(-)

diff --git a/theories/logic/compatibility.v b/theories/logic/compatibility.v
index 96ad668..5e14b32 100644
--- a/theories/logic/compatibility.v
+++ b/theories/logic/compatibility.v
@@ -108,5 +108,22 @@ Section compatibility.
     value_case.
   Qed.
 
+  Lemma refines_load e e' A :
+    (REL e << e' : ref A) -∗
+    REL !e << !e' : A.
+  Proof.
+    iIntros "H".
+    rel_bind_ap e e' "H" v v' "H".
+    iDestruct "H" as (l l' -> ->) "#H".
+    rel_load_l_atomic.
+    iInv (relocN .@ "ref" .@ (l,l')) as (w w') "[Hw1 [>Hw2 #Hw]]" "Hclose"; simpl.
+    iModIntro. iExists _; iFrame "Hw1".
+    iNext. iIntros "Hw1".
+    rel_load_r.
+    iMod ("Hclose" with "[Hw1 Hw2]").
+    { iNext. iExists w,w'; by iFrame. }
+    value_case.
+  Qed.
+
 End compatibility.
 
diff --git a/theories/typing/fundamental.v b/theories/typing/fundamental.v
index 99840fe..f4e7964 100644
--- a/theories/typing/fundamental.v
+++ b/theories/typing/fundamental.v
@@ -259,16 +259,8 @@ Section fundamental.
   Proof.
     iIntros "IH".
     intro_clause.
-    rel_bind_ap e e' "IH" v v' "IH".
-    iDestruct "IH" as (l l') "(% & % & Hinv)"; simplify_eq/=.
-    rel_load_l_atomic.
-    iInv (relocN .@ "ref" .@ (l,l')) as (w w') "[Hw1 [>Hw2 #Hw]]" "Hclose"; simpl.
-    iModIntro. iExists _; iFrame "Hw1".
-    iNext. iIntros "Hw1".
-    rel_load_r.
-    iMod ("Hclose" with "[Hw1 Hw2]").
-    { iNext. iExists w,w'; by iFrame. }
-    value_case.
+    iApply refines_load.
+    by iApply "IH".
   Qed.
 
   Lemma bin_log_related_store Δ Γ e1 e2 e1' e2' τ :
-- 
GitLab