From 35308b0f55c83a0d2ddb2000e68c79e1737edb80 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 18 Jun 2018 14:07:55 +0200
Subject: [PATCH] Sequential triples with a persistent precondition and no
 initial quantifier are atomic

---
 theories/program_logic/atomic.v | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/theories/program_logic/atomic.v b/theories/program_logic/atomic.v
index 19f7da799..a42c58776 100644
--- a/theories/program_logic/atomic.v
+++ b/theories/program_logic/atomic.v
@@ -108,4 +108,18 @@ Section lemmas.
     (* FIXME: Using ssreflect rewrite does not work? *)
     rewrite ->!tele_app_bind. iIntros "HΦ". iApply "HΦ". done.
   Qed.
+
+  (* Sequential triples with a persistent precondition and no initial quantifier
+  are atomic. *)
+  Lemma seq_wp_atomic e Eo (α : [tele] → iProp) (β : [tele] → TB → iProp)
+        (f : [tele] → TB → val Λ) {HP : ∀.. x, Persistent (α x)} :
+    (∀ Φ, ∀.. x, α x -∗ (∀.. y, β x y -∗ Φ (f x y)) -∗ WP e {{ Φ }}) -∗
+    atomic_wp e Eo α β f.
+  Proof.
+    simpl in HP. iIntros "Hwp" (Q Φ) "HQ HΦ". iApply fupd_wp.
+    iMod ("HΦ") as "[#Hα [Hclose _]]". iMod ("Hclose" with "Hα") as "HΦ".
+    iApply wp_fupd. iApply ("Hwp" with "Hα"). iIntros "!>" (y) "Hβ".
+    iMod ("HΦ") as "[_ [_ Hclose]]". iMod ("Hclose" with "Hβ") as "HΦ".
+    rewrite ->!tele_app_bind. iApply "HΦ". done.
+  Qed.
 End lemmas.
-- 
GitLab