From 889ac80b96f5224be6226fdfa2c4f9abce81e496 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Tue, 20 Dec 2016 15:49:30 +0100
Subject: [PATCH] prove calling a function

---
 opam.pins                      |  2 +-
 theories/lang/derived.v        | 45 ++++++++++++++++++++--------------
 theories/typing/function.v     | 31 +++++++++++++++++------
 theories/typing/type_context.v |  5 ++++
 4 files changed, 56 insertions(+), 27 deletions(-)

diff --git a/opam.pins b/opam.pins
index c51c3e1b..90d82d5a 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 1c9e858188578a65bf014ed8a8a9404f87054848
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq e2b843075894275afd52c19c83e4f5f812afdbab
diff --git a/theories/lang/derived.v b/theories/lang/derived.v
index 40ea3607..dbf09fff 100644
--- a/theories/lang/derived.v
+++ b/theories/lang/derived.v
@@ -22,27 +22,36 @@ Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val → iProp Σ.
 
 (** Proof rules for working on the n-ary argument list. *)
-Lemma wp_app (P : expr → iProp Σ) (Q : val → iProp Σ) E f el Φ :
+Lemma wp_app_ind {n} (Q : nat → val → iProp Σ) E f (el : vec expr n) (vs : list val) Φ :
   is_Some (to_val f) →
-  ([∗ list] e ∈ el, P e) -∗ □ (∀ e, P e -∗ WP e @ E {{ Q }}) -∗
-    (∀ vl, ([∗ list] v ∈ vl, Q v) -∗ WP App f (of_val <$> vl) @ E {{ Φ }}) -∗
-    WP App f el @ E {{ Φ }}.
+   ([∗ list] k ↦ e ∈ el, WP e @ E {{ Q k }}) -∗
+   (∀ vl : vec val n, ([∗ list] k ↦ v ∈ vl, Q k v) -∗
+                    WP App f (map of_val (vs ++ vl)) @ E {{ Φ }}) -∗
+    WP App f (map of_val vs ++ el) @ E {{ Φ }}.
 Proof.
-  iIntros (Hf) "Hel #HPQ HΦ".
-  assert (el = ((of_val <$> ([] : list val)) ++ el)) as -> by reflexivity.
-  rewrite big_sepL_app. iDestruct "Hel" as "[Hvl Hel]".
-  iAssert ([∗ list] y ∈ [], Q y)%I with "[Hvl]" as "Hvl".
-  { by rewrite big_sepL_nil. }
-  remember [] as vl. clear Heqvl. iInduction el as [|e el] "IH" forall (vl).
-  - rewrite app_nil_r. by iApply "HΦ".
-  - destruct Hf as [vf Hf]. set (K := AppRCtx vf vl el).
-    rewrite (_ : App f ((of_val <$> vl) ++ e :: el) = fill_item K e); last first.
+  iIntros (Hf) "Hel HΦ". iInduction el as [|e n el] "IH" forall (vs Q).
+  - iSpecialize ("HΦ" $! [#]). rewrite !app_nil_r. iApply "HΦ".
+    by rewrite !big_sepL_nil.
+  - destruct Hf as [vf Hf]. set (K := AppRCtx vf vs el).
+    rewrite (_ : App f ((map of_val vs) ++ e ::: el) = fill_item K e); last first.
     { simpl. f_equal. by erewrite of_to_val. }
-    iApply wp_bindi. rewrite big_sepL_cons. iDestruct "Hel" as "[He Hel]".
-    iApply (wp_wand with "[He]"); first by iApply "HPQ". iIntros (v) "HQ".
-    simpl. erewrite of_to_val by done. iSpecialize ("IH" $! (vl ++ [v])).
-    rewrite [of_val <$> vl ++ [v]]map_app /= -app_assoc /=. iApply ("IH" with "Hel HΦ").
-    rewrite big_sepL_app big_sepL_singleton. iFrame.
+    iApply wp_bindi. rewrite vec_to_list_cons big_sepL_cons. iDestruct "Hel" as "[He Hel]".
+    iApply (wp_wand with "He"). iIntros (v) "HQ".
+    simpl. erewrite of_to_val by done. iSpecialize ("IH" $! (vs ++ [v])).
+    rewrite [map of_val (vs ++ [#v])]map_app /= -app_assoc /=.
+    iApply ("IH" with "Hel"). iIntros (vl) "Hvl".
+    iSpecialize ("HΦ" $! (v ::: vl)). rewrite -app_assoc /=. iApply "HΦ".
+    rewrite big_sepL_cons. iFrame.
+Qed.
+
+Lemma wp_app {n} (Q : nat → val → iProp Σ) E f (el : vec expr n) Φ :
+  is_Some (to_val f) →
+  ([∗ list] k ↦ e ∈ el, WP e @ E {{ Q k }}) -∗
+    (∀ vl : vec val n, ([∗ list] k ↦ v ∈ vl, Q k v) -∗
+                    WP App f (of_val <$> (vl : list val)) @ E {{ Φ }}) -∗
+    WP App f el @ E {{ Φ }}.
+Proof.
+  iIntros (Hf). iApply (wp_app_ind _ _ _ _ []). done.
 Qed.
 
 (** Proof rules for the sugar *)
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 7d8e766c..33a480ef 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -101,11 +101,27 @@ Section fn.
     rewrite tctx_interp_cons. iIntros "[Hf HT]".
     wp_bind p. iApply (wp_hasty with "Hf"). iIntros (v) "[% Hf]".
     iMod (HTsat with "LFT HE HL HT") as "(HE & HL & HT)". rewrite tctx_interp_app.
-    iDestruct "HT" as "[Hargs HT']". clear HTsat.
-    (* TODO: I have no idea how to reduce all the ps properly to their values. This induction is probably not right, but at least it checks the case of the empty list. *)
-    iInduction ps as [|p' n ps] "IH" forall (tys).
-    - iDestruct "Hf" as (f) "[EQ #Hf]". iDestruct "EQ" as %[=->].
-      iSpecialize ("Hf" $! x [#] k). simpl.
+    iDestruct "HT" as "[Hargs HT']". clear HTsat. rewrite -vec_to_list_cons.
+    iApply (wp_app (λ i v, match i with O => ⌜v = k⌝ ∗ _ | S i =>
+                           ∀ ty, ⌜(tys x : list type) !! i = Some ty⌝ →
+                                 tctx_elt_interp tid (TCtx_hasty v ty) end)%I
+            with "* [Hargs HC]"); first wp_done.
+    - rewrite big_sepL_cons. iSplitR "Hargs".
+      { iApply wp_value'. iSplit; first done. iApply "HC". }
+      clear dependent ty k p.
+      rewrite /tctx_interp. rewrite big_sepL_zip_with. iApply (big_sepL_mono with "Hargs").
+      simpl. iIntros (i p Hp) "HT". assert (Hlen := lookup_lt_Some _ _ _ Hp).
+      edestruct (lookup_lt_is_Some_2 (tys x)) as [ty Hty].
+      { move: Hlen. rewrite !vec_to_list_length. done. }
+      iSpecialize ("HT" with "* []"); first done.
+      iApply (wp_hasty with "HT"). iIntros (v') "[% Hown]". iIntros (ty') "#EQ".
+      rewrite Hty. iDestruct "EQ" as %[=<-]. iExists v'. iFrame "Hown".
+      iPureIntro. exact: eval_path_of_val.
+    - iIntros (vl'). assert (Hvl := Vector.eta vl'). remember (Vector.hd vl') as kv.
+      remember (Vector.tl vl') as vl. rewrite Hvl. simpl in *. clear dependent vl'.
+      rewrite big_sepL_cons. iIntros "[[% HC] Hvl]". subst kv.
+      iDestruct "Hf" as (f) "[EQ #Hf]". iDestruct "EQ" as %[=->].
+      iSpecialize ("Hf" $! x vl k). 
       iMod (HEsat with "[%] HE HL") as (q') "[HE' Hclose]"; first done.
       iApply ("Hf" with "LFT HE' [] [HC Hclose HT']").
       + by rewrite /llctx_interp big_sepL_nil.
@@ -115,9 +131,8 @@ Section fn.
         iIntros (args) "_ HT". iSpecialize ("HC" with "* []"); first by (iPureIntro; apply elem_of_list_singleton).
         iApply ("HC" $! args with "HL"). rewrite tctx_interp_singleton tctx_interp_cons.
         iFrame.
-      + done.
-    - (* 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.
+      + 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
        (cps : vec path m) (ctyl : vec type m) `{!LstCopy ctyl, !LstSend ctyl} :
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index 225d2457..67e025dd 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -20,6 +20,10 @@ Section type_context.
     | e => to_val e
     end.
 
+  Lemma eval_path_of_val (v : val) :
+    eval_path v = Some v.
+  Proof. destruct v. done. simpl. rewrite (decide_left _). done. Qed.
+
   (* TODO: Consider mking this a pair of a path and the rest. We could
      then e.g. formulate tctx_elt_hasty_path more generally. *)
   Inductive tctx_elt : Type :=
@@ -35,6 +39,7 @@ Section type_context.
     end%I.
   (* Block tctx_elt_interp from reducing with simpl when x is a constructor. *)
   Global Arguments tctx_elt_interp : simpl never.
+
   Definition tctx_interp (tid : thread_id) (T : tctx) : iProp Σ :=
     ([∗ list] x ∈ T, tctx_elt_interp tid x)%I.
 
-- 
GitLab