From 40803f1d66580988fbb12ccfc91016aea192c012 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Mon, 19 Dec 2016 15:36:16 +0100
Subject: [PATCH] prove typing a function

---
 opam.pins                  |  2 +-
 theories/lang/lang.v       |  8 ++++++++
 theories/typing/function.v | 25 ++++++++++++++++++++-----
 theories/typing/programs.v |  2 +-
 4 files changed, 30 insertions(+), 7 deletions(-)

diff --git a/opam.pins b/opam.pins
index 722cf26d..c51c3e1b 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 2472f932c13e0e00b08eb1e00c2fcaaf78b260a8
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 1c9e858188578a65bf014ed8a8a9404f87054848
diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index 3b493477..1142d32e 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -502,6 +502,14 @@ Lemma stuck_not_head_step σ e' σ' ef :
   ¬head_step stuck_term σ e' σ' ef.
 Proof. inversion 1. Qed.
 
+Lemma Forall_of_val_is_val l :
+  Forall (λ ei : expr, is_Some (to_val ei)) (of_val <$> l).
+Proof.
+  induction l; constructor.
+  - rewrite to_of_val. eauto.
+  - apply IHl.
+Qed.
+
 (** Equality and other typeclass stuff *)
 Instance base_lit_dec_eq : EqDecision base_lit.
 Proof. solve_decision. Defined.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 5f396c52..4969c06d 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -114,14 +114,29 @@ Section fn.
         iApply ("HC" $! args with "HL"). rewrite tctx_interp_singleton tctx_interp_cons.
         iFrame.
       + done.
-    - (* The IH is not usable here. *)
+    - (* TODO: The IH is not usable here. What we really want is to do induction over "how many of the arguments still need to be evaluated", so the base case has all the ps evaluated and the inductive case evaluates one of them. *)
   Abort.
 
-  Lemma typed_fn {A n} E L T E' (tys : A → vec type n) ty fb kb (argsb : vec binder n) e `{!CopyC T} :
+  Lemma typed_fn {A n} E L T E' (tys : A → vec type n) ty fb kb
+        (argsb : vec binder n) ef e `{!CopyC T, !SendC T} :
+    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) [] [CctxElt k [] 1 (λ v, [TCtx_hasty (v!!!0) (ty x)])]
                  (TCtx_hasty f (fn E' tys ty) :: zip_with (TCtx_hasty ∘ of_val) args (tys x) ++ T)
-                 (subst fb f $ subst_vec (kb ::: argsb) (Vector.map of_val $ k ::: args) e)) →
-    typed_instruction_ty E L T (Rec fb (kb :: argsb) e) (fn E' tys ty).
+                 (subst' fb f $ subst_vec (kb ::: argsb) (Vector.map of_val $ k ::: args) e)) →
+    typed_instruction_ty E L T ef (fn E' tys ty).
   Proof.
-  Abort.
+    iIntros (-> Hc Hbody). iIntros (tid qE) "!# #LFT $ $ #HT". iApply wp_value.
+    { simpl. rewrite decide_left. done. }
+    rewrite tctx_interp_singleton. iLöb as "IH". iExists _. iSplit.
+    { simpl. rewrite decide_left. done. }
+    iExists _. iSplit; first done. iAlways. clear qE. 
+    iIntros (x args k). iIntros (tid' qE) "_ HE HL HC HT'". 
+    move:(Forall_of_val_is_val (k :: args))=>?.
+    evar (eb:expr). assert (subst_l (kb :: argsb) (of_val <$> k :: args) e = Some eb).
+    { subst eb. rewrite -!vec_to_list_cons -vec_to_list_map -subst_vec_eq. eauto. }
+    rewrite [elctx_interp]lock [llctx_interp]lock [tctx_interp]lock.
+    wp_rec. unlock. subst eb. iApply (Hbody with "* LFT HE HL HC").
+    rewrite tctx_interp_cons tctx_interp_app. iFrame "HT' IH".
+    iApply sendc_change_tid. done.
+  Qed.
 End fn.
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index b9bfe9c2..30ba48b6 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -1,5 +1,5 @@
 From iris.base_logic Require Import big_op.
-From lrust.lang Require Export notation memcpy.
+From lrust.lang Require Export notation.
 From lrust.lang Require Import proofmode.
 From lrust.lifetime Require Import frac_borrow reborrow borrow creation.
 From lrust.typing Require Export type lft_contexts type_context cont_context.
-- 
GitLab