Cleanup

theories/examples/stack/module_refinement.v

@@ -16,49 +16,6 @@ Section Mod_refinement.
 
   Instance sint_persistent `{logrelG Σ, stackPreG Σ} τi vv : PersistentP (sint τi vv).
   Proof. apply _. Qed.
-
-  Lemma interp_subst_up_2 Δ1 Δ2 τ τi :
-    ⟦ τ ⟧ (Δ1 ++ Δ2) ≡ ⟦ τ.[upn (length Δ1) (ren (+1))] ⟧ (Δ1 ++ τi :: Δ2).
-  Proof.
-    revert Δ1 Δ2. induction τ => Δ1 Δ2; simpl; eauto.
-    - intros vv; simpl; properness; eauto. by apply IHτ1. by apply IHτ2.
-    - intros vv; simpl; properness; eauto. by apply IHτ1. by apply IHτ2.
-    - unfold interp_expr. intros vv; simpl; properness; eauto. by apply IHτ1. by apply IHτ2.
-    - apply fixpoint_proper=> τ' ww /=.
-      properness; auto. apply (IHτ (_ :: _)).
-    - intros vv; simpl.
-      rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl; properness.
-      { by rewrite !lookup_app_l. }
-      rewrite !lookup_app_r; [|lia ..].
-      assert ((length Δ1 + S (x - length Δ1) - length Δ1) = S (x - length Δ1)) as Hwat.
-      { lia. }
-      rewrite Hwat. simpl. done.
-    - unfold interp_expr.
-      intros vv; simpl; properness; auto. apply (IHτ (_ :: _)).
-    - intros vv; simpl; properness; auto. apply (IHτ (_ :: _)).
-    - intros vv; simpl; properness; auto. by apply IHτ.
-  Qed.
-  Lemma interp_subst_2 τ τi Δ :
-    ⟦ τ ⟧ Δ ≡ ⟦ τ.[ren (+1)] ⟧ (τi :: Δ).
-  Proof. by apply (interp_subst_up_2 []). Qed.
-
-  Lemma bin_log_weaken_2 τi Δ Γ e1 e2 τ :
-    {⊤,⊤;Δ;Γ} ⊨ e1 ≤log≤ e2 : τ -∗
-    {⊤,⊤;τi::Δ;Autosubst_Classes.subst (ren (+1)) <$>Γ} ⊨ e1 ≤log≤ e2 : τ.[ren (+1)].
-  Proof.
-    rewrite bin_log_related_eq /bin_log_related_def.
-    iIntros "Hlog" (vvs ρ) "#Hs #HΓ".
-    iSpecialize ("Hlog" $! vvs with "Hs [HΓ]").
-    { by rewrite interp_env_ren. }
-    unfold interp_expr.
-    iIntros (j K) "Hj /=".
-    iMod ("Hlog" with "Hj") as "Hlog".
-    iApply (wp_mono with "Hlog").
-    iIntros (v). simpl.
-    iDestruct 1 as (v') "[Hj Hτ]".
-    iExists v'. iFrame.
-    by rewrite -interp_subst_2.
-  Qed.
   
   Lemma module_refinement `{SPG : stackPreG Σ} Δ Γ :
     {⊤,⊤;Δ;Γ} ⊨ FG_stack.stackmod ≤log≤ CG_stack.stackmod : TForall $ TExists $ TProd (TProd
@@ -115,7 +72,7 @@ Section Mod_refinement.
       { unlock CG_locked_pop. simpl_subst/=. reflexivity. }
       replace (TSum TUnit (TVar 1))
       with (TSum TUnit (TVar 0)).[ren (+1)] by done.
-      iApply bin_log_weaken_2.
+      iApply bin_log_related_weaken_2.
       pose (SG := StackG Σ _ γ).
       change γ with stack_name.
       iApply (FG_CG_pop_refinement' (stackN.@(stk,stk'))).

theories/logrel/logrel_binary.v

@@ -199,6 +199,24 @@ Section related_facts.
     iMod "HP". iApply ("HI" with "HP").
   Qed.
 
+  Lemma bin_log_related_weaken_2 τi Δ Γ e1 e2 τ :
+    {⊤,⊤;Δ;Γ} ⊨ e1 ≤log≤ e2 : τ -∗
+    {⊤,⊤;τi::Δ;Autosubst_Classes.subst (ren (+1)) <$>Γ} ⊨ e1 ≤log≤ e2 : τ.[ren (+1)].
+  Proof.
+    rewrite bin_log_related_eq /bin_log_related_def.
+    iIntros "Hlog" (vvs ρ) "#Hs #HΓ".
+    iSpecialize ("Hlog" $! vvs with "Hs [HΓ]").
+    { by rewrite interp_env_ren. }
+    unfold interp_expr.
+    iIntros (j K) "Hj /=".
+    iMod ("Hlog" with "Hj") as "Hlog".
+    iApply (wp_mono with "Hlog").
+    iIntros (v). simpl.
+    iDestruct 1 as (v') "[Hj Hτ]".
+    iExists v'. iFrame.
+    by rewrite -interp_ren.
+  Qed.
+
 End related_facts.
 
 (** Monadic-like operations on logrel *)

theories/logrel/semtypes.v

@@ -218,6 +218,32 @@ Section semtypes.
     apply interp_subst.
   Qed.
 
+  Lemma interp_ren_up Δ1 Δ2 E τ τi :
+    interp E E τ (Δ1 ++ Δ2) ≡ interp E E (τ.[upn (length Δ1) (ren (+1))]) (Δ1 ++ τi :: Δ2).
+  Proof.
+    revert E Δ1 Δ2. induction τ => E Δ1 Δ2; simpl; eauto.
+    - intros vv; simpl; properness; eauto. by apply IHτ1. by apply IHτ2.
+    - intros vv; simpl; properness; eauto. by apply IHτ1. by apply IHτ2.
+    - unfold interp_expr. intros vv; simpl; properness; eauto. by apply IHτ1. by apply IHτ2.
+    - apply fixpoint_proper=> τ' ww /=.
+      properness; auto. apply (IHτ _ (_ :: _)).
+    - intros vv; simpl.
+      rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl; properness.
+      { by rewrite !lookup_app_l. }
+      rewrite !lookup_app_r; [|lia ..].
+      assert ((length Δ1 + S (x - length Δ1) - length Δ1) = S (x - length Δ1)) as Hwat.
+      { lia. }
+      rewrite Hwat. simpl. done.
+    - unfold interp_expr.
+      intros vv; simpl; properness; auto. apply (IHτ _ (_ :: _)).
+    - intros vv; simpl; properness; auto. apply (IHτ _ (_ :: _)).
+    - intros vv; simpl; properness; auto. by apply IHτ.
+  Qed.
+
+  Lemma interp_ren τ τi E Δ :
+    interp E E τ Δ ≡ interp E E (τ.[ren (+1)]) (τi :: Δ).
+  Proof. by apply (interp_ren_up []). Qed.
+
   Lemma interp_EqType_agree τ v v' E1 E2 Δ :
     EqType τ → interp E1 E2 τ Δ (v, v') ⊢ ⌜v = v'⌝.
   Proof.