From 6f3dc0a97cec738f74604c741dca34f49bb0a9fe Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Thu, 14 Dec 2017 18:09:23 +0100
Subject: [PATCH] Full circle for the "awkward" example

---
 theories/examples/various.v | 45 +++++++++++++++++++++++++++++++++++++
 1 file changed, 45 insertions(+)

diff --git a/theories/examples/various.v b/theories/examples/various.v
index e67b225..6aed660 100644
--- a/theories/examples/various.v
+++ b/theories/examples/various.v
@@ -140,6 +140,51 @@ Section refinement.
         rel_vals; eauto.
   Qed.
 
+
+  Lemma refinement25 `{oneshotG Σ} Γ :
+    Γ ⊨
+      (λ: "f", "f" #();; #1)
+    ≤log≤
+      (let: "x" := ref #0 in
+       (λ: "f", "x" <- #1;; "f" #();; !"x"))
+    : ((Unit → Unit) → TNat).
+  Proof.
+    iIntros (Δ).
+    rel_alloc_r as x "Hx".
+    rel_let_r.
+    iMod new_pending as (γ) "Ht".
+    iMod (inv_alloc shootN _ ((x ↦ₛ #0 ∗ pending γ ∨ x ↦ₛ #1 ∗ shot γ))%I with "[Hx Ht]") as "#Hinv".
+    { iNext. iLeft. iFrame. }
+    iApply bin_log_related_arrow; auto.
+    iIntros "!#" (f1 f2) "#Hf".
+    rel_let_l. rel_let_r.
+    iInv shootN as ">[[Hx Hp] | [Hx #Hs]]" "Hcl";
+      rel_store_r; rel_seq_r.
+    - iMod (shoot γ with "Hp") as "#Hs".
+      iMod ("Hcl" with "[Hx]") as "_".
+      { iNext. iRight. by iFrame. }
+      iApply (bin_log_related_seq with "[Hf]"); auto.
+      + iApply (bin_log_related_app with "Hf").
+        rel_finish.
+      + iInv shootN as "[[>Hx >Hp] | [>Hx _]]" "Hcl";
+          rel_load_r.
+        { iExFalso. iApply (shot_not_pending with "Hs Hp"). }
+        iMod ("Hcl" with "[Hx]") as "_".
+        { iNext. iRight. by iFrame. }
+        rel_finish.
+    - iMod ("Hcl" with "[Hx]") as "_".
+      { iNext. iRight. by iFrame. }
+      iApply (bin_log_related_seq with "[Hf]"); auto.
+      + iApply (bin_log_related_app with "Hf").
+        rel_finish.
+      + iInv shootN as "[[>Hx >Hp] | [>Hx _]]" "Hcl";
+          rel_load_r.
+        { iExFalso. iApply (shot_not_pending with "Hs Hp"). }
+        iMod ("Hcl" with "[Hx]") as "_".
+        { iNext. iRight. by iFrame. }
+        rel_finish.
+  Qed.
+
   (* Also known as "callback with lock" *)
   Definition i3 x x' b b' : iProp Σ :=
     ((∃ (n : nat), x ↦ᵢ #n ∗ x' ↦ₛ #n ∗
-- 
GitLab