Move the related_arrow rule to relational_properties

F_mu_ref_conc/examples/bit.v

@@ -68,8 +68,8 @@ Section bit_refinement.
     simpl.
     iApply (bin_log_related_pack _ bitτi).
     repeat iApply bin_log_related_pair.
-    - iApply bin_log_related_arrow; try by unlock.
-      iAlways. iIntros ([v1 v2]) "/= #Hi".
+    - iApply bin_log_related_arrow_val; try by unlock.
+      iAlways. iIntros (v1 v2) "/= Hi".
       iDestruct "Hi" as (b) "[% %]"; simplify_eq.
       unlock.
       rel_rec_l.
@@ -77,8 +77,8 @@ Section bit_refinement.
       rel_op_r.
       rel_vals; destruct b; simpl; eauto.
     - unfold flip_nat.
-      iApply bin_log_related_arrow; try by unlock.
-      iAlways. iIntros ([v1 v2]) "/= #Hi".
+      iApply bin_log_related_arrow_val; try by unlock.
+      iAlways. iIntros (v1 v2) "/= #Hi".
       iDestruct "Hi" as (b) "[% %]"; simplify_eq.
       unlock.
       rel_rec_l.
@@ -157,8 +157,8 @@ Section heapify_refinement.
     { iNext. unfold interp_ref_inv. simpl.
       iExists (init1,init2). simpl. by iFrame. }
     repeat iApply bin_log_related_pair.
-    - iApply bin_log_related_arrow; try by unlock.
-      iAlways. iIntros ([v1 v2]) "/= #Hi".
+    - iApply bin_log_related_arrow_val; try by unlock.
+      iAlways. iIntros (v1 v2) "/= #Hi".
       iDestruct "Hi" as "[% %]"; simplify_eq.
       rel_rec_l.
       rel_rec_r.
@@ -174,8 +174,8 @@ Section heapify_refinement.
       iIntros (vvs ρ) "Hspec HΓ /=". unfold env_subst.
       rewrite !Closed_subst_p_id.
       iApply "Hview".
-    - iApply bin_log_related_arrow; try by unlock.
-      iAlways. iIntros ([v1 v2]) "/= #Hi".
+    - iApply bin_log_related_arrow_val; try by unlock.
+      iAlways. iIntros (v1 v2) "/= #Hi".
       iDestruct "Hi" as "[% %]"; simplify_eq.
       rel_rec_l.
       rel_rec_r.

F_mu_ref_conc/examples/counter.v

@@ -204,13 +204,13 @@ Section CG_Counter.
     {⊤,⊤;Δ;Γ} ⊨ FG_increment $/ LocV cnt ≤log≤ CG_increment $/ LocV cnt' $/ LocV l : TArrow TUnit TUnit.
   Proof.
     iIntros "#Hinv".
-    iApply bin_log_related_arrow.
+    iApply bin_log_related_arrow_val.
     { unfold FG_increment. unlock; simpl_subst. reflexivity. }
     { unfold CG_increment. unlock; simpl_subst. reflexivity. }
     { unfold FG_increment. unlock; simpl_subst/=. solve_closed. (* TODO: add a clause to the reflection mechanism that reifies a [lambdasubst] expression as a closed one *) }
     { unfold CG_increment. unlock; simpl_subst/=. solve_closed. }
 
-    iAlways. iIntros ([v v']) "[% %]"; simpl in *; subst.
+    iAlways. iIntros (v v') "[% %]"; simpl in *; subst.
     iApply (bin_log_FG_increment_logatomic (fun n => (l ↦ₛ (#♭v false)) ∗ cnt' ↦ₛ #nv n)%I _ _ _ [] cnt with "[Hinv]").
     iAlways.
     iInv counterN as ">Hcnt" "Hcl". iModIntro.
@@ -235,12 +235,12 @@ Section CG_Counter.
     {⊤,⊤;Δ;Γ} ⊨ counter_read $/ LocV cnt ≤log≤ counter_read $/ LocV cnt' : TArrow TUnit TNat.
   Proof.
     iIntros "#Hinv".
-    iApply bin_log_related_arrow.
+    iApply bin_log_related_arrow_val.
     { unfold counter_read. unlock. simpl. reflexivity. }
     { unfold counter_read. unlock. simpl. reflexivity. }
     { unfold counter_read. unlock. simpl. solve_closed. }
     { unfold counter_read. unlock. simpl. solve_closed. }
-    iAlways. iIntros ([v v']) "[% %]"; simpl in *; subst.
+    iAlways. iIntros (v v') "[% %]"; simpl in *; subst.
     iApply (bin_log_counter_read_atomic_l (fun n => (l ↦ₛ (#♭v false)) ∗ cnt' ↦ₛ #nv n)%I _ _ _ [] cnt with "[Hinv]").
     iAlways. iInv counterN as (n) "[>Hl [>Hcnt >Hcnt']]" "Hclose". 
     iModIntro. 
@@ -263,7 +263,7 @@ Section CG_Counter.
   Proof.
     unfold FG_counter, CG_counter.
     iApply bin_log_related_arrow; try by (unlock; eauto).
-    iAlways. iIntros ([? ?]) "/= [% %]"; simplify_eq/=.
+    iAlways. iIntros (? ?) "/= ?"; simplify_eq/=.
     unlock. rel_rec_l. rel_rec_r.
     rel_apply_r bin_log_related_newlock_r; auto.
     iIntros (l) "Hl".

F_mu_ref_conc/examples/stack/refinement.v

@@ -92,7 +92,7 @@ Section Stack_refinement.
     unfold FG_pop, CG_locked_pop. unlock.
     simpl_subst/=.
     iApply bin_log_related_arrow; eauto.
-    iAlways. iIntros ([? ?]) "[% %]". simplify_eq/=.
+    iAlways. iIntros (? ?) "ZZ". simplify_eq/=. iClear "ZZ".
     rel_rec_r.
     rel_rec_l.
     iLöb as "IH".
@@ -195,9 +195,9 @@ Section Stack_refinement.
         iSplitL; last by (iIntros (?); congruence).
         iIntros (?). iNext. iIntros "Hst".
         rel_if_l.
-        close_sinv "Hclose" "[-]".
+        close_sinv "Hclose" "[Hoe Hst Hst' Hl HLK2]".
         do 2 rel_rec_l.
-        iApply "IH".
+        by iApply "IH".
   Qed.
 
   Lemma FG_CG_iter_refinement st st' (τi : D) l Δ {τP : ∀ ww, PersistentP (τi ww)} {SH : stackG Σ} Γ:
@@ -208,8 +208,8 @@ Section Stack_refinement.
     Transparent FG_read_iter CG_snap_iter.
     unfold FG_read_iter, CG_snap_iter. unlock.
     simpl_subst/=.
-    iApply bin_log_related_arrow; eauto.
-    iAlways. iIntros ([f1 f2]) "#Hff /=".
+    iApply bin_log_related_arrow_val; eauto.
+    iAlways. iIntros (f1 f2) "#Hff /=".
     rel_rec_r.
     rel_rec_l.
     Transparent FG_iter CG_iter. unlock FG_iter CG_iter.
@@ -281,12 +281,11 @@ Section Stack_refinement.
       rel_rec_l.
       rel_snd_l.
       rel_rec_l.
-      close_sinv "Hclose" "[Hoe Hst' Hst Hl HLK]".
-      iSpecialize ("Hff" $! (y1,y2) with "Hτ").
+      close_sinv "Hclose" "[Hoe Hst' Hst Hl HLK]".      
       simpl.
-      iApply (bin_log_related_app _ _ _ _ _ _ _ TUnit). (* TODO: abbreivate this as related_let *)
+      iApply (bin_log_related_app _ _ _ _ _ _ _ TUnit with "[] [Hτ]"). (* TODO: abbreivate this as related_let *)
       + iApply bin_log_related_arrow; eauto.
-        iAlways. iIntros ([? ?]) "[% %]"; simplify_eq/=.
+        iAlways. iIntros (? ?) "?"; simplify_eq/=.
         rel_rec_l.
         rel_rec_l.
         rel_rec_r.
@@ -297,8 +296,10 @@ Section Stack_refinement.
         iDestruct "HLK_tail" as (? ?) "[% [? HLK_tail]]"; simplify_eq/=.
         by iApply "IH".
       + clear.
-        iClear "IH Histk HLK_tail HLK HLK' Hτ".
-        iApply (related_ret with "[Hff]"). done.
+        iClear "IH Histk HLK_tail HLK HLK'".
+        iSpecialize ("Hff" $! (y1,y2) with "Hτ").
+        iApply (related_ret with "[Hff]"). 
+        done.
   Qed.
 End Stack_refinement.
 
@@ -377,8 +378,8 @@ Section Full_refinement.
     repeat rel_rec_r.
 
     repeat iApply bin_log_related_pair.
-    - iApply bin_log_related_arrow; eauto.
-      iAlways. iIntros ([v1 v2]) "#Hτ /=".
+    - iApply bin_log_related_arrow_val; eauto.
+      iAlways. iIntros (v1 v2) "#Hτ /=".
       replace_l ((FG_push $/ LocV st) v1)%E.
       { unlock FG_push. simpl_subst/=. reflexivity. }
       replace_r ((CG_locked_push $/ LocV st' $/ LocV l) v2)%E.

F_mu_ref_conc/hax.v

@@ -17,39 +17,6 @@ Section hax.
   Notation D := (prodC valC valC -n> iProp Σ).
   Implicit Types Δ : listC D.
 
-  Lemma bin_log_related_arrow Δ Γ E (f x f' x' : binder) (e e' eb eb' : expr) (τ τ' : type) :
-    e = (rec: f x := eb)%E →
-    e' = (rec: f' x' := eb')%E →
-    Closed ∅ e →
-    Closed ∅ e' →
-    □(∀ vv, ⟦ τ ⟧ Δ vv -∗
-      {⊤,⊤;Δ;Γ} ⊨ App e (of_val (vv.1)) ≤log≤ App e' (of_val (vv.2)) : τ') -∗
-    {E,E;Δ;Γ} ⊨ e ≤log≤ e' : TArrow τ τ'.
-  Proof.
-    iIntros (????) "#H".
-    subst e e'.
-    rewrite bin_log_related_eq.
-    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj".
-    cbn-[subst_p].
-    iModIntro.
-    rewrite {2}/env_subst Closed_subst_p_id.
-    iApply wp_value.
-    { simpl. erewrite decide_left. done. }
-    rewrite /env_subst Closed_subst_p_id.
-    iExists (RecV f' x' eb').
-    iFrame "Hj". iAlways. iIntros (vv) "Hvv".
-    iSpecialize ("H" $! vv with "Hvv Hs []").
-    { iAlways. iApply "HΓ". }    
-    Unshelve. all: trivial.
-    assert (Closed ∅ ((rec: f x := eb) (vv.1))%E).
-    { unfold Closed in *. simpl.
-      intros. split_and?; auto. apply of_val_closed. }
-    assert (Closed ∅ ((rec: f' x' := eb') (vv.2))%E).
-    { unfold Closed in *. simpl.
-      intros. split_and?; auto. apply of_val_closed. }
-    rewrite /env_subst. rewrite !Closed_subst_p_id. done.
-  Qed.
-
   Lemma weird_bind e Q :
     WP App e tt {{ Q }} ⊢ WP e {{ v, WP (App v tt) {{ Q }} }}.
   Proof.

F_mu_ref_conc/relational_properties.v

@@ -68,25 +68,53 @@ Section properties.
     iModIntro. iApply wp_value; eauto.
   Qed.
 
-  Lemma bin_log_related_spec_ctx Δ Γ E1 E2 e e' τ ℶ :
-    (ℶ ⊢ (∃ ρ, spec_ctx ρ) -∗ {E1,E2;Δ;Γ} ⊨ e ≤log≤ e' : τ)%I →
-    (ℶ ⊢ {E1,E2;Δ;Γ} ⊨ e ≤log≤ e' : τ)%I.
-  Proof.
-    intros Hp.
-    rewrite bin_log_related_eq /bin_log_related_def.
-    iIntros "Hctx". iIntros (vvs ρ') "#Hspec".
-    rewrite (persistentP (spec_ctx _)).
-    rewrite (uPred.always_sep_dup' (spec_ctx _)).
-    iDestruct "Hspec" as "#[Hspec #Hspec']".
-    iRevert "Hspec'".
-    rewrite (uPred.always_elim (spec_ctx _)).
-    iAssert (∃ ρ, spec_ctx ρ)%I as "Hρ".
-    { eauto. }
-    iClear "Hspec".
-    iRevert (vvs ρ').
-    fold (bin_log_related_def E1 E2 Δ Γ e e' τ).
-    rewrite -bin_log_related_eq.
-    iApply (Hp with "Hctx Hρ").
+  Lemma bin_log_related_arrow_val Δ Γ E (f x f' x' : binder) (e e' eb eb' : expr) (τ τ' : type) :
+    e = (rec: f x := eb)%E →
+    e' = (rec: f' x' := eb')%E →
+    Closed ∅ e →
+    Closed ∅ e' →
+    □(∀ v1 v2, ⟦ τ ⟧ Δ (v1, v2) -∗
+      {⊤,⊤;Δ;Γ} ⊨ App e (of_val v1) ≤log≤ App e' (of_val v2) : τ') -∗
+    {E,E;Δ;Γ} ⊨ e ≤log≤ e' : TArrow τ τ'.
+  Proof.
+    iIntros (????) "#H".
+    subst e e'.
+    rewrite bin_log_related_eq.
+    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj".
+    cbn-[subst_p].
+    iModIntro.
+    rewrite {2}/env_subst Closed_subst_p_id.
+    iApply wp_value.
+    { simpl. erewrite decide_left. done. }
+    rewrite /env_subst Closed_subst_p_id.
+    iExists (RecV f' x' eb').
+    iFrame "Hj". iAlways. iIntros ([v1 v2]) "Hvv".
+    iSpecialize ("H" $! v1 v2 with "Hvv Hs []").
+    { iAlways. iApply "HΓ". }    
+    assert (Closed ∅ ((rec: f x := eb) v1)%E).
+    { unfold Closed in *. simpl.
+      intros. split_and?; auto. apply of_val_closed. }
+    assert (Closed ∅ ((rec: f' x' := eb') v2)%E).
+    { unfold Closed in *. simpl.
+      intros. split_and?; auto. apply of_val_closed. }
+    rewrite /env_subst. rewrite !Closed_subst_p_id. done.
+  Qed.
+
+  Lemma bin_log_related_arrow Δ Γ E (f x f' x' : binder) (f1 f2 eb eb' : expr) (τ τ' : type) :
+    f1 = (rec: f x := eb)%E →
+    f2 = (rec: f' x' := eb')%E →
+    Closed ∅ f1 →
+    Closed ∅ f2 →
+    □(∀ (v1 v2 : val), {⊤,⊤;Δ;Γ} ⊨ v1 ≤log≤ v2 : τ -∗
+      {⊤,⊤;Δ;Γ} ⊨ f1 v1 ≤log≤ f2 v2 : τ') -∗
+    {E,E;Δ;Γ} ⊨ f1 ≤log≤ f2 : TArrow τ τ'.
+  Proof.
+    iIntros (????) "#H".
+    iApply bin_log_related_arrow_val; eauto.
+    iAlways. iIntros (v1 v2) "Hvv".
+    iApply "H".
+    iApply (related_ret ⊤).
+    by iApply interp_ret.
   Qed.
 
   (** ** Reductions on the left *)