subtyping_rules.v 18 KB
Newer Older
Daniël Louwrink's avatar
Daniël Louwrink committed
1 2
(** This file defines all of the semantic subtyping rules for term types and
session types. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
3 4 5 6 7 8 9 10 11 12 13 14
From iris.bi.lib Require Import core.
From iris.base_logic.lib Require Import invariants.
From iris.proofmode Require Import tactics.
From actris.logrel Require Export subtyping term_types session_types.

Section subtyping_rules.
  Context `{heapG Σ, chanG Σ}.
  Implicit Types A : ltty Σ.
  Implicit Types S : lsty Σ.

  (** Generic rules *)
  Lemma lty_le_refl {k} (M : lty Σ k) :  M <: M.
Robbert Krebbers's avatar
Robbert Krebbers committed
15
  Proof. destruct k. by iIntros (v) "!> H". by iModIntro. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53
  Lemma lty_le_trans {k} (M1 M2 M3 : lty Σ k) : M1 <: M2 - M2 <: M3 - M1 <: M3.
  Proof.
    destruct k.
    - iIntros "#H1 #H2" (v) "!> H". iApply "H2". by iApply "H1".
    - iIntros "#H1 #H2 !>". by iApply iProto_le_trans.
  Qed.

  Lemma lty_bi_le_refl {k} (M : lty Σ k) :  M <:> M.
  Proof. iSplit; iApply lty_le_refl. Qed.
  Lemma lty_bi_le_trans {k} (M1 M2 M3 : lty Σ k) : M1 <:> M2 - M2 <:> M3 - M1 <:> M3.
  Proof. iIntros "#[H11 H12] #[H21 H22]". iSplit; by iApply lty_le_trans. Qed.
  Lemma lty_bi_le_sym {k} (M1 M2 : lty Σ k) : M1 <:> M2 - M2 <:> M1.
  Proof. iIntros "#[??]"; by iSplit. Qed.

  Lemma lty_le_l {k} (M1 M2 M3 : lty Σ k) : M1 <:> M2 - M2 <: M3 - M1 <: M3.
  Proof. iIntros "#[H1 _] #H2". by iApply lty_le_trans. Qed.
  Lemma lty_le_r {k} (M1 M2 M3 : lty Σ k) : M1 <: M2 - M2 <:> M3 - M1 <: M3.
  Proof. iIntros "#H1 #[H2 _]". by iApply lty_le_trans. Qed.

  Lemma lty_le_rec_unfold {k} (C : lty Σ k  lty Σ k) `{!Contractive C} :
     lty_rec C <:> C (lty_rec C).
  Proof.
    iSplit.
    - rewrite {1}/lty_rec fixpoint_unfold. iApply lty_le_refl.
    - rewrite {2}/lty_rec fixpoint_unfold. iApply lty_le_refl.
  Qed.

  Lemma lty_le_rec {k} (C1 C2 : lty Σ k  lty Σ k) `{Contractive C1, Contractive C2} :
    ( M1 M2,  (M1 <: M2) - C1 M1 <: C2 M2) -
    lty_rec C1 <: lty_rec C2.
  Proof.
    iIntros "#Hle". iLöb as "IH".
    iApply lty_le_l; [iApply lty_le_rec_unfold|].
    iApply lty_le_r; [|iApply lty_bi_le_sym; iApply lty_le_rec_unfold].
    by iApply "Hle".
  Qed.

  (** Term subtyping *)
Jonas Kastberg's avatar
Jonas Kastberg committed
54
  Lemma lty_le_any A :  A <: any.
Robbert Krebbers's avatar
Robbert Krebbers committed
55
  Proof. by iIntros (v) "!> H". Qed.
Jonas Kastberg's avatar
Jonas Kastberg committed
56
  Lemma lty_copyable_any : @{iPropI Σ} lty_copyable any.
Robbert Krebbers's avatar
Robbert Krebbers committed
57 58 59 60 61 62 63 64 65
  Proof. iIntros (v) "!> #Hv !>". iFrame "Hv". Qed.

  Lemma lty_le_copy A B : A <: B - copy A <: copy B.
  Proof. iIntros "#Hle". iIntros (v) "!> #HA !>". by iApply "Hle". Qed.
  Lemma lty_le_copy_elim A :  copy A <: A.
  Proof. by iIntros (v) "!> #H". Qed.
  Lemma lty_copyable_copy A : @{iPropI Σ} lty_copyable (copy A).
  Proof. iIntros (v) "!> #Hv !>". iFrame "Hv". Qed.

66
  Lemma lty_le_copy_inv_mono A B : A <: B - copy- A <: copy- B.
Robbert Krebbers's avatar
Robbert Krebbers committed
67 68 69 70 71 72 73 74 75 76
  Proof.
    iIntros "#Hle !>" (v) "#HA". iApply (coreP_wand (ltty_car A v) with "[] HA").
    iIntros "{HA} !> !>". iApply "Hle".
  Qed.
  Lemma lty_le_copy_inv_intro A :  A <: copy- A.
  Proof. iIntros "!>" (v). iApply coreP_intro. Qed.
  Lemma lty_le_copy_inv_elim A :  copy- (copy A) <: A.
  Proof. iIntros (v) "!> #H". iApply (coreP_elim with "H"). Qed.
  Lemma lty_copyable_copy_inv A :  lty_copyable (copy- A).
  Proof. iIntros (v) "!> #Hv !>". iFrame "Hv". Qed.
77 78 79 80 81 82 83
  Lemma lty_le_copy_inv_elim_copyable A : lty_copyable A - copy- A <: A.
  Proof.
    iIntros "#Hcp".
    iApply lty_le_trans.
    - iApply lty_le_copy_inv_mono. iApply "Hcp".
    - iApply lty_le_copy_inv_elim.
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105

  Lemma lty_copyable_unit : @{iPropI Σ} lty_copyable ().
  Proof. iIntros (v) "!> #Hv !>". iFrame "Hv". Qed.
  Lemma lty_copyable_bool : @{iPropI Σ} lty_copyable lty_bool.
  Proof. iIntros (v) "!> #Hv !>". iFrame "Hv". Qed.
  Lemma lty_copyable_int : @{iPropI Σ} lty_copyable lty_int.
  Proof. iIntros (v) "!> #Hv !>". iFrame "Hv". Qed.

  Lemma lty_le_arr A11 A12 A21 A22 :
     (A21 <: A11) -  (A12 <: A22) -
    (A11  A12) <: (A21  A22).
  Proof.
    iIntros "#H1 #H2" (v) "!> H". iIntros (w) "H'".
    iApply (wp_step_fupd); first done.
    { iIntros "!>!>!>". iExact "H2". }
    iApply (wp_wand with "(H (H1 H'))"). iIntros (v') "H Hle !>".
    by iApply "Hle".
  Qed.
  Lemma lty_le_arr_copy A11 A12 A21 A22 :
     (A21 <: A11) -  (A12 <: A22) -
    (A11  A12) <: (A21  A22).
  Proof. iIntros "#H1 #H2" (v) "!> #H !>". by iApply lty_le_arr. Qed.
106 107 108 109
  (* This rule is really trivial, since → is syntactic sugar for copy (... ⊸ ...),
     but we include it anyway for completeness' sake. *)
  Lemma lty_copyable_arr_copy A B : @{iPropI Σ} lty_copyable (A  B).
  Proof. iApply lty_copyable_copy. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
110 111 112 113 114 115 116 117 118 119

  Lemma lty_le_prod A11 A12 A21 A22 :
     (A11 <: A21) -  (A12 <: A22) -
    A11 * A12 <: A21 * A22.
  Proof.
    iIntros "#H1 #H2" (v) "!>". iDestruct 1 as (w1 w2 ->) "[H1' H2']".
    iExists _, _.
    iDestruct ("H1" with "H1'") as "$".
    by iDestruct ("H2" with "H2'") as "$".
  Qed.
120

Robbert Krebbers's avatar
Robbert Krebbers committed
121 122 123 124 125 126 127 128
  Lemma lty_le_prod_copy A B :
     copy A * copy B <:> copy (A * B).
  Proof.
    iSplit; iModIntro; iIntros (v) "#Hv"; iDestruct "Hv" as (v1 v2 ->) "[Hv1 Hv2]".
    - iModIntro. iExists v1, v2. iSplit; [done|]. iSplitL; auto.
    - iExists v1, v2. iSplit; [done|]. auto.
  Qed.

129 130 131 132 133 134 135 136 137 138
  Lemma lty_copyable_prod A B :
    lty_copyable A - lty_copyable B - lty_copyable (A * B).
  Proof.
    iIntros "#HcpA #HcpB". rewrite /lty_copyable /tc_opaque.
    iApply lty_le_r; last by iApply lty_le_prod_copy.
    iApply lty_le_prod.
    - iApply "HcpA".
    - iApply "HcpB".
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
139 140 141 142 143 144 145 146 147 148 149 150 151 152 153
  Lemma lty_le_sum A11 A12 A21 A22 :
     (A11 <: A21) -  (A12 <: A22) -
    A11 + A12 <: A21 + A22.
  Proof.
    iIntros "#H1 #H2" (v) "!> [H | H]"; iDestruct "H" as (w ->) "H".
    - iDestruct ("H1" with "H") as "H1'". iLeft; eauto.
    - iDestruct ("H2" with "H") as "H2'". iRight; eauto.
  Qed.
  Lemma lty_le_sum_copy A B :
     copy A + copy B <:> copy (A + B).
  Proof.
    iSplit; iModIntro; iIntros (v);
      iDestruct 1 as "#[Hv|Hv]"; iDestruct "Hv" as (w ?) "Hw";
      try iModIntro; first [iLeft; by auto|iRight; by auto].
  Qed.
154 155 156 157 158 159 160 161 162
  Lemma lty_copyable_sum A B :
    lty_copyable A - lty_copyable B - lty_copyable (A + B).
  Proof.
    iIntros "#HcpA #HcpB". rewrite /lty_copyable /tc_opaque.
    iApply lty_le_r; last by iApply lty_le_sum_copy.
    iApply lty_le_sum.
    - iApply "HcpA".
    - iApply "HcpB".
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
163

Jonas Kastberg's avatar
Jonas Kastberg committed
164 165 166
  Lemma lty_le_forall C1 C2 :
     ( A, C1 A <: C2 A) -
    ( A, C1 A) <: ( A, C2 A).
Robbert Krebbers's avatar
Robbert Krebbers committed
167
  Proof.
Jonas Kastberg's avatar
Jonas Kastberg committed
168 169 170 171 172
    iIntros "#Hle" (v) "!> H". iIntros (w).
    iApply (wp_step_fupd); first done.
    { iIntros "!>!>!>". iExact "Hle". }
    iApply (wp_wand with "H"). iIntros (v') "H Hle' !>".
    by iApply "Hle'".
Robbert Krebbers's avatar
Robbert Krebbers committed
173 174
  Qed.

Jonas Kastberg's avatar
Jonas Kastberg committed
175
  Lemma lty_le_exist C1 C2 :
176
     ( A, C1 A <: C2 A) -
Jonas Kastberg's avatar
Jonas Kastberg committed
177
    ( A, C1 A) <: ( A, C2 A).
Robbert Krebbers's avatar
Robbert Krebbers committed
178
  Proof.
Jonas Kastberg's avatar
Jonas Kastberg committed
179
    iIntros "#Hle" (v) "!>". iDestruct 1 as (A) "H". iExists A. by iApply "Hle".
Robbert Krebbers's avatar
Robbert Krebbers committed
180
  Qed.
Jonas Kastberg's avatar
Jonas Kastberg committed
181 182 183 184 185
  Lemma lty_le_exist_elim C B :
     C B <:  A, C A.
  Proof. iIntros "!>" (v) "Hle". by iExists B. Qed.
  Lemma lty_le_exist_copy F :
     ( A, copy (F A)) <:> copy ( A, F A).
Robbert Krebbers's avatar
Robbert Krebbers committed
186
  Proof.
Jonas Kastberg's avatar
Jonas Kastberg committed
187 188
    iSplit; iIntros "!>" (v); iDestruct 1 as (A) "#Hv";
      iExists A; repeat iModIntro; iApply "Hv".
Robbert Krebbers's avatar
Robbert Krebbers committed
189
  Qed.
190 191

  Lemma lty_copyable_exist (C : ltty Σ  ltty Σ) :
Daniël Louwrink's avatar
Daniël Louwrink committed
192
    ( M, lty_copyable (C M)) - lty_copyable (lty_exist C).
193 194 195
  Proof.
    iIntros "#Hle". rewrite /lty_copyable /tc_opaque.
    iApply lty_le_r; last by iApply lty_le_exist_copy.
196
    iApply lty_le_exist. iApply "Hle".
197
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
198

Daniël Louwrink's avatar
Daniël Louwrink committed
199 200
  (* TODO: Try to add Löb induction in the type system, and use it to prove μX.int → X <:> μX.int → int → X *)

Robbert Krebbers's avatar
Robbert Krebbers committed
201
  (* TODO(COPY): Commuting rule for μ, allowing `copy` to move outside the μ *)
202
  Lemma lty_copyable_rec C `{!Contractive C} :
Robbert Krebbers's avatar
Robbert Krebbers committed
203 204 205 206 207 208 209 210 211 212 213 214 215 216 217
    ( A,  lty_copyable A - lty_copyable (C A)) - lty_copyable (lty_rec C).
  Proof.
    iIntros "#Hcopy".
    iLöb as "IH".
    iIntros (v) "!> Hv".
    rewrite /lty_rec.
    rewrite {2}fixpoint_unfold.
    iSpecialize ("Hcopy" with "IH").
    iSpecialize ("Hcopy" with "Hv").
    iDestruct "Hcopy" as "#Hcopy".
    iModIntro.
    iEval (rewrite fixpoint_unfold).
    iApply "Hcopy".
  Qed.

Daniël Louwrink's avatar
Daniël Louwrink committed
218
  Lemma lty_le_ref_uniq A1 A2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
219
     (A1 <: A2) -
Daniël Louwrink's avatar
Daniël Louwrink committed
220
    ref_uniq A1 <: ref_uniq A2.
Robbert Krebbers's avatar
Robbert Krebbers committed
221 222 223 224 225 226 227 228 229 230 231 232 233
  Proof.
    iIntros "#H1" (v) "!>". iDestruct 1 as (l w ->) "[Hl HA]".
    iDestruct ("H1" with "HA") as "HA".
    iExists l, w. by iFrame.
  Qed.

  Lemma lty_le_shr_ref A1 A2 :
     (A1 <:> A2) -
    ref_shr A1 <: ref_shr A2.
  Proof.
    iIntros "#[Hle1 Hle2]" (v) "!>". iDestruct 1 as (l ->) "Hinv".
    iExists l. iSplit; first done.
    iApply (inv_iff with "Hinv"). iIntros "!> !>". iSplit.
234 235
    - iDestruct 1 as (v) "[Hl #HA]". iExists v. iIntros "{$Hl} !>". by iApply "Hle1".
    - iDestruct 1 as (v) "[Hl #HA]". iExists v. iIntros "{$Hl} !>". by iApply "Hle2".
Robbert Krebbers's avatar
Robbert Krebbers committed
236 237 238 239 240 241 242 243 244 245 246 247 248 249 250
  Qed.
  Lemma lty_copyable_shr_ref A :
     lty_copyable (ref_shr A).
  Proof. iIntros (v) "!> #Hv !>". iFrame "Hv". Qed.

  Lemma lty_le_chan S1 S2 :
     (S1 <: S2) - chan S1 <: chan S2.
  Proof.
    iIntros "#Hle" (v) "!> H".
    iApply (iProto_mapsto_le with "H [Hle]"). eauto.
  Qed.

  (** Session subtyping *)
  Lemma lty_le_send A1 A2 S1 S2 :
     (A2 <: A1) -  (S1 <: S2) -
251
    (<!!> TY A1 ; S1) <: (<!!> TY A2 ; S2).
Robbert Krebbers's avatar
Robbert Krebbers committed
252
  Proof.
253
    iIntros "#HAle #HSle !>" (v) "H". iExists v.
Robbert Krebbers's avatar
Robbert Krebbers committed
254
    iDestruct ("HAle" with "H") as "$". by iModIntro.
Robbert Krebbers's avatar
Robbert Krebbers committed
255 256 257 258
  Qed.

  Lemma lty_le_recv A1 A2 S1 S2 :
     (A1 <: A2) -  (S1 <: S2) -
259
    (<??> TY A1 ; S1) <: (<??> TY A2 ; S2).
Robbert Krebbers's avatar
Robbert Krebbers committed
260
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
261 262
    iIntros "#HAle #HSle !>" (v) "H". iExists v.
    iDestruct ("HAle" with "H") as "$". by iModIntro.
Robbert Krebbers's avatar
Robbert Krebbers committed
263 264
  Qed.

265 266 267
  Lemma lty_le_exist_elim_l k (M : lty Σ k  lmsg Σ) S :
    ( (A : lty Σ k), (<??> M A) <: S) -
    ((<?? (A : lty Σ k)> M A) <: S).
268 269
  Proof. iIntros "#Hle !>". iApply (iProto_le_exist_elim_l_inhabited M). auto. Qed.

270 271 272
  Lemma lty_le_exist_elim_r k (M : lty Σ k  lmsg Σ) S :
    ( (A : lty Σ k), S <: (<!!> M A)) -
    (S <: (<!! (A : lty Σ k)> M A)).
273 274 275
  Proof. iIntros "#Hle !>". iApply (iProto_le_exist_elim_r_inhabited _ M). auto. Qed.

  Lemma lty_le_exist_intro_l k (M : lty Σ k  lmsg Σ) (A : lty Σ k) :
276 277
     (<!! X> M X) <: (<!!> M A).
  Proof. iIntros "!>". iApply (iProto_le_exist_intro_l). Qed.
278 279

  Lemma lty_le_exist_intro_r k (M : lty Σ k  lmsg Σ) (A : lty Σ k) :
280 281
     (<??> M A) <: (<?? X> M X).
  Proof. iIntros "!>". iApply (iProto_le_exist_intro_r). Qed.
282

283
  (* Elimination rules need inhabited variant of telescopes in the model *)
Robbert Krebbers's avatar
Tweaks.  
Robbert Krebbers committed
284
  Lemma lty_le_texist_elim_l {kt} (M : ltys Σ kt  lmsg Σ) S :
285 286
    ( Xs, (<??> M Xs) <: S) -
    (<??.. Xs> M Xs) <: S.
Robbert Krebbers's avatar
Tweaks.  
Robbert Krebbers committed
287 288 289 290 291
  Proof.
    iIntros "H". iInduction kt as [|k kt] "IH"; simpl; [done|].
    iApply lty_le_exist_elim_l; iIntros (X).
    iApply "IH". iIntros (Xs). iApply "H".
  Qed.
292

293
  Lemma lty_le_texist_elim_r {kt : ktele Σ} (M : ltys Σ kt  lmsg Σ) S :
294 295
    ( Xs, S <: (<!!> M Xs)) -
    S <: (<!!.. Xs> M Xs).
Robbert Krebbers's avatar
Tweaks.  
Robbert Krebbers committed
296 297 298 299 300
  Proof.
    iIntros "H". iInduction kt as [|k kt] "IH"; simpl; [done|].
    iApply lty_le_exist_elim_r; iIntros (X).
    iApply "IH". iIntros (Xs). iApply "H".
  Qed.
301

302
  Lemma lty_le_texist_intro_l {kt : ktele Σ} (M : ltys Σ kt  lmsg Σ) Ks :
303
     (<!!.. Xs> M Xs) <: (<!!> M Ks).
Robbert Krebbers's avatar
Tweaks.  
Robbert Krebbers committed
304 305 306 307
  Proof.
    induction Ks as [|k kT X Xs IH]; simpl; [iApply lty_le_refl|].
    iApply lty_le_trans; [by iApply lty_le_exist_intro_l|]. iApply IH.
  Qed.
308

309
  Lemma lty_le_texist_intro_r {kt : ktele Σ} (M : ltys Σ kt  lmsg Σ) Ks :
310
     (<??> M Ks) <: (<??.. Xs> M Xs).
Robbert Krebbers's avatar
Tweaks.  
Robbert Krebbers committed
311 312 313 314
  Proof.
    induction Ks as [|k kt X Xs IH]; simpl; [iApply lty_le_refl|].
    iApply lty_le_trans; [|by iApply lty_le_exist_intro_r]. iApply IH.
  Qed.
315

316
  Lemma lty_le_swap_recv_send A1 A2 S :
317
     (<??> TY A1; <!!> TY A2; S) <: (<!!> TY A2; <??> TY A1; S).
Robbert Krebbers's avatar
Robbert Krebbers committed
318
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
319 320 321 322 323 324
    iIntros "!>" (v1 v2).
    iApply iProto_le_trans;
      [iApply iProto_le_base; iApply (iProto_le_exist_intro_l _ v2)|].
    iApply iProto_le_trans;
      [|iApply iProto_le_base; iApply (iProto_le_exist_intro_r _ v1)]; simpl.
    iApply iProto_le_base_swap.
Robbert Krebbers's avatar
Robbert Krebbers committed
325 326
  Qed.

327
  Lemma lty_le_swap_recv_select A Ss :
328
     (<??> TY A; lty_select Ss) <: lty_select ((λ S, <??> TY A; S) <$> Ss)%lty.
Robbert Krebbers's avatar
Robbert Krebbers committed
329 330 331 332 333
  Proof.
    iIntros "!>" (v1 x2).
    iApply iProto_le_trans;
      [iApply iProto_le_base; iApply (iProto_le_exist_intro_l _ x2)|]; simpl.
    iApply iProto_le_payload_elim_r.
Jonas Kastberg's avatar
Nit  
Jonas Kastberg committed
334
    iMod 1 as %HSs. revert HSs.
Robbert Krebbers's avatar
Robbert Krebbers committed
335 336 337
    rewrite !lookup_total_alt !lookup_fmap fmap_is_Some; iIntros ([S ->]) "/=".
    iApply iProto_le_trans; [iApply iProto_le_base_swap|]. iSplitL; [by eauto|].
    iModIntro. by iExists v1.
338 339 340
  Qed.

  Lemma lty_le_swap_branch_send A Ss :
341
     lty_branch ((λ S, <!!> TY A; S) <$> Ss)%lty <: (<!!> TY A; lty_branch Ss).
Robbert Krebbers's avatar
Robbert Krebbers committed
342 343 344 345 346
  Proof.
    iIntros "!>" (x1 v2).
    iApply iProto_le_trans;
      [|iApply iProto_le_base; iApply (iProto_le_exist_intro_r _ x1)]; simpl.
    iApply iProto_le_payload_elim_l.
347
    iMod 1 as %HSs. revert HSs.
Robbert Krebbers's avatar
Robbert Krebbers committed
348 349 350
    rewrite !lookup_total_alt !lookup_fmap fmap_is_Some; iIntros ([S ->]) "/=".
    iApply iProto_le_trans; [|iApply iProto_le_base_swap]. iSplitL; [by eauto|].
    iModIntro. by iExists v2.
351 352
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
353 354 355 356
  Lemma lty_le_select (Ss1 Ss2 : gmap Z (lsty Σ)) :
     ([ map] S1;S2  Ss1; Ss2, S1 <: S2) -
    lty_select Ss1 <: lty_select Ss2.
  Proof.
357
    iIntros "#H !>" (x); iMod 1 as %[S2 HSs2]. iExists x.
Robbert Krebbers's avatar
Robbert Krebbers committed
358 359 360 361 362
    iDestruct (big_sepM2_forall with "H") as "{H} [>% H]".
    assert (is_Some (Ss1 !! x)) as [S1 HSs1] by naive_solver.
    rewrite HSs1. iSplitR; [by eauto|].
    iIntros "!>". rewrite !lookup_total_alt HSs1 HSs2 /=.
    by iApply ("H" with "[] []").
Robbert Krebbers's avatar
Robbert Krebbers committed
363 364 365 366 367
  Qed.
  Lemma lty_le_select_subseteq (Ss1 Ss2 : gmap Z (lsty Σ)) :
    Ss2  Ss1 
     lty_select Ss1 <: lty_select Ss2.
  Proof.
368
    intros; iIntros "!>" (x); iMod 1 as %[S HSs2]. iExists x.
Robbert Krebbers's avatar
Robbert Krebbers committed
369 370 371
    assert (Ss1 !! x = Some S) as HSs1 by eauto using lookup_weaken.
    rewrite HSs1. iSplitR; [by eauto|].
    iIntros "!>". by rewrite !lookup_total_alt HSs1 HSs2 /=.
Robbert Krebbers's avatar
Robbert Krebbers committed
372 373 374 375 376 377
  Qed.

  Lemma lty_le_branch (Ss1 Ss2 : gmap Z (lsty Σ)) :
     ([ map] S1;S2  Ss1; Ss2, S1 <: S2) -
    lty_branch Ss1 <: lty_branch Ss2.
  Proof.
378
    iIntros "#H !>" (x); iMod 1 as %[S1 HSs1]. iExists x.
Robbert Krebbers's avatar
Robbert Krebbers committed
379 380 381 382 383
    iDestruct (big_sepM2_forall with "H") as "{H} [>% H]".
    assert (is_Some (Ss2 !! x)) as [S2 HSs2] by naive_solver.
    rewrite HSs2. iSplitR; [by eauto|].
    iIntros "!>". rewrite !lookup_total_alt HSs1 HSs2 /=.
    by iApply ("H" with "[] []").
Robbert Krebbers's avatar
Robbert Krebbers committed
384 385 386 387 388
  Qed.
  Lemma lty_le_branch_subseteq (Ss1 Ss2 : gmap Z (lsty Σ)) :
    Ss1  Ss2 
     lty_branch Ss1 <: lty_branch Ss2.
  Proof.
389
    intros; iIntros "!>" (x); iMod 1 as %[S HSs1]. iExists x.
Robbert Krebbers's avatar
Robbert Krebbers committed
390 391 392
    assert (Ss2 !! x = Some S) as HSs2 by eauto using lookup_weaken.
    rewrite HSs2. iSplitR; [by eauto|].
    iIntros "!>". by rewrite !lookup_total_alt HSs1 HSs2 /=.
Robbert Krebbers's avatar
Robbert Krebbers committed
393 394 395 396 397 398 399 400 401
  Qed.

  (** Algebraic laws *)
  Lemma lty_le_app S11 S12 S21 S22 :
    (S11 <: S21) - (S12 <: S22) -
    (S11 <++> S12) <: (S21 <++> S22).
  Proof. iIntros "#H1 #H2 !>". by iApply iProto_le_app. Qed.

  Lemma lty_le_app_id_l S :  (END <++> S) <:> S.
Robbert Krebbers's avatar
Robbert Krebbers committed
402
  Proof. rewrite /lty_app left_id. iSplit; by iModIntro. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
403
  Lemma lty_le_app_id_r S :  (S <++> END) <:> S.
Robbert Krebbers's avatar
Robbert Krebbers committed
404
  Proof. rewrite /lty_app right_id. iSplit; by iModIntro. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
405 406
  Lemma lty_le_app_assoc S1 S2 S3 :
     (S1 <++> S2) <++> S3 <:> S1 <++> (S2 <++> S3).
Robbert Krebbers's avatar
Robbert Krebbers committed
407
  Proof. rewrite /lty_app assoc. iSplit; by iModIntro. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
408

409
  Lemma lty_le_app_send A S1 S2 :  (<!!> TY A; S1) <++> S2 <:> (<!!> TY A; S1 <++> S2).
Robbert Krebbers's avatar
Robbert Krebbers committed
410
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
411 412
    rewrite /lty_app iProto_app_message iMsg_app_exist.
    setoid_rewrite iMsg_app_base. iSplit; by iIntros "!> /=".
Robbert Krebbers's avatar
Robbert Krebbers committed
413
  Qed.
414
  Lemma lty_le_app_recv A S1 S2 :  (<??> TY A; S1) <++> S2 <:> (<??> TY A; S1 <++> S2).
Robbert Krebbers's avatar
Robbert Krebbers committed
415
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
416 417
    rewrite /lty_app iProto_app_message iMsg_app_exist.
    setoid_rewrite iMsg_app_base. iSplit; by iIntros "!> /=".
Robbert Krebbers's avatar
Robbert Krebbers committed
418 419 420 421 422
  Qed.

  Lemma lty_le_app_choice a (Ss : gmap Z (lsty Σ)) S2 :
     lty_choice a Ss <++> S2 <:> lty_choice a ((.<++> S2) <$> Ss)%lty.
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
423 424 425 426
    rewrite /lty_app /lty_choice iProto_app_message iMsg_app_exist;
      setoid_rewrite iMsg_app_base; setoid_rewrite lookup_total_alt;
      setoid_rewrite lookup_fmap; setoid_rewrite fmap_is_Some.
    iSplit; iIntros "!> /="; destruct a; iIntros (x); iExists x;
427
      iMod 1 as %[S ->]; iSplitR; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446
  Qed.
  Lemma lty_le_app_select A Ss S2 :
     lty_select Ss <++> S2 <:> lty_select ((.<++> S2) <$> Ss)%lty.
  Proof. apply lty_le_app_choice. Qed.
  Lemma lty_le_app_branch A Ss S2 :
     lty_branch Ss <++> S2 <:> lty_branch ((.<++> S2) <$> Ss)%lty.
  Proof. apply lty_le_app_choice. Qed.

  Lemma lty_le_dual S1 S2 : S2 <: S1 - lty_dual S1 <: lty_dual S2.
  Proof. iIntros "#H !>". by iApply iProto_le_dual. Qed.
  Lemma lty_le_dual_l S1 S2 : lty_dual S2 <: S1 - lty_dual S1 <: S2.
  Proof. iIntros "#H !>". by iApply iProto_le_dual_l. Qed.
  Lemma lty_le_dual_r S1 S2 : S2 <: lty_dual S1 - S1 <: lty_dual S2.
  Proof. iIntros "#H !>". by iApply iProto_le_dual_r. Qed.

  Lemma lty_le_dual_end :  lty_dual (Σ:=Σ) END <:> END.
  Proof. rewrite /lty_dual iProto_dual_end=> /=. apply lty_bi_le_refl. Qed.

  Lemma lty_le_dual_message a A S :
447
     lty_dual (lty_message a (TY A; S)) <:> lty_message (action_dual a) (TY A; (lty_dual S)).
Robbert Krebbers's avatar
Robbert Krebbers committed
448
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
449 450
    rewrite /lty_dual iProto_dual_message iMsg_dual_exist.
    setoid_rewrite iMsg_dual_base. iSplit; by iIntros "!> /=".
Robbert Krebbers's avatar
Robbert Krebbers committed
451
  Qed.
452
  Lemma lty_le_dual_send A S :  lty_dual (<!!> TY A; S) <:> (<??> TY A; lty_dual S).
Robbert Krebbers's avatar
Robbert Krebbers committed
453
  Proof. apply lty_le_dual_message. Qed.
454
  Lemma lty_le_dual_recv A S :  lty_dual (<??> TY A; S) <:> (<!!> TY A; lty_dual S).
Robbert Krebbers's avatar
Robbert Krebbers committed
455 456 457 458 459
  Proof. apply lty_le_dual_message. Qed.

  Lemma lty_le_dual_choice a (Ss : gmap Z (lsty Σ)) :
     lty_dual (lty_choice a Ss) <:> lty_choice (action_dual a) (lty_dual <$> Ss).
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
460 461 462 463
    rewrite /lty_dual /lty_choice iProto_dual_message iMsg_dual_exist;
      setoid_rewrite iMsg_dual_base; setoid_rewrite lookup_total_alt;
      setoid_rewrite lookup_fmap; setoid_rewrite fmap_is_Some.
    iSplit; iIntros "!> /="; destruct a; iIntros (x); iExists x;
464
      iMod 1 as %[S ->]; iSplitR; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
465 466 467 468 469 470 471 472
  Qed.

  Lemma lty_le_dual_select (Ss : gmap Z (lsty Σ)) :
     lty_dual (lty_select Ss) <:> lty_branch (lty_dual <$> Ss).
  Proof. iApply lty_le_dual_choice. Qed.
  Lemma lty_le_dual_branch (Ss : gmap Z (lsty Σ)) :
     lty_dual (lty_branch Ss) <:> lty_select (lty_dual <$> Ss).
  Proof. iApply lty_le_dual_choice. Qed.
473

Robbert Krebbers's avatar
Robbert Krebbers committed
474
End subtyping_rules.