Merge branch 'master' of https://gitlab.mpi-sws.org/iris/actris

theories/logrel/environments.v

@@ -10,9 +10,10 @@ relations on environments are defined:
 In addition, some lemmas/rules about these definitions are proved, corresponding
 to the syntactic typing rules that are typically found in substructural type
 systems. *)
-From actris.logrel Require Export term_types subtyping.
-From iris.proofmode Require Import tactics.
 From iris.algebra Require Export list.
+From iris.bi.lib Require Import core.
+From actris.logrel Require Export term_types subtyping_rules.
+From iris.proofmode Require Import tactics.
 
 Inductive env_item Σ := EnvItem {
   env_item_name : string;
@@ -56,6 +57,12 @@ Arguments env_filter_ne _ !_ !_ / : simpl nomatch.
 factored out. *)
 Arguments filter _ _ _ _ _ !_ / : simpl nomatch.
 
+Instance env_lookup {Σ} : Lookup string (ltty Σ) (env Σ) := λ x Γ,
+  match env_filter_eq x Γ with
+  | [EnvItem _ A] => Some A
+  | _ => None
+  end.
+
 Definition env_cons {Σ} (b : binder) (A : ltty Σ) (Γ : env Σ) : env Σ :=
   if b is BNamed x then EnvItem x A :: env_filter_ne x Γ else Γ.
 
@@ -83,10 +90,6 @@ Section env.
     - rewrite filter_cons_True /=; last naive_solver.
       by rewrite -Permutation_middle -IH.
   Qed.
-  Lemma env_filter_eq_perm' Γ Γ' x :
-    env_filter_eq x Γ = Γ' →
-    Γ ≡ₚ Γ' ++ env_filter_ne x Γ.
-  Proof. intros <-. apply env_filter_eq_perm. Qed.
 
   Lemma env_filter_ne_anon Γ : env_filter_ne BAnon Γ = Γ.
   Proof. induction Γ as [|[y A] Γ IH]; by f_equal/=. Qed.
@@ -103,6 +106,18 @@ Section env.
     env_filter_ne x (EnvItem y A :: Γ) = EnvItem y A :: env_filter_ne x Γ.
   Proof. intros. rewrite /env_filter_ne filter_cons_True; naive_solver. Qed.
 
+  Lemma env_lookup_perm Γ x A:
+    Γ !! x = Some A →
+    Γ ≡ₚ EnvItem x A :: env_filter_ne x Γ.
+  Proof.
+    rewrite /lookup /env_lookup=> ?.
+    destruct (env_filter_eq x Γ) as [|[x' ?] [|??]] eqn:Hx; simplify_eq/=.
+    assert (EnvItem x' A ∈ env_filter_eq x Γ)
+      as [? _]%elem_of_list_filter; simplify_eq/=.
+    { rewrite Hx. set_solver. }
+    by rewrite {1}(env_filter_eq_perm Γ x') Hx.
+  Qed.
+
   (** env typing *)
   Global Instance env_ltyped_Permutation vs :
     Proper ((≡ₚ) ==> (⊣⊢)) (@env_ltyped Σ vs).	
@@ -205,4 +220,22 @@ Section env.
     iDestruct (env_ltyped_app with "Hvs") as "[Hvs1 Hvs2]".
     iApply env_ltyped_app. iSplitL "Hvs1"; [by iApply "H"|by iApply "H'"].
   Qed.
+  Lemma env_le_copy x A :
+    ⊢ env_le [EnvItem x A] [EnvItem x A; EnvItem x (copy- A)].
+  Proof.
+    iIntros "!>" (vs) "Hvs".
+    iDestruct (env_ltyped_cons with "Hvs") as (v ?) "[HA _]".
+    iAssert (ltty_car (copy- A) v)%lty as "#HAm"; [by iApply coreP_intro|].
+    iApply env_ltyped_cons. iExists _; iSplit; [done|]. iFrame "HA".
+    iApply env_ltyped_cons. iExists _; iSplit; [done|]. iFrame "HAm".
+    iApply env_ltyped_nil.
+  Qed.
+  Lemma env_le_copyable x A :
+    lty_copyable A -∗
+    env_le [EnvItem x A] [EnvItem x A; EnvItem x A].
+  Proof.
+    iIntros "#H". iApply env_le_trans; [iApply env_le_copy|].
+    iApply env_le_cons; [iApply lty_le_refl|].
+    iApply env_le_cons; [by iApply lty_le_copy_inv_elim_copyable|iApply env_le_nil].
+  Qed.
 End env.

theories/logrel/lib/mutex.v

@@ -118,10 +118,10 @@ Section rules.
   Qed.
 
   Lemma ltyped_mutex_acquire Γ (x : string) A :
-    env_filter_eq x Γ = [EnvItem x (mutex A)] →
+    Γ !! x = Some (mutex A)%lty →
     ⊢ Γ ⊨ mutex_acquire x : A ⫤ env_cons x (mutex_guard A) Γ.
   Proof.
-    iIntros (HΓx%env_filter_eq_perm' vs) "!> HΓ /=". rewrite {1}HΓx /=.
+    iIntros (HΓx%env_lookup_perm vs) "!> HΓ /=". rewrite {1}HΓx /=.
     iDestruct (env_ltyped_cons with "HΓ") as (vl Hvs) "[Hlock HΓ]"; rewrite Hvs.
     iDestruct "Hlock" as (γ l lk ->) "#Hlock". rewrite /mutex_acquire.
     wp_apply (acquire_spec with "Hlock"); iIntros "[Hlocked Hinner]".
@@ -131,11 +131,11 @@ Section rules.
   Qed.
 
   Lemma ltyped_mutex_release Γ Γ' (x : string) e A :
-    env_filter_eq x Γ' = [EnvItem x (mutex_guard A)] →
+    Γ' !! x = Some (mutex_guard A)%lty →
     (Γ ⊨ e : A ⫤ Γ') -∗
     Γ ⊨ mutex_release x e : () ⫤ env_cons x (mutex A) Γ'.
   Proof.
-    iIntros (HΓx%env_filter_eq_perm') "#He". iIntros (vs) "!> HΓ /=".
+    iIntros (HΓx%env_lookup_perm) "#He". iIntros (vs) "!> HΓ /=".
     wp_apply (wp_wand with "(He HΓ)"). iIntros (v) "[HA HΓ']".
     rewrite {2}HΓx /=.
     iDestruct (env_ltyped_cons with "HΓ'") as (vl Hvs) "[Hguard HΓ']"; rewrite Hvs.

theories/logrel/session_typing_rules.v

@@ -25,11 +25,11 @@ Section session_typing_rules.
   Qed.
 
   Lemma ltyped_send Γ Γ' (x : string) e A S :
-    env_filter_eq x Γ' = [EnvItem x (chan (<!!> TY A; S))] →
+    Γ' !! x = Some (chan (<!!> TY A; S))%lty →
     (Γ ⊨ e : A ⫤ Γ') -∗
     Γ ⊨ send x e : () ⫤ env_cons x (chan S) Γ'.
   Proof.
-    iIntros (HΓx%env_filter_eq_perm') "#He !>". iIntros (vs) "HΓ /=".
+    iIntros (HΓx%env_lookup_perm) "#He !>". iIntros (vs) "HΓ /=".
     wp_apply (wp_wand with "(He HΓ)"); iIntros (v) "[HA HΓ']".
     rewrite {2}HΓx /=.
     iDestruct (env_ltyped_cons with "HΓ'") as (c Hvs) "[Hc HΓ']". rewrite Hvs.
@@ -49,7 +49,7 @@ Section session_typing_rules.
 
   Lemma ltyped_recv_texist {kt} Γ1 Γ2 M x (xc : string) (e : expr)
       (A : kt -k> ltty Σ) (S : kt -k> lsty Σ) (B : ltty Σ) :
-    env_filter_eq xc Γ1 = [EnvItem xc (chan (<??> M))] →
+    Γ1 !! xc = Some (chan (<??> M))%lty →
     LtyMsgTele M A S →
     (∀ Ys,
       env_cons x (ktele_app A Ys) (env_cons xc (chan (ktele_app S Ys)) Γ1) ⊨ e : B ⫤ Γ2) -∗
@@ -57,7 +57,7 @@ Section session_typing_rules.
           env_filter_eq x (env_filter_ne xc Γ1) ++ env_filter_ne x Γ2.
   Proof.
     rewrite /LtyMsgTele.
-    iIntros (HΓxc%env_filter_eq_perm' HM) "#He !>". iIntros (vs) "HΓ1 /=".
+    iIntros (HΓxc%env_lookup_perm HM) "#He !>". iIntros (vs) "HΓ1 /=".
     rewrite {2}HΓxc /=.
     iDestruct (env_ltyped_cons with "HΓ1") as (c Hvs) "[Hc HΓ1]". rewrite Hvs.
     rewrite {2}(env_filter_eq_perm (env_filter_ne xc Γ1) x).
@@ -79,10 +79,10 @@ Section session_typing_rules.
   Qed.
 
   Lemma ltyped_recv Γ (x : string) A S :
-    env_filter_eq x Γ = [EnvItem x (chan (<??> TY A; S))] →
+    Γ !! x = Some (chan (<??> TY A; S))%lty →
     ⊢ Γ ⊨ recv x : A ⫤ env_cons x (chan S) Γ.
   Proof.
-    iIntros (HΓx%env_filter_eq_perm') "!>". iIntros (vs) "HΓ /=".
+    iIntros (HΓx%env_lookup_perm) "!>". iIntros (vs) "HΓ /=".
     rewrite {1}HΓx /=.
     iDestruct (env_ltyped_cons with "HΓ") as (c Hvs) "[Hc HΓ]". rewrite Hvs.
     wp_recv (v) as "HA". iFrame "HA". iApply env_ltyped_cons; eauto with iFrame.
@@ -91,11 +91,11 @@ Section session_typing_rules.
   Definition select : val := λ: "c" "i", send "c" "i".
 
   Lemma ltyped_select Γ (x : string) (i : Z) (S : lsty Σ) Ss :
+    Γ !! x = Some (chan (lty_select Ss))%lty →
     Ss !! i = Some S →
-    env_filter_eq x Γ = [EnvItem x (chan (lty_select Ss))] →
     ⊢ Γ ⊨ select x #i : () ⫤ env_cons x (chan S) Γ.
   Proof.
-    iIntros (Hin HΓx%env_filter_eq_perm'); iIntros "!>" (vs) "HΓ /=".
+    iIntros (HΓx%env_lookup_perm Hin); iIntros "!>" (vs) "HΓ /=".
     rewrite {1}HΓx /=.
     iDestruct (env_ltyped_cons with "HΓ") as (c Hvs) "[Hc HΓ]". rewrite Hvs.
     rewrite /select. wp_send with "[]"; [by eauto|]. iSplit; [done|].

theories/logrel/term_typing_rules.v

@@ -26,10 +26,10 @@ Section term_typing_rules.
 
   (** Variable properties *)
   Lemma ltyped_var Γ (x : string) A :
-    env_filter_eq x Γ = [EnvItem x A] →
+    Γ !! x = Some A →
     ⊢ Γ ⊨ x : A ⫤ env_cons x (copy- A) Γ.
   Proof.
-    iIntros (HΓx%env_filter_eq_perm') "!>"; iIntros (vs) "HΓ /=".
+    iIntros (HΓx%env_lookup_perm) "!>"; iIntros (vs) "HΓ /=".
     rewrite {1}HΓx /=.
     iDestruct (env_ltyped_cons with "HΓ") as (v Hvs) "[HA HΓ]". rewrite Hvs.
     iAssert (ltty_car (copy- A) v)%lty as "#HAm"; [by iApply coreP_intro|].
@@ -196,10 +196,10 @@ Section term_typing_rules.
   Qed.
 
   Lemma ltyped_fst Γ A1 A2 (x : string) :
-    env_filter_eq x Γ = [EnvItem x (A1 * A2)] →
+    Γ !! x = Some (A1 * A2)%lty →
     ⊢ Γ ⊨ Fst x : A1 ⫤ env_cons x (copy- A1 * A2) Γ.
   Proof.
-    iIntros (HΓx%env_filter_eq_perm' vs) "!> HΓ /=". rewrite {1}HΓx /=.
+    iIntros (HΓx%env_lookup_perm vs) "!> HΓ /=". rewrite {1}HΓx /=.
     iDestruct (env_ltyped_cons with "HΓ") as (v Hvs) "[HA HΓ]"; rewrite Hvs.
     iDestruct "HA" as (v1 v2 ->) "[HA1 HA2]". wp_pures.
     iAssert (ltty_car (copy- A1) v1)%lty as "#HA1m"; [by iApply coreP_intro|].
@@ -208,10 +208,10 @@ Section term_typing_rules.
   Qed.
 
   Lemma ltyped_snd Γ A1 A2 (x : string) :
-    env_filter_eq x Γ = [EnvItem x (A1 * A2)] →
+    Γ !! x = Some (A1 * A2)%lty →
     ⊢ Γ ⊨ Snd x : A2 ⫤ env_cons x (A1 * copy- A2) Γ.
   Proof.
-    iIntros (HΓx%env_filter_eq_perm' vs) "!> HΓ /=". rewrite {1}HΓx /=.
+    iIntros (HΓx%env_lookup_perm vs) "!> HΓ /=". rewrite {1}HΓx /=.
     iDestruct (env_ltyped_cons with "HΓ") as (v Hvs) "[HA HΓ]"; rewrite Hvs.
     iDestruct "HA" as (v1 v2 ->) "[HA1 HA2]". wp_pures.
     iAssert (ltty_car (copy- A2) v2)%lty as "#HA2m"; [by iApply coreP_intro|].
@@ -317,10 +317,10 @@ Section term_typing_rules.
   Qed.
 
   Lemma ltyped_load Γ (x : string) A :
-    env_filter_eq x Γ = [EnvItem x (ref_uniq A)] →
+    Γ !! x = Some (ref_uniq A)%lty →
     ⊢ Γ ⊨ ! x : A ⫤ env_cons x (ref_uniq (copy- A)) Γ.
   Proof.
-    iIntros (HΓx%env_filter_eq_perm' vs) "!> HΓ /=". rewrite {1}HΓx /=.
+    iIntros (HΓx%env_lookup_perm vs) "!> HΓ /=". rewrite {1}HΓx /=.
     iDestruct (env_ltyped_cons with "HΓ") as (v Hvs) "[HA HΓ]"; rewrite Hvs.
     iDestruct "HA" as (l w ->) "[? HA]". wp_load.
     iAssert (ltty_car (copy- A) w)%lty as "#HAm"; [by iApply coreP_intro|].
@@ -329,11 +329,11 @@ Section term_typing_rules.
   Qed.
 
   Lemma ltyped_store Γ Γ' (x : string) e A B :
-    env_filter_eq x Γ' = [EnvItem x (ref_uniq A)] →
+    Γ' !! x = Some (ref_uniq A)%lty →
     (Γ ⊨ e : B ⫤ Γ') -∗
     Γ ⊨ x <- e : () ⫤ env_cons x (ref_uniq B) Γ'.
   Proof.
-    iIntros (HΓx%env_filter_eq_perm') "#He"; iIntros (vs) "!> HΓ /=".
+    iIntros (HΓx%env_lookup_perm) "#He"; iIntros (vs) "!> HΓ /=".
     wp_apply (wp_wand with "(He HΓ)"). iIntros (v) "[HB HΓ']".
     rewrite {2}HΓx /=.
     iDestruct (env_ltyped_cons with "HΓ'") as (vl Hvs) "[HA HΓ']"; rewrite Hvs.