Commit 0b9a055c authored by Jonas Kastberg's avatar Jonas Kastberg

Merge branch 'daniel/copy_derived_rules' into 'master'

Derived rules about copying

See merge request !14
parents 860d808b c52fd7fa
Pipeline #27588 passed with stage
in 19 minutes and 17 seconds
......@@ -61,7 +61,7 @@ Section subtyping_rules.
Lemma lty_copyable_copy A : @{iPropI Σ} lty_copyable (copy A).
Proof. iIntros (v) "!> #Hv !>". iFrame "Hv". Qed.
Lemma lty_le_copy_inv A B : A <: B - copy- A <: copy- B.
Lemma lty_le_copy_inv_mono A B : A <: B - copy- A <: copy- B.
Proof.
iIntros "#Hle !>" (v) "#HA". iApply (coreP_wand (ltty_car A v) with "[] HA").
iIntros "{HA} !> !>". iApply "Hle".
......@@ -72,6 +72,13 @@ Section subtyping_rules.
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.
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.
Lemma lty_copyable_unit : @{iPropI Σ} lty_copyable ().
Proof. iIntros (v) "!> #Hv !>". iFrame "Hv". Qed.
......@@ -94,6 +101,10 @@ Section subtyping_rules.
(A21 <: A11) - (A12 <: A22) -
(A11 A12) <: (A21 A22).
Proof. iIntros "#H1 #H2" (v) "!> #H !>". by iApply lty_le_arr. Qed.
(* 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.
Lemma lty_le_prod A11 A12 A21 A22 :
(A11 <: A21) - (A12 <: A22) -
......@@ -104,7 +115,7 @@ Section subtyping_rules.
iDestruct ("H1" with "H1'") as "$".
by iDestruct ("H2" with "H2'") as "$".
Qed.
(* TODO(COPY): Show derived rules about copyability of products, sums, etc. *)
Lemma lty_le_prod_copy A B :
copy A * copy B <:> copy (A * B).
Proof.
......@@ -113,6 +124,16 @@ Section subtyping_rules.
- iExists v1, v2. iSplit; [done|]. auto.
Qed.
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.
Lemma lty_le_sum A11 A12 A21 A22 :
(A11 <: A21) - (A12 <: A22) -
A11 + A12 <: A21 + A22.
......@@ -128,6 +149,15 @@ Section subtyping_rules.
iDestruct 1 as "#[Hv|Hv]"; iDestruct "Hv" as (w ?) "Hw";
try iModIntro; first [iLeft; by auto|iRight; by auto].
Qed.
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.
Lemma lty_le_forall C1 C2 :
( A, C1 A <: C2 A) -
......@@ -139,7 +169,6 @@ Section subtyping_rules.
iApply (wp_wand with "H"). iIntros (v') "H Hle' !>".
by iApply "Hle'".
Qed.
(* TODO(COPY) TODO(VALUERES): Do the forall type former, once we have the value restriction *)
Lemma lty_le_exist C1 C2 :
( A, C1 A <: C2 A) -
......@@ -157,8 +186,18 @@ Section subtyping_rules.
iExists A; repeat iModIntro; iApply "Hv".
Qed.
Lemma lty_copyable_exist (C : ltty Σ ltty Σ) :
( M, lty_copyable (C M)) - lty_copyable (lty_exist C).
Proof.
iIntros "#Hle". rewrite /lty_copyable /tc_opaque.
iApply lty_le_r; last by iApply lty_le_exist_copy.
iApply lty_le_exist. iApply "Hle".
Qed.
(* TODO: Try to add Löb induction in the type system, and use it to prove μX.int → X <:> μX.int → int → X *)
(* TODO(COPY): Commuting rule for μ, allowing `copy` to move outside the μ *)
Lemma lty_rec_copy C `{!Contractive C} :
Lemma lty_copyable_rec C `{!Contractive C} :
( A, lty_copyable A - lty_copyable (C A)) - lty_copyable (lty_rec C).
Proof.
iIntros "#Hcopy".
......
Markdown is supported
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