From dcac3c038470c0b81ae18b6b0db1e43c76648711 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 22 Dec 2016 16:40:34 +0100
Subject: [PATCH] State [wp_app_vec] with a vector of predicates instead of 2
 parameters predicates.

---
 theories/lang/derived.v    | 56 +++++++++++++++++++-------------------
 theories/lang/lang.v       |  4 +--
 theories/typing/function.v | 30 +++++++++-----------
 3 files changed, 43 insertions(+), 47 deletions(-)

diff --git a/theories/lang/derived.v b/theories/lang/derived.v
index c9be4fac..11795f1f 100644
--- a/theories/lang/derived.v
+++ b/theories/lang/derived.v
@@ -22,47 +22,47 @@ Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val → iProp Σ.
 
 (** Proof rules for working on the n-ary argument list. *)
-Lemma wp_app_ind (Q : nat → val → iProp Σ) E f el (vs : list val) Φ :
+Lemma wp_app_ind E f (el : list expr) (Ql : vec (val → iProp Σ) (length el)) vs Φ:
   is_Some (to_val f) →
-   ([∗ list] k ↦ e ∈ el, WP e @ E {{ Q k }}) -∗
-   (∀ vl : vec val (length el), ([∗ 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 {{ Φ }}.
+  ([∗ list] eQ ∈ zip el Ql, WP eQ.1 @ E {{ eQ.2 }}) -∗
+    (∀ vl : vec val (length el), ([∗ list] vQ ∈ zip vl Ql, vQ.2 $ vQ.1) -∗
+                    WP App f (of_val <$> vs ++ vl) @ E {{ Φ }}) -∗
+    WP App f ((of_val <$> vs) ++ el) @ E {{ Φ }}.
 Proof.
-  iIntros (Hf) "Hel HΦ". iInduction el as [|e 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"). 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.
+  intros [vf Hf]. revert vs Ql. induction el as [|e el IH]=>/= vs Ql; inv_vec Ql.
+  - iIntros "_ H". iSpecialize ("H" $! [#]). rewrite !app_nil_r big_sepL_nil.
+      by iApply "H".
+  - intros Q Ql. rewrite /= big_sepL_cons /=. iIntros "[He Hl] HΦ".
+    assert (App f ((of_val <$> vs) ++ e :: el) = fill_item (AppRCtx vf vs el) e)
+      as -> by rewrite /= (of_to_val f) //.
+    iApply wp_bindi. iApply (wp_wand with "He"). iIntros (v) "HQ /=".
+    rewrite cons_middle (assoc app) -(fmap_app _ _ [v]) (of_to_val f) //.
+    iApply (IH _ _ with "Hl"). iIntros "* Hvl". rewrite -assoc.
+    iApply ("HΦ" $! (v:::vl)). rewrite /= big_sepL_cons. iFrame.
 Qed.
 
-Lemma wp_app_vec (Q : nat → val → iProp Σ) E f el Φ :
+Lemma wp_app_vec E f el (Ql : vec (val → iProp Σ) (length el)) Φ :
   is_Some (to_val f) →
-  ([∗ list] k ↦ e ∈ el, WP e @ E {{ Q k }}) -∗
-    (∀ vl : vec val (length el), ([∗ list] k ↦ v ∈ vl, Q k v) -∗
+  ([∗ list] eQ ∈ zip el Ql, WP eQ.1 @ E {{ eQ.2 }}) -∗
+    (∀ vl : vec val (length el), ([∗ list] vQ ∈ zip vl Ql, vQ.2 $ vQ.1) -∗
                     WP App f (of_val <$> (vl : list val)) @ E {{ Φ }}) -∗
     WP App f el @ E {{ Φ }}.
 Proof.
   iIntros (Hf). iApply (wp_app_ind _ _ _ _ []). done.
 Qed.
 
-Lemma wp_app (Q : nat → val → iProp Σ) E f el Φ :
-  is_Some (to_val f) →
-  ([∗ list] k ↦ e ∈ el, WP e @ E {{ Q k }}) -∗
-    (∀ vl : list val, ⌜length vl = length el⌝ -∗ ([∗ list] k ↦ v ∈ vl, Q k v) -∗
-                    WP App f (of_val <$> (vl : list val)) @ E {{ Φ }}) -∗
+Lemma wp_app (Ql : list (val → iProp Σ)) E f el Φ :
+  length Ql = length el → is_Some (to_val f) →
+  ([∗ list] eQ ∈ zip el Ql, WP eQ.1 @ E {{ eQ.2 }}) -∗
+    (∀ vl : list val, ⌜length vl = length el⌝ -∗
+            ([∗ list] k ↦ vQ ∈ zip vl Ql, vQ.2 $ vQ.1) -∗
+             WP App f (of_val <$> (vl : list val)) @ E {{ Φ }}) -∗
     WP App f el @ E {{ Φ }}.
 Proof.
-  iIntros (Hf) "Hel HΦ". iApply (wp_app_vec with "* Hel"); first done.
-  iIntros (vl). iApply ("HΦ" $! (vec_to_list vl)). by rewrite vec_to_list_length.
+  iIntros (Hlen Hf) "Hel HΦ". rewrite -(vec_to_list_of_list Ql).
+  generalize (list_to_vec Ql). rewrite Hlen. clear Hlen Ql=>Ql.
+  iApply (wp_app_vec with "Hel"); first done. iIntros (vl) "Hvl".
+  iApply ("HΦ" with "[%] Hvl"). by rewrite vec_to_list_length.
 Qed.
 
 (** Proof rules for the sugar *)
diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index d3e01fd6..3e733278 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -123,7 +123,7 @@ Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
   | BinOpLCtx op e2 => BinOp op e e2
   | BinOpRCtx op v1 => BinOp op (of_val v1) e
   | AppLCtx e2 => App e e2
-  | AppRCtx v vl el => App (of_val v) (map of_val vl ++ e :: el)
+  | AppRCtx v vl el => App (of_val v) ((of_val <$> vl) ++ e :: el)
   | ReadCtx o => Read o e
   | WriteLCtx o e2 => Write o e e2
   | WriteRCtx o v1 => Write o (of_val v1) e
@@ -587,6 +587,6 @@ Proof.
     + destruct K as [|Ki K].
       * simpl in *. subst. inversion Hstep.
       * destruct Ki; simpl in *; done.
-    + destruct (map of_val vl); last done. destruct (fill K e'); done.
+    + destruct (of_val <$> vl); last done. destruct (fill K e'); done.
   - by eapply stuck_not_head_step.
 Qed.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 7b070360..b2f133b2 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -106,23 +106,17 @@ Section typing.
     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.
-    iApply (wp_app_vec (λ 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". }
+    iApply (wp_app_vec _ _ (_::_) ((λ v, ⌜v = k⌝):::
+               vmap (λ ty (v : val), tctx_elt_interp tid (TCtx_hasty v ty)) (tys x))%I
+            with "* [Hargs]"); first wp_done.
+    - rewrite /= big_sepL_cons. iSplitR "Hargs"; first by iApply wp_value'.
       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.
-    - simpl. iIntros (vl'). inv_vec vl'=>kv vl. rewrite big_sepL_cons.
-      iIntros "[[% HC] Hvl]". subst kv. iDestruct "Hf" as (f) "[EQ #Hf]".
+      rewrite /tctx_interp vec_to_list_map zip_with_fmap_r
+              (zip_with_zip (λ e ty, (e, _))) zip_with_zip !big_sepL_fmap.
+      iApply (big_sepL_mono' with "Hargs"). iIntros (i [p ty]) "HT/=".
+      iApply (wp_hasty with "HT"). setoid_rewrite tctx_hasty_val. iIntros (?) "? $".
+    - simpl. iIntros (vl'). inv_vec vl'=>kv vl. rewrite /= big_sepL_cons.
+      iIntros "/= [% 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 "HEAP LFT Htl HE' [] [HC Hclose HT']").
@@ -133,7 +127,9 @@ Section typing.
         iSpecialize ("HC" with "* []"); first by (iPureIntro; apply elem_of_list_singleton).
         iApply ("HC" $! args with "Htl HL"). rewrite tctx_interp_singleton tctx_interp_cons.
         iFrame.
-      + rewrite /tctx_interp big_sepL_zip_with. done.
+      + rewrite /tctx_interp vec_to_list_map zip_with_fmap_r
+                (zip_with_zip (λ v ty, (v, _))) zip_with_zip !big_sepL_fmap.
+        iApply (big_sepL_mono' with "Hvl"). by iIntros (i [v ty']).
   Qed.
 
   Lemma type_fn {A m} E L E' fb kb (argsb : list binder) e
-- 
GitLab