Hack: Restructure FG_CG_pop_refinement to not unfold fixpoints.

theories/examples/stack/refinement.v

@@ -84,15 +84,32 @@ 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) : TArrow TUnit (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/=.
-    iApply bin_log_related_arrow; eauto.
-    iAlways. iIntros (? ?) "ZZ". simplify_eq/=. iClear "ZZ".
-    rel_rec_r.
-    rel_rec_l.
+    iApply bin_log_related_arrow_val; eauto.
+    { rewrite /FG_pop. unlock. eauto. }
+    { rewrite /CG_locked_pop. unlock. eauto. }
+    { rewrite /FG_pop. unlock. simpl_subst/=. eauto. }
+    { rewrite /CG_locked_pop. unlock. simpl_subst/=. eauto. }
+
+    iAlways. iIntros (? ?) "[% %]". simplify_eq/=.
     iLöb as "IH".
+
+
+    rewrite {2}/FG_pop {2}/CG_locked_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.
@@ -105,6 +122,7 @@ Section Stack_refinement.
     iDestruct "HLK" as (istk2 w) "(% & Histk & HLK)". simplify_eq/=.
     iDestruct "HLK" as "[[% %] | HLK]"; simplify_eq/=.
     - (* The stack is empty *)
+      rel_rec_r.
       rel_apply_r (bin_log_related_acquire_r with "Hl").
       { solve_ndisj. }
       iIntros "Hl /=".
@@ -162,6 +180,8 @@ Section Stack_refinement.
         iDestruct "HLK2" as "[[% %]|HLK2]"; simplify_eq/=.
         iDestruct "HLK2" as (ym1 ym2 zm1 zm2)
                               "[% [% [#Hrel #HLK2_tail]]]"; simplify_eq/=.
+
+        rel_rec_r.
         rel_apply_r (bin_log_related_acquire_r with "Hl").
         { solve_ndisj. }
         iIntros "Hl /=".
@@ -193,8 +213,9 @@ 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".
+        rewrite /FG_pop /CG_locked_pop. unlock. simpl_subst/=.
+        rel_rec_l.
+        iApply "IH".
   Qed.
 
   Lemma FG_CG_iter_refinement st st' (τi : D) l Δ {τP : ∀ ww, PersistentP (τi ww)} {SH : stackG Σ} Γ: