Added value typing judgement and value rules for lam and rec

theories/logrel/term_typing_judgment.v

@@ -42,6 +42,40 @@ Section ltyped.
   Qed.
 End ltyped.
 
+Definition ltyped_val `{!heapG Σ} (v : val) (A : ltty Σ) : iProp Σ :=
+  tc_opaque (■ (ltty_car A) v)%I.
+Instance: Params (@ltyped_val) 2 := {}.
+Notation "⊨ᵥ v : A" := (ltyped_val v A)
+                         (at level 100, v at next level, A at level 200).
+Arguments ltyped_val : simpl never.
+
+Section ltyped_val.
+  Context `{!heapG Σ}.
+
+  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 Σ _).
+  Proof. solve_proper. Qed.
+  Global Instance ltyped_val_proper :
+    Proper ((=) ==> (≡) ==> (≡)) (@ltyped_val Σ _).
+  Proof. solve_proper. Qed.
+
+End ltyped_val.
+
+Section ltyped_rel.
+  Context `{!heapG Σ}.
+
+  Lemma ltyped_val_ltyped Γ v A : (⊨ᵥ v : A) -∗ Γ ⊨ v : A.
+  Proof.
+    iIntros "#HA" (vs) "!> HΓ".
+    iApply wp_value. iFrame "HΓ".
+    rewrite /ltyped_val. simpl.
+    iApply "HA".
+  Qed.
+
+End ltyped_rel.
+
 Lemma ltyped_safety `{heapPreG Σ} e σ es σ' e' :
   (∀ `{heapG Σ}, ∃ A, ⊢ [] ⊨ e : A ⫤ []) →
   rtc erased_step ([e], σ) (es, σ') → e' ∈ es →

theories/logrel/term_typing_rules.v

@@ -118,7 +118,6 @@ Section term_typing_rules.
     iApply wp_frame_r. iFrame "HΓ". iApply ("Hf" $! v with "HA1").
   Qed.
 
-
   Lemma ltyped_lam Γ1 Γ2 x e A1 A2 :
     (env_cons x A1 Γ1 ⊨ e : A2 ⫤ []) -∗
     Γ1 ++ Γ2 ⊨ (λ: x, e) : A1 ⊸ A2 ⫤ Γ2.
@@ -132,6 +131,20 @@ 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 ⫤ []) -∗
+    ⊨ᵥ (λ: 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_nil. }
+    rewrite subst_map_binder_insert /= delete_empty subst_map_empty.
+    iApply (wp_wand with "He'"). by iIntros (w) "[$ _]".
+  Qed.
+
   (* Typing rule for introducing copyable functions *)
   Definition env_copy_minus : env Σ → env Σ :=
     fmap (λ xA, EnvItem (env_item_name xA) (lty_copy_minus  (env_item_type xA))).
@@ -157,6 +170,24 @@ Section term_typing_rules.
     iApply (wp_wand with "He'"). iIntros (w) "[$ _]".
   Qed.
 
+  Lemma ltyped_rec_val f x e A1 A2 :
+    (env_cons f (A1 → A2) (env_cons x A1 []) ⊨ e : A2 ⫤ []) -∗
+    ⊨ᵥ (rec: f x := e)%V : A1 → A2.
+  Proof.
+    iIntros "#He". simpl. iLöb as "IH".
+    iIntros (v) "!>!> HA1". wp_pures. set (r := RecV f x _).
+    iDestruct ("He"$! (binder_insert f r (binder_insert x v ∅))
+                 with "[HA1]") as "He'".
+    { iApply (env_ltyped_insert').
+      { rewrite /ltyped_val /=. iApply "IH". }
+      iApply (env_ltyped_insert' with "HA1").
+      iApply env_ltyped_nil. }
+    rewrite !subst_map_binder_insert_2 !binder_delete_empty subst_map_empty.
+    iApply (wp_wand with "He'").
+    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) -∗