An alternative proof of the closure refinement

theories/examples/various.v

@@ -10,6 +10,32 @@ Section refinement.
   Context `{logrelG Σ}.
   Notation D := (prodC valC valC -n> iProp Σ).
 
+  Lemma refinement1' Γ :
+    Γ ⊨
+      let: "x" := ref #1 in
+      (λ: "f", "f" #();; !"x")
+    ≤log≤
+      (λ: "f", "f" #();; #1)
+    : ((Unit → Unit) → TNat)%F.
+  Proof.
+  iIntros (Δ).
+  rel_alloc_l as x "Hx".
+  rel_let_l.
+  iMod (inv_alloc (nroot.@"xinv") _ (x ↦ᵢ #1)%I with "Hx") as "#Hinv".
+  iApply bin_log_related_rec; auto.
+  iAlways. cbn.
+  iApply (bin_log_related_seq); auto.
+  - iApply bin_log_related_app; last by iApply bin_log_related_unit.
+    iApply bin_log_related_var.
+    apply lookup_insert.
+  - rel_load_l_atomic.
+    iInv (nroot.@"xinv") as "Hx" "Hcl".
+    iModIntro. iExists _; iFrame "Hx"; simpl.
+    iNext. iIntros "Hx".
+    iMod ("Hcl" with "Hx") as "_".
+    iApply bin_log_related_nat.
+  Qed.
+
   Lemma refinement1 Γ :
     Γ ⊨
       let: "x" := ref #1 in
@@ -92,12 +118,12 @@ Section refinement.
       + rel_load_l_atomic.
         iInv shootN as "[[[Hx >Hp] | [Hx Hs']] Hy]" "Hcl".
         { iExFalso. iApply (shot_not_pending with "Hs Hp"). }
-        iModIntro. iExists _; iFrame. iNext.
+        iModIntro. iExists _; iFrame. iNext. simpl.
         iIntros "Hx".
         rel_load_r.
-        iMod ("Hcl" with "[-]").
+        iMod ("Hcl" with "[-]") as "_".
         { iNext. iFrame. iRight; by iFrame. }
-        rel_vals; eauto.
+        iApply bin_log_related_nat.
     - iMod ("Hcl" with "[$Hy Hx]") as "_".
       { iNext. iRight. by iFrame. }
       iApply (bin_log_related_seq with "[Hf]"); auto.