From 8338156f9b1623c063c49e53faaf993b0f6c6468 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Mon, 21 Sep 2020 13:07:50 +0200
Subject: [PATCH] Added value typing judgement and value rules for lam and rec

---
 theories/logrel/term_typing_judgment.v | 34 ++++++++++++++++++++++++++
 theories/logrel/term_typing_rules.v    | 33 ++++++++++++++++++++++++-
 2 files changed, 66 insertions(+), 1 deletion(-)

diff --git a/theories/logrel/term_typing_judgment.v b/theories/logrel/term_typing_judgment.v
index 2d08421..0954cf4 100644
--- a/theories/logrel/term_typing_judgment.v
+++ b/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 →
diff --git a/theories/logrel/term_typing_rules.v b/theories/logrel/term_typing_rules.v
index fe4d68a..4f76d9d 100644
--- a/theories/logrel/term_typing_rules.v
+++ b/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) -∗
-- 
GitLab