From eae9c2c89311bdd1d9ce0a5a02cc677abcc5922e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 25 Mar 2020 16:01:15 +0100
Subject: [PATCH] Prove stepping (i.e., non-value) version of `atomic_wp_seq`.

---
 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 401d690a2..c035e92bc 100644
--- a/theories/program_logic/atomic.v
+++ b/theories/program_logic/atomic.v
@@ -118,6 +118,20 @@ Section lemmas.
     rewrite ->!tele_app_bind. iIntros "HΦ". iApply "HΦ". done.
   Qed.
 
+  (** This version matches the Texan triple, i.e., with a later in front of the
+  [(∀.. y, β x y -∗ Φ (f x y))]. *)
+  Lemma atomic_wp_seq_step e Eo α β f {HL : ∀.. x, Laterable (α x)} :
+    TCEq (to_val e) None →
+    atomic_wp e Eo α β f -∗
+    ∀ Φ, ∀.. x, α x -∗ ▷ (∀.. y, β x y -∗ Φ (f x y)) -∗ WP e {{ Φ }}.
+  Proof.
+    iIntros (?) "H"; iIntros (Φ x) "Hα HΦ".
+    iApply (wp_step_fupd _ _ ⊤ _ (∀.. y : TB, β x y -∗ Φ (f x y))
+      with "[$HΦ //]"); first done.
+    iApply (atomic_wp_seq with "H Hα"); first done.
+    iIntros (y) "Hβ HΦ". by iApply "HΦ".
+  Qed.
+
   (* Sequential triples with the empty mask for a physically atomic [e] are atomic. *)
   Lemma atomic_seq_wp_atomic e Eo α β f `{!Atomic WeaklyAtomic e} :
     (∀ Φ, ∀.. x, α x -∗ (∀.. y, β x y -∗ Φ (f x y)) -∗ WP e @ ∅ {{ Φ }}) -∗
-- 
GitLab