Some more examples

From "The effects of higher-order state and control on local relational reasoning"

_CoqProject

@@ -36,6 +36,7 @@ theories/examples/stack/refinement.v
 theories/examples/stack/module_refinement.v
 theories/examples/stack/mailbox.v
 theories/examples/stack/helping.v
+theories/examples/various.v
 theories/tests/typetest.v
 theories/tests/tactics.v
 theories/tests/tactics2.v

theories/examples/counter.v

@@ -44,7 +44,7 @@ Section CG_Counter.
   Proof.
     iIntros (?) "Hx Hl Hlog".
     unfold CG_increment. unlock. simpl_subst/=.
-    rel_rec_r.
+    rel_seq_r.
     rel_apply_r (bin_log_related_acquire_r with "Hl"); eauto.
     iIntros "Hl".
     rel_rec_r.

theories/examples/various.v

+(* Some refinement from the paper
+   "The effects of higher-order state and control on local relational reasoning"
+   D. Dreyer, G. Neis, L. Birkedal
+*)
+From iris.proofmode Require Import tactics.
+From iris.algebra Require Import csum agree excl.
+From iris_logrel Require Import logrel.
+
+Lemma bin_log_related_seq `{logrelG Σ} τ1 E Δ Γ e1 e2 e1' e2' τ2
+`{Closed ∅ e2} `{Closed ∅ e2'} :
+  ↑logrelN ⊆ E →
+  {E,E;Δ;Γ} ⊨ e1 ≤log≤ e1' : τ1 -∗
+  {E,E;Δ;Γ} ⊨ e2 ≤log≤ e2' : τ2 -∗
+  {E,E;Δ;Γ} ⊨ (e1;; e2) ≤log≤ (e1';; e2') : τ2.
+Proof.
+  iIntros (?) "He1 He2".
+  rel_bind_l e1.
+  rel_bind_r e1'.
+  iApply (related_bind with "He1 [He2]").
+  iIntros (?) "? /=".
+  rel_rec_l.
+  rel_rec_r.
+  done.
+Qed.
+
+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)
+    : TArrow (TArrow TUnit TUnit) TNat.
+  Proof.
+  iIntros (Δ).
+  rel_alloc_l as x "Hx".
+  iMod (inv_alloc (nroot.@"xinv") _ (x ↦ᵢ #1)%I with "Hx") as "#Hinv".
+  rel_let_l.
+  iApply bin_log_related_arrow; auto.
+  iIntros "!#" (f1 f2) "Hf".
+  rel_let_l. rel_let_r.
+  iApply (bin_log_related_seq with "[Hf]"); auto.
+  - iApply (bin_log_related_app with "Hf").
+    by rel_vals.
+  - rel_load_l_atomic.
+    iInv (nroot.@"xinv") as "Hx" "Hcl".
+    iModIntro. iExists _; iFrame "Hx".
+    iNext. iIntros "Hx".
+    iMod ("Hcl" with "Hx").
+    rel_vals; eauto.
+  Qed.
+
+  Definition oneshotR := csumR (exclR unitR) (agreeR unitR).
+  Class oneshotG Σ := { oneshot_inG :> inG Σ oneshotR }.
+  Definition oneshotΣ : gFunctors := #[GFunctor oneshotR].
+  Instance subG_oneshotΣ {Σ} : subG oneshotΣ Σ → oneshotG Σ.
+  Proof. solve_inG. Qed.
+
+  Definition pending γ `{oneshotG Σ} := own γ (Cinl (Excl ())).
+  Definition shot γ `{oneshotG Σ} := own γ (Cinr (to_agree ())).
+  Lemma new_pending `{oneshotG Σ} : (|==> ∃ γ, pending γ)%I.
+  Proof. by apply own_alloc. Qed.
+  Lemma shoot γ `{oneshotG Σ} : pending γ ==∗ shot γ.
+  Proof.
+    apply own_update.
+    intros n [f |]; simpl; eauto.
+    destruct f; simpl; try by inversion 1.
+  Qed.
+  Definition shootN := nroot .@ "shootN".
+  Lemma shot_not_pending γ `{oneshotG Σ} :
+    shot γ -∗ pending γ -∗ False.
+  Proof.
+    iIntros "Hs Hp".
+    iPoseProof (own_valid_2 with "Hs Hp") as "H".
+    iDestruct "H" as %[].
+  Qed.
+
+  Lemma refinement2 `{oneshotG Σ} Γ :
+    Γ ⊨
+      let: "x" := ref #0 in
+      (λ: "f", "x" <- #1;; "f" #();; !"x")
+    ≤log≤
+      (let: "x" := ref #1 in
+       λ: "f", "f" #();; !"x")
+    : TArrow (TArrow TUnit TUnit) TNat.
+  Proof.
+    iIntros (Δ).
+    rel_alloc_l as x "Hx".
+    rel_alloc_r as y "Hy".
+    rel_let_l; rel_let_r.
+    iApply fupd_logrel.
+    iMod new_pending as (γ) "Ht". (*TODO typeclasses for this?*)
+    iModIntro.
+    iMod (inv_alloc shootN _ ((x ↦ᵢ #0 ∗ pending γ ∨ x ↦ᵢ #1 ∗ shot γ) ∗ y ↦ₛ #1)%I with "[Hx Ht $Hy]") as "#Hinv".
+    { iNext. iLeft. iFrame. }
+    iApply bin_log_related_arrow; auto.
+    iIntros "!#" (f1 f2) "Hf".
+    rel_let_l. rel_let_r.
+    rel_store_l_atomic.
+    iInv shootN as "[[[Hx Hp] | [Hx #Hs]] Hy]" "Hcl";
+      iModIntro; iExists _; iFrame "Hx"; iNext; iIntros "Hx"; rel_rec_l.
+    - iApply fupd_logrel'.
+      iMod (shoot γ with "Hp") as "#Hs".
+      iModIntro.
+      iMod ("Hcl" with "[$Hy Hx]") as "_".
+      { iNext. iRight. by iFrame. }
+      iApply (bin_log_related_seq with "[Hf]"); auto.
+      + iApply (bin_log_related_app with "Hf").
+        by rel_vals.
+      + 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.
+        iIntros "Hx".
+        rel_load_r.
+        iMod ("Hcl" with "[-]").
+        { iNext. iFrame. iRight; by iFrame. }
+        rel_vals; eauto.
+    - iMod ("Hcl" with "[$Hy Hx]") as "_".
+      { iNext. iRight. by iFrame. }
+      iApply (bin_log_related_seq with "[Hf]"); auto.
+      + iApply (bin_log_related_app with "Hf").
+        by rel_vals.
+      + 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.
+        iIntros "Hx".
+        rel_load_r.
+        iMod ("Hcl" with "[-]").
+        { iNext. iFrame. iRight; by iFrame. }
+        rel_vals; eauto.
+  Qed.
+
+End refinement.

theories/logrel/proofmode/tactics_rel.v

@@ -195,7 +195,7 @@ Tactic Notation "rel_pure_r" open_constr(ef) :=
       [reflexivity                 (* e = fill K e1 *)
       |apply _                     (* PureExec ϕ e1 e2 *)
       |try (exact I || reflexivity || tac_rel_done)  (* φ *)
-      |solve_ndisj                 (* ↑specN ⊆ E1 *)
+      |solve_ndisj  || fail "rel_pure_r: cannot solve ↑specN ⊆ ?"
       |simpl; reflexivity          (* eres = fill K e2 *)
       |simpl_subst/=               (* new goal *)])
   || fail "rel_pure_r: cannot find the reduct".