Skip to content
Snippets Groups Projects
Commit d2372b49 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Avoid inconsistent sealing of subtyping. Instead give better type class precedences.

parent 0609eec7
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/logrel/subtyping.v
+ 2
− 11
View file @ d2372b49
......@@ -5,17 +5,10 @@ having both [A <: B] and [B <: A]. Finally, the notion of a *copyable type* is
defined in terms of subtyping: a type [A] is copyable when [A <: copy A]. *)
From actris.logrel Require Export model term_types.
Definition lsty_le_def {Σ} (P1 P2 : lsty Σ) :=
iProto_le (lsty_car P1) (lsty_car P2).
Definition lsty_le_aux : seal (@lsty_le_def). by eexists. Qed.
Definition lsty_le := lsty_le_aux.(unseal).
Definition lsty_le_eq : @lsty_le = @lsty_le_def := lsty_le_aux.(seal_eq).
Arguments lsty_le {_} _ _.
Definition lty_le {Σ k} : lty Σ k → lty Σ k → iProp Σ :=
match k with
| tty_kind => λ A1 A2, ■ ∀ v, ltty_car A1 v -∗ ltty_car A2 v
| lty_kind => λ P1 P2, ■ lsty_le P1 P2
| lty_kind => λ P1 P2, ■ iProto_le (lsty_car P1) (lsty_car P2)
end%I.
Arguments lty_le : simpl never.
Infix "<:" := lty_le (at level 70) : bi_scope.
......@@ -40,9 +33,7 @@ Section subtyping.
Proof. rewrite /lty_bi_le /=. apply _. Qed.
Global Instance lty_le_ne : NonExpansive2 (@lty_le Σ k).
Proof.
rewrite /lty_le lsty_le_eq. destruct k; rewrite ?/lsty_le_def; solve_proper.
Qed.
Proof. destruct k; solve_proper. Qed.
Global Instance lty_le_proper {k} : Proper ((≡) ==> (≡) ==> (≡)) (@lty_le Σ k).
Proof. apply (ne_proper_2 _). Qed.
Global Instance lty_bi_le_ne {k} : NonExpansive2 (@lty_bi_le Σ k).
......
theories/logrel/subtyping_rules.v
+ 38
− 72
View file @ d2372b49
......@@ -12,14 +12,12 @@ Section subtyping_rules.
(** Generic rules *)
Lemma lty_le_refl {k} (M : lty Σ k) : ⊢ M <: M.
Proof. destruct k. by iIntros (v) "!> H".
rewrite /lty_le lsty_le_eq /lsty_le_def. by iModIntro. Qed.
Proof. destruct k. by iIntros (v) "!> H". by iModIntro. Qed.
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 !>".
rewrite /lty_le lsty_le_eq /lsty_le_def. by iApply iProto_le_trans.
- iIntros "#H1 #H2 !>". by iApply iProto_le_trans.
Qed.
Lemma lty_bi_le_refl {k} (M : lty Σ k) : ⊢ M <:> M.
......@@ -131,11 +129,9 @@ Section subtyping_rules.
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.
iIntros "#HcpA #HcpB". rewrite /lty_copyable /=.
iApply lty_le_r; last by iApply lty_le_prod_copy.
iApply lty_le_prod.
- iApply "HcpA".
- iApply "HcpB".
iApply lty_le_prod. iApply "HcpA". iApply "HcpB".
Qed.
Lemma lty_le_sum A11 A12 A21 A22 :
......@@ -156,11 +152,9 @@ Section subtyping_rules.
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.
iIntros "#HcpA #HcpB". rewrite /lty_copyable /=.
iApply lty_le_r; last by iApply lty_le_sum_copy.
iApply lty_le_sum.
- iApply "HcpA".
- iApply "HcpB".
iApply lty_le_sum. iApply "HcpA". iApply "HcpB".
Qed.
Lemma lty_le_forall C1 C2 :
......@@ -169,7 +163,7 @@ Section subtyping_rules.
Proof.
iIntros "#Hle" (v) "!> H". iIntros (w).
iApply (wp_step_fupd); first done.
{ iIntros "!>!>!>". iExact "Hle". }
{ iIntros "!> !> !>". iExact "Hle". }
iApply (wp_wand with "H"). iIntros (v') "H Hle' !>".
by iApply "Hle'".
Qed.
......@@ -241,8 +235,7 @@ Section subtyping_rules.
▷ (S1 <: S2) -∗ chan S1 <: chan S2.
Proof.
iIntros "#Hle" (v) "!> H".
iApply (iProto_mapsto_le with "H [Hle]").
rewrite /lty_le lsty_le_eq. eauto.
iApply (iProto_mapsto_le with "H [Hle]"). eauto.
Qed.
(** Session subtyping *)
......@@ -250,7 +243,6 @@ Section subtyping_rules.
▷ (A2 <: A1) -∗ ▷ (S1 <: S2) -∗
(<!!> TY A1 ; S1) <: (<!!> TY A2 ; S2).
Proof.
rewrite /lty_le lsty_le_eq.
iIntros "#HAle #HSle !>" (v) "H". iExists v.
iDestruct ("HAle" with "H") as "$". by iModIntro.
Qed.
......@@ -259,7 +251,6 @@ Section subtyping_rules.
▷ (A1 <: A2) -∗ ▷ (S1 <: S2) -∗
(<??> TY A1 ; S1) <: (<??> TY A2 ; S2).
Proof.
rewrite /lty_le lsty_le_eq.
iIntros "#HAle #HSle !>" (v) "H". iExists v.
iDestruct ("HAle" with "H") as "$". by iModIntro.
Qed.
......@@ -268,7 +259,6 @@ Section subtyping_rules.
(∀ (A : lty Σ k), (<??> M A) <: S) -∗
(<?? (A : lty Σ k)> M A) <: S.
Proof.
rewrite /lty_le lsty_le_eq.
iIntros "#Hle !>". iApply (iProto_le_exist_elim_l_inhabited M). auto.
Qed.
......@@ -276,23 +266,16 @@ Section subtyping_rules.
(∀ (A : lty Σ k), S <: (<!!> M A)) -∗
S <: (<!! (A : lty Σ k)> M A).
Proof.
rewrite /lty_le lsty_le_eq.
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) :
⊢ (<!! X> M X) <: (<!!> M A).
Proof.
rewrite /lty_le lsty_le_eq.
iIntros "!>". iApply (iProto_le_exist_intro_l).
Qed.
Proof. iIntros "!>". iApply (iProto_le_exist_intro_l). Qed.
Lemma lty_le_exist_intro_r k (M : lty Σ k → lmsg Σ) (A : lty Σ k) :
⊢ (<??> M A) <: (<?? X> M X).
Proof.
rewrite /lty_le lsty_le_eq.
iIntros "!>". iApply (iProto_le_exist_intro_r).
Qed.
Proof. iIntros "!>". iApply (iProto_le_exist_intro_r). Qed.
Lemma lty_le_texist_elim_l {kt} (M : ltys Σ kt → lmsg Σ) S :
(∀ Xs, (<??> M Xs) <: S) -∗
......@@ -329,7 +312,6 @@ Section subtyping_rules.
Lemma lty_le_swap_recv_send A1 A2 S :
⊢ (<??> TY A1; <!!> TY A2; S) <: (<!!> TY A2; <??> TY A1; S).
Proof.
rewrite /lty_le lsty_le_eq.
iIntros "!>" (v1 v2).
iApply iProto_le_trans;
[iApply iProto_le_base; iApply (iProto_le_exist_intro_l _ v2)|].
......@@ -341,7 +323,6 @@ Section subtyping_rules.
Lemma lty_le_swap_recv_select A Ss :
⊢ (<??> TY A; lty_select Ss) <: lty_select ((λ S, <??> TY A; S) <$> Ss)%lty.
Proof.
rewrite /lty_le lsty_le_eq.
iIntros "!>" (v1 x2).
iApply iProto_le_trans;
[iApply iProto_le_base; iApply (iProto_le_exist_intro_l _ x2)|]; simpl.
......@@ -355,7 +336,6 @@ Section subtyping_rules.
Lemma lty_le_swap_branch_send A Ss :
⊢ lty_branch ((λ S, <!!> TY A; S) <$> Ss)%lty <: (<!!> TY A; lty_branch Ss).
Proof.
rewrite /lty_le lsty_le_eq.
iIntros "!>" (x1 v2).
iApply iProto_le_trans;
[|iApply iProto_le_base; iApply (iProto_le_exist_intro_r _ x1)]; simpl.
......@@ -370,7 +350,6 @@ Section subtyping_rules.
▷ ([∗ map] S1;S2 ∈ Ss1; Ss2, S1 <: S2) -∗
lty_select Ss1 <: lty_select Ss2.
Proof.
rewrite /lty_le lsty_le_eq.
iIntros "#H !>" (x); iMod 1 as %[S2 HSs2]. iExists x.
iDestruct (big_sepM2_forall with "H") as "{H} [>% H]".
assert (is_Some (Ss1 !! x)) as [S1 HSs1] by naive_solver.
......@@ -382,7 +361,6 @@ Section subtyping_rules.
Ss2 ⊆ Ss1 →
⊢ lty_select Ss1 <: lty_select Ss2.
Proof.
rewrite /lty_le lsty_le_eq.
intros; iIntros "!>" (x); iMod 1 as %[S HSs2]. iExists x.
assert (Ss1 !! x = Some S) as HSs1 by eauto using lookup_weaken.
rewrite HSs1. iSplitR; [by eauto|].
......@@ -393,7 +371,6 @@ Section subtyping_rules.
▷ ([∗ map] S1;S2 ∈ Ss1; Ss2, S1 <: S2) -∗
lty_branch Ss1 <: lty_branch Ss2.
Proof.
rewrite /lty_le lsty_le_eq.
iIntros "#H !>" (x); iMod 1 as %[S1 HSs1]. iExists x.
iDestruct (big_sepM2_forall with "H") as "{H} [>% H]".
assert (is_Some (Ss2 !! x)) as [S2 HSs2] by naive_solver.
......@@ -405,7 +382,6 @@ Section subtyping_rules.
Ss1 ⊆ Ss2 →
⊢ lty_branch Ss1 <: lty_branch Ss2.
Proof.
rewrite /lty_le lsty_le_eq.
intros; iIntros "!>" (x); iMod 1 as %[S HSs1]. iExists x.
assert (Ss2 !! x = Some S) as HSs2 by eauto using lookup_weaken.
rewrite HSs2. iSplitR; [by eauto|].
......@@ -416,29 +392,25 @@ Section subtyping_rules.
Lemma lty_le_app S11 S12 S21 S22 :
(S11 <: S21) -∗ (S12 <: S22) -∗
(S11 <++> S12) <: (S21 <++> S22).
Proof. rewrite /lty_le lsty_le_eq.
iIntros "#H1 #H2 !>". by iApply iProto_le_app. Qed.
Proof. iIntros "#H1 #H2 !>". by iApply iProto_le_app. Qed.
Lemma lty_le_app_id_l S : ⊢ (END <++> S) <:> S.
Proof. rewrite /lty_app left_id.
iSplit; rewrite /lty_le lsty_le_eq /lsty_le_def; by iModIntro. Qed.
Proof. rewrite /lty_app left_id. iSplit; by iModIntro. Qed.
Lemma lty_le_app_id_r S : ⊢ (S <++> END) <:> S.
Proof. rewrite /lty_app right_id.
iSplit; rewrite /lty_le lsty_le_eq /lsty_le_def; by iModIntro. Qed.
Proof. rewrite /lty_app right_id. iSplit; by iModIntro. Qed.
Lemma lty_le_app_assoc S1 S2 S3 :
⊢ (S1 <++> S2) <++> S3 <:> S1 <++> (S2 <++> S3).
Proof. rewrite /lty_app assoc.
iSplit; rewrite /lty_le lsty_le_eq /lsty_le_def; by iModIntro. Qed.
Proof. rewrite /lty_app assoc. iSplit; by iModIntro. Qed.
Lemma lty_le_app_send A S1 S2 : ⊢ (<!!> TY A; S1) <++> S2 <:> (<!!> TY A; S1 <++> S2).
Proof.
rewrite /lty_app iProto_app_message iMsg_app_exist. setoid_rewrite iMsg_app_base.
iSplit; rewrite /lty_le lsty_le_eq /lsty_le_def; by iIntros "!> /=".
iSplit; by iIntros "!> /=".
Qed.
Lemma lty_le_app_recv A S1 S2 : ⊢ (<??> TY A; S1) <++> S2 <:> (<??> TY A; S1 <++> S2).
Proof.
rewrite /lty_app iProto_app_message iMsg_app_exist. setoid_rewrite iMsg_app_base.
iSplit; rewrite /lty_le lsty_le_eq /lsty_le_def; by iIntros "!> /=".
iSplit; by iIntros "!> /=".
Qed.
Lemma lty_le_app_choice a (Ss : gmap Z (lsty Σ)) S2 :
......@@ -447,7 +419,7 @@ Section subtyping_rules.
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; rewrite /lty_le lsty_le_eq; iIntros "!> /="; destruct a;
iSplit; iIntros "!> /="; destruct a;
iIntros (x); iExists x; iMod 1 as %[S ->]; iSplitR; eauto.
Qed.
Lemma lty_le_app_select A Ss S2 :
......@@ -458,13 +430,11 @@ Section subtyping_rules.
Proof. apply lty_le_app_choice. Qed.
Lemma lty_le_dual S1 S2 : S2 <: S1 -∗ lty_dual S1 <: lty_dual S2.
Proof. rewrite /lty_le lsty_le_eq. iIntros "#H !>". by iApply iProto_le_dual. Qed.
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. rewrite /lty_le lsty_le_eq. iIntros "#H !>".
by iApply iProto_le_dual_l. Qed.
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. rewrite /lty_le lsty_le_eq. iIntros "#H !>".
by iApply iProto_le_dual_r. Qed.
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.
......@@ -473,8 +443,7 @@ Section subtyping_rules.
⊢ lty_dual (lty_message a (TY A; S)) <:> lty_message (action_dual a) (TY A; (lty_dual S)).
Proof.
rewrite /lty_dual iProto_dual_message iMsg_dual_exist.
setoid_rewrite iMsg_dual_base.
iSplit; rewrite /lty_le lsty_le_eq /lsty_le_def; by iIntros "!> /=".
setoid_rewrite iMsg_dual_base. iSplit; by iIntros "!> /=".
Qed.
Lemma lty_le_dual_send A S : ⊢ lty_dual (<!!> TY A; S) <:> (<??> TY A; lty_dual S).
Proof. apply lty_le_dual_message. Qed.
......@@ -487,7 +456,7 @@ Section subtyping_rules.
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; rewrite /lty_le lsty_le_eq; iIntros "!> /="; destruct a;
iSplit; iIntros "!> /="; destruct a;
iIntros (x); iExists x; iMod 1 as %[S ->]; iSplitR; eauto.
Qed.
......@@ -498,46 +467,43 @@ Section subtyping_rules.
⊢ lty_dual (lty_branch Ss) <:> lty_select (lty_dual <$> Ss).
Proof. iApply lty_le_dual_choice. Qed.
(** The instances below make it possible to use the tactics [iIntros],
[iExist], [iSplitL]/[iSplitR], [iFrame] and [iModIntro] on [lty_le] goals.
These instances have higher precedence than the ones in [proto.v] to avoid
needless unfolding of the subtyping relation. *)
Global Instance lty_le_from_forall_l k (M : lty Σ k → lmsg Σ) (S : lsty Σ) :
FromForall (lty_le (<?? X> M X) S)%lty (λ X, (lty_le (<??> M X) S)%lty) | 10.
FromForall ((<?? X> M X) <: S) (λ X, (<??> M X) <: S)%I | 0.
Proof. apply lty_le_exist_elim_l. Qed.
Global Instance lty_le_from_forall_r k (S : lsty Σ) (M : lty Σ k → lmsg Σ) :
FromForall (lty_le S (<!! X> M X))%lty (λ X, (lty_le S (<!!> M X))%lty) | 11.
FromForall (S <: (<!! X> M X)) (λ X, S <: (<!!> M X))%I | 1.
Proof. apply lty_le_exist_elim_r. Qed.
Global Instance lty_le_from_exist_l k (M : lty Σ k → lmsg Σ) S :
FromExist ((<!! X> M X) <: S) (λ X, (<!!> M X) <: S)%I | 10.
FromExist ((<!! X> M X) <: S) (λ X, (<!!> M X) <: S)%I | 0.
Proof.
rewrite /FromExist. iDestruct 1 as (x) "H".
iApply (lty_le_trans with "[] H"). iApply lty_le_exist_intro_l.
Qed.
Global Instance lty_le_from_exist_r k (M : lty Σ k → lmsg Σ) S :
FromExist (S <: <?? X> M X) (λ X, S <: (<??> M X))%I | 11.
FromExist (S <: <?? X> M X) (λ X, S <: (<??> M X))%I | 1.
Proof.
rewrite /FromExist. iDestruct 1 as (x) "H".
iApply (lty_le_trans with "H"). iApply lty_le_exist_intro_r.
Qed.
Lemma lty_le_base_send A (S1 S2 : lsty Σ) :
▷ (S1 <: S2) -∗
(<!!> TY A ; S1) <: (<!!> TY A ; S2).
Proof. iIntros "H". iApply lty_le_send. iApply lty_le_refl. eauto. Qed.
Global Instance lty_le_from_modal_send A (S1 S2 : lsty Σ) :
FromModal (modality_instances.modality_laterN 1) (S1 <: S2)
((<!!> TY A; S1) <: (<!!> TY A; S2)) (S1 <: S2).
Proof. apply lty_le_base_send. Qed.
Lemma lty_le_base_recv A (S1 S2 : lsty Σ) :
▷ (S1 <: S2) -∗
(<??> TY A ; S1) <: (<??> TY A ; S2).
Proof. iIntros "H". iApply lty_le_recv. iApply lty_le_refl. eauto. Qed.
((<!!> TY A; S1) <: (<!!> TY A; S2)) (S1 <: S2) | 0.
Proof.
rewrite /FromModal. iIntros "H". iApply lty_le_send. iApply lty_le_refl. done.
Qed.
Global Instance lty_le_from_modal_recv A (S1 S2 : lsty Σ) :
FromModal (modality_instances.modality_laterN 1) (S1 <: S2)
((<??> TY A; S1) <: (<??> TY A; S2)) (S1 <: S2).
Proof. apply lty_le_base_recv. Qed.
((<??> TY A; S1) <: (<??> TY A; S2)) (S1 <: S2) | 0.
Proof.
rewrite /FromModal. iIntros "H". iApply lty_le_recv. iApply lty_le_refl. done.
Qed.
End subtyping_rules.
Hint Extern 0 (environments.envs_entails _ (?x <: ?y)) =>
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment