Refactoring

theories/logrel/types.v

+From stdpp Require Import pretty.
+From actris.utils Require Import switch.
 From actris.logrel Require Export ltyping session_types.
 From actris.channel Require Import proto proofmode.
 From iris.heap_lang Require Export lifting metatheory.
 From iris.base_logic.lib Require Import invariants.
+From iris.heap_lang.lib Require Import assert.
 From iris.heap_lang Require Import notation proofmode lib.par spin_lock.
 
 Section types.
@@ -233,6 +236,50 @@ Section properties.
       by rewrite -delete_insert_ne // -subst_map_insert.
   Qed.
 
+  Fixpoint lty_arr_list (As : list (lty Σ)) (B : lty Σ) : lty Σ :=
+    match As with
+    | [] => B
+    | A :: As => A ⊸ lty_arr_list As B
+    end.
+
+  Lemma lty_arr_list_spec_step A As (e : expr) B ws y i :
+    (∀ v, lty_car A v -∗
+          WP subst_map (<[ y +:+ pretty i := v ]>ws)
+             (switch_lams y (S i) (length As) e) {{ lty_arr_list As B }}) -∗
+    WP subst_map ws (switch_lams y i (length (A::As)) e)
+       {{ lty_arr_list (A::As) B }}.
+  Proof.
+    iIntros "H". wp_pures. iIntros (v) "HA".
+    iDestruct ("H" with "HA") as "H".
+    rewrite subst_map_insert.
+    wp_apply "H".
+  Qed.
+
+  Lemma lty_arr_list_spec As (e : expr) B ws y i n :
+    n = length As →
+    (∀ vs, ([∗ list] A;v ∈ As;vs, (lty_car A) v) -∗
+           WP subst_map (map_string_seq y i vs ∪ ws) e {{ lty_car B }}) -∗
+    WP subst_map ws (switch_lams y i n e) {{ lty_arr_list As B }}.
+  Proof.
+    iIntros (Hlen) "H". iRevert (Hlen).
+    iInduction As as [|A As] "IH" forall (ws i e n)=> /=.
+    - iIntros (->).
+      iDestruct ("H" $! [] with "[$]") as "H"=> /=.
+      by rewrite left_id_L.
+    - iIntros (->). iApply lty_arr_list_spec_step.
+      iIntros (v) "HA".
+      iApply ("IH" with "[H HA]")=> //.
+      iIntros (vs) "HAs".
+      iSpecialize ("H" $!(v::vs))=> /=.
+      rewrite insert_union_singleton_l.
+      rewrite insert_union_singleton_l.
+      rewrite (map_union_comm ({[y +:+ pretty i := v]})); last first.
+      { apply map_disjoint_singleton_l_2.
+        apply lookup_map_string_seq_None_lt. eauto. }
+      rewrite assoc_L.
+      iApply ("H" with "[HA HAs]"). iFrame "HA HAs".
+  Qed.
+
   (** Product properties  *)
   Global Instance lty_prod_copy `{!LTyCopy A1, !LTyCopy A2} : LTyCopy (A1 * A2).
   Proof. iIntros (v). apply _. Qed.
@@ -700,74 +747,18 @@ Section properties.
       by wp_pures.
     Qed.
 
-    From stdpp Require Import pretty.
-    From actris.utils Require Import switch.
-    From iris.heap_lang.lib Require Import assert.
-
-    Fixpoint lty_arr_list (As : list (lty Σ)) (B : lty Σ) : lty Σ :=
-      match As with
-      | [] => B
-      | A :: As => A ⊸ lty_arr_list As B
-      end.
-
     Definition chanbranch (xs : list Z) : val := λ: "c",
       switch_lams "f" 0 (length xs) $
       let: "y" := recv "c" in
       switch_body "y" 0 xs (assert: #false) $ λ i, ("f" +:+ pretty i) "c".
 
-    Lemma lty_arr_list_spec_step A As (e : expr) B ws y i :
-      (∀ v, lty_car A v -∗
-      WP subst_map (<[ y +:+ pretty i := v ]>ws) (switch_lams y (S i) (length As) e) {{ lty_arr_list As B }}) -∗
-      WP subst_map ws (switch_lams y i (length (A::As)) e) {{ lty_arr_list (A::As) B }}.
-    Proof.
-      iIntros "H".
-      simpl.
-      wp_pures.
-      iIntros (v) "HA".
-      iDestruct ("H" with "HA") as "H".
-      wp_pures.
-      rewrite subst_map_insert.
-      iApply "H".
-    Qed.
-
-    Lemma lty_arr_list_spec As (e : expr) B ws y i n :
-      n = length As →
-      (∀ vs, ([∗ list] A;v ∈ As;vs, (lty_car A) v) -∗
-      WP subst_map (map_string_seq y i vs ∪ ws) e {{ lty_car B }}) -∗
-      WP subst_map ws (switch_lams y i n e) {{ lty_arr_list As B }}.
-    Proof.
-      iIntros (Hlen) "H".
-      iRevert (Hlen).
-      iInduction As as [|A As] "IH" forall (ws i e n)=> /=.
-      - iIntros (->).
-        iDestruct ("H" $! [] with "[$]") as "H"=> /=.
-        by rewrite left_id_L.
-      - iIntros (Hlen). rewrite Hlen. iApply lty_arr_list_spec_step.
-        iIntros (v) "HA".
-        iApply ("IH" with "[H HA]")=> //.
-        iIntros (vs) "HAs".
-        iSpecialize ("H" $!(v::vs)).
-
-        simpl.
-        rewrite insert_union_singleton_l.
-        rewrite insert_union_singleton_l.
-        rewrite (map_union_comm ({[y +:+ pretty i := v]})); last first.
-        { apply map_disjoint_singleton_l_2.
-          apply lookup_map_string_seq_None_lt. eauto. }
-        rewrite assoc_L.
-        iApply ("H" with "[HA HAs]"). iFrame.
-    Qed.
-
     Lemma ltyped_chanbranch Ps A xs :
       Forall (λ x, is_Some (Ps !! x)) xs →
       ⊢ ∅ ⊨ chanbranch xs : chan (lsty_branch Ps) ⊸
                               lty_arr_list
                                 ((λ x, (chan (Ps !!! x) ⊸ A)%lty) <$> xs) A.
     Proof.
-      intros Hxs.
-      iIntros "!>" (vs) "Hvs".
-      rewrite /chanbranch.
-      simpl.
+      iIntros (Hxs) "!>". iIntros (vs) "Hvs".
       iApply wp_value.
       iIntros (c) "Hc".
       wp_lam=> /=.
@@ -780,9 +771,8 @@ Section properties.
         strings.length ws) as Heq.
       { admit. }                (* This can be asserted using big_sepL2_alt, but
                                    then we get the map on a weird form *)
-      rewrite -insert_union_singleton_r=> //;
-        last by apply lookup_map_string_seq_None.
-      simpl.
+      rewrite -insert_union_singleton_r=> /=;
+        last by apply lookup_map_string_seq_None=> /=.
       rewrite lookup_insert.
       wp_recv (x) as "%".
       wp_pures.
@@ -822,7 +812,7 @@ Section properties.
       rewrite insert_commute=> //.
       rewrite lookup_insert.
       by iApply "HA".
-    Qed.
+    Admitted.
 
   End with_chan.
 End properties.