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

Added symmetry relation for bi-subtyping

parent 12a45a0c
No related branches found
No related tags found
No related merge requests found
Pipeline #26965 passed
Stage: build
Hide whitespace changes
Inline Side-by-side
theories/logrel/subtyping.v
+ 4
− 0
View file @ 65509b98
...@@ -58,6 +58,8 @@ Section subtype. ...@@ -58,6 +58,8 @@ Section subtype.
Proof. iSplit; iApply lty_le_refl. Qed. Proof. iSplit; iApply lty_le_refl. Qed.
Lemma lty_bi_le_trans A1 A2 A3 : ⊢ A1 <:> A2 -∗ A2 <:> A3 -∗ A1 <:> A3. 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. Proof. iIntros "#[H11 H12] #[H21 H22]". iSplit; by iApply lty_le_trans. Qed.
Lemma lty_bi_le_sym A1 A2 : ⊢ A1 <:> A2 -∗ A2 <:> A1.
Proof. iIntros "[$$]". Qed.
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.
...@@ -201,6 +203,8 @@ Section subtype. ...@@ -201,6 +203,8 @@ Section subtype.
Proof. iSplit; iApply lsty_le_refl. Qed. Proof. iSplit; iApply lsty_le_refl. Qed.
Lemma lsty_bi_le_trans S1 S2 S3 : ⊢ S1 <s:> S2 -∗ S2 <s:> S3 -∗ S1 <s:> S3. 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. Proof. iIntros "#[H11 H12] #[H21 H22]". iSplit; by iApply lsty_le_trans. Qed.
Lemma lsty_bi_le_sym S1 S2 : ⊢ S1 <s:> S2 -∗ S2 <s:> S1.
Proof. iIntros "[$$]". 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) -∗
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment