Separate out the `counter_read_refinement` proof.

F_mu_ref_conc/examples/counter.v

@@ -380,6 +380,31 @@ Section CG_Counter.
       iApply bin_log_related_unit.
   Qed.
 
+  Lemma counter_read_refinement l cnt cnt' Γ :
+    inv counterN (counter_inv l cnt cnt') -∗
+    Γ ⊨ counter_read #cnt ≤log≤ counter_read #cnt' : TArrow TUnit TNat.
+  Proof.
+    iIntros "#Hinv".
+    Transparent counter_read.
+    unfold counter_read. unlock.
+    iApply (bin_log_related_rec_r _ _ _ []); auto. simpl.
+    iApply (bin_log_related_rec_l _ _ []); auto. simpl. iNext.      
+    iApply bin_log_related_rec; simpl. iAlways. cbn.
+    iApply (bin_log_related_load_l _ _ _ []).
+    iInv counterN as (n) "[>Hl [Hcnt >Hcnt']]" "Hclose". 
+    iModIntro. 
+    iExists (#nv n). iFrame "Hcnt".
+    iIntros "Hcnt". simpl.
+    iApply (bin_log_related_load_r _ [] with "[Hcnt']"); auto.
+    { solve_ndisj. }
+    iIntros "Hcnt'".
+    iMod ("Hclose" with "[Hl Hcnt Hcnt']").
+    { iNext. iExists _. by iFrame. }
+    simpl.
+    iApply (bin_log_related_val); auto.
+    intros. simpl. eauto.
+  Qed.
+  
   Lemma FG_CG_counter_refinement :
     ∅ ⊨ FG_counter ≤log≤ CG_counter : TProd (TArrow TUnit TUnit) (TArrow TUnit TNat).
   Proof.
@@ -413,26 +438,9 @@ Section CG_Counter.
     iApply (bin_log_related_rec_r _ _ _ []); auto. 
     rewrite /= !Closed_subst_id /=.
     
-    iApply (bin_log_related_pair _ with "[]"); last first.
-    - Transparent counter_read.
-      unfold counter_read. unlock.
-      iApply (bin_log_related_rec_r _ _ _ []); auto. simpl.
-      iApply (bin_log_related_rec_l _ _ []); auto. simpl. iNext.      
-      iApply bin_log_related_rec; simpl. iAlways. cbn.
-      iApply (bin_log_related_load_l _ _ _ []).
-      iInv counterN as (n) "[>Hl [Hcnt >Hcnt']]" "Hclose". 
-        iModIntro. 
-        iExists (#nv n). iFrame "Hcnt".
-        iIntros "Hcnt". simpl.
-      iApply (bin_log_related_load_r _ [] with "[Hcnt']"); auto.
-        { solve_ndisj. }
-      iIntros "Hcnt'".
-      iMod ("Hclose" with "[Hl Hcnt Hcnt']").
-      { iNext. iExists _. by iFrame. }
-      simpl.
-      iApply (bin_log_related_val); auto.
-      intros. simpl. eauto.
-   - iApply (FG_CG_increment_refinement with "Hinv").
+    iApply (bin_log_related_pair _ with "[]").
+    - iApply (FG_CG_increment_refinement with "Hinv").
+    - iApply (counter_read_refinement with "Hinv").
   Qed.
 
 End CG_Counter.