From 360d8ac0d044fcc0a410bc041b482faf051f1293 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 9 Jun 2018 11:56:27 +0200
Subject: [PATCH] Prove that atomic triples imply "normal" triples

---
 theories/bi/lib/atomic.v        |  4 ++--
 theories/program_logic/atomic.v | 20 ++++++++++++++++++++
 2 files changed, 22 insertions(+), 2 deletions(-)

diff --git a/theories/bi/lib/atomic.v b/theories/bi/lib/atomic.v
index 3ee47bfb0..bca0f2a1c 100644
--- a/theories/bi/lib/atomic.v
+++ b/theories/bi/lib/atomic.v
@@ -1,5 +1,5 @@
-From iris.bi Require Export bi updates.
-From iris.bi.lib Require Import fixpoint laterable.
+From iris.bi Require Export bi updates laterable.
+From iris.bi.lib Require Import fixpoint.
 From stdpp Require Import coPset namespaces.
 From iris.proofmode Require Import coq_tactics tactics reduction.
 Set Default Proof Using "Type".
diff --git a/theories/program_logic/atomic.v b/theories/program_logic/atomic.v
index 75d33c763..56039b128 100644
--- a/theories/program_logic/atomic.v
+++ b/theories/program_logic/atomic.v
@@ -1,3 +1,4 @@
+From stdpp Require Import namespaces.
 From iris.program_logic Require Export weakestpre.
 From iris.proofmode Require Import tactics classes.
 From iris.bi.lib Require Export atomic.
@@ -90,3 +91,22 @@ Notation "'<<<' α '>>>' e @ Eo '<<<' β , 'RET' v '>>>'" :=
   (at level 20, Eo, α, β, v at level 200,
    format "'[hv' '<<<'  α  '>>>'  '/  ' e  @  Eo  '/' '[    ' '<<<'  β ,  '/' 'RET'  v  '>>>' ']' ']'")
   : stdpp_scope.
+
+(** Theory *)
+Section lemmas.
+  Context `{irisG Λ Σ} {TA TB : tele}.
+  Notation iProp := (iProp Σ).
+  Implicit Types (α : TA → iProp) (β : TA → TB → iProp) (f : TA → TB → val Λ).
+
+  Lemma atomic_wp_seq e Eo α β f {HL : ∀.. x, Laterable (α x)} :
+    atomic_wp e Eo α β f -∗
+    ∀ Φ, ∀.. x, α x -∗ (∀.. y, β x y -∗ Φ (f x y)) -∗ WP e {{ Φ }}.
+  Proof.
+    rewrite ->tforall_forall in HL.
+    iIntros "Hwp" (Φ x) "Hα HΦ". iApply ("Hwp" with "[HΦ]"); first iAccu.
+    iAuIntro. iApply (aacc_intro with "Hα"); first solve_ndisj.
+    iSplit; first by eauto. iIntros (y) "Hβ !>".
+    (* FIXME: Using ssreflect rewrite does not work? *)
+    rewrite ->!tele_app_bind. iIntros "HΦ". iApply "HΦ". done.
+  Qed.
+End lemmas.
-- 
GitLab