Merge branch 'daniel/plainly' into 'master'

Plainly

See merge request iris/actris!10

theories/logrel/copying.v

@@ -23,25 +23,35 @@ Section copying.
     ⊢ copy A <: A.
   Proof. by iIntros (v) "!> #H". Qed.
 
-  (* TODO(COPY): have A <: copy- A rule *)
   (* TODO(COPY): Show derived rules about copyability of products, sums, etc. *)
   (* TODO(COPY): Commuting rule for μ, allowing `copy` to move outside the μ *)
 
-  (* TODO(COPY) *)
-  Lemma coreP_desired_lemma (P : iProp Σ) :
-    □ (P -∗ □ P) -∗ coreP P -∗ P.
+  Lemma lty_le_copy_minus_copy A :
+    ⊢ copy- (copy A) <: A.
   Proof.
-    iIntros "HP Hcore".
-  Admitted.
+    iIntros (v) "!> #Hv".
+    iDestruct (coreP_elim with "Hv") as "Hw".
+    iApply "Hw".
+  Qed.
 
   Lemma lty_le_copy_minus A :
-    copyable A -∗ copy- A <: A.
+    ⊢ A <: copy- A.
+  Proof. iIntros "!>" (v). iApply coreP_intro. Qed.
+
+  (* TODO: Wait for this to be merged into Iris and then bump Iris version *)
+  Lemma actris_coreP_wand (P Q : iProp Σ) : <affine> ■ (P -∗ Q) -∗ coreP P -∗ coreP Q.
+  Proof.
+    rewrite /coreP. iIntros "#HPQ HP" (R) "#HR #HQR". iApply ("HP" with "HR").
+    iIntros "!> !> HP". iApply "HQR". by iApply "HPQ".
+  Qed.
+
+  Lemma lty_copy_minus_mono A B :
+    A <: B -∗ copy- A <: copy- B.
   Proof.
-    iIntros "#HA". iIntros (v) "!> #Hv".
-    iSpecialize ("HA" $! v).
-    iApply coreP_desired_lemma.
-    - iModIntro. iApply "HA".
-    - iApply "Hv".
+    iIntros "#Hsub !>" (v) "#HA".
+    iApply (actris_coreP_wand (A v)).
+    - iModIntro. iClear "HA". iModIntro. iApply "Hsub".
+    - iApply "HA".
   Qed.
 
   (* Copyability of types *)
@@ -111,7 +121,7 @@ Section copying.
 
   (* Copyability of recursive types *)
   Lemma lty_rec_copy C `{!Contractive C} :
-    □ (∀ A, ▷ copyable A -∗ copyable (C A)) -∗ copyable (lty_rec C).
+    (∀ A, ▷ copyable A -∗ copyable (C A)) -∗ copyable (lty_rec C).
   Proof.
     iIntros "#Hcopy".
     iLöb as "IH".
@@ -150,7 +160,7 @@ Section copying.
   Qed.
 
   Definition env_copy (Γ Γ' : gmap string (lty Σ)) : iProp Σ :=
-    □ ∀ vs, env_ltyped Γ vs -∗ □ env_ltyped Γ' vs.
+    (■ ∀ vs, env_ltyped Γ vs -∗ □ env_ltyped Γ' vs)%I.
 
   Lemma env_copy_empty : ⊢ env_copy ∅ ∅.
   Proof. iIntros (vs) "!> _ !> ". by rewrite /env_ltyped. Qed.

theories/logrel/ltyping.v

@@ -99,7 +99,7 @@ Section Environment.
   Qed.
 
   Definition env_split (Γ Γ1 Γ2 : gmap string (lty Σ)) : iProp Σ :=
-    □ ∀ vs, env_ltyped Γ vs ∗-∗ (env_ltyped Γ1 vs ∗ env_ltyped Γ2 vs).
+    (■ ∀ vs, env_ltyped Γ vs ∗-∗ (env_ltyped Γ1 vs ∗ env_ltyped Γ2 vs))%I.
 
   Lemma env_split_id_l Γ : ⊢ env_split Γ ∅ Γ.
   Proof.
@@ -161,8 +161,8 @@ End Environment.
 (* The semantic typing judgement *)
 Definition ltyped `{!heapG Σ}
     (Γ Γ' : gmap string (lty Σ)) (e : expr) (A : lty Σ) : iProp Σ :=
-  □ ∀ vs, env_ltyped Γ vs -∗
-          WP subst_map vs e {{ v, A v ∗ env_ltyped Γ' vs }}.
+  (■ ∀ vs, env_ltyped Γ vs -∗
+           WP subst_map vs e {{ v, A v ∗ env_ltyped Γ' vs }})%I.
 
 Notation "Γ ⊨ e : A ⫤ Γ'" := (ltyped Γ Γ' e A)
   (at level 100, e at next level, A at level 200).

theories/logrel/subtyping.v

@@ -5,7 +5,7 @@ From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode.
 
 Definition lty_le {Σ} (A1 A2 : lty Σ) : iProp Σ :=
-  □ ∀ v, A1 v -∗ A2 v.
+  (■ ∀ v, A1 v -∗ A2 v)%I.
 Arguments lty_le {_} _%lty _%lty.
 Infix "<:" := lty_le (at level 70).
 Instance: Params (@lty_le) 1 := {}.
@@ -25,7 +25,7 @@ Instance lty_bi_le_proper {Σ} : Proper ((≡) ==> (≡) ==> (≡)) (@lty_bi_le
 Proof. solve_proper. Qed.
 
 Definition lsty_le {Σ} (P1 P2 : lsty Σ) : iProp Σ :=
-  □ iProto_le P1 P2.
+  (■ iProto_le P1 P2)%I.
 Arguments lsty_le {_} _%lsty _%lsty.
 Infix "<s:" := lsty_le (at level 70).
 Instance: Params (@lsty_le) 1 := {}.
@@ -137,7 +137,7 @@ Section subtype.
   Qed.
 
   Lemma lty_le_rec `{Contractive C1, Contractive C2} :
-    (□ ∀ A B, ▷ (A <: B) -∗ C1 A <: C2 B) -∗
+    (∀ A B, ▷ (A <: B) -∗ C1 A <: C2 B) -∗
     lty_rec C1 <: lty_rec C2.
   Proof.
     iIntros "#Hle".
@@ -196,7 +196,8 @@ Section subtype.
   Qed.
 
   Lemma lsty_le_refl (S : lsty Σ) : ⊢ S <s: S.
-  Proof. iApply iProto_le_refl. Qed.
+  Proof. iModIntro. iApply iProto_le_refl. Qed.
+
   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.
 
@@ -462,11 +463,11 @@ Section subtype.
   Qed.
 
   Lemma lsty_le_rec `{Contractive C1, Contractive C2} :
-    (□ ∀ S S', ▷ (S <s: S') -∗ C1 S <s: C2 S') -∗
+    (∀ S S', ▷ (S <s: S') -∗ C1 S <s: C2 S') -∗
     lsty_rec C1 <s: lsty_rec C2.
   Proof.
-    iIntros "#Hle !>".
-    iLöb as "IH".
+    iIntros "#Hle".
+    iLöb as "IH". iModIntro.
     rewrite /lsty_rec.
     iEval (rewrite fixpoint_unfold).
     iEval (rewrite (fixpoint_unfold (lsty_rec1 C2))).