show typing a let-bound instruction

theories/typing/bool.v

@@ -12,14 +12,14 @@ Section bool.
   Global Instance bool_send : Send bool.
   Proof. iIntros (tid1 tid2 vl). done. Qed.
 
-  Lemma typed_bool (b : Datatypes.bool) E L :
+  Lemma type_bool (b : Datatypes.bool) E L :
     typed_instruction_ty E L [] #b bool.
   Proof.
     iIntros (tid qE) "!# _ $ $ _". wp_value. rewrite tctx_interp_singleton.
     iExists _. iSplitR; first done. iExists _. done.
   Qed.
 
-  Lemma typed_if E L C T e1 e2 p:
+  Lemma type_if E L C T e1 e2 p:
     typed_body E L C T e1 → typed_body E L C T e2 →
     typed_body E L C (TCtx_hasty p bool :: T) (if: p then e1 else e2).
   Proof.

theories/typing/cont.v

@@ -8,7 +8,7 @@ Section cont_typing.
   Context `{typeG Σ}.
 
   (** Jumping to and defining a continuation. *)
-  Lemma typed_jump {n} E L k T' T (args : vec val n) :
+  Lemma type_jump {n} E L k T' T (args : vec val n) :
     tctx_incl E L T (T' args) →
     typed_body E L [CCtx_iscont k L n T'] T (k (of_val <$> (args : list _))).
   Proof.
@@ -18,7 +18,7 @@ Section cont_typing.
     simpl. iApply ("HC" with "* HL HT").
   Qed.
 
-  Lemma typed_cont {n} E L1 L2 C T T' kb (argsb : vec binder n) e1 econt e2 :
+  Lemma type_cont {n} E L1 L2 C T T' kb (argsb : vec binder n) e1 econt e2 :
     e1 = Rec kb argsb econt → Closed (kb :b: argsb +b+ []) econt → Closed (kb :b: []) e2 →
     (∀ k args, typed_body E L1 (CCtx_iscont k L1 n T' :: C) (T' args)
                           (subst' kb k $ subst_vec argsb (Vector.map of_val $ args) econt)) →

theories/typing/function.v

@@ -91,7 +91,7 @@ Section fn.
   Qed.
 
   (* TODO: Define some syntactic sugar for calling and letrec like we do on paper. *)
-  Lemma typed_call {A n} E L E' T T' (tys : A → vec type n) ty k p (ps : vec path n) x :
+  Lemma type_call {A n} E L E' T T' (tys : A → vec type n) ty k p (ps : vec path n) x :
     tctx_incl E L T (zip_with TCtx_hasty ps (tys x) ++ T') → elctx_sat E L (E' x) →
     typed_body E L [CCtx_iscont k L 1 (λ v, (TCtx_hasty (v!!!0) (ty x)) :: T')]
                (TCtx_hasty p (fn E' tys ty) :: T) (p (of_val k :: ps)).
@@ -133,7 +133,7 @@ Section fn.
       + rewrite /tctx_interp big_sepL_zip_with. done.
   Qed.
 
-  Lemma typed_fn {A n m} E L E' (tys : A → vec type n) ty fb kb (argsb : vec binder n) ef e
+  Lemma type_fn {A n m} E L E' (tys : A → vec type n) ty fb kb (argsb : vec binder n) ef e
        (cps : vec path m) (ctyl : vec type m) `{!LstCopy ctyl, !LstSend ctyl} :
     ef = Rec fb (kb :: argsb) e → Closed (fb :b: kb :b: argsb +b+ []) e →
     (∀ x f k (args : vec val n), typed_body (E' x) [] [CCtx_iscont k [] 1 (λ v, [TCtx_hasty (v!!!0) (ty x)])]

theories/typing/int.v

@@ -12,14 +12,14 @@ Section int.
   Global Instance int_send : Send int.
   Proof. iIntros (tid1 tid2 vl). done. Qed.
 
-  Lemma typed_int (z : Z) E L :
+  Lemma type_int (z : Z) E L :
     typed_instruction_ty E L [] #z int.
   Proof.
     iIntros (tid qE) "!# _ $ $ _". wp_value. rewrite tctx_interp_singleton.
     iExists _. iSplitR; first done. iExists _. done.
   Qed.
 
-  Lemma typed_plus E L p1 p2 :
+  Lemma type_plus E L p1 p2 :
     typed_instruction_ty E L [TCtx_hasty p1 int; TCtx_hasty p2 int] (p1 + p2) int.
   Proof.
     iIntros (tid qE) "!# _ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
@@ -32,7 +32,7 @@ Section int.
     iExists _. done.
   Qed.
 
-  Lemma typed_minus E L p1 p2 :
+  Lemma type_minus E L p1 p2 :
     typed_instruction_ty E L [TCtx_hasty p1 int; TCtx_hasty p2 int] (p1 - p2) int.
   Proof.
     iIntros (tid qE) "!# _ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
@@ -45,7 +45,7 @@ Section int.
     iExists _. done.
   Qed.
 
-  Lemma typed_le E L p1 p2 :
+  Lemma type_le E L p1 p2 :
     typed_instruction_ty E L [TCtx_hasty p1 int; TCtx_hasty p2 int] (p1 ≤ p2) bool.
   Proof.
     iIntros (tid qE) "!# _ $ $". rewrite tctx_interp_cons tctx_interp_singleton.

theories/typing/programs.v

@@ -46,3 +46,20 @@ Section typing.
 End typing.
 
 Notation typed_instruction_ty E L T1 e ty := (typed_instruction E L T1 e (λ v : val, [TCtx_hasty v ty])).
+
+Section typing_rules.
+  Context `{typeG Σ}.
+
+  Lemma type_let E L T1 T2 T C xb e e' :
+    Closed (xb :b: []) e' →
+    typed_instruction E L T1 e T2 →
+    (∀ v : val, typed_body E L C (T2 v ++ T) (subst' xb v e')) →
+    typed_body E L C (T1 ++ T) (let: xb := e in e').
+  Proof.
+    iIntros (Hc He He' tid qE) "#LFT HE HL HC HT". rewrite tctx_interp_app.
+    iDestruct "HT" as "[HT1 HT]". wp_bind e. iApply (wp_wand with "[HE HL HT1]").
+    { iApply (He with "LFT HE HL HT1"). }
+    iIntros (v) "/= (HE & HL & HT2)". iApply wp_let; first wp_done. iModIntro.
+    iApply (He' with "LFT HE HL HC [HT2 HT]"). rewrite tctx_interp_app. by iFrame.
+  Qed.
+End typing_rules.