Merge branch 'robbert' of bitbucket.org:Danya/iris-logrel

theories/examples/stack/refinement.v

@@ -84,13 +84,22 @@ Section Stack_refinement.
     inv stackN (sinv τi st st' l) -∗
     {⊤,⊤;τi::Δ;Γ} ⊨ (FG_pop $/ LitV (Loc st)) #() ≤log≤ (CG_locked_pop $/ LitV (Loc st') $/ LitV (Loc l)) #() : TSum TUnit (TVar 0).
   Proof.
+Transparent CG_locked_pop FG_pop CG_pop.
     iIntros "#Hinv".
-    Transparent CG_locked_pop FG_pop CG_pop.
-    unfold FG_pop, CG_locked_pop. unlock.
-    simpl_subst/=.
-    rel_rec_l.
-    rel_rec_r.
     iLöb as "IH".
+    rewrite {2}/FG_pop. unlock.  simpl_subst/=.
+
+replace ((rec: "pop" "st" <> :=
+             let: "stv" := ! "st" in
+             let: "x" := ! (Unfold "stv") in
+             match: "x" with
+               InjL <> => InjL #()
+             | InjR "x" =>
+               let: "y" := Fst "x" in let: "ys" := Snd "x" in if: CAS "st" "stv" "ys" then InjR "y" else ("pop" "st") #()
+             end))%E with
+(of_val FG_pop) by (by rewrite /FG_pop; unlock).
+
+    rel_rec_l.
     rel_load_l_atomic.
     iInv stackN as (istk v h) "[Hoe [Hst' [Hst [#HLK Hl]]]]" "Hclose".
     iExists _. iFrame.
@@ -103,6 +112,8 @@ Section Stack_refinement.
     iDestruct "HLK" as (istk2 w) "(% & Histk & HLK)". simplify_eq/=.
     iDestruct "HLK" as "[[% %] | HLK]"; simplify_eq/=.
     - (* The stack is empty *)
+      rewrite {2}/CG_locked_pop. unlock. simpl_subst/=.
+      rel_rec_r.
       rel_apply_r (bin_log_related_acquire_r with "Hl").
       { solve_ndisj. }
       iIntros "Hl /=".
@@ -160,6 +171,8 @@ Section Stack_refinement.
         iDestruct "HLK2" as "[[% %]|HLK2]"; simplify_eq/=.
         iDestruct "HLK2" as (ym1 ym2 zm1 zm2)
                               "[% [% [#Hrel #HLK2_tail]]]"; simplify_eq/=.
+        rewrite {2}/CG_locked_pop. unlock. simpl_subst/=.
+        rel_rec_r.
         rel_apply_r (bin_log_related_acquire_r with "Hl").
         { solve_ndisj. }
         iIntros "Hl /=".
@@ -191,8 +204,8 @@ Section Stack_refinement.
         iIntros (?). iNext. iIntros "Hst".
         rel_if_l.
         close_sinv "Hclose" "[Hoe Hst Hst' Hl HLK2]".
-        do 2 rel_rec_l.
-        by iApply "IH".
+        rel_rec_l.
+        iApply "IH".
   Qed.
 
   Lemma FG_CG_pop_refinement st st' (τi : D) l {τP : ∀ ww, PersistentP (τi ww)} Δ Γ :