From 4357c43de4f47ee8586532d0df169eeaa6a8dced Mon Sep 17 00:00:00 2001
From: Gaurav Parthasarathy <gauravp@student.ethz.ch>
Date: Mon, 8 Jul 2019 16:49:36 +0200
Subject: [PATCH] formatting change and proof simplifcation due to Accepted
 state definition change

---
 theories/logatom/rdcss/rdcss.v | 12 ++++--------
 1 file changed, 4 insertions(+), 8 deletions(-)

diff --git a/theories/logatom/rdcss/rdcss.v b/theories/logatom/rdcss/rdcss.v
index 85a975a5..fe90d7a7 100644
--- a/theories/logatom/rdcss/rdcss.v
+++ b/theories/logatom/rdcss/rdcss.v
@@ -186,11 +186,9 @@ Section rdcss.
   (* After the prophecy said we are going to win the race, we commit and run the AU,
      switching from [pending] to [accepted]. *)
   Definition accepted_state Q (proph_winner : option proph_id) (p_ghost_winner : proph_id) :=
-    ((∃ vs, proph p_ghost_winner vs) ∗ Q ∗
-     match proph_winner with
-       None => True
-     | Some p => ⌜p = p_ghost_winner⌝
-     end)%I.
+    ((∃ vs, proph p_ghost_winner vs) ∗
+     Q ∗
+     ⌜match proph_winner with None => True | Some p => p = p_ghost_winner end⌝)%I.
 
   (* The same thread then wins the CmpXchg and moves from [accepted] to [done].
      Then, the [γ_t] token guards the transition to take out [Q].
@@ -463,9 +461,7 @@ Section rdcss.
         iModIntro. iMod "Hgc_close" as "_".
         (* close descr inv *)
         iModIntro. iSplitL "Q Hp_ghost Hp Hvs Hs Hln'".
-        { iModIntro. iNext. iExists _. iFrame "Hp". iLeft. iFrame.
-          iRight. iSplitL "Hp_ghost"; first by iExists _.
-          destruct (proph_extract_winner vs) eqn:Hvts; iFrame. }
+        { iModIntro. iNext. iExists _. iFrame "Hp". eauto 12 with iFrame. }
         (* close outer inv *)
         iModIntro. iSplitR "Token_a HQ Hn●".
         { by eauto 12 with iFrame. }
-- 
GitLab