Merge branch 'jonas/n_choice' into 'master'

n-ary choice

Closes #3

See merge request !5

theories/logrel/session_types.v

 From actris.logrel Require Export ltyping lsty.
+From iris.algebra Require Import gmap.
 From iris.heap_lang Require Export lifting metatheory.
 From iris.base_logic.lib Require Import invariants.
 From iris.heap_lang Require Import notation proofmode.
@@ -9,24 +10,26 @@ Section protocols.
 
   Definition lsty_end : lsty Σ := Lsty END.
 
+  Definition lsty_message (a : action) (A : lty Σ) (P : lsty Σ) : lsty Σ :=
+    Lsty (<a> v, MSG v {{ A v }}; lsty_car P).
+
   Definition lsty_send (A : lty Σ) (P : lsty Σ) : lsty Σ :=
-    Lsty (<!> v, MSG v {{ A v }}; lsty_car P).
+    lsty_message Send A P.
   Definition lsty_recv (A : lty Σ) (P : lsty Σ) : lsty Σ :=
-    Lsty (<?> v, MSG v {{ A v }}; lsty_car P).
+    lsty_message Recv A P.
 
-  Definition lsty_branch (P1 P2 : lsty Σ) : lsty Σ :=
-    Lsty (P1 <&> P2).
-  Definition lsty_select (P1 P2 : lsty Σ) : lsty Σ :=
-    Lsty (P1 <+> P2).
+  Definition lsty_choice (a : action) (Ps : gmap Z (lsty Σ)) : lsty Σ :=
+    Lsty (<a> x : Z, MSG #x {{ ⌜is_Some (Ps !! x)⌝ }}; lsty_car (Ps !!! x)).
 
-  Definition lsty_rec1 (C : lsty Σ → lsty Σ)
-             `{!Contractive C}
-             (rec : lsty Σ) : lsty Σ :=
-    Lsty (C rec).
+  Definition lsty_select (Ps : gmap Z (lsty Σ)) : lsty Σ :=
+    lsty_choice Send Ps.
+  Definition lsty_branch (Ps : gmap Z (lsty Σ)) : lsty Σ :=
+    lsty_choice Recv Ps.
 
+  Definition lsty_rec1 (C : lsty Σ → lsty Σ) `{!Contractive C}
+    (rec : lsty Σ) : lsty Σ := Lsty (C rec).
   Instance lsty_rec1_contractive C `{!Contractive C} : Contractive (lsty_rec1 C).
   Proof. solve_contractive. Qed.
-
   Definition lsty_rec (C : lsty Σ → lsty Σ) `{!Contractive C} : lsty Σ :=
     fixpoint (lsty_rec1 C).
 
@@ -34,109 +37,57 @@ Section protocols.
     Lsty (iProto_dual P).
 
   Definition lsty_app (P1 P2 : lsty Σ) : lsty Σ :=
-    Lsty (iProto_app P1 P2).
-
+    Lsty (P1 <++> P2).
 End protocols.
 
 Section Propers.
   Context `{heapG Σ, protoG Σ}.
 
-  Global Instance lsty_send_ne : NonExpansive2 (@lsty_send Σ).
+  Global Instance lsty_message_ne a : NonExpansive2 (@lsty_message Σ a).
+  Proof. intros n A A' ? P P' ?. by apply iProto_message_ne; simpl. Qed.
+  Global Instance lsty_message_contractive n a :
+    Proper (dist_later n ==> dist_later n ==> dist n) (@lsty_message Σ a).
   Proof.
-    intros n A A' H1 P P' H2.
-    rewrite /lsty_send.
-    apply Lsty_ne.
-    apply iProto_message_ne; simpl; try done.
+    intros A A' ? P P' ?.
+    apply iProto_message_contractive; simpl; done || by destruct n.
   Qed.
 
+  Global Instance lsty_send_ne : NonExpansive2 (@lsty_send Σ).
+  Proof. solve_proper. Qed.
   Global Instance lsty_send_contractive n :
     Proper (dist_later n ==> dist_later n ==> dist n) (@lsty_send Σ).
-  Proof.
-    intros A A' H1 P P' H2.
-    rewrite /lsty_send.
-    apply Lsty_ne.
-    apply iProto_message_contractive; simpl; try done.
-    intros v.
-    destruct n as [|n]; try done.
-    apply H1.
-  Qed.
+  Proof. solve_contractive. Qed.
 
   Global Instance lsty_recv_ne : NonExpansive2 (@lsty_recv Σ).
-  Proof.
-    intros n A A' H1 P P' H2.
-    rewrite /lsty_recv.
-    apply Lsty_ne.
-    apply iProto_message_ne; simpl; try done.
-  Qed.
-
+  Proof. solve_proper. Qed.
   Global Instance lsty_recv_contractive n :
     Proper (dist_later n ==> dist_later n ==> dist n) (@lsty_recv Σ).
-  Proof.
-    intros A A' H1 P P' H2.
-    rewrite /lsty_recv.
-    apply Lsty_ne.
-    apply iProto_message_contractive; simpl; try done.
-    intros v.
-    destruct n as [|n]; try done.
-    apply H1.
-  Qed.
+  Proof. solve_contractive. Qed.
 
-  Global Instance lsty_branch_ne : NonExpansive2 (@lsty_branch Σ).
+  Global Instance lsty_choice_ne a : NonExpansive (@lsty_choice Σ a).
   Proof.
-    intros n A A' H1 P P' H2.
-    rewrite /lsty_branch.
-    apply Lsty_ne.
-    apply iProto_message_ne; simpl; try done.
-    intros v. destruct v; done.
+    intros n Ps1 Ps2 Pseq. apply iProto_message_ne; simpl; solve_proper.
   Qed.
-
-  Global Instance lsty_branch_contractive n :
-    Proper (dist_later n ==> dist_later n ==> dist n) (@lsty_branch Σ).
+  Global Instance lsty_choice_contractive a : Contractive (@lsty_choice Σ a).
   Proof.
-    intros A A' H1 P P' H2.
-    rewrite /lsty_branch.
-    apply Lsty_ne.
-    apply iProto_message_contractive; simpl; try done.
-    intros v.
-    destruct v; destruct n as [|n]; try done.
+    intros ? Ps1 Ps2 ?.
+    apply iProto_message_contractive; destruct n; simpl; done || solve_proper.
   Qed.
 
-  Global Instance lsty_select_ne : NonExpansive2 (@lsty_select Σ).
-  Proof.
-    intros n A A' H1 P P' H2.
-    rewrite /lsty_select.
-    apply Lsty_ne.
-    apply iProto_message_ne; simpl; try done.
-    intros v. destruct v; done.
-  Qed.
+  Global Instance lsty_select_ne : NonExpansive (@lsty_select Σ).
+  Proof. solve_proper. Qed.
+  Global Instance lsty_select_contractive : Contractive (@lsty_select Σ).
+  Proof. solve_contractive. Qed.
 
-  Global Instance lsty_select_contractive n :
-    Proper (dist_later n ==> dist_later n ==> dist n) (@lsty_select Σ).
-  Proof.
-    intros A A' H1 P P' H2.
-    rewrite /lsty_select.
-    apply Lsty_ne.
-    apply iProto_message_contractive; simpl; try done.
-    intros v.
-    destruct v; destruct n as [|n]; try done.
-  Qed.
+  Global Instance lsty_branch_ne : NonExpansive (@lsty_branch Σ).
+  Proof. solve_proper. Qed.
+  Global Instance lsty_branch_contractive : Contractive (@lsty_branch Σ).
+  Proof. solve_contractive. Qed.
 
   Global Instance lsty_dual_ne : NonExpansive (@lsty_dual Σ).
-  Proof.
-    intros n P P' HP.
-    rewrite /lsty_dual.
-    apply Lsty_ne.
-    by apply iProto_dual_ne.
-  Qed.
-
+  Proof. solve_proper. Qed.
   Global Instance lsty_app_ne : NonExpansive2 (@lsty_app Σ).
-  Proof.
-    intros n P1 P1' H1 P2 P2' H2.
-    rewrite /lsty_app.
-    apply Lsty_ne.
-    by apply iProto_app_ne.
-  Qed.
-
+  Proof. solve_proper. Qed.
 End Propers.
 
 Notation "'END'" := lsty_end : lsty_scope.
@@ -144,6 +95,4 @@ Notation "<!!> A ; P" :=
   (lsty_send A P) (at level 20, A, P at level 200) : lsty_scope.
 Notation "<??> A ; P" :=
   (lsty_recv A P) (at level 20, A, P at level 200) : lsty_scope.
-Infix "<+++>" := lsty_select (at level 60) : lsty_scope.
-Infix "<&&&>" := lsty_branch (at level 85) : lsty_scope.
 Infix "<++++>" := lsty_app (at level 60) : lsty_scope.

theories/logrel/subtyping.v

@@ -5,30 +5,26 @@ From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode.
 
 Definition lty_le {Σ} (A1 A2 : lty Σ) : iProp Σ :=
-  □ ∀ v, (A1 v -∗ A2 v).
-
+  □ ∀ v, A1 v -∗ A2 v.
 Arguments lty_le {_} _%lty _%lty.
 Infix "<:" := lty_le (at level 70).
 Instance: Params (@lty_le) 1 := {}.
 
 Instance lty_le_ne {Σ} : NonExpansive2 (@lty_le Σ).
 Proof. solve_proper. Qed.
-Instance lty_le_proper {Σ} :
-  Proper ((≡) ==> (≡) ==> (≡)) (@lty_le Σ).
+Instance lty_le_proper {Σ} : Proper ((≡) ==> (≡) ==> (≡)) (@lty_le Σ).
 Proof. solve_proper. Qed.
 
 Definition lsty_le {Σ} (P1 P2 : lsty Σ) : iProp Σ :=
-  □ (iProto_le P1 P2).
-
+  □ iProto_le P1 P2.
 Arguments lsty_le {_} _%lsty _%lsty.
 Infix "<p:" := lsty_le (at level 70).
 Instance: Params (@lsty_le) 1 := {}.
 
 Instance lsty_le_ne {Σ} : NonExpansive2 (@lsty_le Σ).
-Proof. solve_proper_prepare. f_equiv. solve_proper. Qed.
-Instance lsty_le_proper {Σ} :
-  Proper ((≡) ==> (≡) ==> (≡)) (@lsty_le Σ).
-Proof. apply ne_proper_2. apply _. Qed.
+Proof. solve_proper. Qed.
+Instance lsty_le_proper {Σ} : Proper ((≡) ==> (≡) ==> (≡)) (@lsty_le Σ).
+Proof. solve_proper. Qed.
 
 Section subtype.
   Context `{heapG Σ, chanG Σ}.
@@ -153,21 +149,11 @@ Section subtype.
     mutex A1 <: mutex A2.
   Proof.
     iIntros "#Hle1 #Hle2" (v) "!>". iDestruct 1 as (γ l lk ->) "Hinv".
-    rewrite /spin_lock.is_lock.
     iExists γ, l, lk. iSplit; first done.
-    rewrite /spin_lock.is_lock.
-    iDestruct "Hinv" as (l' ->) "Hinv".
-    iExists l'.
-    iSplit; first done.
-    iApply (inv_iff with "Hinv"); iIntros "!> !>". iSplit.
-    - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl".
-      destruct v; first done.
-      iDestruct "HA" as "[Hown HA]". iDestruct "HA" as (inner) "[Hinner HA]".
-      iDestruct ("Hle1" with "HA") as "HA". eauto with iFrame.
-    - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl".
-      destruct v; first done.
-      iDestruct "HA" as "[Hown HA]". iDestruct "HA" as (inner) "[Hinner HA]".
-      iDestruct ("Hle2" with "HA") as "HA". eauto with iFrame.
+    iApply (spin_lock.is_lock_iff with "Hinv").
+    iIntros "!> !>". iSplit.
+    - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl". by iApply "Hle1".
+    - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl". by iApply "Hle2".
   Qed.
 
   Lemma lty_mutexguard_le A1 A2 :
@@ -176,22 +162,11 @@ Section subtype.
   Proof.
     iIntros "#Hle1 #Hle2" (v) "!>".
     iDestruct 1 as (γ l lk w ->) "[Hinv [Hlock Hinner]]".
-    rewrite /spin_lock.is_lock.
     iExists γ, l, lk, w. iSplit; first done.
-    rewrite /spin_lock.is_lock.
-    iFrame "Hlock Hinner".
-    iDestruct "Hinv" as (l' ->) "Hinv".
-    iExists l'.
-    iSplit; first done.
-    iApply (inv_iff with "Hinv"); iIntros "!> !>". iSplit.
-    - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl".
-      destruct v; first done.
-      iDestruct "HA" as "[Hown HA]". iDestruct "HA" as (inner) "[Hinner HA]".
-      iDestruct ("Hle1" with "HA") as "HA". eauto with iFrame.
-    - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl".
-      destruct v; first done.
-      iDestruct "HA" as "[Hown HA]". iDestruct "HA" as (inner) "[Hinner HA]".
-      iDestruct ("Hle2" with "HA") as "HA". eauto with iFrame.
+    iFrame "Hlock Hinner". iApply (spin_lock.is_lock_iff with "Hinv").
+    iIntros "!> !>". iSplit.
+    - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl". by iApply "Hle1".
+    - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl". by iApply "Hle2".
   Qed.
 
   Lemma lsty_le_refl P : ⊢ P <p: P.
@@ -216,7 +191,7 @@ Section subtype.
     (<??> A1 ; P1) <p: (<??> A2 ; P2).
   Proof.
     iIntros "#HAle #HPle !>".
-    iApply iProto_le_recv=> /=.
+    iApply iProto_le_recv; simpl.
     iIntros (x) "H !>".
     iDestruct ("HAle" with "H") as "H".
     eauto with iFrame.
@@ -230,34 +205,82 @@ Section subtype.
     iExists _, _,
       (tele_app (TT:=[tele _]) (λ x2, (x2, A2 x2, (P:iProto Σ)))),
       (tele_app (TT:=[tele _]) (λ x1, (x1, A1 x1, (P:iProto Σ)))),
-    x2, x1.
-    simpl.
+      x2, x1; simpl.
     do 2 (iSplit; [done|]).
     iFrame "HP1 HP2".
     iModIntro.
     do 2 (iSplitR; [iApply iProto_le_refl|]). by iFrame.
   Qed.
 
-  Lemma lsty_select_le P11 P12 P21 P22 :
-    ▷ (P11 <p: P21) -∗ ▷ (P12 <p: P22) -∗
-    (P11 <+++> P12) <p: (P21 <+++> P22).
+  Lemma lsty_select_le_subseteq (Ps1 Ps2 : gmap Z (lsty Σ)) :
+    Ps2 ⊆ Ps1 →
+    ⊢ lsty_select Ps1 <p: lsty_select Ps2.
   Proof.
-    iIntros "#H1 #H2 !>".
-    rewrite /lsty_select /iProto_branch=> /=.
-    iApply iProto_le_send=> /=.
-    iIntros (x) "_ !>".
-    destruct x; eauto with iFrame.
+    iIntros (Hsub) "!>".
+    iApply iProto_le_send; simpl.
+    iIntros (x) ">% !> /=".
+    iExists _. iSplit; first done.
+    iSplit.
+    { iNext. iPureIntro. by eapply lookup_weaken_is_Some. }
+    iNext.
+    destruct H1 as [P H1].
+    assert (Ps1 !! x = Some P) by eauto using lookup_weaken.
+    rewrite (lookup_total_correct Ps1 x P) //.
+    rewrite (lookup_total_correct Ps2 x P) //.
+    iApply iProto_le_refl.
   Qed.
 
-  Lemma lsty_branch_le P11 P12 P21 P22 :
-    ▷ (P11 <p: P21) -∗ ▷ (P12 <p: P22) -∗
-    (P11 <&&&> P12) <p: (P21 <&&&> P22).
+  Lemma lsty_select_le (Ps1 Ps2 : gmap Z (lsty Σ)) :
+    (▷ [∗ map] i ↦ P1;P2 ∈ Ps1; Ps2, P1 <p: P2) -∗
+    lsty_select Ps1 <p: lsty_select Ps2.
   Proof.
-    iIntros "#H1 #H2 !>".
-    rewrite /lsty_branch /iProto_branch=> /=.
-    iApply iProto_le_recv=> /=.
-    iIntros (x) "_ !>".
-    destruct x; eauto with iFrame.
+    iIntros "#H1 !>".
+    iApply iProto_le_send; simpl.
+    iIntros (x) ">H !>"; iDestruct "H" as %Hsome.
+    iExists x. iSplit=> //. iSplit.
+    - iNext. 
+      iDestruct (big_sepM2_forall with "H1") as "[% _]".
+      iPureIntro. naive_solver.
+    - iNext.
+      iDestruct (big_sepM2_forall with "H1") as "[% H]".
+      iApply ("H" with "[] []").
+      + iPureIntro. apply lookup_lookup_total; naive_solver.
+      + iPureIntro. by apply lookup_lookup_total.
+  Qed.
+
+  Lemma lsty_branch_le_subseteq (Ps1 Ps2 : gmap Z (lsty Σ)) :
+    Ps1 ⊆ Ps2 →
+    ⊢ lsty_branch Ps1 <p: lsty_branch Ps2.
+  Proof.
+    iIntros (Hsub) "!>".
+    iApply iProto_le_recv; simpl.
+    iIntros (x) ">% !> /=".
+    iExists _. iSplit; first done.
+    iSplit.
+    { iNext. iPureIntro. by eapply lookup_weaken_is_Some. }
+    iNext.
+    destruct H1 as [P ?].
+    assert (Ps2 !! x = Some P) by eauto using lookup_weaken.
+    rewrite (lookup_total_correct Ps1 x P) //.
+    rewrite (lookup_total_correct Ps2 x P) //.
+    iApply iProto_le_refl.
+  Qed.
+
+  Lemma lsty_branch_le (Ps1 Ps2 : gmap Z (lsty Σ)) :
+    (▷ [∗ map] i ↦ P1;P2 ∈ Ps1; Ps2, P1 <p: P2) -∗
+    lsty_branch Ps1 <p: lsty_branch Ps2.
+  Proof.
+    iIntros "#H1 !>". iApply iProto_le_recv.
+    iIntros (x) ">H !>"; iDestruct "H" as %Hsome.
+    iExists x. iSplit; first done. iSplit.
+    - iNext.
+      iDestruct (big_sepM2_forall with "H1") as "[% _]".
+      iPureIntro. by naive_solver.
+    - iNext.
+      iDestruct (big_sepM2_forall with "H1") as "[% H]".
+      iApply ("H" with "[] []").
+      + iPureIntro. by apply lookup_lookup_total.
+      + iPureIntro. by apply lookup_lookup_total; naive_solver.
   Qed.
 
   Lemma lsty_app_le P11 P12 P21 P22 :
@@ -285,9 +308,8 @@ Section subtype.
     (□ ∀ P P', ▷ (P <p: P') -∗ C1 P <p: C2 P') -∗
     lsty_rec C1 <p: lsty_rec C2.
   Proof.
-    iIntros "#Hle".
+    iIntros "#Hle !>".
     iLöb as "IH".
-    iIntros "!>".
     rewrite /lsty_rec.
     iEval (rewrite fixpoint_unfold).
     iEval (rewrite (fixpoint_unfold (lsty_rec1 C2))).

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,48 @@ 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))=> /=.
+      do 2 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.
@@ -684,36 +729,56 @@ Section properties.
       iExists v, c. eauto with iFrame.
     Qed.
 
-    Definition chanfst : val := λ: "c", send "c" #true;; "c".
-    Lemma ltyped_chanfst P1 P2:
-      ⊢ ∅ ⊨ chanfst : chan (P1 <+++> P2) → chan P1.
+    Definition chanselect : val := λ: "c" "i", send "c" "i";; "c".
+    Lemma ltyped_chanselect Γ (c : val) (i : Z) P Ps :
+      Ps !! i = Some P →
+      (Γ ⊨ c : chan (lsty_select Ps)) -∗
+      Γ ⊨ chanselect c #i : chan P.
     Proof.
-      iIntros (vs) "!> _ /=". iApply wp_value.
-      iIntros "!>" (c) "Hc". rewrite /chanfst. wp_select.
-      wp_pures. iExact "Hc".
+      iIntros (Hin) "#Hc !>".
+      iIntros (vs) "H /=".
+      rewrite /chanselect.
+      iMod (wp_value_inv with "(Hc H)") as "Hc'".
+      wp_send with "[]"; [by eauto|].
+      rewrite (lookup_total_correct Ps i P)=> //.
+      by wp_pures.
     Qed.
 
-    Definition chansnd : val := λ: "c", send "c" #false;; "c".
-    Lemma ltyped_chansnd P1 P2:
-      ⊢ ∅ ⊨ chansnd : chan (P1 <+++> P2) → chan P2.
-    Proof.
-      iIntros (vs) "!> _ /=". iApply wp_value.
-      iIntros "!>" (c) "Hc". rewrite /chansnd. wp_select.
-      wp_pures. iExact "Hc".
-    Qed.
+    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".
 
-    Definition chanbranch : val := λ: "c",
-      let b := recv "c" in if: b then InjL "c" else InjR "c".
-
-    Lemma ltyped_chanbranch P1 P2:
-      ⊢ ∅ ⊨ chanbranch : chan (P1 <&&&> P2) → chan P1 + chan P2.
+    Lemma ltyped_chanbranch Ps A xs :
+      (∀ x, x ∈ xs ↔ is_Some (Ps !! x)) →
+      ⊢ ∅ ⊨ chanbranch xs : chan (lsty_branch Ps) ⊸
+        lty_arr_list ((λ x, (chan (Ps !!! x) ⊸ A)%lty) <$> xs) A.
     Proof.
-      iIntros (vs) "!> _ /=". iApply wp_value.
-      iIntros "!>" (c) "Hc". rewrite /chanbranch. wp_pures.
-      wp_branch; wp_pures.
-      - iLeft. iExists c. iSplit=> //.
-      - iRight. iExists c. iSplit=> //.
+      iIntros (Hdom) "!>". iIntros (vs) "Hvs".
+      iApply wp_value. iIntros (c) "Hc". wp_lam.
+      rewrite -subst_map_singleton.
+      iApply lty_arr_list_spec.
+      { by rewrite fmap_length. }
+      iIntros (ws) "H".
+      rewrite big_sepL2_fmap_l.
+      iDestruct (big_sepL2_length with "H") as %Heq.
+      rewrite -insert_union_singleton_r; last by apply lookup_map_string_seq_None.
+      rewrite /= lookup_insert.
+      wp_recv (x) as "HPsx". iDestruct "HPsx" as %HPs_Some.
+      wp_pures.
+      rewrite -subst_map_insert.
+      assert (x ∈ xs) as Hin by naive_solver.
+      pose proof (list_find_elem_of (x =.) xs x) as [[n z] Hfind_Some]; [done..|].
+      iApply switch_body_spec.
+      { apply fmap_Some_2, Hfind_Some. }
+      { by rewrite lookup_insert. }
+      simplify_map_eq. rewrite lookup_map_string_seq_Some.
+      assert (xs !! n = Some x) as Hxs_Some.
+      { by apply list_find_Some in Hfind_Some as [? [-> _]]. }
+      assert (is_Some (ws !! n)) as [w Hws_Some].
+      { apply lookup_lt_is_Some_2. rewrite -Heq. eauto using lookup_lt_Some. }
+      iDestruct (big_sepL2_lookup _ xs ws n with "H") as "HA"; [done..|].
+      rewrite Hws_Some. by iApply "HA".
     Qed.
-
   End with_chan.
 End properties.