diff --git a/theories/logrel/subtyping_rules.v b/theories/logrel/subtyping_rules.v index 679bc3132e82ae43c4b53b56f546ce9b1044bf7b..2715f374499420f08a5ef2a7e22ca8c34e573b12 100644 --- a/theories/logrel/subtyping_rules.v +++ b/theories/logrel/subtyping_rules.v @@ -171,7 +171,7 @@ Section subtyping_rules. Qed. Lemma lty_le_exist C1 C2 : - (∀ A, C1 A <: C2 A) -∗ + ▷ (∀ A, C1 A <: C2 A) -∗ (∃ A, C1 A) <: (∃ A, C2 A). Proof. iIntros "#Hle" (v) "!>". iDestruct 1 as (A) "H". iExists A. by iApply "Hle". diff --git a/theories/logrel/term_types.v b/theories/logrel/term_types.v index c28e957848503fcf6f28b4c7f92a7f798da1d4b4..b69d653d7f06c18f548b41d1b3c2641084f48170 100644 --- a/theories/logrel/term_types.v +++ b/theories/logrel/term_types.v @@ -27,7 +27,7 @@ Definition lty_sum {Σ} (A1 A2 : ltty Σ) : ltty Σ := Ltty (λ w, Definition lty_forall `{heapG Σ} {k} (C : lty Σ k → ltty Σ) : ltty Σ := Ltty (λ w, ∀ A, WP w #() {{ ltty_car (C A) }})%I. Definition lty_exist {Σ k} (C : lty Σ k → ltty Σ) : ltty Σ := - Ltty (λ w, ∃ A, ltty_car (C A) w)%I. + Ltty (λ w, ∃ A, ▷ ltty_car (C A) w)%I. Definition lty_ref_mut `{heapG Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w, ∃ (l : loc) (v : val), ⌜w = #l⌝ ∗ l ↦ v ∗ ▷ ltty_car A v)%I. @@ -115,6 +115,9 @@ Section term_types. Global Instance lty_forall_ne `{heapG Σ} k n : Proper (pointwise_relation _ (dist n) ==> dist n) (@lty_forall Σ _ k). Proof. solve_proper. Qed. + Global Instance lty_exist_contractive k n : + Proper (pointwise_relation _ (dist_later n) ==> dist n) (@lty_exist Σ k). + Proof. solve_contractive. Qed. Global Instance lty_exist_ne k n : Proper (pointwise_relation _ (dist n) ==> dist n) (@lty_exist Σ k). Proof. solve_proper. Qed. diff --git a/theories/logrel/term_typing_rules.v b/theories/logrel/term_typing_rules.v index 605ee561c2f24f079838438af97b1bebb72a522c..383be7e69ef5db2d8d4607f4069a7339769f0aa5 100644 --- a/theories/logrel/term_typing_rules.v +++ b/theories/logrel/term_typing_rules.v @@ -240,19 +240,22 @@ Section properties. wp_apply (wp_wand with "(He [HΓ //])"); iIntros (w) "[HB \$]". by iExists M. Qed. - Lemma ltyped_unpack {k} Γ1 Γ2 Γ3 (x : string) e (C : lty Σ k → ltty Σ) A : - Γ1 !! x = Some (lty_exist C) → - (∀ X, Γ1 ⊨ e : A ⫤ Γ2) -∗ - (Γ1 ⊨ e : A ⫤ Γ2). + Lemma ltyped_unpack {k} Γ1 Γ2 Γ3 x e1 e2 (C : lty Σ k → ltty Σ) B : + (Γ1 ⊨ e1 : ∃ M, C M ⫤ Γ2) -∗ + (∀ Y, Γ2 ⊨ e2 : B ⫤ Γ3) -∗ + Γ1 ⊨ (let: x := e1 in e2) : B ⫤ binder_delete x Γ3. Proof. - iIntros (Hx) "#He". iIntros (vs) "!> HΓ". - iDestruct (env_ltyped_lookup with "HΓ") as (v Hv) "[HB HΓ]"; first done. - iDestruct ("HB") as (B) "HB". - iDestruct (env_ltyped_insert _ _ x with "HB HΓ") as "HΓ". - rewrite /binder_insert insert_delete (insert_id _ _ _ Hv). - iApply (wp_wand with "(He HΓ)"). eauto. + iIntros "#He1 #He2 !>". iIntros (vs) "HΓ1"=> /=. + wp_apply (wp_wand with "(He1 HΓ1)"); iIntros (v) "[HC HΓ2]". + iDestruct "HC" as (X) "HX". wp_pures. + iDestruct (env_ltyped_insert _ _ x with "HX HΓ2") as "HΓ2". + iDestruct ("He2" with "HΓ2") as "He2'". + destruct x as [|x]; rewrite /= -?subst_map_insert //. + wp_apply (wp_wand with "He2'"). + iIntros (w) "[\$ HΓ3]". by iApply env_ltyped_delete. Qed. + (** Mutable Reference properties *) Lemma ltyped_alloc Γ1 Γ2 e A : (Γ1 ⊨ e : A ⫤ Γ2) -∗ @@ -304,7 +307,7 @@ Section properties. iFrame "HΓ'". Qed. - (** Weak Reference properties *) + (** Shared Reference properties *) Lemma ltyped_upgrade_shared Γ Γ' e A : (Γ ⊨ e : ref_mut (copy A) ⫤ Γ') -∗ Γ ⊨ e : ref_shr A ⫤ Γ'.