From f9bcc1f9ebf63e6d77c85094b2b7e23f22970385 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 22 Dec 2016 11:08:09 +0100
Subject: [PATCH] Make typing lemmas about continuations and functions easier
 to apply.

By letting them only speak about lits in their conclusions, and use [length] as the length parameter of vec. Also simplified substitutions of vectors.
---
 theories/lang/derived.v        | 20 ++++++-------
 theories/lang/lang.v           | 23 +++++----------
 theories/typing/cont.v         | 32 ++++++++++----------
 theories/typing/cont_context.v |  2 +-
 theories/typing/function.v     | 53 +++++++++++++++++-----------------
 5 files changed, 60 insertions(+), 70 deletions(-)

diff --git a/theories/lang/derived.v b/theories/lang/derived.v
index c4da9c23..c9be4fac 100644
--- a/theories/lang/derived.v
+++ b/theories/lang/derived.v
@@ -22,20 +22,20 @@ Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val → iProp Σ.
 
 (** Proof rules for working on the n-ary argument list. *)
-Lemma wp_app_ind {n} (Q : nat → val → iProp Σ) E f (el : vec expr n) (vs : list val) Φ :
+Lemma wp_app_ind (Q : nat → val → iProp Σ) E f el (vs : list val) Φ :
   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) -∗
+   (∀ 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 {{ Φ }}.
 Proof.
-  iIntros (Hf) "Hel HΦ". iInduction el as [|e n el] "IH" forall (vs Q).
+  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.
+    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 vec_to_list_cons big_sepL_cons. iDestruct "Hel" as "[He Hel]".
+    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 /=.
@@ -44,10 +44,10 @@ Proof.
     rewrite big_sepL_cons. iFrame.
 Qed.
 
-Lemma wp_app_vec {n} (Q : nat → val → iProp Σ) E f (el : vec expr n) Φ :
+Lemma wp_app_vec (Q : nat → val → iProp Σ) E f el Φ :
   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) -∗
+    (∀ vl : vec val (length el), ([∗ list] k ↦ v ∈ vl, Q k v) -∗
                     WP App f (of_val <$> (vl : list val)) @ E {{ Φ }}) -∗
     WP App f el @ E {{ Φ }}.
 Proof.
@@ -61,10 +61,8 @@ Lemma wp_app (Q : nat → val → iProp Σ) E f el Φ :
                     WP App f (of_val <$> (vl : list val)) @ E {{ Φ }}) -∗
     WP App f el @ E {{ Φ }}.
 Proof.
-  iIntros (Hf) "Hel HΦ". rewrite -(vec_to_list_of_list el).
-  iApply (wp_app_vec with "* Hel"); first done.
-  iIntros (vl). iApply ("HΦ" $! (vec_to_list vl)).
-  rewrite vec_to_list_length vec_to_list_of_list. done.
+  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.
 Qed.
 
 (** Proof rules for the sugar *)
diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index 1142d32e..d3e01fd6 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -163,15 +163,14 @@ Fixpoint subst_l (xl : list binder) (esl : list expr) (e : expr) : option expr :
   | _, _ => None
   end.
 
-Definition subst_vec {n} (xl : vec binder n) (el : vec expr n) : expr → expr :=
-  Vector.rect2 (λ _ _ _, expr → expr) id
-               (λ n _ _ rec x e, rec ∘ subst' x e) xl el.
-
-Lemma subst_vec_eq {n} (xl : vec binder n) (el : vec expr n) e :
-  Some $ subst_vec xl el e = subst_l xl el e.
+Definition subst_v (xl : list binder) (esl : vec expr (length xl))
+                   (e : expr) : expr :=
+  from_option id (Var "" (* Dummy *)) (subst_l xl esl e).
+Lemma subst_v_eq (xl : list binder) (esl : vec expr (length xl)) e :
+  Some $ subst_v xl esl e = subst_l xl esl e.
 Proof.
-  revert n xl el e. eapply (vec_rect2 (λ n xl el, ∀ e, Some $ subst_vec xl el e = subst_l xl el e)); first done.
-  move=>n xl el IH x es e. simpl. apply IH.
+  unfold subst_v. destruct subst_l eqn:EQ; first done. exfalso. revert esl e EQ.
+  induction xl=>/= esl; inv_vec esl; first done. simpl. eauto.
 Qed.
 
 (** The stepping relation *)
@@ -502,14 +501,6 @@ 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/cont.v b/theories/typing/cont.v
index 7128abf6..3db8c352 100644
--- a/theories/typing/cont.v
+++ b/theories/typing/cont.v
@@ -8,34 +8,34 @@ Section typing.
   Context `{typeG Σ}.
 
   (** Jumping to and defining a continuation. *)
-  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 _))).
+  Lemma type_jump E L C T k args T' :
+    CCtx_iscont k L _ T' ∈ C →
+    tctx_incl E L T (T' (list_to_vec args)) →
+    typed_body E L C T (k (of_val <$> args)).
   Proof.
-    iIntros (Hincl tid qE) "#HEAP #LFT Htl HE HL HC HT".
+    iIntros (HC Hincl tid qE) "#HEAP #LFT Htl HE HL HC HT".
     iMod (Hincl with "LFT HE HL HT") as "(HE & HL & HT)".
-    iSpecialize ("HC" with "HE * []"); first by (iPureIntro; apply elem_of_list_singleton).
-    simpl. iApply ("HC" with "* Htl HL HT").
+    iSpecialize ("HC" with "HE * []"); first done.
+    rewrite -{3}(vec_to_list_of_list args). iApply ("HC" with "* Htl HL HT").
   Qed.
 
-  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)) →
-    (∀ k, typed_body E (L1 ++ L2) (CCtx_iscont k L1 n T' :: C) T (subst' kb k e2)) →
-    typed_body E (L1 ++ L2) C T (let: kb := e1 in e2).
+  Lemma type_cont E L1 L2 C T argsb econt e2 T' kb :
+    Closed (kb :b: argsb +b+ []) econt → Closed (kb :b: []) e2 →
+    (∀ k args, typed_body E L1 (CCtx_iscont k L1 _ T' :: C) (T' args)
+                          (subst' kb k $ subst_v argsb (vmap of_val args) econt)) →
+    (∀ k, typed_body E (L1 ++ L2) (CCtx_iscont k L1 _ T' :: C) T (subst' kb k e2)) →
+    typed_body E (L1 ++ L2) C T (let: kb := Rec kb argsb econt in e2).
   Proof.
-    iIntros (-> Hc1 Hc2 Hecont He2 tid qE) "#HEAP #LFT Htl HE HL HC HT". iApply wp_let'.
+    iIntros (Hc1 Hc2 Hecont He2 tid qE) "#HEAP #LFT Htl HE HL HC HT". iApply wp_let'.
     { simpl. rewrite decide_left. done. }
     iModIntro. iApply (He2 with "* HEAP LFT Htl HE HL [HC] HT"). clear He2.
     iIntros "HE". iLöb as "IH". iIntros (x) "H".
     iDestruct "H" as %[->|?]%elem_of_cons; last by iApply ("HC" with "HE *").
     iIntros (args) "Htl HL HT". iApply wp_rec; try done.
-    { apply Forall_of_val_is_val. }
-    { rewrite -vec_to_list_map -subst_vec_eq. eauto. }
+    { rewrite Forall_fmap Forall_forall=>? _. rewrite /= to_of_val. eauto. }
+    { by rewrite -vec_to_list_map -subst_v_eq. }
     (* FIXME: iNext here unfolds things in the context. *)
     iNext. iApply (Hecont with "* HEAP LFT Htl HE HL [HC] HT").
     by iApply "IH".
   Qed.
-
 End typing.
diff --git a/theories/typing/cont_context.v b/theories/typing/cont_context.v
index b9c109be..4ba6cdfa 100644
--- a/theories/typing/cont_context.v
+++ b/theories/typing/cont_context.v
@@ -11,7 +11,7 @@ Section cont_context_def.
 
   Record cctx_elt : Type :=
     CCtx_iscont { cctxe_k : val; cctxe_L : llctx;
-              cctxe_n : nat; cctxe_T : vec val cctxe_n → tctx }.
+                  cctxe_n : nat; cctxe_T : vec val cctxe_n → tctx }.
   Definition cctx := list cctx_elt.
 End cont_context_def.
 Add Printing Constructor cctx_elt.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index dfea82ae..7b070360 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -95,7 +95,8 @@ Section typing.
   Qed.
 
   (* TODO: Define some syntactic sugar for calling and letrec like we do on paper. *)
-  Lemma type_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} E L E' T T' p (ps : list path)
+                        (tys : A → vec type (length ps)) ty k 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)).
@@ -104,10 +105,10 @@ Section typing.
     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. rewrite -vec_to_list_cons.
+    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
+                               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". }
@@ -120,42 +121,42 @@ Section typing.
       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). 
+    - simpl. iIntros (vl'). inv_vec vl'=>kv 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 "HEAP LFT Htl HE' [] [HC Hclose HT']").
       + by rewrite /llctx_interp big_sepL_nil.
       + iIntros "HE'". iApply fupd_cctx_interp. iMod ("Hclose" with "HE'") as "[HE HL]".
-        iSpecialize ("HC" with "HE").  iModIntro. iIntros (y) "IN".
-        iDestruct "IN" as %->%elem_of_list_singleton.
-        iIntros (args) "Htl _ HT". iSpecialize ("HC" with "* []"); first by (iPureIntro; apply elem_of_list_singleton).
+        iSpecialize ("HC" with "HE"). iModIntro. iIntros (y) "IN".
+        iDestruct "IN" as %->%elem_of_list_singleton. iIntros (args) "Htl _ HT".
+        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.
   Qed.
 
-  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)])]
-                 (TCtx_hasty f (fn E' tys ty) ::
-                  zip_with (TCtx_hasty ∘ of_val) args (tys x) ++
-                  zip_with TCtx_hasty cps ctyl)
-                 (subst' fb f $ subst_vec (kb ::: argsb) (Vector.map of_val $ k ::: args) e)) →
-    typed_instruction_ty E L (zip_with TCtx_hasty cps ctyl) ef (fn E' tys ty).
+  Lemma type_fn {A m} E L E' fb kb (argsb : list binder) e
+        (tys : A → vec type (length argsb)) ty
+        (cps : vec path m) (ctyl : vec type m) `{!LstCopy ctyl, !LstSend ctyl} :
+    Closed (fb :b: kb :b: argsb +b+ []) e →
+    (∀ x f k (args : vec val _),
+        typed_body (E' x) [] [CCtx_iscont 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) ++
+                      zip_with TCtx_hasty cps ctyl)
+                   (subst' fb f $ subst_v (kb :: argsb) (vmap of_val $ k ::: args) e)) →
+    typed_instruction_ty E L (zip_with TCtx_hasty cps ctyl)
+                         (Rec fb (kb :: argsb) e) (fn E' tys ty).
   Proof.
-    iIntros (-> Hc Hbody tid qE) "#HEAP #LFT $ $ $ #HT". iApply wp_value.
+    iIntros (Hc Hbody tid qE) "#HEAP #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) "_ _ Htl HE HL HC HT'".
-    iApply wp_rec; try done.
-    { apply Forall_of_val_is_val. }
-    { rewrite -!vec_to_list_cons -vec_to_list_map -subst_vec_eq. eauto. }
+    iExists _. iSplit; first done. iAlways. clear qE.
+    iIntros (x args k tid' qE) "_ _ Htl HE HL HC HT'". iApply wp_rec; try done.
+    { rewrite Forall_fmap Forall_forall=>? _. rewrite /= to_of_val. eauto. }
+    { by rewrite -vec_to_list_cons -vec_to_list_map -subst_v_eq. }
     iApply (Hbody with "* HEAP LFT Htl HE HL HC").
     rewrite tctx_interp_cons tctx_interp_app. iFrame "HT' IH".
     iApply tctx_send. by iNext.
-- 
GitLab