From 908a83a4ce62d9804219674cfa34131806530de1 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Wed, 2 Nov 2016 09:40:34 +0100
Subject: [PATCH] simplify atomic triples as suggested by Robbert

---
 atomic.v      | 4 ++--
 atomic_incr.v | 4 ++--
 atomic_sync.v | 6 +++---
 peritem.v     | 4 ++--
 4 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/atomic.v b/atomic.v
index ee42b90..be3168a 100644
--- a/atomic.v
+++ b/atomic.v
@@ -18,6 +18,6 @@ Section atomic.
     (∀ P Q, (P ={Eo, Ei}=> ∃ x:A,
                        α x ★
                        ((α x ={Ei, Eo}=★ P) ∧
-                        (∀ v, β x v ={Ei, Eo}=★ Q x v))
-     ) -★ {{ P }} e @ ⊤ {{ v, (∃ x: A, Q x v) }})%I.
+                        (∀ v, β x v ={Ei, Eo}=★ Q v))
+     ) -★ {{ P }} e @ ⊤ {{ Q }})%I.
 End atomic.
diff --git a/atomic_incr.v b/atomic_incr.v
index 9b17c02..6e5dbba 100644
--- a/atomic_incr.v
+++ b/atomic_incr.v
@@ -46,7 +46,7 @@ Section incr.
       iSpecialize ("Hvs'" $! #x').
       wp_cas_suc.
       iMod ("Hvs'" with "[Hl]") as "HQ"; first by iFrame.
-      iModIntro. wp_if. by iExists x'.
+      iModIntro. wp_if. done.
     - iDestruct "Hvs'" as "[Hvs' _]".
       wp_cas_fail.
       iMod ("Hvs'" with "[Hl]") as "HP"; first by iFrame.
@@ -80,7 +80,7 @@ Section user.
     (* prove worker triple *)
     iDestruct (incr_atomic_spec N l with "Hh") as "Hincr"=>//.
     rewrite /incr_triple /atomic_triple.
-    iSpecialize ("Hincr"  $! True%I (fun _ _ => True%I) with "[]").
+    iSpecialize ("Hincr"  $! True%I (fun _ => True%I) with "[]").
     - iIntros "!# _".
       (* open the invariant *)
       iInv N as (x') ">Hl'" "Hclose".
diff --git a/atomic_sync.v b/atomic_sync.v
index 0466de9..02c6b22 100644
--- a/atomic_sync.v
+++ b/atomic_sync.v
@@ -57,9 +57,9 @@ Section atomic_sync.
     iIntros (f). iApply wp_wand_r. iSplitR; first by iApply "Hsyncer".
     iIntros (f') "#Hsynced {Hsyncer}".
     iAlways. iIntros (α β x) "#Hseq".
-    iIntros (P Q) "#Hvss !# HP". 
+    iIntros (P Q) "#Hvss !# HP".
     (* TODO: Why can't I iApply "Hsynced"? *)
-    iSpecialize ("Hsynced" $! P (fun v => ∃ x, Q x v)%I x).
+    iSpecialize ("Hsynced" $! P Q x).
     iApply wp_wand_r. iSplitL "HP".
     - iApply ("Hsynced" with "[]")=>//.
       iAlways. iIntros "[HR HP]". iDestruct "HR" as (g) "[HÏ• Hg1]".
@@ -81,7 +81,7 @@ Section atomic_sync.
         apply cmra_update_exclusive. by rewrite pair_op dec_agree_idemp. }
       iMod ("Hvs2" with "[Hg1 Hβ]").
       { iExists g'. iFrame. }
-      iModIntro. iSplitL "Hg2 HÏ•'"; last by iExists g''.
+      iModIntro. iSplitL "Hg2 HÏ•'"; last done.
       iExists g'. by iFrame.
     - iIntros (?) "?". done.
   Qed.
diff --git a/peritem.v b/peritem.v
index f58658e..ce12b47 100644
--- a/peritem.v
+++ b/peritem.v
@@ -133,7 +133,7 @@ Lemma new_stack_spec' Φ RI:
   Proof.
     iIntros (HN) "(#Hh & HRx & #? & HΦ)".
     iDestruct (push_atomic_spec N s x with "Hh") as "Hpush"=>//.
-    iSpecialize ("Hpush" $! (R x) (fun _ ret => (∃ hd, evs γ hd x) ★ ret = #())%I with "[]").
+    iSpecialize ("Hpush" $! (R x) (fun ret => (∃ hd, evs γ hd x) ★ ret = #())%I with "[]").
     - iIntros "!# Rx".
       (* open the invariant *)
       iInv N as "[IH1 ?]" "Hclose".
@@ -180,7 +180,7 @@ Lemma new_stack_spec' Φ RI:
         iModIntro. iSplitL; last auto. by iExists hd'.
     - iApply wp_wand_r. iSplitL "HRx Hpush".
       + by iApply "Hpush".
-      + iIntros (?) "H". iDestruct "H" as (_) "[? %]". subst.
+      + iIntros (?) "[? %]". subst.
         by iApply "HΦ".
   Qed.
 
-- 
GitLab