Addressing review comments

theories/logrel/examples/compute_list_par.v

@@ -79,7 +79,7 @@ Section compute_example.
               (lty_chan compute_type_service → ())%lty);
       [ iApply env_le_refl | iApply lty_le_copy_elim | iApply env_le_refl | ].
     iApply ltyped_val_ltyped.
-    iApply ltyped_rec_val.
+    iApply ltyped_val_rec.
     iApply ltyped_post_nil.
     iApply ltyped_app.
     { iApply (ltyped_lam []). iApply ltyped_post_nil. iApply ltyped_unit. }
@@ -256,7 +256,7 @@ Section compute_example.
       { iApply iProto_le_trans.
         { iApply iProto_le_app; [ iApply iProto_le_refl | ].
           iApply compute_type_client_unfold_app_stop. }
-        rewrite lsty_car_app.
+        rewrite -lsty_car_app.
         iApply lsty_car_mono.
         iApply lty_napp_swap.
         iApply recv_type_stop_type_swap. }
@@ -267,7 +267,7 @@ Section compute_example.
         iSplitL "Hf".
         - iRight. iFrame "Hf". done.
         - rewrite lookup_total_insert.
-          rewrite lsty_car_app lty_app_end_l lty_app_end_r.
+          rewrite -lsty_car_app lty_app_end_l lty_app_end_r.
           iFrame "Hcounter Hc". }
       iIntros "_". wp_pures. iApply "HΦ". iFrame "Hl Hlk Hsf". }
     wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl".
@@ -282,7 +282,7 @@ Section compute_example.
       rewrite assoc. rewrite assoc. rewrite assoc.
       iApply iProto_le_app; [ | iApply iProto_le_refl ].
       iApply iProto_le_app; [ | iApply iProto_le_refl ].
-      rewrite lsty_car_app.
+      rewrite -lsty_car_app.
       iApply lsty_car_mono.
       iApply lty_napp_swap.
       iApply recv_type_cont_type_swap. }
@@ -299,7 +299,7 @@ Section compute_example.
       rewrite assoc.
       rewrite left_id.
       rewrite assoc.
-      repeat rewrite lsty_car_app.
+      repeat rewrite -lsty_car_app.
       rewrite -lty_napp_S_r.
       rewrite Nat.add_succ_r.
       rewrite -plus_n_O.
@@ -374,7 +374,7 @@ Section compute_example.
                            ref_uniq (lty_list A).
   Proof.
     iApply ltyped_val_ltyped.
-    iApply ltyped_lam_val=> //.
+    iApply ltyped_val_lam=> //.
     iApply ltyped_post_nil.
     iApply (ltyped_lam [EnvItem "xs" _]).
     iIntros "!>" (vs) "HΓ". simpl.
@@ -467,8 +467,7 @@ Section compute_example.
       iApply ltyped_compute_client. }
     iApply ltyped_app.
     { iApply ltyped_compute_service. }
-    iApply ltyped_subsumption;
-      [ iApply env_le_refl | | iApply env_le_refl | ].
+    iApply ltyped_subsumption; [ iApply env_le_refl | | iApply env_le_refl | ].
     { iApply lty_le_arr; [ iApply lty_le_refl | ].
       iApply lty_le_arr; [ | iApply lty_le_refl ].
       iApply lty_le_arr; [ | iApply lty_le_refl ].

theories/logrel/session_types.v

@@ -165,7 +165,7 @@ Section session_types.
   Qed.
 
   Lemma lsty_car_app (S T : lsty Σ) :
-    (lsty_car S <++> lsty_car T)%proto ≡ lsty_car (S <++> T).
+    lsty_car (S <++> T) = (lsty_car S <++> lsty_car T)%proto.
   Proof. eauto. Qed.
 
 End session_types.

theories/logrel/term_typing_judgment.v

@@ -43,8 +43,8 @@ Section ltyped.
 End ltyped.
 
 Definition ltyped_val `{!heapG Σ} (v : val) (A : ltty Σ) : iProp Σ :=
-  tc_opaque (■ (ltty_car A) v)%I.
-Instance: Params (@ltyped_val) 2 := {}.
+  tc_opaque (■ ltty_car A v)%I.
+Instance: Params (@ltyped_val) 3 := {}.
 Notation "⊨ᵥ v : A" := (ltyped_val v A)
                          (at level 100, v at next level, A at level 200).
 Arguments ltyped_val : simpl never.
@@ -54,11 +54,11 @@ Section ltyped_val.
 
   Global Instance ltyped_val_plain v A : Plain (ltyped_val v A).
   Proof. rewrite /ltyped_val /=. apply _. Qed.
-  Global Instance ltyped_val_ne n :
-    Proper ((=) ==> dist n ==> dist n) (@ltyped_val Σ _).
+  Global Instance ltyped_val_ne n v :
+    Proper (dist n ==> dist n) (@ltyped_val Σ _ v).
   Proof. solve_proper. Qed.
-  Global Instance ltyped_val_proper :
-    Proper ((=) ==> (≡) ==> (≡)) (@ltyped_val Σ _).
+  Global Instance ltyped_val_proper v :
+    Proper ((≡) ==> (≡)) (@ltyped_val Σ _ v).
   Proof. solve_proper. Qed.
 
 End ltyped_val.
@@ -70,7 +70,7 @@ Section ltyped_rel.
   Proof.
     iIntros "#HA" (vs) "!> HΓ".
     iApply wp_value. iFrame "HΓ".
-    rewrite /ltyped_val. simpl.
+    rewrite /ltyped_val /=.
     iApply "HA".
   Qed.
 

theories/logrel/term_typing_rules.v

@@ -45,6 +45,13 @@ Section term_typing_rules.
     iApply (wp_wand with "(He (HleΓ1 HΓ1))").
     iIntros (v) "[Hτ HΓ2]". iSplitL "Hτ"; [by iApply "Hle"|by iApply "HleΓ2"].
   Qed.
+  Theorem ltyped_val_subsumption v τ τ' :
+    τ' <: τ -∗
+    (⊨ᵥ v : τ') -∗ (⊨ᵥ v : τ).
+  Proof.
+    iIntros "#Hle #Hv". iIntros "!>". iApply "Hle".
+    rewrite /ltyped_val /=. iApply "Hv".
+  Qed.
   Lemma ltyped_post_nil Γ1 Γ2 e τ :
     (Γ1 ⊨ e : τ ⫤ Γ2) -∗ (Γ1 ⊨ e : τ ⫤ []).
   Proof.
@@ -53,12 +60,18 @@ Section term_typing_rules.
   Qed.
 
   (** Basic properties *)
+  Lemma ltyped_val_unit : ⊢ ⊨ᵥ #() : ().
+  Proof. eauto. Qed.
   Lemma ltyped_unit Γ : ⊢ Γ ⊨ #() : ().
-  Proof. iIntros "!>" (vs) "$ /=". iApply wp_value. eauto. Qed.
+  Proof. iApply ltyped_val_ltyped. iApply ltyped_val_unit. Qed.
+  Lemma ltyped_val_bool (b : bool) : ⊢ ⊨ᵥ #b : lty_bool.
+  Proof. eauto. Qed.
   Lemma ltyped_bool Γ (b : bool) : ⊢ Γ ⊨ #b : lty_bool.
-  Proof. iIntros "!>" (vs) "$ /=". iApply wp_value. eauto. Qed.
+  Proof. iApply ltyped_val_ltyped. iApply ltyped_val_bool. Qed.
+  Lemma ltyped_val_int (z: Z) : ⊢ ⊨ᵥ #z : lty_int.
+  Proof. eauto. Qed.
   Lemma ltyped_int Γ (i : Z) : ⊢ Γ ⊨ #i : lty_int.
-  Proof. iIntros "!>" (vs) "$ /=". iApply wp_value. eauto. Qed.
+  Proof. iApply ltyped_val_ltyped. iApply ltyped_val_int. Qed.
 
   (** Operations *)
   Lemma ltyped_un_op Γ1 Γ2 op e A B :
@@ -131,17 +144,16 @@ Section term_typing_rules.
     iApply (wp_wand with "He'"). by iIntros (w) "[$ _]".
   Qed.
 
-  Lemma ltyped_lam_val x e A1 A2 :
-    ([EnvItem x A1] ⊨ e : A2 ⫤ []) -∗
+  Lemma ltyped_val_lam x e A1 A2 :
+    ((env_cons x A1 []) ⊨ e : A2 ⫤ []) -∗
     ⊨ᵥ (λ: x, e) : A1 ⊸ A2.
   Proof.
     iIntros "#He !>" (v) "HA1".
     wp_pures.
     iDestruct ("He" $!(binder_insert x v ∅) with "[HA1]") as "He'".
-    { replace ([EnvItem x A1]) with (env_cons x A1 []) by done.
-      iApply (env_ltyped_insert' ∅ ∅ x A1 v with "HA1").
+    { iApply (env_ltyped_insert' ∅ ∅ x A1 v with "HA1").
       iApply env_ltyped_nil. }
-    rewrite subst_map_binder_insert /= delete_empty subst_map_empty.
+    rewrite subst_map_binder_insert /= binder_delete_empty subst_map_empty.
     iApply (wp_wand with "He'"). by iIntros (w) "[$ _]".
   Qed.
 
@@ -170,9 +182,9 @@ Section term_typing_rules.
     iApply (wp_wand with "He'"). iIntros (w) "[$ _]".
   Qed.
 
-  Lemma ltyped_rec_val f x e A1 A2 :
+  Lemma ltyped_val_rec f x e A1 A2 :
     (env_cons f (A1 → A2) (env_cons x A1 []) ⊨ e : A2 ⫤ []) -∗
-    ⊨ᵥ (rec: f x := e)%V : A1 → A2.
+    ⊨ᵥ (rec: f x := e) : A1 → A2.
   Proof.
     iIntros "#He". simpl. iLöb as "IH".
     iIntros (v) "!>!> HA1". wp_pures. set (r := RecV f x _).
@@ -187,7 +199,6 @@ Section term_typing_rules.
     iIntros (w) "[$ _]".
   Qed.
 
-
   Lemma ltyped_let Γ1 Γ2 Γ3 x e1 e2 A1 A2 :
     (Γ1 ⊨ e1 : A1 ⫤ Γ2) -∗
     (env_cons x A1 Γ2 ⊨ e2 : A2 ⫤ Γ3) -∗