Skip to content
Snippets Groups Projects
Commit 904fdbe1 authored by Jonas Kastberg's avatar Jonas Kastberg
Browse files

Added bi subtyping relation

parent ec1c6439
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/logrel/subtyping.v
+ 60
− 59
View file @ 904fdbe1
...@@ -9,23 +9,41 @@ Definition lty_le {Σ} (A1 A2 : lty Σ) : iProp Σ := ...@@ -9,23 +9,41 @@ Definition lty_le {Σ} (A1 A2 : lty Σ) : iProp Σ :=
Arguments lty_le {_} _%lty _%lty. Arguments lty_le {_} _%lty _%lty.
Infix "<:" := lty_le (at level 70). Infix "<:" := lty_le (at level 70).
Instance: Params (@lty_le) 1 := {}. Instance: Params (@lty_le) 1 := {}.
Instance lty_le_ne {Σ} : NonExpansive2 (@lty_le Σ). Instance lty_le_ne {Σ} : NonExpansive2 (@lty_le Σ).
Proof. solve_proper. Qed. Proof. solve_proper. Qed.
Instance lty_le_proper {Σ} : Proper ((≡) ==> (≡) ==> (≡)) (@lty_le Σ). Instance lty_le_proper {Σ} : Proper ((≡) ==> (≡) ==> (≡)) (@lty_le Σ).
Proof. solve_proper. Qed. Proof. solve_proper. Qed.
Definition lty_bi_le {Σ} (A1 A2 : lty Σ) : iProp Σ :=
A1 <: A2 ∧ A2 <: A1.
Arguments lty_bi_le {_} _%lty _%lty.
Infix "<:>" := lty_bi_le (at level 70).
Instance: Params (@lty_bi_le) 1 := {}.
Instance lty_bi_le_ne {Σ} : NonExpansive2 (@lty_bi_le Σ).
Proof. solve_proper. Qed.
Instance lty_bi_le_proper {Σ} : Proper ((≡) ==> (≡) ==> (≡)) (@lty_bi_le Σ).
Proof. solve_proper. Qed.
Definition lsty_le {Σ} (P1 P2 : lsty Σ) : iProp Σ := Definition lsty_le {Σ} (P1 P2 : lsty Σ) : iProp Σ :=
□ iProto_le P1 P2. □ iProto_le P1 P2.
Arguments lsty_le {_} _%lsty _%lsty. Arguments lsty_le {_} _%lsty _%lsty.
Infix "<s:" := lsty_le (at level 70). Infix "<s:" := lsty_le (at level 70).
Instance: Params (@lsty_le) 1 := {}. Instance: Params (@lsty_le) 1 := {}.
Instance lsty_le_ne {Σ} : NonExpansive2 (@lsty_le Σ). Instance lsty_le_ne {Σ} : NonExpansive2 (@lsty_le Σ).
Proof. solve_proper. Qed. Proof. solve_proper. Qed.
Instance lsty_le_proper {Σ} : Proper ((≡) ==> (≡) ==> (≡)) (@lsty_le Σ). Instance lsty_le_proper {Σ} : Proper ((≡) ==> (≡) ==> (≡)) (@lsty_le Σ).
Proof. solve_proper. Qed. Proof. solve_proper. Qed.
Definition lsty_bi_le {Σ} (S1 S2 : lsty Σ) : iProp Σ :=
S1 <s: S2 ∧ S2 <s: S1.
Arguments lty_bi_le {_} _%lsty _%lsty.
Infix "<s:>" := lsty_bi_le (at level 70).
Instance: Params (@lsty_bi_le) 1 := {}.
Instance lsty_bi_le_ne {Σ} : NonExpansive2 (@lsty_bi_le Σ).
Proof. solve_proper. Qed.
Instance lsty_bi_le_proper {Σ} : Proper ((≡) ==> (≡) ==> (≡)) (@lsty_bi_le Σ).
Proof. solve_proper. Qed.
Section subtype. Section subtype.
Context `{heapG Σ, chanG Σ}. Context `{heapG Σ, chanG Σ}.
Implicit Types A : lty Σ. Implicit Types A : lty Σ.
...@@ -33,10 +51,14 @@ Section subtype. ...@@ -33,10 +51,14 @@ Section subtype.
Lemma lty_le_refl (A : lty Σ) : ⊢ A <: A. Lemma lty_le_refl (A : lty Σ) : ⊢ A <: A.
Proof. by iIntros (v) "!> H". Qed. Proof. by iIntros (v) "!> H". Qed.
Lemma lty_le_trans A1 A2 A3 : A1 <: A2 -∗ A2 <: A3 -∗ A1 <: A3. Lemma lty_le_trans A1 A2 A3 : A1 <: A2 -∗ A2 <: A3 -∗ A1 <: A3.
Proof. iIntros "#H1 #H2" (v) "!> H". iApply "H2". by iApply "H1". Qed. Proof. iIntros "#H1 #H2" (v) "!> H". iApply "H2". by iApply "H1". Qed.
Lemma lty_bi_le_refl A : ⊢ A <:> A.
Proof. iSplit; iApply lty_le_refl. Qed.
Lemma lty_bi_le_trans A1 A2 A3 : ⊢ A1 <:> A2 -∗ A2 <:> A3 -∗ A1 <:> A3.
Proof. iIntros "#[H11 H12] #[H21 H22]". iSplit; by iApply lty_le_trans. Qed.
  • Robbert Krebbers @robbertkrebbers ·
    Owner

    While you're at it, also add symmetry :)

  • Jonas Kastberg @jihgfee ·
    Author Maintainer

    What exactly do you want here? Lemma lty_bi_le_sym A1 A2 : ⊢ (A1 <: A2 ∧ A2 <: A1) *-* A1 <:> A2. ?

    Or just in one direction

  • Robbert Krebbers @robbertkrebbers ·
    Owner

    That's anti-symmetry, and just the the definition.

    Symmetry is A1 <:> A2 -∗ A2 <:> A1.

  • Jonas Kastberg @jihgfee ·
    Author Maintainer

    Derp. Of course it is. My bad - Added!

  • Please register or sign in to reply
Lemma lty_le_copy A : ⊢ copy A <: A. Lemma lty_le_copy A : ⊢ copy A <: A.
Proof. by iIntros (v) "!> #H". Qed. Proof. by iIntros (v) "!> #H". Qed.
...@@ -103,15 +125,12 @@ Section subtype. ...@@ -103,15 +125,12 @@ Section subtype.
⊢ C B <: ∃ A, C A. ⊢ C B <: ∃ A, C A.
Proof. iIntros "!>" (v) "Hle". by iExists B. Qed. Proof. iIntros "!>" (v) "Hle". by iExists B. Qed.
Lemma lty_le_rec_1 (C : lty Σ → lty Σ) `{!Contractive C} : Lemma lty_le_rec_unfold (C : lty Σ → lty Σ) `{!Contractive C} :
⊢ lty_rec C <: C (lty_rec C). ⊢ lty_rec C <:> C (lty_rec C).
Proof. Proof.
rewrite {1}/lty_rec {1}fixpoint_unfold {1}/lty_rec_aux. iApply lty_le_refl. iSplit.
Qed. - rewrite {1}/lty_rec {1}fixpoint_unfold {1}/lty_rec_aux. iApply lty_le_refl.
Lemma lty_le_rec_2 (C : lty Σ → lty Σ) `{!Contractive C} : - rewrite {2}/lty_rec {1}fixpoint_unfold {1}/lty_rec_aux. iApply lty_le_refl.
⊢ C (lty_rec C) <: lty_rec C.
Proof.
rewrite {2}/lty_rec {1}fixpoint_unfold {1}/lty_rec_aux. iApply lty_le_refl.
Qed. Qed.
Lemma lty_le_rec `{Contractive C1, Contractive C2} : Lemma lty_le_rec `{Contractive C1, Contractive C2} :
...@@ -175,10 +194,14 @@ Section subtype. ...@@ -175,10 +194,14 @@ Section subtype.
Lemma lsty_le_refl (S : lsty Σ) : ⊢ S <s: S. Lemma lsty_le_refl (S : lsty Σ) : ⊢ S <s: S.
Proof. iApply iProto_le_refl. Qed. Proof. iApply iProto_le_refl. Qed.
Lemma lsty_le_trans S1 S2 S3 : S1 <s: S2 -∗ S2 <s: S3 -∗ S1 <s: S3. Lemma lsty_le_trans S1 S2 S3 : S1 <s: S2 -∗ S2 <s: S3 -∗ S1 <s: S3.
Proof. iIntros "#H1 #H2 !>". by iApply iProto_le_trans. Qed. Proof. iIntros "#H1 #H2 !>". by iApply iProto_le_trans. Qed.
Lemma lsty_bi_le_refl S : ⊢ S <s:> S.
Proof. iSplit; iApply lsty_le_refl. Qed.
Lemma lsty_bi_le_trans S1 S2 S3 : ⊢ S1 <s:> S2 -∗ S2 <s:> S3 -∗ S1 <s:> S3.
Proof. iIntros "#[H11 H12] #[H21 H22]". iSplit; by iApply lsty_le_trans. Qed.
Lemma lsty_le_send A1 A2 S1 S2 : Lemma lsty_le_send A1 A2 S1 S2 :
▷ (A2 <: A1) -∗ ▷ (S1 <s: S2) -∗ ▷ (A2 <: A1) -∗ ▷ (S1 <s: S2) -∗
(<!!> A1 ; S1) <s: (<!!> A2 ; S2). (<!!> A1 ; S1) <s: (<!!> A2 ; S2).
...@@ -292,21 +315,14 @@ Section subtype. ...@@ -292,21 +315,14 @@ Section subtype.
(S11 <++> S12) <s: (S21 <++> S22). (S11 <++> S12) <s: (S21 <++> S22).
Proof. iIntros "#H1 #H2 !>". by iApply iProto_le_app. Qed. Proof. iIntros "#H1 #H2 !>". by iApply iProto_le_app. Qed.
Lemma lsty_le_app_assoc_l S1 S2 S3 : Lemma lsty_le_app_assoc S1 S2 S3 :
⊢ S1 <++> (S2 <++> S3) <s: (S1 <++> S2) <++> S3. ⊢ (S1 <++> S2) <++> S3 <s:> S1 <++> (S2 <++> S3).
Proof. rewrite assoc. iApply lsty_le_refl. Qed. Proof. rewrite assoc. iApply lsty_bi_le_refl. Qed.
Lemma lsty_le_app_assoc_r S1 S2 S3 :
⊢ (S1 <++> S2) <++> S3 <s: S1 <++> (S2 <++> S3). Lemma lsty_le_app_id_l S : ⊢ (END <++> S) <s:> S.
Proof. rewrite assoc. iApply lsty_le_refl. Qed. Proof. rewrite left_id. iApply lsty_bi_le_refl. Qed.
Lemma lsty_le_app_id_r S : ⊢ (S <++> END) <s:> S.
Lemma lsty_le_app_id_l_l S : ⊢ (END <++> S) <s: S. Proof. rewrite right_id. iApply lsty_bi_le_refl. Qed.
Proof. rewrite left_id. iApply lsty_le_refl. Qed.
Lemma lsty_le_app_id_l_r S : ⊢ (S <++> END) <s: S.
Proof. rewrite right_id. iApply lsty_le_refl. Qed.
Lemma lsty_le_app_id_r_l S : ⊢ S <s: (END <++> S).
Proof. rewrite left_id. iApply lsty_le_refl. Qed.
Lemma lsty_le_app_id_r_r S : ⊢ S <s: (S <++> END).
Proof. rewrite right_id. iApply lsty_le_refl. Qed.
Lemma lsty_le_dual S1 S2 : S2 <s: S1 -∗ lsty_dual S1 <s: lsty_dual S2. Lemma lsty_le_dual S1 S2 : S2 <s: S1 -∗ lsty_dual S1 <s: lsty_dual S2.
Proof. iIntros "#H !>". by iApply iProto_le_dual. Qed. Proof. iIntros "#H !>". by iApply iProto_le_dual. Qed.
...@@ -315,41 +331,26 @@ Section subtype. ...@@ -315,41 +331,26 @@ Section subtype.
Lemma lsty_le_dual_r S1 S2 : S2 <s: lsty_dual S1 -∗ S1 <s: lsty_dual S2. Lemma lsty_le_dual_r S1 S2 : S2 <s: lsty_dual S1 -∗ S1 <s: lsty_dual S2.
Proof. iIntros "#H !>". by iApply iProto_le_dual_r. Qed. Proof. iIntros "#H !>". by iApply iProto_le_dual_r. Qed.
Lemma lsty_le_dual_message_l a A S : Lemma lsty_le_dual_message a A S :
⊢ lsty_dual (lsty_message a A S) <s: lsty_message (action_dual a) A (lsty_dual S). ⊢ lsty_dual (lsty_message a A S) <s:>
lsty_message (action_dual a) A (lsty_dual S).
Proof. Proof.
iIntros "!>". rewrite /lsty_dual iProto_dual_message_tele. iApply iProto_le_refl. iSplit; iIntros "!>"; rewrite /lsty_dual iProto_dual_message_tele;
iApply iProto_le_refl.
Qed. Qed.
Lemma lsty_le_dual_message_r a A S : Lemma lsty_le_dual_send A S : ⊢ lsty_dual (<!!> A; S) <s:> (<??> A; lsty_dual S).
⊢ lsty_message (action_dual a) A (lsty_dual S) <s: lsty_dual (lsty_message a A S). Proof. apply lsty_le_dual_message. Qed.
Lemma lsty_le_dual_recv A S : ⊢ lsty_dual (<??> A; S) <s:> (<!!> A; lsty_dual S).
Proof. apply lsty_le_dual_message. Qed.
Lemma lsty_le_dual_end : ⊢ lsty_dual (Σ:=Σ) END <s:> END.
Proof. rewrite /lsty_dual iProto_dual_end=> /=. apply lsty_bi_le_refl. Qed.
Lemma lsty_le_rec_unfold (C : lsty Σ → lsty Σ) `{!Contractive C} :
⊢ lsty_rec C <s:> C (lsty_rec C).
Proof. Proof.
iIntros "!>". rewrite /lsty_dual iProto_dual_message_tele. iApply iProto_le_refl. iSplit.
Qed. - rewrite {1}/lsty_rec {1}fixpoint_unfold {1}/lsty_rec1. iApply lsty_le_refl.
Lemma lsty_le_dual_send_l A S : ⊢ lsty_dual (<!!> A; S) <s: (<??> A; lsty_dual S). - rewrite {2}/lsty_rec {1}fixpoint_unfold {1}/lsty_rec1. iApply lsty_le_refl.
Proof. apply lsty_le_dual_message_l. Qed.
Lemma lsty_le_dual_send_r A S : ⊢ (<!!> A; lsty_dual S) <s: lsty_dual (<??> A; S).
Proof. apply: lsty_le_dual_message_r. Qed.
Lemma lsty_le_dual_recv_l A S : ⊢ lsty_dual (<??> A; S) <s: (<!!> A; lsty_dual S).
Proof. apply lsty_le_dual_message_l. Qed.
Lemma lsty_le_dual_recv_r A S : ⊢ (<??> A; lsty_dual S) <s: lsty_dual (<!!> A; S).
Proof. apply: lsty_le_dual_message_r. Qed.
Lemma lsty_le_dual_end_l : ⊢ lsty_dual (Σ:=Σ) END <s: END.
Proof. rewrite /lsty_dual iProto_dual_end=> /=. apply lsty_le_refl. Qed.
Lemma lsty_le_dual_end_r : ⊢ END <s: lsty_dual (Σ:=Σ) END.
Proof. rewrite /lsty_dual iProto_dual_end=> /=. apply lsty_le_refl. Qed.
Lemma lsty_le_rec_1 (C : lsty Σ → lsty Σ) `{!Contractive C} :
⊢ lsty_rec C <s: C (lsty_rec C).
Proof.
rewrite {1}/lsty_rec {1}fixpoint_unfold {1}/lsty_rec1.
iApply lsty_le_refl.
Qed.
Lemma lsty_le_rec_2 (C : lsty Σ → lsty Σ) `{!Contractive C} :
⊢ C (lsty_rec C) <s: lsty_rec C.
Proof.
rewrite {2}/lsty_rec {1}fixpoint_unfold {1}/lsty_rec1.
iApply lsty_le_refl.
Qed. Qed.
Lemma lsty_le_rec `{Contractive C1, Contractive C2} : Lemma lsty_le_rec `{Contractive C1, Contractive C2} :
......
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