Add the "single return" example

theories/examples/various.v

@@ -123,7 +123,7 @@ Section refinement.
                  b ↦ᵢ #true ∗ b' ↦ₛ #true)
                ∨ (b ↦ᵢ #false ∗ b' ↦ₛ #false))%I.
   Definition i3n := nroot .@ "i3".
-  Lemma refinement3  Γ :
+  Lemma refinement3 Γ :
     Γ ⊨
       let: "b" := ref #true in
       let: "x" := ref #0 in
@@ -212,7 +212,7 @@ Section refinement.
      Without locking in the first expression, the callback can reenter
      the body in a forked thread to change the value of x
   *)
-  Lemma refinement4  Γ `{!lockG Σ}:
+  Lemma refinement4 Γ `{!lockG Σ}:
     Γ ⊨
       (let: "x" := ref #1 in
        let: "l" := newlock #() in
@@ -261,4 +261,42 @@ Section refinement.
     rel_vals; eauto.
   Qed.
 
+  (* "Single return" example *)
+  Lemma refinement5 Γ :
+    Γ ⊨
+      (λ: "f", let: "x" := ref #0 in
+               let: "y" := ref #0 in
+               "f" #();;
+               "x" <- !"y";;
+               "y" <- #1;;
+               !"x")
+    ≤log≤
+      (λ: "f", let: "x" := ref #0 in
+               let: "y" := ref #0 in
+               "f" #();;
+               "x" <- !"y";;
+               "y" <- #2;;
+               !"x")
+    : TArrow (TArrow TUnit TUnit) TNat.
+  Proof.
+    iIntros (Δ).
+    iApply bin_log_related_arrow; eauto.
+    iAlways.
+    iIntros (f1 f2) "Hf".
+    rel_let_l. rel_let_r.
+    rel_alloc_l as x "Hx". rel_let_l.
+    rel_alloc_l as y "Hy". rel_let_l.
+    rel_alloc_r as x' "Hx'". rel_let_r.
+    rel_alloc_r as y' "Hy'". rel_let_r.
+    iApply (bin_log_related_seq with "[Hf]"); eauto.
+    { iApply (bin_log_related_app with "Hf").
+      iApply bin_log_related_unit. }
+    rel_load_l. rel_load_r.
+    rel_store_l. rel_store_r.
+    rel_let_l. rel_let_r.
+    rel_store_l. rel_store_r.
+    rel_let_l. rel_let_r.
+    rel_load_l. rel_load_r.
+    iApply bin_log_related_nat.
+  Qed.
 End refinement.