From ce200ea55b6b24a186b340b9cf5bedfc57b18e3f Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Sun, 4 Sep 2022 17:14:52 +0200 Subject: [PATCH 1/7] Add Persistent instances --- theories/Dot/lr/dot_lty.v | 3 +++ theories/iris_extra/dlang.v | 3 +++ theories/iris_extra/lty.v | 3 +++ theories/iris_extra/saved_interp_dep.v | 3 +++ 4 files changed, 12 insertions(+) diff --git a/theories/Dot/lr/dot_lty.v b/theories/Dot/lr/dot_lty.v index 708d007a..ac6bebc0 100644 --- a/theories/Dot/lr/dot_lty.v +++ b/theories/Dot/lr/dot_lty.v @@ -329,6 +329,9 @@ Notation "d ↗ ψ" := (dm_to_type d ψ) (at level 20). Section dm_to_type. Context `{HdotG : !dlangG Σ} `{rinterp : !RecTyInterp Σ}. + #[global] Instance dm_to_type_persistent d ψ: Persistent (d ↗ ψ). + Proof. destruct d; apply _. Qed. + Lemma dm_to_type_agree {d ψ1 ψ2} args v : d ↗ ψ1 -∗ d ↗ ψ2 -∗ ▷ (ψ1 args v ≡ ψ2 args v). Proof. destruct d; simpl; [ | apply stamp_σ_to_type_agree | by iIntros "[]" ]. diff --git a/theories/iris_extra/dlang.v b/theories/iris_extra/dlang.v index 99f72389..2915a300 100644 --- a/theories/iris_extra/dlang.v +++ b/theories/iris_extra/dlang.v @@ -71,6 +71,9 @@ Module Type LiftWp (Import VS : VlSortsSig). Lemma stamp_σ_to_type_intro s σ (φ : hoEnvD Σ) : s ↝n φ -∗ s ↗n[ σ ] hoEnvD_inst σ φ. Proof. rewrite /stamp_σ_to_type. iIntros; iExists φ; auto. Qed. + + #[global] Instance stamp_σ_to_type_persistent σ s ψ : + Persistent (s ↗n[ σ ] ψ) := _. End mapsto. Typeclasses Opaque stamp_σ_to_type. diff --git a/theories/iris_extra/lty.v b/theories/iris_extra/lty.v index f2f594a2..9c0dab2c 100644 --- a/theories/iris_extra/lty.v +++ b/theories/iris_extra/lty.v @@ -342,6 +342,9 @@ Section env_oltyped. Definition env_oltyped_cons ρ τ (Γ : sCtx Σ) : sG⟦ τ :: Γ ⟧* ρ ⊣⊢ sG⟦ Γ ⟧* (stail ρ) ∧ oClose τ ρ (shead ρ) := reflexivity _. + #[global] Instance env_oltyped_persistent (Γ : sCtx Σ) ρ: Persistent (sG⟦ Γ ⟧* ρ). + Proof. elim: Γ ρ => [|τ Γ IHΓ] ρ /=; apply _. Qed. + #[global] Instance env_oltyped_ne ρ : NonExpansive (env_oltyped ρ). Proof. move: ρ => + n G1 G2. diff --git a/theories/iris_extra/saved_interp_dep.v b/theories/iris_extra/saved_interp_dep.v index f0b319b0..8e553463 100644 --- a/theories/iris_extra/saved_interp_dep.v +++ b/theories/iris_extra/saved_interp_dep.v @@ -95,6 +95,9 @@ Section saved_ho_sem_type. saved_anything_own (F := hoEnvPredOF s) γ (ho_pack (existT n Φ)). Notation "γ ⤇n[ n ] φ" := (saved_ho_sem_type_own γ n φ) (at level 20). + #[global] Instance saved_ho_sem_type_own_persistent γ n φ : + Persistent (γ ⤇n[ n ] φ) := _. + #[global] Instance saved_ho_sem_type_own_contractive γ i : Contractive (saved_ho_sem_type_own γ i). Proof. From 9f1ba9cdcc16717aa2e420521e81a4a81339fac3 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Sun, 4 Sep 2022 17:15:34 +0200 Subject: [PATCH 2/7] Proof refactoring --- theories/Dot/hkdot/sem_kind_dot.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/Dot/hkdot/sem_kind_dot.v b/theories/Dot/hkdot/sem_kind_dot.v index bfe2481b..4f27d915 100644 --- a/theories/Dot/hkdot/sem_kind_dot.v +++ b/theories/Dot/hkdot/sem_kind_dot.v @@ -68,7 +68,7 @@ Section TMem_lemmas. Lemma oTMemK_eq l K args ρ v : oTMemK l K args ρ v ⊣⊢ ∃ ψ d, ⌜v ,, l ↘ d⌝ ∧ d ↗ ψ ∧ K ρ (packHoLtyO ψ) (packHoLtyO ψ). - Proof. apply bi_exist_nested_swap. Qed. + Proof. by rewrite /cTMemK/= bi_exist_nested_swap. Qed. Lemma cTMemAnyKind_eq l d ρ : cTMemAnyKind l ρ [(l, d)] ⊣⊢ oDTMemAnyKind ρ d. From abce3406f899072f4f4c8e994dd20ab8ae6a546e Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Sun, 4 Sep 2022 18:15:03 +0200 Subject: [PATCH 3/7] Extra steps in abandoned proof --- theories/Dot/hkdot/hkdot.v | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/theories/Dot/hkdot/hkdot.v b/theories/Dot/hkdot/hkdot.v index eb388c91..73285b9f 100644 --- a/theories/Dot/hkdot/hkdot.v +++ b/theories/Dot/hkdot/hkdot.v @@ -951,8 +951,11 @@ Section dot_experimental_kinds. rewrite /sr_kintv/=. rewrite !envApply_oTAppV_eq. iEval asimpl. - (* iApply sf_kind_sub_trans. - iApply (sfkind_respects with "[] (HT [])"). *) + iApply sf_kind_sub_trans. + { iApply (sfkind_respects with "[] (HT [])"). + { iIntros "% %". iSplit; iIntros "$". } + admit. + } Abort. From 4c6a8dd4c24274e85465f6f65f3f3819af1d5ed3 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Sun, 4 Sep 2022 17:48:54 +0200 Subject: [PATCH 4/7] Comment out path_equiv --- theories/Dot/hkdot/path_equiv.v | 2 ++ theories/Dot/hkdot/path_equiv2.v | 2 ++ 2 files changed, 4 insertions(+) diff --git a/theories/Dot/hkdot/path_equiv.v b/theories/Dot/hkdot/path_equiv.v index 7d08b0e9..c01365fe 100644 --- a/theories/Dot/hkdot/path_equiv.v +++ b/theories/Dot/hkdot/path_equiv.v @@ -8,6 +8,7 @@ From D.Dot Require Import dlang_inst path_wp. From D.pure_program_logic Require Import weakestpre. From D.Dot Require Import dot_lty dot_semtypes sem_kind_dot unary_lr. +(* Implicit Types (Σ : gFunctors) (v w : vl) (e : tm) (d : dm) (ds : dms) (p : path) (ρ : env) (l : label) (T : ty) (K : kind). @@ -232,3 +233,4 @@ Print hoD *) End foo. +*) diff --git a/theories/Dot/hkdot/path_equiv2.v b/theories/Dot/hkdot/path_equiv2.v index dc82dd1c..7621bd76 100644 --- a/theories/Dot/hkdot/path_equiv2.v +++ b/theories/Dot/hkdot/path_equiv2.v @@ -9,6 +9,7 @@ From D.Dot Require Import syn path_repl. From D.Dot Require Import dlang_inst path_wp. From D.Dot Require Import dot_lty dot_semtypes sem_kind_dot unary_lr. From D.Dot Require Import hkdot. +(* Import HkDot. (* Import last to override side effects. *) From D Require Import proper. @@ -894,3 +895,4 @@ End foo. (* Exercise for the reader: remember the point is that all _consumers_ respect path equality. So for each elimination rule from supported types, we must prove functionality! *) +*) From 6d1ba6847a5c30b20cbcf772f14d9dd28c91e399 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Sun, 4 Sep 2022 17:38:59 +0200 Subject: [PATCH 5/7] Persistent updates for gDOT: Definitions (does not compile) --- theories/Dot/examples/sem/semtyp_lemmas/sub_lr.v | 2 +- theories/Dot/hkdot/hkdot.v | 5 +++-- theories/Dot/hkdot/sem_kind_dot.v | 2 +- theories/Dot/lr/dot_lty.v | 3 ++- theories/Dot/lr/dot_semtypes.v | 9 +++++---- theories/Dot/lr/sem_unstamped_typing.v | 15 +++++++-------- 6 files changed, 19 insertions(+), 17 deletions(-) diff --git a/theories/Dot/examples/sem/semtyp_lemmas/sub_lr.v b/theories/Dot/examples/sem/semtyp_lemmas/sub_lr.v index 9f712e88..1bc4a24a 100644 --- a/theories/Dot/examples/sem/semtyp_lemmas/sub_lr.v +++ b/theories/Dot/examples/sem/semtyp_lemmas/sub_lr.v @@ -18,7 +18,7 @@ Section defs. (** Legacy: (double)-indexed subtyping. *) Definition sstpi `{!dlangG Σ} i j Γ τ1 τ2 : iProp Σ := - |==> sstpi' i j Γ τ1 τ2. + sstpi' i j Γ τ1 τ2. #[global] Arguments sstpi /. End defs. (** Indexed subtyping *) diff --git a/theories/Dot/hkdot/hkdot.v b/theories/Dot/hkdot/hkdot.v index 73285b9f..a5b40277 100644 --- a/theories/Dot/hkdot/hkdot.v +++ b/theories/Dot/hkdot/hkdot.v @@ -12,6 +12,7 @@ From D.Dot Require defs_lr binding_lr dsub_lr path_repl_lr sub_lr examples_lr. From D.Dot Require hoas ex_utils. From D.Dot Require Import sem_kind sem_kind_dot. +Require Import D.iris_extra.proofmode_pupd. Set Implicit Arguments. Unset Strict Implicit. @@ -31,7 +32,7 @@ Notation sstpiK_env i T1 T2 K ρ := (▷^i K ρ (envApply T1 ρ) (envApply T2 ρ Notation sstpiK' i Γ T1 T2 K := (∀ ρ, sG⟦Γ⟧*ρ → sstpiK_env i T1 T2 K ρ)%I. Definition sstpiK `{dlangG Σ} i Γ T1 T2 (K : sf_kind Σ) : iProp Σ := - |==> sstpiK' i Γ T1 T2 K. + sstpiK' i Γ T1 T2 K. Arguments sstpiK : simpl never. #[global] Instance : Params (@sstpiK) 4 := {}. Notation "Γ s⊨ T1 <:[ i ] T2 ∷ K" := (sstpiK i Γ T1 T2 K) @@ -46,7 +47,7 @@ Notation "Γ s⊨ T ∷[ i ] K" := (Γ s⊨ T <:[ i ] T ∷ K) (* Semantic SubKinding *) Definition sSkd `{dlangG Σ} i Γ (K1 K2 : sf_kind Σ) : iProp Σ := - |==> ∀ ρ, sG⟦Γ⟧*ρ → ∀ (T1 T2 : hoLtyO Σ), ▷^i (K1 ρ T1 T2 → K2 ρ T1 T2). + ∀ ρ, sG⟦Γ⟧*ρ → ∀ (T1 T2 : hoLtyO Σ), ▷^i (K1 ρ T1 T2 → K2 ρ T1 T2). Arguments sSkd : simpl never. #[global] Instance : Params (@sSkd) 4 := {}. Notation "Γ s⊨ K1 <∷[ i ] K2" := (sSkd i Γ K1 K2) diff --git a/theories/Dot/hkdot/sem_kind_dot.v b/theories/Dot/hkdot/sem_kind_dot.v index 4f27d915..2f49195d 100644 --- a/theories/Dot/hkdot/sem_kind_dot.v +++ b/theories/Dot/hkdot/sem_kind_dot.v @@ -160,7 +160,7 @@ End sem_TMem. (** * Path application and substitution *) Definition sem_kind_path_replI {Σ} p q (K1 K2 : sf_kind Σ) : iProp Σ := - |==> ∀ ρ T1 T2 (Hal : alias_paths p.|[ρ] q.|[ρ]), K1 ρ T1 T2 ≡ K2 ρ T1 T2. + ∀ ρ T1 T2 (Hal : alias_paths p.|[ρ] q.|[ρ]), K1 ρ T1 T2 ≡ K2 ρ T1 T2. (* sKdI = semantic Kind Path Iris; matches [sem_ty_path_replI]. *) Notation "K1 ~sKpI[ p := q ]* K2" := (sem_kind_path_replI p q K1 K2) (at level 70). diff --git a/theories/Dot/lr/dot_lty.v b/theories/Dot/lr/dot_lty.v index ac6bebc0..3a41f1e2 100644 --- a/theories/Dot/lr/dot_lty.v +++ b/theories/Dot/lr/dot_lty.v @@ -1,6 +1,7 @@ (** * Semantic domains for DOT logical relations. *) From iris.proofmode Require Import proofmode. From D Require Export iris_prelude proper lty lr_syn_aux. +From D Require Export iris_extra.proofmode_pupd. From D.Dot Require Import syn. From D.Dot Require Export dlang_inst path_wp. @@ -278,7 +279,7 @@ Notation "T .sTp[ p /]" := (opSubst p T) (at level 65). (** Semantic definition of path replacement. *) Definition sem_ty_path_replI {Σ} p q (T1 T2 : olty Σ) : iProp Σ := - |==> ∀ args ρ v (Hal : alias_paths p.|[ρ] q.|[ρ]), T1 args ρ v ≡ T2 args ρ v. + ∀ args ρ v (Hal : alias_paths p.|[ρ] q.|[ρ]), T1 args ρ v ≡ T2 args ρ v. (* sTpI = semantic Type Path Iris; matches [sem_kind_path_replI] *) Notation "T1 ~sTpI[ p := q ]* T2" := (sem_ty_path_replI p q T1 T2) (at level 70). diff --git a/theories/Dot/lr/dot_semtypes.v b/theories/Dot/lr/dot_semtypes.v index c47fb710..ce6d16ec 100644 --- a/theories/Dot/lr/dot_semtypes.v +++ b/theories/Dot/lr/dot_semtypes.v @@ -1,6 +1,7 @@ (** * Logical relation and semantic judgments. *) From D Require Export iris_prelude proper lty lr_syn_aux. From D Require Import iris_extra.det_reduction. +From D Require Export iris_extra.proofmode_pupd. From D Require Import swap_later_impl. From D.Dot Require Import syn path_repl. From D.Dot Require Export dlang_inst path_wp. @@ -22,18 +23,18 @@ Section judgments. (** Expression typing *) Definition setp `{!dlangG Σ} e Γ τ : iProp Σ := - |==> ∀ ρ, sG⟦Γ⟧* ρ → sE⟦ τ ⟧ ρ (e.|[ρ]). + ∀ ρ, sG⟦Γ⟧* ρ → sE⟦ τ ⟧ ρ (e.|[ρ]). #[global] Arguments setp : simpl never. (** Delayed subtyping. *) Definition sstpd `{!dlangG Σ} i Γ τ1 τ2 : iProp Σ := - |==> ∀ ρ, + ∀ ρ, sG⟦Γ⟧*ρ → ▷^i (oClose τ1 ρ ⊆ oClose τ2 ρ). #[global] Arguments sstpd : simpl never. (** Multi-definition typing *) Definition sdstp `{!dlangG Σ} ds Γ (T : clty Σ) : iProp Σ := - |==> ⌜wf_ds ds⌝ ∧ ∀ ρ, ⌜path_includes (pv (ids 0)) ρ ds ⌝ → sG⟦Γ⟧* ρ → T ρ ds.|[ρ]. + (⌜wf_ds ds⌝ ∧ ∀ ρ, ⌜path_includes (pv (ids 0)) ρ ds ⌝ → sG⟦Γ⟧* ρ → T ρ ds.|[ρ]). #[global] Arguments sdstp : simpl never. (** Definition typing *) @@ -42,7 +43,7 @@ Section judgments. (** Path typing *) Definition sptp `{!dlangG Σ} p i Γ τ : iProp Σ := - |==> ∀ ρ, sG⟦Γ⟧* ρ → + ∀ ρ, sG⟦Γ⟧* ρ → ▷^i path_wp p.|[ρ] (oClose τ ρ). #[global] Arguments sptp : simpl never. End judgments. diff --git a/theories/Dot/lr/sem_unstamped_typing.v b/theories/Dot/lr/sem_unstamped_typing.v index 948ce760..974fea67 100644 --- a/theories/Dot/lr/sem_unstamped_typing.v +++ b/theories/Dot/lr/sem_unstamped_typing.v @@ -19,13 +19,13 @@ Section unstamped_judgs. (* Semantic, Unstamped, Expression TyPing *) Definition suetp e_u Γ T : iProp Σ := - |==> ∃ e_s, ⌜ same_skel_tm e_u e_s⌝ ∧ Γ s⊨ e_s : T. + ∃ e_s, ⌜ same_skel_tm e_u e_s⌝ ∧ Γ s⊨ e_s : T. Definition sudstp ds_u Γ T : iProp Σ := - |==> ∃ ds_s, ⌜ same_skel_dms ds_u ds_s⌝ ∧ Γ s⊨ds ds_s : T. + ∃ ds_s, ⌜ same_skel_dms ds_u ds_s⌝ ∧ Γ s⊨ds ds_s : T. Definition sudtp l d_u Γ T : iProp Σ := - |==> ∃ d_s, ⌜ same_skel_dm d_u d_s⌝ ∧ Γ s⊨ { l := d_s } : T. + ∃ d_s, ⌜ same_skel_dm d_u d_s⌝ ∧ Γ s⊨ { l := d_s } : T. Definition iuetp Γ T e := suetp e V⟦Γ⟧* V⟦T⟧. Definition iudstp Γ T ds := sudstp ds V⟦Γ⟧* C⟦T⟧. @@ -76,11 +76,10 @@ Proof. intros e_u' [n Hsteps]%rtc_nsteps_1. apply (soundness (M := iResUR Σ) _ n). apply (bupd_plain_soundness _). - iDestruct (Hwp HdlangG HswapProp) as "#>Hwp". - iDestruct "Hwp" as (e_s Hsim) ">#Hwp". - iSpecialize ("Hwp" $! ids with "[//]"). - rewrite hsubst_id /= (wptp_safe_n n). - iIntros "!>!>"; iDestruct "Hwp" as %Hsafe; iIntros "!%". + iDestruct (Hwp HdlangG HswapProp) as "#>#(%e_s & %Hsim & -#Hwp)". + iSpecialize ("Hwp" $! ids with "[//]"); rewrite hsubst_id /=. + iMod (wptp_safe_n n with "Hwp") as "Hwp". + iIntros "!>!>"; iRevert "Hwp"; iIntros "!% %Hsafe". eapply same_skel_safe_n_impl, Hsteps; naive_solver. Qed. From 78364f61b65e0207ed840f0edc08b227b97f1c45 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Sun, 4 Sep 2022 17:39:50 +0200 Subject: [PATCH 6/7] Persistent updates for gDOT: Update proofs --- theories/Dot/examples/old_fundamental.v | 16 +- theories/Dot/examples/sem/ex_iris_utils.v | 9 +- .../examples/sem/from_pdot_mutual_rec_sem.v | 14 +- .../Dot/examples/sem/no_russell_paradox.v | 12 +- theories/Dot/examples/sem/positive_div.v | 26 ++-- .../Dot/examples/sem/semtyp_lemmas/sub_lr.v | 2 +- theories/Dot/examples/sem/small_sem_ex.v | 4 +- .../sem/syntyp_lemmas/examples_lr_syn.v | 9 +- .../examples/sem/syntyp_lemmas/sub_lr_syn.v | 2 +- theories/Dot/hkdot/hkdot.v | 138 ++++++++++-------- theories/Dot/hkdot/hkdot_syn.v | 10 +- theories/Dot/lr/dot_semtypes.v | 15 +- theories/Dot/lr/sem_unstamped_typing.v | 62 ++++---- theories/Dot/lr/unary_lr.v | 8 +- theories/Dot/semtyp_lemmas/binding_lr.v | 18 +-- theories/Dot/semtyp_lemmas/defs_lr.v | 22 +-- theories/Dot/semtyp_lemmas/dsub_lr.v | 58 ++++---- theories/Dot/semtyp_lemmas/path_repl_lr.v | 28 ++-- theories/Dot/semtyp_lemmas/prims_lr.v | 10 +- theories/Dot/semtyp_lemmas/tproj_lr.v | 26 ++-- theories/Dot/syntyp_lemmas/path_repl_lr_syn.v | 12 +- 21 files changed, 260 insertions(+), 241 deletions(-) diff --git a/theories/Dot/examples/old_fundamental.v b/theories/Dot/examples/old_fundamental.v index 32bde979..b6dce8ec 100644 --- a/theories/Dot/examples/old_fundamental.v +++ b/theories/Dot/examples/old_fundamental.v @@ -24,30 +24,32 @@ Section storeless_unstamped_lemmas. Lemma uT_ISub {Γ e T1 T2 i} : Γ u⊨ e : T1 -∗ Γ ⊨ T1, 0 <: T2, i -∗ Γ u⊨ iterate tskip i e : T2. Proof. - iIntros "#H1 #Hsub"; iMod "H1" as (e1s Hsk1) "H1"; iModIntro. + pupd; iIntros "#(%e1s & %Hsk1 & H1) #Hsub !>". iExists (iterate tskip i e1s); iSplit; last iApply (sT_ISub with "H1 Hsub"). eauto using same_skel_tm_tskips. Qed. Lemma suetp_var Γ x T : - Γ su⊨ tv (ids x) : T ==∗ Γ s⊨ tv (ids x) : T. + Γ su⊨ tv (ids x) : T -∗ Γ s⊨ tv (ids x) : T. Proof. - iIntros "#H1"; iMod "H1" as (e1s Hsk1) "H1". + pupd'. iIntros "#(%e1s & %Hsk1 & #H1) !>". iMod "H1". by rewrite (same_skel_tv_var_tv_var Hsk1). Qed. Lemma suetp_vlit Γ b T : - Γ su⊨ tv (vlit b) : T ==∗ Γ s⊨ tv (vlit b) : T. + Γ su⊨ tv (vlit b) : T -∗ Γ s⊨ tv (vlit b) : T. Proof. - iIntros "#H1"; iMod "H1" as (e1s Hsk1) "H1". + (* pupd'. iIntros "#(%e1s & %Hsk1 & #H1)". iRevert "H1". pupd. + rewrite (same_skel_tv_vlit_tv_vlit Hsk1). iIntros "$". *) + pupd'. iIntros "#(%e1s & %Hsk1 & #H1) !>". iMod "H1". by rewrite (same_skel_tv_vlit_tv_vlit Hsk1). Qed. Lemma uT_All_Ex {Γ e1 x2 T1 T2} : Γ u⊨ e1 : TAll T1 T2 -∗ Γ u⊨ tv (ids x2) : T1 -∗ Γ u⊨ tapp e1 (tv (ids x2)) : T2.|[ids x2/]. Proof. - iIntros "#H1 #H2"; iMod "H1" as (e1s Hsk1) "H1". - iMod (suetp_var with "H2") as "{H2} H2"; iModIntro. + pupd'. iIntros "#(%e1s & %Hsk1 & #H1) #H2 !>". iMod "H1" as "#H1". + iDestruct (suetp_var with "H2") as "{H2} #>#H2". iIntros "!> !>". by iExists (tapp e1s (tv (ids x2))); iSplit; last iApply (T_All_Ex with "H1 H2"). Qed. diff --git a/theories/Dot/examples/sem/ex_iris_utils.v b/theories/Dot/examples/sem/ex_iris_utils.v index 70b3e0bf..6e21ff89 100644 --- a/theories/Dot/examples/sem/ex_iris_utils.v +++ b/theories/Dot/examples/sem/ex_iris_utils.v @@ -40,13 +40,14 @@ Section loop_sem. Context `{HdlangG : !dlangG Σ}. Context `{SwapPropI Σ}. - Lemma loopSemT : ⊢@{iPropI _} |==> WP hclose hloopTm {{ _, False }}. + Lemma loopSemT : ⊢@{iPropI _} WP hclose hloopTm {{ _, False }}. Proof using Type*. - iDestruct (fundamental_typed (loopTyp [])) as "#>H". - iDestruct "H" as (e_s Hsk1) ">H"; iModIntro. + iIntros "!>". + iDestruct (fundamental_typed (loopTyp [])) as "#>#(%e_s & %Hsk1 & #>#H)". + iIntros "!> !>". iSpecialize ("H" $! ids with "[//]"); rewrite hsubst_id. move E: hloopTm => e. - suff ->: e_s = e. { iApply (wp_wand with "H"). iIntros (v). by rw. } + suff ->: e_s = e. { iApply (wp_wand with "H"). iIntros "%v {H}". by rw. } subst; clear -Hsk1. cbv; repeat constrain_bisimulating. Qed. diff --git a/theories/Dot/examples/sem/from_pdot_mutual_rec_sem.v b/theories/Dot/examples/sem/from_pdot_mutual_rec_sem.v index aae3e397..485d85e1 100644 --- a/theories/Dot/examples/sem/from_pdot_mutual_rec_sem.v +++ b/theories/Dot/examples/sem/from_pdot_mutual_rec_sem.v @@ -251,12 +251,14 @@ Tactic Notation "lrSimpl" "in" constr(iSelP) := Lemma newTypeRef_semTyped Γ : ⊢ newTypeRefΓ Γ u⊨ newTypeRefBody : x1 @; "TypeRef". Proof. - iMod (fundamental_typed (Hx0 Γ)) as (x0_s Hsk) ">#Hx0". - iMod (fundamental_subtype (HvT Γ)) as "#HvT". - iMod (fundamental_subtype (HvF Γ)) as "#HvF". - iMod (fundamental_subtype (Hsublast Γ)) as "#Hsub". - iMod loopSemT as "#Hl". - unstamp_goal_tm; iIntros "!> %ρ #Hg". + iIntros "!>". + iDestruct (fundamental_typed (Hx0 Γ)) as "#>#(%x0_s & %Hsk & #>#Hx0)". + iDestruct (fundamental_subtype (HvT Γ)) as "#>#HvT". + iDestruct (fundamental_subtype (HvF Γ)) as "#>#HvF". + iDestruct (fundamental_subtype (Hsublast Γ)) as "#>#Hsub". + iDestruct loopSemT as "#>#Hl". + iIntros "!>". + unstamp_goal_tm. pupd. iIntros "!> %ρ #Hg". iSpecialize ("Hx0" with "Hg"). wp_abind; rewrite -wp_value; iSimpl. diff --git a/theories/Dot/examples/sem/no_russell_paradox.v b/theories/Dot/examples/sem/no_russell_paradox.v index 35b5a7b1..e97947ca 100644 --- a/theories/Dot/examples/sem/no_russell_paradox.v +++ b/theories/Dot/examples/sem/no_russell_paradox.v @@ -21,7 +21,7 @@ Section Russell. *) Definition uAu u := oSel (pv u) "A" anil ids u. - Definition russell_p : envD Σ := λI ρ v, uAu v -∗ False. + Definition russell_p : envD Σ := λI ρ v, □ (uAu v -∗ False). (* This would internalize as [russell_p ρ v := v : μ x. not (x.A)]. *) Context (s : stamp). @@ -58,7 +58,7 @@ Section Russell. iApply ("Hvav" with "HuauV"). Qed. - Lemma uauEquiv : Hs ⊢ ▷ (uAu v -∗ False) ∗-∗ uAu v. + Lemma uauEquiv : Hs ⊢ ▷ □ (uAu v -∗ False) ∗-∗ uAu v. Proof. iIntros "#Hs"; iSplit. - iIntros "#HnotVAV /=". @@ -68,7 +68,7 @@ Section Russell. eauto using objLookupIntro. } + by iApply (dm_to_type_intro with "Hs"). - + iApply "HnotVAV". + + iIntros "!>!>". rewrite /uAu/= path_wp_pv_eq. iApply "HnotVAV". - iIntros "#Hvav". by iDestruct (later_not_UAU with "Hs Hvav") as "#>[]". Qed. @@ -78,10 +78,10 @@ Section Russell. Lemma taut0 (P : Prop) : ((P → False) ↔ P) → False. Proof. tauto. Qed. (** But with later, there's no paradox — we get instead not (not P). *) Lemma irisTaut (P : iProp Σ) : - (▷ (P -∗ False) ∗-∗ P) -∗ (P -∗ False) -∗ False. - Proof using Type*. iIntros "Eq #NP". iApply "NP". by iApply "Eq". Qed. + (▷ □ (P -∗ False) ∗-∗ P) -∗ □ (P -∗ False) -∗ False. + Proof. iIntros "Eq #NP". iApply "NP". by iApply "Eq". Qed. - Lemma notNotVAV : Hs ⊢ (uAu v -∗ False) → False. + Lemma notNotVAV : Hs ⊢ □ (uAu v -∗ False) → False. Proof. iIntros "#Hs #notVAV". iApply (irisTaut (uAu v)) => //. by iApply uauEquiv. diff --git a/theories/Dot/examples/sem/positive_div.v b/theories/Dot/examples/sem/positive_div.v index 9b74cf8c..cc4e7c09 100644 --- a/theories/Dot/examples/sem/positive_div.v +++ b/theories/Dot/examples/sem/positive_div.v @@ -89,18 +89,18 @@ Section helpers. Lemma wp_nge m n (Hnge : ¬ m > n) : ⊢ WP m > n {{ w, w ≡ vbool false }}. Proof. wp_bin. ev; simplify_eq/=. case_decide; by [|lia]. Qed. - Lemma setp_value Γ (T : olty Σ) v : Γ s⊨ v : T ⊣⊢ |==> ∀ ρ, sG⟦ Γ ⟧* ρ → T anil ρ v.[ρ]. + Lemma setp_value Γ (T : olty Σ) v : Γ s⊨ v : T ⊣⊢ ∀ ρ, sG⟦ Γ ⟧* ρ → T anil ρ v.[ρ]. Proof. rewrite /setp/=; properness => //; iSplit; [rewrite wp_value_inv|rewrite -wp_value]; iIntros "#$". Qed. - Lemma setp_value_eq (T : olty Σ) v : (|==> ∀ ρ, T anil ρ v.[ρ]) ⊣⊢ [] s⊨ v : T. + Lemma setp_value_eq (T : olty Σ) v : ( ∀ ρ, T anil ρ v.[ρ]) ⊣⊢ [] s⊨ v : T. Proof. - iSplit. - - iIntros ">#H !>" (? _). + iSplit; pupd. + - iIntros "#H !>" (? _). rewrite /= -wp_value'. iApply "H". - - iIntros "/= >H !>" (ρ). + - iIntros "/= #H !>" (ρ). iSpecialize ("H" $! ρ with "[//]"). by rewrite /= wp_value_inv'. Qed. @@ -117,7 +117,7 @@ Section div_example. Lemma wp_if_ge : ⊢@{iPropI _} |==> ∀ (n : Z), WP hclose (hmkPosBodyV n) {{ w, ⌜ w =@{vl} n ∧ n > 0 ⌝}}. Proof using Type*. - iMod loopSemT as "#Hl"; iIntros "!> %n". + iDestruct loopSemT as "#>#Hl"; iIntros "!> %n". wp_bind (IfCtx _ _). wp_bin; ev; simplify_eq/=. case_decide; wp_pure; first by auto. @@ -127,8 +127,8 @@ Section div_example. Lemma ty_mkPos : ⊢ [] s⊨ hmkPosV : oAll V⟦ 𝐙 ⟧ (olty0 (λI ρ v, ⌜ ∃ n : Z, v = n ∧ n > 0 ⌝)). Proof using Type*. - rewrite -sT_All_I /setp /= /shead; iMod wp_if_ge as "#Hge". - iIntros "!>" (ρ). rewrite /hsubst/hsubst_hoEnvD. rw. + rewrite -sT_All_I /setp /= /shead. iMod wp_if_ge as "#Hge". + pupd; iIntros "!>" (ρ). rewrite /hsubst/hsubst_hoEnvD. rw. iDestruct 1 as %(_ & n & Hw); simplify_eq/=; rewrite Hw. iApply wp_wand; [iApply "Hge" | naive_solver]. Qed. @@ -142,7 +142,7 @@ Section div_example. Close Scope Z_scope. Lemma sStp_ipos_nat Γ i : ⊢ Γ s⊨ ipos <:[ i ] oInt. - Proof. iIntros "!> % _ !%"; rewrite /pos /pure_interp_prim; naive_solver. Qed. + Proof. pupd; iIntros "!> % _ !%"; rewrite /pos /pure_interp_prim; naive_solver. Qed. Lemma posTMem_widen Γ l i : ⊢ Γ s⊨ oTMemL l ipos ipos <:[ i ] oTMemL l ⊥ oInt. Proof using Type*. @@ -184,8 +184,8 @@ Section div_example. iApply suD_Cons; [done|iApply suD_posDm_ipos|]. iApply suD_Cons; [done| iApply suD_Val|iApply suD_Sing; iApply suD_Val]; iApply (suT_All_I_Strong _ _ _ HctxSub). - - unstamp_goal_tm; iMod wp_if_ge as "#Hge". - iIntros "!> %ρ [[_ [#Hpos _]] %Hnpos]"; lazy in Hnpos. + - pupd; unstamp_goal_tm; iMod wp_if_ge as "#Hge". + pupd; iIntros "!> %ρ [[_ [#Hpos _]] %Hnpos]"; lazy in Hnpos. case: Hnpos => [n Hw]. iApply wp_wand; [rewrite /= {}Hw; iApply "Hge" | iIntros (v [-> Hnpos])]. @@ -193,8 +193,8 @@ Section div_example. iApply (vl_sel_lb with "[] Hpos"). iIntros "!%"; hnf. naive_solver. - iApply suT_All_I. - unstamp_goal_tm. - iIntros "!> %ρ #[[[_ [Hpos _]] %Hw] Harg]". + pupd; unstamp_goal_tm. + pupd; iIntros "!> %ρ #[[[_ [Hpos _]] %Hw] Harg]". rewrite /shead /stail. iSimpl. destruct Hw as [m ->]. setoid_rewrite path_wp_pv_eq. diff --git a/theories/Dot/examples/sem/semtyp_lemmas/sub_lr.v b/theories/Dot/examples/sem/semtyp_lemmas/sub_lr.v index 1bc4a24a..af64290c 100644 --- a/theories/Dot/examples/sem/semtyp_lemmas/sub_lr.v +++ b/theories/Dot/examples/sem/semtyp_lemmas/sub_lr.v @@ -71,7 +71,7 @@ Section StpLemmas. (*───────────────────────────────*) Γ s⊨p p : T2, i + j. Proof. - iIntros ">#HpT1 >#Hsub !> %ρ #Hg". + pupd; iIntros "#HpT1 #Hsub !> %ρ #Hg". iSpecialize ("HpT1" with "Hg"). rewrite !path_wp_eq. iDestruct "HpT1" as (v) "Hpv"; iExists v. diff --git a/theories/Dot/examples/sem/small_sem_ex.v b/theories/Dot/examples/sem/small_sem_ex.v index eedd3e24..9a37a93d 100644 --- a/theories/Dot/examples/sem/small_sem_ex.v +++ b/theories/Dot/examples/sem/small_sem_ex.v @@ -60,8 +60,8 @@ Section small_ex. iApply suD_Cons; [done| by iApply suD_posDm_ipos | ]. iApply suD_Sing; iApply suD_Val. iApply (suT_Sub (T1 := ipos)). - unstamp_goal_tm. - by rewrite setp_value /ipos /pos; iIntros "!> %ρ _ /= !%"; naive_solver. + pupd; unstamp_goal_tm. + rewrite setp_value /ipos /pos; pupd; iIntros "!> %ρ _ /= !%"; naive_solver. iApply sStp_Trans; first iApply sStp_Add_Later. iApply sStp_Trans; first iApply sStp_Add_Later. iApply sLater_Stp_Eq. diff --git a/theories/Dot/examples/sem/syntyp_lemmas/examples_lr_syn.v b/theories/Dot/examples/sem/syntyp_lemmas/examples_lr_syn.v index 326e96a2..ba143cf3 100644 --- a/theories/Dot/examples/sem/syntyp_lemmas/examples_lr_syn.v +++ b/theories/Dot/examples/sem/syntyp_lemmas/examples_lr_syn.v @@ -42,7 +42,7 @@ Section Lemmas. (* We're stuck again! *) Fail iApply "Hsub". Restart. *) - rw. iIntros ">#Hsub >#Hp !> %ρ %v #Hg Heq". + rw. pupd. iIntros "#Hsub #Hp !> %ρ %v #Hg Heq". iSpecialize ("Hp" with "Hg"). iAssert (▷^i ⟦ T1 ⟧ (v .: ρ) v)%I as "#HT1". by iNext i; iDestruct "Heq" as %Heq; @@ -58,7 +58,7 @@ Section Lemmas. Γ ⊨p p : TMu T1, i -∗ Γ ⊨ TSing p, i <: TMu T2, i. Proof. - rw. iIntros ">#Hsub >#Hp !> %ρ %v #Hg /= Heq"; iSpecialize ("Hp" with "Hg"). + rw. pupd. iIntros "#Hsub #Hp !> %ρ %v #Hg /= Heq"; iSpecialize ("Hp" with "Hg"). iSpecialize ("Hsub" $! ρ v with "[#$Hg] [#]"); iNext i; iDestruct "Heq" as %Heq; rewrite -(psubst_one_repl Hrepl1, psubst_one_repl Hrepl2) // @@ -99,10 +99,11 @@ Section Lemmas. Proof. rw. rewrite interp_commute_subst. apply sT_Mu_E. Qed. Lemma suetp_var_lift1 {Γ} x T1 T2 : - (Γ s⊨ tv (ids x) : T1 -∗ Γ s⊨ tv (ids x) : T2) ⊢ + □(Γ s⊨ tv (ids x) : T1 -∗ Γ s⊨ tv (ids x) : T2) ⊢ Γ su⊨ tv (ids x) : T1 -∗ Γ su⊨ tv (ids x) : T2. Proof. - iIntros "#Hr #H1"; iMod (suetp_var with "H1") as "{H1} H1"; iModIntro. + iIntros "#Hr". + rewrite suetp_var. pupd; iIntros "#H1 !>". by iExists (tv (ids x)); iSplit; last iApply ("Hr" with "H1"). Qed. diff --git a/theories/Dot/examples/sem/syntyp_lemmas/sub_lr_syn.v b/theories/Dot/examples/sem/syntyp_lemmas/sub_lr_syn.v index e4be555a..7dd98b8a 100644 --- a/theories/Dot/examples/sem/syntyp_lemmas/sub_lr_syn.v +++ b/theories/Dot/examples/sem/syntyp_lemmas/sub_lr_syn.v @@ -22,6 +22,6 @@ Section judgment_lemmas. (** ** Show this typing judgment is equivalent to the more direct definition. *) Lemma istpi_eq Γ T1 i T2 j : Γ ⊨ T1, i <: T2, j ⊣⊢ - |==> ∀ ρ v, G⟦Γ⟧ ρ → ▷^i V⟦T1⟧ anil ρ v → ▷^j V⟦T2⟧ anil ρ v. + ∀ ρ v, G⟦Γ⟧ ρ → ▷^i V⟦T1⟧ anil ρ v → ▷^j V⟦T2⟧ anil ρ v. Proof. reflexivity. Qed. End judgment_lemmas. diff --git a/theories/Dot/hkdot/hkdot.v b/theories/Dot/hkdot/hkdot.v index a5b40277..2248c28a 100644 --- a/theories/Dot/hkdot/hkdot.v +++ b/theories/Dot/hkdot/hkdot.v @@ -71,7 +71,7 @@ Section gen_lemmas. Lemma sstpiK_mono_ctx i Γ {T1 U1 T2 U2 : olty Σ} (K1 K2 : sf_kind Σ) (Hsub : ⊢ ∀ ρ, sG⟦Γ⟧*ρ → sstpiK_env i T1 U1 K1 ρ -∗ sstpiK_env i T2 U2 K2 ρ) : Γ s⊨ T1 <:[ i ] U1 ∷ K1 ⊢ Γ s⊨ T2 <:[ i ] U2 ∷ K2. - Proof. iIntros ">#HT !>" (ρ) "#Hg /=". iApply (Hsub with "Hg (HT Hg)"). Qed. + Proof. pupd; iIntros "#HT !>" (ρ) "#Hg /=". iApply (Hsub with "Hg (HT Hg)"). Qed. #[global] Instance sSkd_proper i : Proper3 (sSkd (Σ := Σ) i). @@ -84,7 +84,7 @@ Section gen_lemmas. Γ s⊨ T1 <:[ i ] T2 ∷ K -∗ S :: Γ s⊨ oShift T1 <:[ i ] oShift T2 ∷ kShift K. Proof. - iIntros ">#HK !> %ρ /= #[Hg _]". + pupd; iIntros "#HK !> %ρ /= #[Hg _]". by iApply (sf_kind_proper with "(HK Hg)"). Qed. @@ -102,7 +102,7 @@ Section gen_lemmas. Γ s⊨ K1 <∷[ i ] K2 -∗ S :: Γ s⊨ kShift K1 <∷[ i ] kShift K2. Proof. - iIntros ">#HK !> %ρ /= #[Hg _] *". + pupd; iIntros "#HK !> %ρ /= #[Hg _] *". iApply ("HK" with "Hg"). Qed. @@ -111,7 +111,7 @@ Section gen_lemmas. S1 :: Γ s⊨ T <:[ i ] U ∷ K -∗ S2 :: Γ s⊨ T <:[ i ] U ∷ K. Proof. - iIntros ">#HsubS >#HJ !> %ρ /= #[Hg HS]". + pupd; iIntros "#HsubS #HJ !> %ρ /= #[Hg HS]". iApply ("HJ" $! ρ with "[$Hg]"). iApply ("HsubS" $! ρ with "[$Hg $HS] HS"). Qed. @@ -135,7 +135,7 @@ Section gen_lemmas. S1 :: Γ s⊨ K1 <∷[ i ] K2 -∗ S2 :: Γ s⊨ K1 <∷[ i ] K2. Proof. - iIntros ">#HsubS >#HJ !> %ρ /= #[Hg HS] *". + pupd; iIntros "#HsubS #HJ !> %ρ /= #[Hg HS] *". iApply ("HJ" $! ρ with "[$Hg]"). iApply ("HsubS" $! ρ with "[$Hg $HS] HS"). Qed. @@ -158,20 +158,21 @@ Section gen_lemmas. ∀ ρ, sG⟦ Γ ⟧* ρ → ▷^i (oClose T1 ρ ⊆ oClose T2 ρ). Proof. iSplit. - - iIntros "#Hsub %ρ Hg". - iDestruct (sf_star_eq with "(Hsub Hg)") as "{Hsub} Hsub". - by iApply "Hsub". - - iIntros "#Hsub %ρ #Hg"; rewrite sf_star_eq /=. - iApply ("Hsub" with "Hg"). + - iIntros "#Hsub %ρ #Hg". + iDestruct (sf_star_eq with "(Hsub Hg)") as "{Hsub Hg} #Hsub". + iIntros "!>". iApply "Hsub". + - iIntros "#Hsub %ρ #Hg". rewrite sf_star_eq /=. + iSpecialize ("Hsub" with "Hg"). + by iNext. Qed. Lemma ksubtyping_equiv i Γ T1 T2 : Γ s⊨ T1 <:[ i ] T2 ∷ sf_star ⊣⊢ - |==> ∀ ρ, sG⟦ Γ ⟧* ρ → ▷^i (oClose T1 ρ ⊆ oClose T2 ρ). - Proof. rewrite /sstpiK; f_equiv. apply ksubtyping_equiv'. Qed. + ∀ ρ, sG⟦ Γ ⟧* ρ → ▷^i (oClose T1 ρ ⊆ oClose T2 ρ). + Proof. by rewrite /sstpiK ksubtyping_equiv'. Qed. Lemma ksubtyping_spec ρ i Γ T1 T2 : - sstpiK' i Γ T1 T2 sf_star -∗ + □ sstpiK' i Γ T1 T2 sf_star -∗ sG⟦ Γ ⟧* ρ -∗ ▷^i (oClose T1 ρ ⊆ oClose T2 ρ). Proof. @@ -179,29 +180,31 @@ Section gen_lemmas. Qed. Lemma ksubtyping_intro i Γ (T1 T2 : oltyO Σ) : - (|==> ∀ ρ, sG⟦ Γ ⟧* ρ → + ( ∀ ρ, sG⟦ Γ ⟧* ρ → ∀ v, ▷^i (oClose T1 ρ v → oClose T2 ρ v)) -∗ Γ s⊨ T1 <:[ i ] T2 ∷ sf_star. Proof. - apply equiv_entails_1_1. rewrite ksubtyping_equiv; properness; first done. + apply equiv_entails_1_1. + rewrite ksubtyping_equiv; properness; first done. by rewrite -laterN_forall. Qed. Lemma ksubtyping_intro_swap i Γ (T1 T2 : oltyO Σ) : - (|==> ∀ ρ, sG⟦ Γ ⟧* ρ → + ( ∀ ρ, sG⟦ Γ ⟧* ρ → ∀ v, ▷^i oClose T1 ρ v → ▷^i oClose T2 ρ v) -∗ Γ s⊨ T1 <:[ i ] T2 ∷ sf_star. Proof using HswapProp. - rewrite -ksubtyping_intro; iIntros ">#Hsub !> %ρ #Hg *". + rewrite -ksubtyping_intro; pupd; iIntros "#Hsub !> %ρ #Hg *". iApply (impl_laterN with "(Hsub Hg)"). Qed. Lemma kinding_intro Γ i (L T U : oltyO Σ) : - (|==> ∀ ρ, sG⟦ Γ ⟧* ρ → + ( ∀ ρ, sG⟦ Γ ⟧* ρ → ▷^i (oClose L ρ ⊆ oClose T ρ ⊆ oClose U ρ)) -∗ Γ s⊨ T ∷[ i ] sf_kintv L U. Proof. - iIntros ">#Hsub !>" (ρ); rewrite /= sr_kintv_refl /=. iApply "Hsub". + pupd; iIntros "#Hsub !> %ρ #Hg". rewrite /= sr_kintv_refl /=. + by iSpecialize ("Hsub" with "Hg"); iNext. Qed. (** * Prefixes: K for Kinding, KStp for kinded subtyping, Skd for subkinding. *) @@ -209,14 +212,14 @@ Section gen_lemmas. Lemma sK_Sing Γ (T : oltyO Σ) i : ⊢ Γ s⊨ T ∷[ i ] sf_sngl T. Proof. - rewrite -kinding_intro; iIntros "!> %ρ _". by rewrite -subtype_refl. + rewrite -kinding_intro; pupd; iIntros "!> %ρ _". by rewrite -subtype_refl. Qed. Lemma sKStp_Intv Γ (T1 T2 L U : oltyO Σ) i : Γ s⊨ T1 <:[i] T2 ∷ sf_kintv L U -∗ Γ s⊨ T1 <:[i] T2 ∷ sf_kintv T1 T2. Proof. - iIntros ">#Hs !> %ρ Hg"; iDestruct ("Hs" with "Hg") as "{Hs} (_ & #H & _)". + pupd; iIntros "#Hs !> %ρ Hg"; iDestruct ("Hs" with "Hg") as "{Hs} (_ & #H & _)". rewrite /= /sr_kintv; iNext i. iDestruct "H" as "#$". by rewrite -!subtype_refl. Qed. @@ -224,7 +227,7 @@ Section gen_lemmas. Lemma sK_Star Γ (T : oltyO Σ) i : ⊢ Γ s⊨ T ∷[ i ] sf_star. Proof. - rewrite -kinding_intro; iIntros "!> %ρ _ !>". + rewrite -kinding_intro; pupd; iIntros "!> %ρ _ !>". by iSplit; iIntros "%v /="; [iIntros "[]"|iIntros "_"]. Qed. @@ -234,7 +237,7 @@ Section gen_lemmas. Γ s⊨ K1 <∷[ i ] K2 -∗ Γ s⊨ T1 <:[ i ] T2 ∷ K2. Proof. - iIntros ">#H1 >#Hsub !> %ρ #Hg". iApply ("Hsub" with "Hg (H1 Hg)"). + pupd; iIntros "#H1 #Hsub !> %ρ #Hg". iApply ("Hsub" with "Hg (H1 Hg)"). Qed. (** Kind subsumption (for kinding). *) @@ -253,7 +256,7 @@ Section gen_lemmas. oLaterN i (oShift S) :: Γ s⊨ T1 <:[i] T2 ∷ K -∗ Γ s⊨ oLam T1 <:[i] oLam T2 ∷ sf_kpi S K. Proof using HswapProp. - iIntros ">#HTK !> %ρ #Hg * /=" (arg). + pupd; iIntros "#HTK !> %ρ #Hg * /=" (arg). rewrite -impl_laterN. iIntros "Hs". iSpecialize ("HTK" $! (arg .: ρ) with "[$Hg $Hs]"). @@ -271,7 +274,7 @@ Section gen_lemmas. Γ s⊨ U1 <:[ i ] U2 ∷ sf_star -∗ Γ s⊨ sf_kintv L1 U1 <∷[ i ] sf_kintv L2 U2. Proof. - iIntros ">#HsubL >#HsubU !> %ρ #Hg /=" (T1 T2). + pupd; iIntros "#HsubL #HsubU !> %ρ #Hg /=" (T1 T2). iPoseProof (ksubtyping_spec with "HsubL Hg") as "{HsubL} HsubL". iPoseProof (ksubtyping_spec with "HsubU Hg") as "{HsubU Hg} HsubU". iNext i; iIntros "#(HsubL1 & $ & HsubU1)"; iSplit. @@ -284,17 +287,17 @@ Section gen_lemmas. oLaterN i (oShift S2) :: Γ s⊨ K1 <∷[ i ] K2 -∗ Γ s⊨ sf_kpi S1 K1 <∷[ i ] sf_kpi S2 K2. Proof using HswapProp. - iIntros ">#HsubS >#HsubK !> %ρ #Hg /=". + pupd; iIntros "#HsubS #HsubK !> %ρ #Hg /=". iPoseProof (ksubtyping_spec with "HsubS Hg") as "{HsubS} HsubS". - iAssert (∀ arg : vl, let ρ' := arg .: ρ in + iAssert ( □∀ arg : vl, let ρ' := arg .: ρ in ▷^i (oClose S2 ρ arg → ∀ T1 T2 : hoLtyO Σ, K1 ρ' T1 T2 → K2 ρ' T1 T2))%I as "{HsubK} #HsubK". { - iIntros "%arg"; rewrite -mlaterN_impl. + iIntros "%arg !>"; rewrite -mlaterN_impl. iIntros "#HS2 %T1 %T2"; rewrite -mlaterN_impl; iIntros "HK1". iApply ("HsubK" $! (arg .: ρ) with "[$Hg $HS2] HK1"). } - iIntros (T1 T2); iNext i; iIntros "#HTK1 * #HS". + iIntros (T1 T2); iNext i. iIntros "#HTK1 * #HS". iSpecialize ("HsubK" $! arg with "HS"). iApply ("HsubK" with "(HTK1 (HsubS HS))"). Qed. @@ -303,14 +306,14 @@ Section gen_lemmas. prove them anyway, to show they hold regardless of extensions. *) Lemma sSkd_Refl Γ i (K : sf_kind Σ) : ⊢ Γ s⊨ K <∷[ i ] K. - Proof. iIntros "!> %ρ Hg * !> $". Qed. + Proof. pupd; iIntros "!> %ρ Hg * !> $". Qed. Lemma sSkd_Trans Γ i (K1 K2 K3 : sf_kind Σ) : Γ s⊨ K1 <∷[ i ] K2 -∗ Γ s⊨ K2 <∷[ i ] K3 -∗ Γ s⊨ K1 <∷[ i ] K3. Proof. - iIntros ">#Hs1 >#Hs2 !> %ρ #Hg *". + pupd; iIntros "#Hs1 #Hs2 !> %ρ #Hg *". iSpecialize ("Hs1" with "Hg"); iSpecialize ("Hs2" with "Hg"); iNext i. iIntros "{Hg} HK1". iApply ("Hs2" with "(Hs1 HK1)"). Qed. @@ -337,7 +340,7 @@ Section gen_lemmas. (HU : ∀ arg args ρ, envApply U2 ρ (acons arg args) ≡ envApply U1 ρ (acons arg args)) : Γ s⊨ T1 <:[ i ] U1 ∷ sf_kpi S K ⊢ Γ s⊨ T2 <:[ i ] U2 ∷ sf_kpi S K. Proof. - apply sstpiK_mono_ctx; iIntros "%ρ Hg HK"; iNext i; iIntros "%arg #HS". + apply sstpiK_mono_ctx; iIntros "%ρ #Hg #HK"; iNext i; iIntros "%arg #HS". by iApply (sf_kind_proper with "(HK HS)") => args; rewrite /acurry. Qed. @@ -383,7 +386,7 @@ Section gen_lemmas. Γ s⊨ T2 <:[ i ] T3 ∷ K -∗ Γ s⊨ T1 <:[ i ] T3 ∷ K. Proof. - iIntros ">#Hs1 >#Hs2 !> %ρ #Hg". + pupd; iIntros "#Hs1 #Hs2 !> %ρ #Hg". iApply (sf_kind_sub_trans with "(Hs1 Hg) (Hs2 Hg)"). Qed. @@ -392,17 +395,17 @@ Section gen_lemmas. Lemma sKStp_Top Γ (T : oltyO Σ) i : ⊢ Γ s⊨ T <:[ i ] ⊤ ∷ sf_star. - Proof. rewrite -ksubtyping_intro. iIntros "!> %ρ * _ * !> _ //". Qed. + Proof. rewrite -ksubtyping_intro. pupd; iIntros "!> %ρ * _ * !> _ //". Qed. Lemma sKStp_Bot Γ (T : oltyO Σ) i : ⊢ Γ s⊨ ⊥ <:[ i ] T ∷ sf_star. - Proof. rewrite -ksubtyping_intro; iIntros "!> %ρ * _ * !> []". Qed. + Proof. rewrite -ksubtyping_intro; pupd; iIntros "!> %ρ * _ * !> []". Qed. (* XXX <:-..-U *) Lemma sKStp_IntvU {Γ T1 T2 L U i} : Γ s⊨ T1 <:[i] T2 ∷ sf_kintv L U -∗ Γ s⊨ T2 <:[i] U ∷ sf_star. Proof. - rewrite -ksubtyping_intro; iIntros ">#HK !> * Hg *". + rewrite -ksubtyping_intro; pupd; iIntros "#HK !> * Hg *". iDestruct ("HK" with "Hg") as "[_ [_ Hsub]]". iNext i; iApply "Hsub". Qed. @@ -418,7 +421,7 @@ Section gen_lemmas. Γ s⊨ T1 <:[i] T2 ∷ sf_kintv L U -∗ Γ s⊨ L <:[i] T1 ∷ sf_star. Proof. - rewrite -ksubtyping_intro; iIntros ">#HK !> * Hg *". + rewrite -ksubtyping_intro; pupd; iIntros "#HK !> * Hg *". iDestruct ("HK" with "Hg") as "[Hsub _]". iNext i; iApply "Hsub". Qed. @@ -464,7 +467,7 @@ Section dot_types. oLaterN i T :: Γ s⊨p p : U, i -∗ Γ s⊨p p.|[v/] : U.|[v/], i. Proof. - iIntros ">#Hrepl >#H !>" (ρ) "#Hg /=". + pupd; iIntros "#Hrepl #H !>" (ρ) "#Hg /=". iSpecialize ("Hrepl" with "Hg"); rewrite path_wp_pv_eq. rewrite hsubst_comp -subst_swap_base. iSpecialize ("H" $! (v.[ρ] .: ρ) with "[$Hg $Hrepl]"). @@ -479,7 +482,7 @@ Section dot_types. oLaterN i V :: Γ s⊨ T1 <:[ i ] T2 ∷ K -∗ Γ s⊨ T1.|[v/] <:[ i ] T2.|[v/] ∷ K.|[v/]. Proof. - iIntros ">#Hrepl >#H !>" (ρ) "#Hg /=". + pupd; iIntros "#Hrepl #H !>" (ρ) "#Hg /=". iSpecialize ("Hrepl" with "Hg"); rewrite path_wp_pv_eq -subst_swap_base. iSpecialize ("H" $! (v.[ρ] .: ρ) with "[$Hg $Hrepl]"). iApply (sf_kind_proper with "H") => args w /=; @@ -491,7 +494,7 @@ Section dot_types. Γ s⊨p p : S, i -∗ Γ s⊨ oTApp T1 p <:[i] oTApp T2 p ∷ kpSubstOne p K. Proof. - iIntros ">#HTK >#Hp !> %ρ #Hg". + pupd; iIntros "#HTK #Hp !> %ρ #Hg". iApply (strong_path_wp_wand with "(Hp Hg)"). iIntros (v Hal%alias_paths_pv_eq_1) "{Hp} #Hv". iApply (sf_kind_proper with "(HTK Hg Hv)") => args w /=; @@ -510,9 +513,10 @@ Section dot_types. Γ s⊨p pv v : S, i -∗ Γ s⊨ oTAppV T1 v <:[i] oTAppV T2 v ∷ K.|[v/]. Proof. - rewrite -!oTApp_pv; iIntros "#HTK #Hv". - iPoseProof (sKStp_App with "HTK Hv") as ">Happ". - iIntros "!> %ρ #Hg"; rewrite kpSubstOne_eq. + rewrite -!oTApp_pv. + pupd'; iIntros "#HTK #Hv !>". + iPoseProof (sKStp_App with "HTK Hv") as "#>#Happ". + iIntros "!>!> %ρ #Hg"; rewrite kpSubstOne_eq. iApply ("Happ" with "Hg"). Qed. @@ -531,8 +535,10 @@ Section dot_types. oLaterN i (oShift S) :: Γ s⊨ T ∷[i] K -∗ Γ s⊨ oTApp (oLam T) p =[i] T .sTp[ p /] ∷ kpSubstOne p K. Proof using HswapProp. - iIntros "#Hp #HK"; iApply sKEq_Refl. apply sTEq_Beta. - rewrite sK_Lam. iApply (sK_App with "HK Hp"). + iIntros "#Hp #HK". iApply sKEq_Refl. apply sTEq_Beta. + (* rewrite sK_Lam. *) + iDestruct (sK_Lam with "HK") as "{HK}#HK". + iApply (sK_App with "HK Hp"). Qed. Lemma sKEq_BetaV Γ S T (K : sf_kind Σ) i v : @@ -544,14 +550,17 @@ Section dot_types. (* rewrite -oTApp_pv -opSubst_pv_eq kpSubstOne_eq. apply sKEq_Beta. *) iIntros "#Hv #HK"; iApply sKEq_Refl. apply sTEq_BetaV. - rewrite sK_Lam; iApply (sK_AppV with "HK Hv"). + (* rewrite sK_Lam. *) + iDestruct (sK_Lam with "HK") as "{HK}#HK". + + iApply (sK_AppV with "HK Hv"). Qed. Lemma sstpiK_star_to_sstp Γ i T1 T2 : Γ s⊨ T1 <:[ i ] T2 ∷ sf_star ⊢ Γ s⊨ T1 , i <: T2 , i. Proof. - iIntros ">#Hsub !> %ρ %v #Hg". + pupd; iIntros "#Hsub !> %ρ %v #Hg". iDestruct (ksubtyping_spec with "Hsub Hg") as "{Hsub Hg} Hsub". rewrite -laterN_impl. iNext i. iApply ("Hsub" $! v). Qed. @@ -560,7 +569,7 @@ Section dot_types. Γ s⊨ T1 <:[ i ] T2 ∷ sf_star ⊣⊢ Γ s⊨ T1 , i <: T2 , i. Proof using HswapProp. iSplit; first iApply sstpiK_star_to_sstp. - rewrite -ksubtyping_intro_swap /=. iIntros ">#Hsub !> %ρ Hg *". + rewrite -ksubtyping_intro_swap /=. pupd; iIntros "#Hsub !> %ρ Hg *". iApply ("Hsub" with "Hg"). Qed. @@ -573,7 +582,7 @@ Section dot_types. Γ s⊨ K1 <∷[ i ] K2 -∗ Γ s⊨ oTMemK l K1 <:[ i ] oTMemK l K2 ∷ sf_star. Proof. - rewrite -ksubtyping_intro; iIntros ">#HK !> %ρ Hg *". + rewrite -ksubtyping_intro; pupd; iIntros "#HK !> %ρ Hg *". iSpecialize ("HK" with "Hg"); iNext i. iDestruct 1 as (d Hld) "Hφ"; iExists d; iFrame (Hld). iDestruct "Hφ" as (φ) "[Hlφ #HK1]"; iExists φ; iFrame "Hlφ". @@ -583,7 +592,7 @@ Section dot_types. Lemma sKStp_TMem_AnyKind Γ l (K : sf_kind Σ) i : ⊢ Γ s⊨ oTMemK l K <:[ i ] oTMemAnyKind l ∷ sf_star. Proof. - rewrite -ksubtyping_intro; iIntros "!> %ρ #Hg * !>". + rewrite -ksubtyping_intro; pupd; iIntros "!> %ρ #Hg * !>". iDestruct 1 as (d Hl φ) "[Hl _]". iExists d; iFrame (Hl); iExists φ; iFrame "Hl". Qed. @@ -604,11 +613,12 @@ Section dot_types. s ↝[ σ ] T -∗ Γ s⊨ { l := dtysem σ s } : cTMemK l K. Proof. - rewrite sdtp_eq'; iIntros ">#HTK"; iDestruct 1 as (φ Hγφ) "#Hγ". - iIntros "!>" (ρ Hpid) "Hg"; iExists (hoEnvD_inst (σ.|[ρ]) φ). + rewrite sdtp_eq'. iIntros "#HTK (%φ & %Hγφ & #Hγ) !>". + iMod "HTK" as "#HTK". + iIntros "!>!>" (ρ Hpid) "Hg"; iExists (hoEnvD_inst (σ.|[ρ]) φ). iDestruct (dm_to_type_intro with "Hγ") as "-#$"; first done. iApply (sf_kind_proper' with "(HTK Hg)") => args v /=. - f_equiv; symmetry; exact: Hγφ. + do 1!f_equiv; symmetry. exact: Hγφ. Qed. Lemma oSel_equiv_intro ρ p v l d1 ψ1 @@ -616,7 +626,7 @@ Section dot_types. (Hl1 : v ,, l ↘ d1) : d1 ↗ ψ1 ⊢ hoLty_equiv (packHoLtyO ψ1) (envApply (oSel p l) ρ). Proof. - iIntros "#Hl1" (args w). + iIntros "#Hl1 %args %w". rewrite /= alias_paths_elim_eq // path_wp_pv_eq. iSplit; first by iIntros "H"; iExists d1, ψ1; iFrame (Hl1) "Hl1". iDestruct 1 as (d2 ψ2 Hl2) "[Hl2 Hw]"; objLookupDet. @@ -628,7 +638,7 @@ Section dot_types. Γ s⊨p p : oTMemK l K, i -∗ Γ s⊨ oSel p l ∷[i] K. Proof. - iIntros ">#Hp !> %ρ Hg"; iSpecialize ("Hp" with "Hg"); iNext i. + pupd; iIntros "#Hp !> %ρ Hg"; iSpecialize ("Hp" with "Hg"); iNext i. rewrite path_wp_eq. iDestruct "Hp" as (v Hal%alias_paths_pv_eq_1 d1 Hl1 ψ1) "[#Hl1 HK]". iApply (sfkind_respects with "[] HK"). @@ -641,7 +651,7 @@ Section dot_types. Γ s⊨ T1 ∷[i] K -∗ Γ s⊨ T1 <:[i] T2 ∷ K. Proof. - iIntros ">#Hrepl >#Hal >#HK !> %ρ #Hg". + pupd; iIntros "#Hrepl #Hal #HK !> %ρ #Hg". iSpecialize ("Hal" with "Hg"); iSpecialize ("HK" with "Hg"); iNext i. iDestruct "Hal" as %Hal%alias_paths_simpl. iApply (sf_kind_sub_internal_proper with "[] [] HK"). @@ -656,7 +666,7 @@ Section dot_types. Γ s⊨ T1 <:[i] T2 ∷ K1 -∗ Γ s⊨ T1 <:[i] T2 ∷ K2. Proof. - iIntros ">#Hrepl >#Hal >#HK !> %ρ #Hg". + pupd; iIntros "#Hrepl #Hal #HK !> %ρ #Hg". iSpecialize ("Hal" with "Hg"); iSpecialize ("HK" with "Hg"). iNext i. iDestruct "Hal" as %Hal%alias_paths_simpl. iSpecialize ("Hrepl" $! _ _ _ Hal). @@ -945,8 +955,11 @@ Section dot_experimental_kinds. (* This goal is false if T uses singleton types — say T = λ x. x.type, that is, [oLam (oSing (pv (ids 0)))]. *) Proof. - rewrite /sstpiK. - iIntros "/= >#HT [>#Hsub1 >#Hsub2] !> %ρ #Hg"; iSpecialize ("HT" with "Hg"); + rewrite /sstpiK/=. + (* TODO workaround [pupd] limitation *) + iIntros "A [B C]"; iRevert "A B C"; pupd. + iIntros "#HT #Hsub1 #Hsub2 !> %ρ #Hg". + iSpecialize ("HT" with "Hg"); iSpecialize ("Hsub1" with "Hg"); iSpecialize ("Hsub2" with "Hg"); iNext i. rewrite /sr_kintv/=. @@ -1018,13 +1031,14 @@ Section dot_experimental_kinds. So if [T <: { A :: L .. U }] and [isSing T], then we can't conclude [▷ U <: T#A]; but if T is an actual singleton, we can. *) - Definition isSing (T : lty Σ) := (∀ v1 v2, T v1 → T v2 → ⌜ v1 = v2 ⌝)%I. + Definition isSing (T : lty Σ) : iProp Σ := + □ ∀ v1 v2, T v1 → T v2 → ⌜ v1 = v2 ⌝. Lemma isSing_respects_hoLty_equiv {T1 T2 : hoLtyO Σ} args : - hoLty_equiv T1 T2 -∗ isSing (T1 args) -∗ isSing (T2 args). + □ hoLty_equiv T1 T2 -∗ isSing (T1 args) -∗ isSing (T2 args). Proof using Type*. rewrite /isSing /=. - iIntros "#Heq #HS /= %v1 %v2 #H1 #H2". + iIntros "#Heq #HS /= !> %v1 %v2 #H1 #H2". iApply ("HS" with "(Heq H1) (Heq H2)"). Qed. diff --git a/theories/Dot/hkdot/hkdot_syn.v b/theories/Dot/hkdot/hkdot_syn.v index f418db3e..6a7adc64 100644 --- a/theories/Dot/hkdot/hkdot_syn.v +++ b/theories/Dot/hkdot/hkdot_syn.v @@ -38,10 +38,12 @@ Section lemmas. Γ s⊨ oLater V⟦ T ⟧ ∷[ 0 ] K -∗ Γ s⊨ { l := dtysyn T } : cTMemK l K. Proof. - rewrite sdtp_eq'. iIntros ">#HTK !>" (ρ Hpid) "Hg /=". + rewrite sdtp_eq'. pupd; iIntros "#HTK !>" (ρ Hpid) "Hg /=". iExists (λ args, V⟦ T ⟧ args ρ). iDestruct (dm_to_type_syn_intro') as "-#$"; first done. - iApply ("HTK" with "Hg"). + iApply (sfkind_respects with "[] (HTK Hg)"). + iIntros "%%". + by iSplit; iIntros "$". Qed. Lemma sD_Typ_Syn {l Γ T} : @@ -55,7 +57,7 @@ Section lemmas. Lemma suD_Typ_Syn {l Γ T} : ⊢ Γ su⊨ { l := dtysyn T } : cTMem l (oLater V⟦ T ⟧) (oLater V⟦ T ⟧). Proof. - iModIntro. iExists (dtysyn T); iSplit; first done. iApply sD_Typ_Syn. + pupd; iModIntro. iExists (dtysyn T); iSplit; first done. iApply sD_Typ_Syn. Qed. (* This is a decent warmup, but TODO: example type application! *) @@ -67,6 +69,8 @@ Section lemmas. apply sD_TypK_Abs_Syn. Qed. + #[local] Notation IntoPersistent' P := (IntoPersistent false P P). + #[global] Instance sstpiK_persistent i Γ T1 T2 K : IntoPersistent' (sstpiK i Γ T1 T2 K) := _. Lemma sT_New_Singl_Syn n Γ l (K : s_kind Σ n) T : oLater (oTMemK l (s_to_sf (ho_sing K (oLater V⟦T⟧)))) :: Γ s⊨ oLater V⟦T⟧ ∷[ 0 ] s_to_sf K -∗ Γ s⊨ vobj [ (l, dtysyn T) ] : oMu (oTMemK l (s_to_sf K)). diff --git a/theories/Dot/lr/dot_semtypes.v b/theories/Dot/lr/dot_semtypes.v index ce6d16ec..580a76fd 100644 --- a/theories/Dot/lr/dot_semtypes.v +++ b/theories/Dot/lr/dot_semtypes.v @@ -64,15 +64,15 @@ Section JudgEqs. Lemma sstpd_eq_1 Γ T1 i T2 : Γ s⊨ T1 <:[i] T2 ⊣⊢ - |==> ∀ ρ, sG⟦Γ⟧* ρ → ∀ v, ▷^i (T1 anil ρ v → T2 anil ρ v). + ∀ ρ, sG⟦Γ⟧* ρ → ∀ v, ▷^i (T1 anil ρ v → T2 anil ρ v). Proof. - rewrite /sstpd /subtype_lty; f_equiv; f_equiv => ρ. + rewrite /sstpd /subtype_lty; repeat f_equiv. by rewrite laterN_forall. Qed. Lemma sstpd_eq Γ T1 i T2 : Γ s⊨ T1 <:[i] T2 ⊣⊢ - |==> ∀ ρ v, sG⟦Γ⟧* ρ → ▷^i (T1 anil ρ v → T2 anil ρ v). + ∀ ρ v, sG⟦Γ⟧* ρ → ▷^i (T1 anil ρ v → T2 anil ρ v). Proof. rewrite sstpd_eq_1; properness. apply: forall_swap_impl. Qed. End JudgEqs. @@ -230,6 +230,7 @@ Section misc_lemmas. Proof. rewrite !oDTMem_unfold. iIntros "#HsubL #HsubU"; iDestruct 1 as (φ) "#(Hφl & #HLφ & #HφU)". + rewrite /= /dot_intv_type_pred. iExists φ; iSplit; first done; iSplit; iIntros "%w #Hw". - iApply ("HLφ" with "(HsubL Hw)"). - iApply ("HsubU" with "(HφU Hw)"). @@ -265,7 +266,7 @@ Section misc_lemmas. Lemma sdtp_eq (Γ : sCtx Σ) (T : clty Σ) l d : Γ s⊨ { l := d } : T ⊣⊢ - |==> ∀ ρ, ⌜path_includes (pv (ids 0)) ρ [(l, d)]⌝ → sG⟦Γ⟧* ρ → T ρ [(l, d.|[ρ])]. + ∀ ρ, ⌜path_includes (pv (ids 0)) ρ [(l, d)]⌝ → sG⟦Γ⟧* ρ → T ρ [(l, d.|[ρ])]. Proof. rewrite /sdtp /sdstp pure_True ?(left_id _ bi_and); by [> | exact: NoDup_singleton]. @@ -273,13 +274,13 @@ Section misc_lemmas. Lemma sdtp_eq' (Γ : sCtx Σ) (T : dlty Σ) l d : Γ s⊨ { l := d } : dty2clty l T ⊣⊢ - |==> ∀ ρ, ⌜path_includes (pv (ids 0)) ρ [(l, d)]⌝ → sG⟦Γ⟧* ρ → T ρ d.|[ρ]. + ∀ ρ, ⌜path_includes (pv (ids 0)) ρ [(l, d)]⌝ → sG⟦Γ⟧* ρ → T ρ d.|[ρ]. Proof. by rewrite sdtp_eq; properness; last apply dty2clty_singleton. Qed. Lemma ipwp_terminates {p T i} : [] s⊨p p : T , i ⊢ |==> ▷^i ⌜ terminates (path2tm p) ⌝. Proof. - iIntros ">#H". + iIntros "#>#H". iSpecialize ("H" $! ids with "[//]"); rewrite hsubst_id. iApply (path_wp_terminates with "H"). Qed. @@ -288,7 +289,7 @@ Section misc_lemmas. Lemma sT_Path {Γ τ p} : Γ s⊨p p : τ, 0 -∗ Γ s⊨ path2tm p : τ. Proof. - iIntros ">#Hep !> %ρ #Hg /="; rewrite path2tm_subst. + pupd; iIntros "#Hep !> %ρ #Hg /=". rewrite path2tm_subst. by iApply (path_wp_to_wp with "(Hep Hg)"). Qed. End misc_lemmas. diff --git a/theories/Dot/lr/sem_unstamped_typing.v b/theories/Dot/lr/sem_unstamped_typing.v index 974fea67..ade088bb 100644 --- a/theories/Dot/lr/sem_unstamped_typing.v +++ b/theories/Dot/lr/sem_unstamped_typing.v @@ -147,13 +147,14 @@ Section tmem_unstamped_lemmas. Lemma suD_Typ_Gen {l Γ fakeT s σ} {T : olty Σ} : s ↝[ σ ] T -∗ Γ su⊨ { l := dtysyn fakeT } : cTMem l (oLater T) (oLater T). Proof. - iIntros "#Hs"; iModIntro. iExists (dtysem σ s). + pupd; iIntros "#Hs !>". iExists (dtysem σ s). iSplit; first done; iApply (sD_Typ with "Hs"). Qed. Lemma suD_Typ {l σ Γ fakeT} {T : olty Σ} (HclT : coveringσ σ T) : ⊢ Γ su⊨ { l := dtysyn fakeT } : cTMem l (oLater T) (oLater T). Proof. + iModIntro. iMod (leadsto_envD_equiv_alloc HclT) as (s) "#Hs". iApply (suD_Typ_Gen with "Hs"). Qed. @@ -167,7 +168,7 @@ Section tmem_unstamped_lemmas. Γ su⊨ { l := d1 } : T -∗ Γ su⊨ { l := d2 } : T. Proof. - iIntros "#H1"; iMod "H1" as (d1s Hsk1) "H1"; iModIntro. + pupd; iIntros "#(%d1s & %Hsk1 & H1) !>". iExists d1s; iSplit; last done; iIntros "!%". apply /same_skel_trans_dm /Hsk1 /same_skel_symm_dm /Hsk. Qed. @@ -178,7 +179,7 @@ Section tmem_unstamped_lemmas. Γ su⊨ { l := d } : cTMem l L1 U1 -∗ Γ su⊨ { l := d } : cTMem l L2 U2. Proof. - iIntros "#Hsub1 #Hsub2 #H1"; iMod "H1" as (d1s Hsk1) "#H1"; iModIntro. + pupd; iIntros "#Hsub1 #Hsub2 #(%d1s & %Hsk1 & H1) !>". by iExists d1s; iSplit; last iApply (sD_Typ_Stp with "Hsub1 Hsub2 H1"). Qed. @@ -210,16 +211,14 @@ Section unstamped_lemmas. (*────────────────────────────────────────────────────────────*) Γ su⊨ tapp e1 e2 : T2. Proof. - iIntros "#H1 #H2". - iMod "H1" as (e1s Hsk1) "H1"; iMod "H2" as (e2s Hsk2) "H2"; iModIntro. + pupd; iIntros "#(%e1s & %Hsk1 & H1) #(%e2s & %Hsk2 & H2) !>". by iExists (tapp e1s e2s); iSplit; last iApply (sT_All_E with "H1 H2"). Qed. Lemma uT_All_E {Γ e1 e2 T1 T2} : Γ u⊨ e1 : TAll T1 (shift T2) -∗ Γ u⊨ e2 : T1 -∗ Γ u⊨ tapp e1 e2 : T2. Proof. - iIntros "#H1 #H2". - iMod "H1" as (e1s Hsk1) "H1"; iMod "H2" as (e2s Hsk2) "H2"; iModIntro. + pupd; iIntros "#(%e1s & %Hsk1 & H1) #(%e2s & %Hsk2 & H2) !>". by iExists (tapp e1s e2s); iSplit; last iApply (T_All_E with "H1 H2"). Qed. @@ -229,7 +228,7 @@ Section unstamped_lemmas. (*────────────────────────────────────────────────────────────*) Γ su⊨ tapp e1 (path2tm p2) : T2 .sTp[ p2 /]. Proof. - iIntros "#H1 #H2"; iMod "H1" as (e1s Hsk1) "H1"; iModIntro. + pupd; iIntros "#(%e1s & %Hsk1 & H1) #H2 !>". by iExists (tapp e1s (path2tm p2)); iSplit; last iApply (sT_All_E_p with "H1 H2"). Qed. @@ -239,7 +238,7 @@ Section unstamped_lemmas. (*────────────────────────────────────────────────────────────*) Γ u⊨ tapp e1 (path2tm p2) : T2'. Proof. - iIntros "#H1 #H2"; iMod "H1" as (e1s Hsk1) "H1"; iModIntro. + pupd; iIntros "#(%e1s & %Hsk1 & H1) #H2 !>". by iExists (tapp e1s (path2tm p2)); iSplit; last iApply (T_All_E_p with "H1 H2"). Qed. @@ -249,7 +248,7 @@ Section unstamped_lemmas. (*────────────────────────────────────────────────────────────*) Γ su⊨ tapp e1 (tv v2) : T2.|[ v2 /]. Proof. - iIntros "#H1 #H2"; iMod "H1" as (e1s Hsk1) "H1"; iModIntro. + pupd; iIntros "#(%e1s & %Hsk1 & H1) #H2 !>". iExists (tapp e1s (tv v2)); iSplit; last iApply (sT_All_Ex with "H1"). done. by iApply (sT_Path (p := pv v2)). @@ -259,7 +258,7 @@ Section unstamped_lemmas. Γ su⊨ e : oVMem l T -∗ Γ su⊨ tproj e l : T. Proof. - iIntros "#H1"; iMod "H1" as (e1s Hsk1) "H1"; iModIntro. + pupd; iIntros "#(%e1s & %Hsk1 & H1) !>". by iExists (tproj e1s l); iSplit; last iApply (sT_Obj_E with "H1"). Qed. @@ -274,7 +273,7 @@ Section unstamped_lemmas. (*─────────────────────────*) Γ su⊨ tv (vabs e) : oAll T1 T2. Proof. - iIntros "#H1"; iMod "H1" as (e1s Hsk1) "H1"; iModIntro. + pupd; iIntros "#(%e1s & %Hsk1 & H1) !>". by iExists (tv (vabs e1s)); iSplit; last iApply (sT_All_I_Strong with "H1"). Qed. @@ -283,7 +282,7 @@ Section unstamped_lemmas. shift T1 :: Γ' u⊨ e : T2 -∗ Γ u⊨ tv (vabs e) : TAll T1 T2. Proof. - iIntros "#H1"; iMod "H1" as (e1s Hsk1) "H1"; iModIntro. + pupd; iIntros "#(%e1s & %Hsk1 & H1) !>". by iExists (tv (vabs e1s)); iSplit; last iApply (T_All_I_Strong with "H1"). Qed. @@ -299,7 +298,7 @@ Section unstamped_lemmas. Γ su⊨ e : oLater T -∗ Γ su⊨ tskip e : T. Proof. - iIntros "#H1"; iMod "H1" as (e1s Hsk1) "H1"; iModIntro. + pupd; iIntros "#(%e1s & %Hsk1 & H1) !>". by iExists (tskip e1s); iSplit; last iApply (sT_Skip with "H1"). Qed. @@ -313,7 +312,7 @@ Section unstamped_lemmas. Γ s⊨ T1 <:[0] T2 -∗ Γ su⊨ e : T2. Proof. - iIntros "#H1 #H2"; iMod "H1" as (e1s Hsk1) "H1"; iModIntro. + pupd; iIntros "#(%e1s & %Hsk1 & H1) #H2 !>". by iExists e1s; iSplit; last iApply (sT_Sub with "H1 H2"). Qed. @@ -327,8 +326,8 @@ Section unstamped_lemmas. oLater T :: Γ su⊨ds ds : T -∗ Γ su⊨ tv (vobj ds) : oMu T. Proof. - iIntros "#H1"; iMod "H1" as (ds1 Hsk1) "H1"; iModIntro. - by iExists (tv (vobj ds1)); iSplit; last iApply (sT_Obj_I with "H1"). + pupd; iIntros "#(%ds1s & %Hsk1 & H1) !>". + by iExists (tv (vobj ds1s)); iSplit; last iApply (sT_Obj_I with "H1"). Qed. Lemma uT_Obj_I Γ T ds : @@ -339,7 +338,7 @@ Section unstamped_lemmas. Lemma suT_Path Γ τ p : Γ s⊨p p : τ, 0 -∗ Γ su⊨ path2tm p : τ. Proof. - iIntros "#H1"; iModIntro. + pupd; iIntros "#H1 !>". by iExists (path2tm p); iSplit; last iApply (sT_Path with "H1"). Qed. (* Primitives *) @@ -348,7 +347,7 @@ Section unstamped_lemmas. Γ su⊨ e1 : oPrim B1 -∗ Γ su⊨ tun u e1 : oPrim Br. Proof. - iIntros "#H1"; iMod "H1" as (e1s Hsk1) "H1"; iModIntro. + pupd; iIntros "#(%e1s & %Hsk1 & H1) !>". by iExists (tun u e1s); iSplit; last iApply (sT_Un with "H1"). Qed. @@ -356,7 +355,7 @@ Section unstamped_lemmas. Γ u⊨ e1 : TPrim B1 -∗ Γ u⊨ tun u e1 : TPrim Br. Proof. - iIntros "#H1"; iMod "H1" as (e1s Hsk1) "H1"; iModIntro. + pupd; iIntros "#(%e1s & %Hsk1 & H1) !>". by iExists (tun u e1s); iSplit; last iApply (T_Un with "H1"). Qed. @@ -365,8 +364,7 @@ Section unstamped_lemmas. Γ su⊨ e2 : oPrim B2 -∗ Γ su⊨ tbin b e1 e2 : oPrim Br. Proof. - iIntros "#H1 #H2". - iMod "H1" as (e1s Hsk1) "H1"; iMod "H2" as (e2s Hsk2) "H2"; iModIntro. + pupd; iIntros "#(%e1s & %Hsk1 & H1) #(%e2s & %Hsk2 & H2) !>". by iExists (tbin b e1s e2s); iSplit; last iApply (sT_Bin with "H1 H2"). Qed. @@ -375,8 +373,7 @@ Section unstamped_lemmas. Γ u⊨ e2 : TPrim B2 -∗ Γ u⊨ tbin b e1 e2 : TPrim Br. Proof. - iIntros "#H1 #H2". - iMod "H1" as (e1s Hsk1) "H1"; iMod "H2" as (e2s Hsk2) "H2"; iModIntro. + pupd; iIntros "#(%e1s & %Hsk1 & H1) #(%e2s & %Hsk2 & H2) !>". by iExists (tbin b e1s e2s); iSplit; last iApply (T_Bin with "H1 H2"). Qed. @@ -384,9 +381,7 @@ Section unstamped_lemmas. Γ su⊨ e1 : oBool -∗ Γ su⊨ e2 : T -∗ Γ su⊨ e3 : T -∗ Γ su⊨ tif e1 e2 e3 : T. Proof. - iIntros "#H1 #H2 #H3". - iMod "H1" as (e1s Hsk1) "H1"; iMod "H2" as (e2s Hsk2) "H2"; - iMod "H3" as (e3s Hsk3) "H3"; iModIntro. + pupd; iIntros "#(%e1s & %Hsk1 & H1) #(%e2s & %Hsk2 & H2) #(%e3s & %Hsk3 & H3) !>". by iExists (tif e1s e2s e3s); iSplit; last iApply (sT_If with "H1 H2 H3"). Qed. @@ -406,8 +401,7 @@ Section unstamped_lemmas. Γ su⊨ { l := d1 } : T1 -∗ Γ su⊨ds ds2 : T2 -∗ Γ su⊨ds (l, d1) :: ds2 : cAnd T1 T2. Proof. - iIntros "#H1 #H2". - iMod "H1" as (d1s Hsk1) "H1"; iMod "H2" as (ds2s Hsk2) "H2"; iModIntro. + pupd; iIntros "#(%d1s & %Hsk1 & H1) #(%ds2s & %Hsk2 & H2) !>". iExists ((l, d1s) :: ds2s); iSplit; last iApply (sD_Cons with "H1 H2"); naive_solver. Qed. @@ -421,7 +415,7 @@ Section unstamped_lemmas. Lemma suD_Sing Γ d l (T : cltyO Σ) : Γ su⊨ { l := d } : T -∗ Γ su⊨ds [(l, d)] : cAnd T cTop. Proof. - iIntros "#H1"; iMod "H1" as (d1s Hsk1) "H1"; iModIntro. + pupd; iIntros "#(%d1s & %Hsk1 & H1) !>". by iExists [(l, d1s)]; iSplit; last iApply (sD_Sing with "H1"). Qed. @@ -433,7 +427,7 @@ Section unstamped_lemmas. Γ su⊨ tv v1 : T -∗ Γ su⊨ { l := dpt (pv v1) } : cVMem l T. Proof. - iIntros "#H1"; iMod "H1" as (e1s Hsk1) "H1"; iModIntro. + pupd; iIntros "#(%e1s & %Hsk1 & H1) !>". destruct (same_skel_tv_tv Hsk1) as [v1s ->]. by iExists (dpt (pv v1s)); iSplit; last iApply (sD_Val with "H1"). Qed. @@ -447,7 +441,7 @@ Section unstamped_lemmas. Γ s⊨p p : T, 0 -∗ Γ su⊨ { l := dpt p } : cVMem l T. Proof. - iIntros "#H1"; iModIntro. + pupd; iIntros "#H1 !>". by iExists (dpt p); iSplit; last iApply (sD_Path with "H1"). Qed. @@ -460,7 +454,7 @@ Section unstamped_lemmas. oAnd (oLater T) (oSing (pself (pv (ids 1)) l)) :: Γ su⊨ds ds : T -∗ Γ su⊨ { l := dpt (pv (vobj ds)) } : cVMem l (oMu T). Proof. - iIntros "#H1"; iMod "H1" as (ds1s Hsk1) "H1"; iModIntro. + pupd; iIntros "#(%ds1s & %Hsk1 & H1) !>". by iExists (dpt (pv (vobj ds1s))); iSplit; last iApply (sD_Val_New with "H1"). Qed. @@ -474,7 +468,7 @@ Section unstamped_lemmas. Γ su⊨ { l := dpt p1 } : cVMem l T1 -∗ Γ su⊨ { l := dpt p1 } : cVMem l T2. Proof. - iIntros "#Hsub #H1"; iMod "H1" as (d1s Hsk1) "H1"; iModIntro. + pupd; iIntros "#Hsub #(%d1s & %Hsk1 & H1) !>". destruct (same_skel_dpt_dpt Hsk1) as [p1s ->]. by iExists (dpt p1s); iSplit; last iApply (sD_Path_Stp with "Hsub H1"). Qed. diff --git a/theories/Dot/lr/unary_lr.v b/theories/Dot/lr/unary_lr.v index f29991e4..070cb400 100644 --- a/theories/Dot/lr/unary_lr.v +++ b/theories/Dot/lr/unary_lr.v @@ -338,21 +338,21 @@ Section judgment_definitions. Context `{HdotG : !dlangG Σ}. Lemma idstp_eq Γ T ds : Γ ⊨ds ds : T ⊣⊢ - |==> ⌜wf_ds ds⌝ ∧ ∀ ρ, ⌜path_includes (pv (ids 0)) ρ ds ⌝ → G⟦Γ⟧ ρ → Ds⟦T⟧ ρ ds.|[ρ]. + (⌜wf_ds ds⌝ ∧ ∀ ρ, ⌜path_includes (pv (ids 0)) ρ ds ⌝ → G⟦Γ⟧ ρ → Ds⟦T⟧ ρ ds.|[ρ]). Proof. reflexivity. Qed. Lemma ietp_eq Γ e T : - Γ ⊨ e : T ⊣⊢ |==> ∀ ρ, G⟦Γ⟧ ρ → E⟦T⟧ ρ (e.|[ρ]). + Γ ⊨ e : T ⊣⊢ ∀ ρ, G⟦Γ⟧ ρ → E⟦T⟧ ρ (e.|[ρ]). Proof. reflexivity. Qed. Lemma istpd_eq Γ T1 i T2 : Γ ⊨ T1 <:[i] T2 ⊣⊢ - |==> ∀ ρ v, G⟦Γ⟧ ρ → ▷^i (V⟦T1⟧ anil ρ v → V⟦T2⟧ anil ρ v). + ∀ ρ v, G⟦Γ⟧ ρ → ▷^i (V⟦T1⟧ anil ρ v → V⟦T2⟧ anil ρ v). Proof. apply sstpd_eq. Qed. Lemma iptp_eq Γ p T i : Γ ⊨p p : T , i ⊣⊢ - |==> ∀ ρ, G⟦Γ⟧ ρ → + ∀ ρ, G⟦Γ⟧ ρ → ▷^i path_wp (p.|[ρ]) (λ v, V⟦T⟧ anil ρ v). Proof. reflexivity. Qed. End judgment_definitions. diff --git a/theories/Dot/semtyp_lemmas/binding_lr.v b/theories/Dot/semtyp_lemmas/binding_lr.v index 0428df2b..5b544f54 100644 --- a/theories/Dot/semtyp_lemmas/binding_lr.v +++ b/theories/Dot/semtyp_lemmas/binding_lr.v @@ -14,9 +14,9 @@ Section LambdaIntros. (*─────────────────────────*) Γ s⊨ tv (vabs e) : oAll T1 T2. Proof. - rewrite Hctx; iIntros ">HeT !> %ρ Hg /=". + rewrite Hctx; pupd; iIntros "#HeT !> %ρ #Hg /=". rewrite -wp_value'. iExists _; iSplit; first done. - iIntros (v) "Hv"; rewrite up_sub_compose. + iIntros "%v Hv"; rewrite up_sub_compose. (* Factor ▷ out of [sG⟦ Γ ⟧* ρ] before [iNext]. *) rewrite senv_TLater_commute. iNext. iApply ("HeT" $! (v .: ρ) with "[Hv $Hg]"). @@ -40,7 +40,7 @@ Section Sec. (*──────────────────────*) ⊢ Γ s⊨p pv (ids x) : shiftN x τ, 0. Proof. - iIntros "/= !> %ρ #Hg"; rewrite path_wp_pv_eq. + pupd; iIntros "/= !> %ρ #Hg"; rewrite path_wp_pv_eq. by rewrite s_interp_env_lookup // id_subst. Qed. @@ -48,7 +48,7 @@ Section Sec. Γ s⊨ e : oLaterN i T -∗ Γ s⊨ iterate tskip i e : T. Proof. - iIntros ">#He !> %ρ #Hg"; rewrite tskip_subst; iApply wp_bind. + pupd; iIntros "#He !> %ρ #Hg"; rewrite tskip_subst; iApply wp_bind. wp_wapply "(He Hg)"; iIntros "{He} /= %v Hv". by wp_pure. Qed. @@ -63,7 +63,7 @@ Section Sec. (*───────────────────────────────*) Γ s⊨ e : T2. Proof. - iIntros ">HeT1 >Hsub !> %ρ #Hg". + pupd; iIntros "#HeT1 #Hsub !> %ρ #Hg". wp_wapply "(HeT1 Hg)". iIntros (v) "HvT1 /=". iApply ("Hsub" with "Hg HvT1"). @@ -76,7 +76,7 @@ Section Sec. *) Lemma sTMu_equiv {Γ T v} : (Γ s⊨ tv v : oMu T) ≡ (Γ s⊨ tv v : T.|[v/]). Proof. - iSplit; iIntros ">#Htp !> %ρ #Hg /="; + iSplit; pupd; iIntros "#Htp !> %ρ #Hg /="; iDestruct (wp_value_inv' with "(Htp Hg)") as "{Htp} Hgoal"; by rewrite -wp_value /= hoEnvD_subst_one. Qed. @@ -87,7 +87,7 @@ Section Sec. (*────────────────────────────────────────────────────────────*) Γ s⊨ tapp e1 (tv v2) : T2.|[v2/]. Proof. - iIntros ">He1 >Hv2Arg !> %ρ #Hg". + pupd; iIntros "#He1 #Hv2Arg !> %ρ #Hg". iSpecialize ("Hv2Arg" with "Hg"); rewrite /= wp_value_inv'. wp_wapply "(He1 Hg)"; iIntros "{Hg} %v /=". iDestruct 1 as (t ->) "HvFun"; iSpecialize ("HvFun" with "Hv2Arg"). @@ -101,7 +101,7 @@ Section Sec. (*────────────────────────────────────────────────────────────*) Γ s⊨ tapp e1 e2 : T2. Proof. - iIntros "/= >He1 >He2 !> %ρ #Hg". + pupd; iIntros "/= #He1 #He2 !> %ρ #Hg". wp_wapply "(He1 Hg)"; iIntros "%v"; iDestruct 1 as (t ->) "Hv /=". wp_wapply "(He2 Hg)"; iIntros "{Hg} %w Hw /=". iSpecialize ("Hv" with "Hw"). wp_pure. wp_wapply "Hv". @@ -113,7 +113,7 @@ Section Sec. (*─────────────────────────*) Γ s⊨ tproj e l : T. Proof. - iIntros ">He !> %ρ Hg". + pupd; iIntros "#He !> %ρ Hg". wp_wapply "(He Hg)"; iIntros "%v /=". iDestruct 1 as (? Hl pmem ->) "Hv /=". wp_pure. by rewrite -path_wp_to_wp. diff --git a/theories/Dot/semtyp_lemmas/defs_lr.v b/theories/Dot/semtyp_lemmas/defs_lr.v index 8ec0f41b..71fb5437 100644 --- a/theories/Dot/semtyp_lemmas/defs_lr.v +++ b/theories/Dot/semtyp_lemmas/defs_lr.v @@ -12,7 +12,7 @@ Section Sec. Γ s⊨p p : T, 0 -∗ Γ s⊨ { l := dpt p } : cVMem l T. Proof. - rewrite sdtp_eq'; iIntros ">#Hv !>" (ρ Hpid) "#Hg". + rewrite sdtp_eq'; pupd; iIntros "#Hv !>" (ρ Hpid) "#Hg". rewrite oDVMem_eq; iApply ("Hv" with "Hg"). Qed. @@ -23,7 +23,7 @@ Section Sec. Γ s⊨ tv v : T -∗ Γ s⊨p pv v : T, 0. Proof. - iIntros "/= >#Hp !> %ρ Hg". rewrite path_wp_pv_eq -wp_value_inv'. + pupd; iIntros "/= #Hp !> %ρ Hg". rewrite path_wp_pv_eq -wp_value_inv'. iApply ("Hp" with "Hg"). Qed. @@ -37,8 +37,8 @@ Section Sec. oAnd (oLater T) (oSing (pself (pv (ids 1)) l)) :: Γ s⊨ds ds : T -∗ Γ s⊨ { l := dpt (pv (vobj ds)) } : cVMem l (oMu T). Proof. - rewrite sdtp_eq'; iMod 1 as (Hwf) "#Hds"; - iIntros "!>" (ρ Hpid%path_includes_field_aliases) "#Hg". + rewrite sdtp_eq'. pupd. + iIntros "[%Hwf #Hds] !>" (ρ Hpid%path_includes_field_aliases) "#Hg". rewrite oDVMem_eq path_wp_pv_eq /=. iLöb as "IH". iEval rewrite -clty_commute norm_selfSubst. iApply ("Hds" $! (vobj _ .: ρ) with "[%] [$IH $Hg //]"). @@ -50,7 +50,7 @@ Section Sec. Γ s⊨ { l := dpt p } : cVMem l T1 -∗ Γ s⊨ { l := dpt p } : cVMem l T2. Proof. - rewrite !sdtp_eq'; iIntros ">#Hsub >#Hd !>" (ρ Hpid) "#Hg". + rewrite !sdtp_eq'; pupd; iIntros "#Hsub #Hd !>" (ρ Hpid) "#Hg". iSpecialize ("Hd" $! ρ Hpid with "Hg"). iApply (oDVMem_respects_sub with "(Hsub Hg) Hd"). Qed. @@ -61,7 +61,7 @@ Section Sec. Γ s⊨ { l := d } : cTMem l L1 U1 -∗ Γ s⊨ { l := d } : cTMem l L2 U2. Proof. - rewrite !sdtp_eq'; iIntros ">#HL >#HU >#Hd !>" (ρ Hpid) "#Hg". + rewrite !sdtp_eq'; pupd; iIntros "#HL #HU #Hd !>" (ρ Hpid) "#Hg". iSpecialize ("Hd" $! ρ Hpid with "Hg"). iApply (oDTMem_respects_sub with "(HL Hg) (HU Hg) Hd"). Qed. @@ -70,11 +70,11 @@ Section Sec. s ↝[ σ ] T -∗ Γ s⊨ { l := dtysem σ s } : cTMem l (oLater T) (oLater T). Proof. - rewrite !sdtp_eq'; iDestruct 1 as (φ Hγφ) "#Hγ". + rewrite !sdtp_eq'; pupd; iDestruct 1 as (φ Hγφ) "#Hγ". iIntros "!>" (ρ Hpid) "#Hg"; rewrite oDTMem_unfold /=. iExists (hoEnvD_inst (σ.|[ρ]) φ); iSplit. by iApply (dm_to_type_intro with "Hγ"). - by iSplit; iIntros (v) "#H"; iNext; iApply Hγφ. + iSplit; iIntros "%v #H"; iNext; by iApply Hγφ. Qed. Lemma sD_Typ_Abs {Γ} T L U s σ l : @@ -94,7 +94,7 @@ Section Sec. oLater T :: Γ s⊨ds ds : T -∗ Γ s⊨p pv (vobj ds) : oMu T, 0. Proof. - iMod 1 as (Hwf) "#Hds". iIntros "!> %ρ #Hg /=". + pupd; iIntros "[%Hwf #Hds] !> %ρ #Hg /=". rewrite path_wp_pv_eq /=. iLöb as "IH". iApply clty_commute. rewrite norm_selfSubst. iApply ("Hds" $! (vobj _ .: ρ) with "[%] [$IH $Hg]"). @@ -107,14 +107,14 @@ Section Sec. Proof. by rewrite sP_Obj_I sT_Path. Qed. Lemma sD_Nil Γ : ⊢ Γ s⊨ds [] : cTop. - Proof. by iModIntro; iSplit; last iIntros "**". Qed. + Proof. by pupd; iIntros "!>"; iSplit; last iIntros "**". Qed. Lemma sD_Cons Γ d ds l (T1 T2 : cltyO Σ) : dms_hasnt ds l → Γ s⊨ { l := d } : T1 -∗ Γ s⊨ds ds : T2 -∗ Γ s⊨ds (l, d) :: ds : cAnd T1 T2. Proof. - rewrite sdtp_eq; iIntros (Hlds) ">#HT1 >[% #HT2] !>"; iSplit. + rewrite sdtp_eq => Hlds; pupd; iIntros "#HT1 [% #HT2] !>"; iSplit. by iIntros "!%"; cbn; constructor => //; by rewrite -dms_hasnt_notin_eq. iIntros (ρ [Hpid Hpids]%path_includes_split) "#Hg". iSpecialize ("HT1" $! _ Hpid with "Hg"). diff --git a/theories/Dot/semtyp_lemmas/dsub_lr.v b/theories/Dot/semtyp_lemmas/dsub_lr.v index 063bad27..e846e931 100644 --- a/theories/Dot/semtyp_lemmas/dsub_lr.v +++ b/theories/Dot/semtyp_lemmas/dsub_lr.v @@ -31,52 +31,52 @@ Section DStpLemmas. Lemma sStp_Refl {Γ} T i : ⊢ Γ s⊨ T <:[i] T. - Proof. iIntros "!> %ρ _ !>"; by rewrite -subtype_refl. Qed. + Proof. pupd; iIntros "!> %ρ _ !>"; by rewrite -subtype_refl. Qed. Lemma sStp_Trans {Γ T1 T2 T3 i} : Γ s⊨ T1 <:[i] T2 -∗ Γ s⊨ T2 <:[i] T3 -∗ Γ s⊨ T1 <:[i] T3. Proof. - iIntros ">#Hsub1 >#Hsub2 !> %ρ #Hg *". + pupd; iIntros "#Hsub1 #Hsub2 !> %ρ #Hg *". iApply (subtype_trans with "(Hsub1 Hg) (Hsub2 Hg)"). Qed. Lemma sStp_Top Γ T i : ⊢ Γ s⊨ T <:[i] oTop. - Proof. rewrite sstpd_eq_1. by iIntros "!> ** !> **". Qed. + Proof. rewrite sstpd_eq_1. pupd; by iIntros "!> ** !> **". Qed. Lemma sBot_Stp Γ T i : ⊢ Γ s⊨ oBot <:[i] T. - Proof. rewrite sstpd_eq_1. by iIntros "!> /= ** !> []". Qed. + Proof. rewrite sstpd_eq_1. pupd; by iIntros "!> /= ** !> []". Qed. Lemma sAnd1_Stp Γ T1 T2 i : ⊢ Γ s⊨ oAnd T1 T2 <:[i] T1. - Proof. rewrite sstpd_eq. by iIntros "!> /= %ρ %v _ !> [$ _]". Qed. + Proof. rewrite sstpd_eq. pupd; by iIntros "!> /= %ρ %v _ !> [$ _]". Qed. Lemma sAnd2_Stp Γ T1 T2 i : ⊢ Γ s⊨ oAnd T1 T2 <:[i] T2. - Proof. rewrite sstpd_eq. by iIntros "!> /= %ρ %v _ !> [_ $]". Qed. + Proof. rewrite sstpd_eq. pupd; by iIntros "!> /= %ρ %v _ !> [_ $]". Qed. Lemma sStp_And Γ T U1 U2 i : Γ s⊨ T <:[i] U1 -∗ Γ s⊨ T <:[i] U2 -∗ Γ s⊨ T <:[i] oAnd U1 U2. Proof. - rewrite !sstpd_eq; iIntros ">#H1 >#H2 !> %ρ %v #Hg". + rewrite !sstpd_eq; pupd; iIntros "#H1 #H2 !> %ρ %v #Hg". iSpecialize ("H1" $! ρ v with "Hg"); iSpecialize ("H2" $! ρ v with "Hg"). iNext i; iIntros "#H". iSplit; [iApply "H1" | iApply "H2"]; iApply "H". Qed. Lemma sStp_Or1 Γ T1 T2 i : ⊢ Γ s⊨ T1 <:[i] oOr T1 T2. - Proof. rewrite sstpd_eq. by iIntros "!> /= %ρ %v _ !>"; eauto. Qed. + Proof. rewrite sstpd_eq. pupd; by iIntros "!> /= %ρ %v _ !>"; eauto. Qed. Lemma sStp_Or2 Γ T1 T2 i : ⊢ Γ s⊨ T2 <:[i] oOr T1 T2. - Proof. rewrite sstpd_eq. by iIntros "!> /= %ρ %v _ !>"; eauto. Qed. + Proof. rewrite sstpd_eq. pupd; by iIntros "!> /= %ρ %v _ !>"; eauto. Qed. Lemma sOr_Stp Γ T1 T2 U i : Γ s⊨ T1 <:[i] U -∗ Γ s⊨ T2 <:[i] U -∗ Γ s⊨ oOr T1 T2 <:[i] U. Proof. - rewrite !sstpd_eq; iIntros ">#H1 >#H2 !> * #Hg". + rewrite !sstpd_eq; pupd; iIntros "#H1 #H2 !> * #Hg". iSpecialize ("H1" $! ρ v with "Hg"); iSpecialize ("H2" $! ρ v with "Hg"). iNext i; iIntros "#[HT | HT]"; [iApply "H1" | iApply "H2"]; iApply "HT". Qed. @@ -84,7 +84,7 @@ Section DStpLemmas. Lemma sDistr_And_Or_Stp Γ {S T U i} : ⊢ Γ s⊨ oAnd (oOr S T) U <:[i] oOr (oAnd S U) (oAnd T U). Proof. rewrite sstpd_eq. - by iIntros "!> %ρ %v #Hg !> [[HS|HT] Hu] /="; [iLeft|iRight]; iFrame. + by pupd; iIntros "!> %ρ %v #Hg !> [[HS|HT] Hu] /="; [iLeft|iRight]; iFrame. Qed. (* XXX must we state the two separate halves? *) @@ -95,7 +95,7 @@ Section DStpLemmas. Lemma sStp_Add_LaterN {Γ T i j} : ⊢ Γ s⊨ T <:[i] oLaterN j T. - Proof. rewrite sstpd_eq; iIntros "!> ** !> $". Qed. + Proof. rewrite sstpd_eq; pupd; iIntros "!> ** !> $". Qed. Lemma sStp_Add_Later {Γ T i} : ⊢ Γ s⊨ T <:[i] oLater T. Proof. apply sStp_Add_LaterN. Qed. @@ -104,7 +104,7 @@ Section DStpLemmas. Γ s⊨p p : oTMem l L U, i -∗ Γ s⊨ L <:[i] oSel p l. Proof. - rewrite sstpd_eq; iIntros ">#Hp !> %ρ %v Hg". + rewrite sstpd_eq; pupd; iIntros "#Hp !> %ρ %v Hg". iSpecialize ("Hp" with "Hg"); iNext i; iIntros "#HL". iApply (path_wp_wand with "Hp"); iIntros (w). iApply (vl_sel_lb with "HL"). @@ -114,7 +114,7 @@ Section DStpLemmas. Γ s⊨p p : oTMem l L U, i -∗ Γ s⊨ oSel p l <:[i] U. Proof. - rewrite sstpd_eq; iIntros ">#Hp !> %ρ %v Hg". + rewrite sstpd_eq; pupd; iIntros "#Hp !> %ρ %v Hg". iSpecialize ("Hp" with "Hg"); iNext i; iIntros "Hφ". iDestruct (path_wp_agree with "Hp Hφ") as (w Hw) "[Hp Hφ]". iApply (vl_sel_ub with "Hφ Hp"). @@ -129,7 +129,7 @@ Section DStpLemmas. oLaterN i T1 :: Γ s⊨ T1 <:[i] T2 -∗ Γ s⊨ oMu T1 <:[i] oMu T2. Proof. - rewrite !sstpd_eq; iIntros ">#Hstp !> %ρ %v Hg". + rewrite !sstpd_eq; pupd; iIntros "#Hstp !> %ρ %v Hg". iApply mlaterN_impl; iIntros "#HT1". iApply ("Hstp" $! (v .: ρ) v with "[$Hg $HT1] HT1"). Qed. @@ -151,7 +151,7 @@ Section DStpLemmas. Γ s⊨ T1 <:[i] T2 -∗ Γ s⊨ oVMem l T1 <:[i] oVMem l T2. Proof. - iIntros ">#Hsub !> %ρ Hg"; iSpecialize ("Hsub" with "Hg"); iNext i. + pupd; iIntros "#Hsub !> %ρ Hg"; iSpecialize ("Hsub" with "Hg"); iNext i. iApply (oVMem_respects_sub with "Hsub"). Qed. @@ -160,7 +160,7 @@ Section DStpLemmas. Γ s⊨ U1 <:[i] U2 -∗ Γ s⊨ oTMem l L1 U1 <:[i] oTMem l L2 U2. Proof. - iIntros ">#HsubL >#HsubU !> %ρ #Hg". + pupd; iIntros "#HsubL #HsubU !> %ρ #Hg". iSpecialize ("HsubL" with "Hg"); iSpecialize ("HsubU" with "Hg"); iNext i. iApply (oTMem_respects_sub with "HsubL HsubU"). Qed. @@ -170,7 +170,7 @@ Section DStpLemmas. oLaterN (i.+1) (oShift T2) :: Γ s⊨ oLater U1 <:[i] oLater U2 -∗ Γ s⊨ oAll T1 U1 <:[i] oAll T2 U2. Proof. - rewrite !sstpd_delay_oLaterN_plus; iIntros ">#HsubT >#HsubU !> %ρ #Hg %v". + rewrite !sstpd_delay_oLaterN_plus; pupd; iIntros "#HsubT #HsubU !> %ρ #Hg %v". rewrite -!mlaterN_impl. iDestruct 1 as (t) "#[Heq #HT1]"; iExists t; iFrame "Heq". iIntros (w); iSpecialize ("HT1" $! w). @@ -191,7 +191,7 @@ Section DStpLemmas. (*───────────────────────────────*) Γ s⊨ T1 <:[i] oLaterN j T2. Proof. - rewrite -sstpd_delay_oLaterN; iIntros ">#Htyp !> %ρ Hg %v HvT1". + rewrite -sstpd_delay_oLaterN; pupd; iIntros "#Htyp !> %ρ Hg %v HvT1". iEval rewrite /= -(path_wp_pv_eq _ (T2 _ _)) -laterN_plus. iApply ("Htyp" $! (v .: ρ) with "[$Hg $HvT1]"). Qed. @@ -204,10 +204,10 @@ Section DStpLemmas. Lemma sAnd_All_1_Stp_Distr Γ S T1 T2 i : ⊢ Γ s⊨ oAnd (oAll S T1) (oAll S T2) <:[i] oAll S (oAnd T1 T2). Proof. - iIntros "!> %ρ _ !> %v [#H1 #H2]". + pupd; iIntros "!> %ρ _ !> %v [#H1 #H2]". iDestruct "H1" as (t ?) "#H1"; iDestruct "H2" as (t' ->) "#H2"; simplify_eq. iExists t; iSplit; first done. - iIntros (w) "#HS". + iIntros "%w #HS". (* Oh. Dreaded conjunction rule. Tho could we use a version for separating conjunction? *) iApply (wp_and with "(H1 HS) (H2 HS)"). @@ -216,10 +216,10 @@ Section DStpLemmas. Lemma sAnd_All_2_Stp_Distr Γ S1 S2 T i : ⊢ Γ s⊨ oAnd (oAll S1 T) (oAll S2 T) <:[i] oAll (oOr S1 S2) T. Proof. - iIntros "!> %ρ _ !> %v [#H1 #H2]". + pupd; iIntros "!> %ρ _ !> %v [#H1 #H2]". iDestruct "H1" as (t ?) "#H1"; iDestruct "H2" as (t' ->) "#H2"; simplify_eq. iExists t; iSplit; first done. - iIntros (w) "#[HS|HS]"; [iApply ("H1" with "HS")|iApply ("H2" with "HS")]. + iIntros "%w #[HS|HS]"; [iApply ("H1" with "HS")|iApply ("H2" with "HS")]. Qed. (** @@ -233,7 +233,7 @@ Section DStpLemmas. Lemma sAnd_Fld_Stp_Distr Γ l T1 T2 i : ⊢ Γ s⊨ oAnd (oVMem l T1) (oVMem l T2) <:[i] oVMem l (oAnd T1 T2). Proof. - iIntros "!> %ρ _ !> %v [#H1 H2]"; rewrite !oVMem_eq. + pupd; iIntros "!> %ρ _ !> %v [#H1 H2]"; rewrite !oVMem_eq. iDestruct "H1" as (pmem Hl) "#H1"; iDestruct "H2" as (pmem' Hl') "#H2". objLookupDet. iExists pmem; iFrame (Hl). by iApply (path_wp_and' with "H1 H2"). @@ -242,9 +242,9 @@ Section DStpLemmas. Lemma sAnd_Typ_Stp_Distr Γ l L1 L2 U1 U2 i : ⊢ Γ s⊨ oAnd (oTMem l L1 U1) (oTMem l L2 U2) <:[i] oTMem l (oOr L1 L2) (oAnd U1 U2). Proof. - iIntros "!> %ρ _ !> %v [H1 H2]"; rewrite !oTMem_eq /dot_intv_type_pred. - iDestruct "H1" as (ψ d Hl) "[Hdψ1 [HLψ1 HψU1]]". - iDestruct "H2" as (ψ' d' Hl') "[Hdψ2 [HLψ2 HψU2]]". objLookupDet. + pupd; iIntros "!> %ρ _ !> %v #[H1 H2]"; rewrite !oTMem_eq /dot_intv_type_pred. + iDestruct "H1" as (ψ d Hl) "[Hdψ1 #[HLψ1 HψU1]]". + iDestruct "H2" as (ψ' d' Hl') "[Hdψ2 #[HLψ2 HψU2]]". objLookupDet. iExists ψ, d. iFrame (Hl). iSplit; first done. iSplit; iIntros (w) "Hw"; iDestruct (dm_to_type_agree anil w with "Hdψ1 Hdψ2") as "Hag". @@ -258,7 +258,7 @@ Section DStpLemmas. Lemma sOr_Fld_Stp_Distr Γ l T1 T2 i : ⊢ Γ s⊨ oVMem l (oOr T1 T2) <:[i] oOr (oVMem l T1) (oVMem l T2). Proof. - iIntros "!> %ρ _ !> %v". rewrite !oVMem_eq. + pupd; iIntros "!> %ρ _ !> %v". rewrite !oVMem_eq. iDestruct 1 as (pmem Hl) "Hp". rewrite path_wp_eq. iDestruct "Hp" as (w Hpw) "[H|H]"; [iLeft|iRight]. all: by rewrite oVMem_eq; iExists (pmem); iFrame (Hl); @@ -301,7 +301,7 @@ Section DStpLemmas. Γ s⊨p p : oLater T, i -∗ Γ s⊨p p : T, i.+1. Proof. - iIntros ">#HpT !> %ρ #Hg"; rewrite -later_laterN laterN_later. + pupd; iIntros "#HpT !> %ρ #Hg"; rewrite -later_laterN laterN_later. iSpecialize ("HpT" with "Hg"); iNext i. iApply (path_wp_later_swap with "HpT"). Qed. diff --git a/theories/Dot/semtyp_lemmas/path_repl_lr.v b/theories/Dot/semtyp_lemmas/path_repl_lr.v index 2092f256..bfa20d3f 100644 --- a/theories/Dot/semtyp_lemmas/path_repl_lr.v +++ b/theories/Dot/semtyp_lemmas/path_repl_lr.v @@ -18,7 +18,7 @@ Section semantic_lemmas. Γ s⊨p p : τ, i -∗ Γ s⊨p p : oSing p, i. Proof. - iIntros ">#Hep !> %ρ Hg"; iApply (strong_path_wp_wand with "(Hep Hg)"). + pupd; iIntros "#Hep !> %ρ Hg"; iApply (strong_path_wp_wand with "(Hep Hg)"). iIntros "%v %Hpv _ !%"; apply alias_paths_pv_eq_1, Hpv. Qed. @@ -26,7 +26,7 @@ Section semantic_lemmas. Γ s⊨p p : T, i -∗ Γ s⊨ oSing p <:[i] T. Proof. - rewrite sstpd_eq; iIntros ">#Hp !> %ρ %v Hg". + rewrite sstpd_eq; pupd; iIntros "#Hp !> %ρ %v Hg". iSpecialize ("Hp" with "Hg"); iNext i. iDestruct 1 as %->%(alias_paths_elim_eq (T _ ρ)). by rewrite path_wp_pv_eq. @@ -37,7 +37,7 @@ Section semantic_lemmas. Γ s⊨ oSing p <:[i] oSing q -∗ Γ s⊨ oSing q <:[i] oSing p. Proof. - rewrite !sstpd_eq; iIntros ">#Hp >#Hps !> %ρ %v #Hg". + rewrite !sstpd_eq; pupd; iIntros "#Hp #Hps !> %ρ %v #Hg". iDestruct (path_wp_eq with "(Hp Hg)") as (w) "[Hpw _] {Hp}". rewrite -alias_paths_pv_eq_1; iSpecialize ("Hps" $! _ w with "Hg Hpw"); iNext i; rewrite /= !alias_paths_pv_eq_1. @@ -49,7 +49,7 @@ Section semantic_lemmas. Γ s⊨p p : oSing q, i -∗ Γ s⊨p q : oTop, i. Proof. - iIntros ">#Hpq !> %ρ Hg /="; iSpecialize ("Hpq" with "Hg"); iNext i. + pupd; iIntros "#Hpq !> %ρ Hg /="; iSpecialize ("Hpq" with "Hg"); iNext i. iDestruct "Hpq" as %(v & _ & Hqv)%alias_paths_simpl%alias_paths_sameres. iIntros "!%". exact: (path_wp_pure_wand Hqv). Qed. @@ -61,16 +61,16 @@ Section semantic_lemmas. Γ s⊨p p : oSing q, i -∗ Γ s⊨ T1 <:[i] T2. Proof. - rewrite sstpd_eq; iIntros ">#Hrepl >#Hal !> %ρ %v #Hg". + rewrite sstpd_eq; pupd; iIntros "#Hrepl #Hal !> %ρ %v #Hg". iSpecialize ("Hal" with "Hg"); iNext i. iDestruct "Hal" as %Hal%alias_paths_simpl. - iRewrite ("Hrepl" $! anil ρ v Hal); iIntros "$". + iRewrite ("Hrepl" $! anil ρ v Hal). iIntros "$". Qed. Lemma sP_Mu_E {Γ T p i} : Γ s⊨p p : oMu T, i -∗ Γ s⊨p p : T .sTp[ p /], i. Proof. - iIntros ">#Hp !> %ρ Hg /=". + pupd; iIntros "#Hp !> %ρ Hg /=". iApply (strong_path_wp_wand with "(Hp Hg)"); iIntros "**". by rewrite oMu_eq sem_psubst_one_repl ?alias_paths_pv_eq_1. Qed. @@ -78,7 +78,7 @@ Section semantic_lemmas. Lemma sP_Mu_I {Γ T p i} : Γ s⊨p p : T .sTp[ p /], i -∗ Γ s⊨p p : oMu T, i. Proof. - iIntros ">#Hp !> %ρ Hg /=". + pupd; iIntros "#Hp !> %ρ Hg /=". iApply (strong_path_wp_wand with "(Hp Hg)"); iIntros "**". by rewrite oMu_eq sem_psubst_one_repl ?alias_paths_pv_eq_1. Qed. @@ -89,7 +89,7 @@ Section semantic_lemmas. (*────────────────────────────────────────────────────────────*) Γ s⊨ tapp e1 (path2tm p2) : T2 .sTp[ p2 /]. Proof. - iIntros ">He1 >Hp2 !> %ρ #Hg /="; iSpecialize ("Hp2" with "Hg"). + pupd; iIntros "#He1 #Hp2 !> %ρ #Hg /="; iSpecialize ("Hp2" with "Hg"). wp_wapply "(He1 Hg)"; iIntros "{Hg} %v". iDestruct 1 as (t ->) "HvFun". rewrite path_wp_eq path2tm_subst /=. iDestruct "Hp2" as (pw Hpwpp) "Hpw"; iSpecialize ("HvFun" with "Hpw"). @@ -105,7 +105,7 @@ Section semantic_lemmas. (*─────────────────────────*) Γ s⊨p p : oVMem l T, i. Proof. - iIntros ">Hp /= !> %ρ Hg"; iSpecialize ("Hp" with "Hg"); iNext i. + pupd; iIntros "#Hp /= !> %ρ Hg"; iSpecialize ("Hp" with "Hg"); iNext i. rewrite path_wp_pself_eq; iDestruct "Hp" as (v q Hlook) "[Hpv #Htw]". iApply (path_wp_wand with "Hpv"). iIntros "/= % <-"; eauto. Qed. @@ -125,7 +125,7 @@ Section semantic_lemmas. (*─────────────────────────*) Γ s⊨p pself p l : T, i. Proof. - iIntros ">Hp !> %ρ Hg /="; iSpecialize ("Hp" with "Hg"); iNext i. + pupd; iIntros "#Hp !> %ρ Hg /="; iSpecialize ("Hp" with "Hg"); iNext i. rewrite path_wp_pself_eq path_wp_eq. iDestruct "Hp" as (vp Hpv d Hlook pmem ->) "H". iExists vp, pmem. eauto. @@ -138,7 +138,7 @@ Section semantic_lemmas. Γ s⊨p q : T, i -∗ Γ s⊨p p : T, i. Proof. - iIntros ">Hep >Heq !> %ρ #Hg"; iSpecialize ("Heq" with "Hg"). + pupd; iIntros "#Hep #Heq !> %ρ #Hg"; iSpecialize ("Heq" with "Hg"). iSpecialize ("Hep" with "Hg"); iNext i. by iDestruct "Hep" as %->%alias_paths_simpl%(alias_paths_elim_eq (T _ _)). Qed. @@ -148,7 +148,7 @@ Section semantic_lemmas. Γ s⊨p pself q l : τ, i -∗ Γ s⊨p pself p l : oSing (pself q l), i. Proof. - iIntros ">Hpq >HqlT !> %ρ #Hg"; iSpecialize ("HqlT" with "Hg"); + pupd; iIntros "#Hpq #HqlT !> %ρ #Hg"; iSpecialize ("HqlT" with "Hg"); iSpecialize ("Hpq" with "Hg"); iNext i; iClear "Hg". iDestruct "Hpq" as %Hal%alias_paths_simpl. rewrite !path_wp_eq; iDestruct "HqlT" as (vql Hql) "_". @@ -162,7 +162,7 @@ Section semantic_lemmas. (*───────────────────────────────*) Γ s⊨p p : T2, i. Proof. - iIntros ">HpT1 >Hsub !> %ρ #Hg". + pupd; iIntros "#HpT1 #Hsub !> %ρ #Hg". iSpecialize ("Hsub" with "Hg"); iSpecialize ("HpT1" with "Hg"); iNext i. iApply (path_wp_wand with "HpT1"); iIntros "%w HvT1 {Hg}". iApply ("Hsub" with "HvT1"). diff --git a/theories/Dot/semtyp_lemmas/prims_lr.v b/theories/Dot/semtyp_lemmas/prims_lr.v index 9f1f0989..b54fe98e 100644 --- a/theories/Dot/semtyp_lemmas/prims_lr.v +++ b/theories/Dot/semtyp_lemmas/prims_lr.v @@ -46,13 +46,13 @@ Section Sec. Import path_wp. Lemma sP_Nat_I Γ n : ⊢ Γ s⊨p pv (vint n) : oInt, 0. Proof. - iIntros "!> %ρ * _ /="; + pupd; iIntros "!> %ρ * _ /="; rewrite path_wp_pv_eq /= /pure_interp_prim /prim_evals_to; naive_solver. Qed. Lemma sP_Bool_I Γ b : ⊢ Γ s⊨p pv (vbool b) : oBool, 0. Proof. - iIntros "!> %ρ _ /="; + pupd; iIntros "!> %ρ _ /="; rewrite path_wp_pv_eq /= /pure_interp_prim /prim_evals_to; naive_solver. Qed. @@ -69,7 +69,7 @@ Section Sec. Γ s⊨ e1 : oPrim B1 -∗ Γ s⊨ tun u e1 : oPrim Br. Proof. - iIntros ">He1 !> %ρ Hg /=". + pupd; iIntros "#He1 !> %ρ Hg /=". wp_bind (UnCtx _); wp_wapply "(He1 Hg)"; iIntros "%v1 %Ha1 /=". by iApply wp_wand; [iApply wp_un|iIntros (? [??])]. Qed. @@ -89,7 +89,7 @@ Section Sec. Γ s⊨ e2 : oPrim B2 -∗ Γ s⊨ tbin b e1 e2 : oPrim Br. Proof. - iIntros ">He1 >He2 !> /= %ρ #Hg". + pupd; iIntros "#He1 #He2 !> /= %ρ #Hg". wp_bind (BinLCtx _ _); wp_wapply "(He1 Hg)"; iIntros "%v1 %Ha1 /=". wp_bind (BinRCtx _ _); wp_wapply "(He2 Hg)"; iIntros "{Hg} %v2 %Ha2 /=". unfold pure_interp_prim in *; ev. @@ -106,7 +106,7 @@ Section Sec. Γ s⊨ e : oBool -∗ Γ s⊨ e1 : T -∗ Γ s⊨ e2 : T -∗ Γ s⊨ tif e e1 e2 : T. Proof. - iIntros ">He >He1 >He2 !> /= %ρ #Hg". + pupd; iIntros "#He #He1 #He2 !> /= %ρ #Hg". wp_bind (IfCtx _ _); wp_wapply "(He Hg)". rewrite /=/pure_interp_prim/=; iIntros (v (b & ->)). case: b; wp_pure; [iApply ("He1" with "Hg") | iApply ("He2" with "Hg")]. diff --git a/theories/Dot/semtyp_lemmas/tproj_lr.v b/theories/Dot/semtyp_lemmas/tproj_lr.v index 6619f663..99e8d281 100644 --- a/theories/Dot/semtyp_lemmas/tproj_lr.v +++ b/theories/Dot/semtyp_lemmas/tproj_lr.v @@ -50,7 +50,7 @@ Section existentials. oLaterN i (oShift S) :: Γ s⊨ T <:[i] oShift U -∗ Γ s⊨ oExists S T <:[i] U. Proof. - iIntros "/= >#Hstp !> %ρ Hg %v"; iApply impl_laterN. + pupd; iIntros "/= #Hstp !> %ρ Hg %v"; iApply impl_laterN. iDestruct 1 as (w) "[HS HT]". iApply ("Hstp" $! (w .: ρ) with "[$Hg $HS] HT"). Qed. @@ -61,7 +61,7 @@ Section existentials. Γ s⊨ T <:[i] opSubst p U -∗ Γ s⊨ T <:[i] oExists S U. Proof. - iIntros "/= >#HpS >#Hstp !> %ρ #Hg". + pupd; iIntros "/= #HpS #Hstp !> %ρ #Hg". iSpecialize ("HpS" with "Hg"); iSpecialize ("Hstp" with "Hg"); iNext i. iApply (subtype_trans with "Hstp"); iIntros "%v HvUp". iDestruct (path_wp_agree with "HpS HvUp") as (w ?) "Hgoal". @@ -167,7 +167,7 @@ Section type_proj. Γ s⊨ T <:[i] U -∗ Γ s⊨ oProj A T <:[i] oProj A U. Proof. - iIntros ">#Hsub !> %ρ Hg %v"; iSpecialize ("Hsub" with "Hg"); iNext i. + pupd; iIntros "#Hsub !> %ρ Hg %v"; iSpecialize ("Hsub" with "Hg"); iNext i. (** From [T <: U] we must show [T#A <: U#A], that is, that any [v] in [T#A] is in [U#A]. Recall the definition of [T#A]: @@ -192,7 +192,7 @@ Section type_proj. Lemma sProj_Stp_U A Γ L U i : ⊢ Γ s⊨ oProj A (oTMem A L U) <:[i] U. Proof. - iIntros "!> %ρ Hg %v"; iNext i. + pupd; iIntros "!> %ρ Hg %v"; iNext i. rewrite oProjN_eq; iDestruct 1 as (w) "(HTw & HselV)". (* After unfolding definitions, we must show that [v] is in [U], @@ -215,7 +215,7 @@ Section type_proj. Γ s⊨ oProj A T <:[i] U. Proof. iIntros "#Hp". - iApply sStp_Trans; first iApply (sProj_Stp_Proj with "Hp"). + iApply sStp_Trans; first iApply (sProj_Stp_Proj with "[Hp]"). by iIntros "!>". iApply sProj_Stp_U. Qed. @@ -235,7 +235,7 @@ Section type_proj. Γ s⊨p p : T, i -∗ Γ s⊨ oSel p A <:[i] oProj A T. Proof. - iIntros "#Hp". rewrite -oProj_oSing. + rewrite -oProj_oSing. iIntros "Hp". iApply sProj_Stp_Proj. iApply (sSngl_Stp_Self with "Hp"). Qed. @@ -347,18 +347,18 @@ Section type_proj. (** *** Auxiliary lemma. *) Lemma oProj_oTMem A (T : olty Σ) σ s : s ↝[ σ ] shift T -∗ - |==> ∀ ρ, oLater T anil ρ ⊆ oProj A (oTMemL A T T) anil ρ. + ∀ ρ, oLater T anil ρ ⊆ oProj A (oTMemL A T T) anil ρ. Proof. (** To prove this theorem, we create an auxiliary definition body [auxD] and an auxiliary object [auxV], whose type member [A] points to [shift T]. *) - iIntros "#Hs". + iIntros "#Hs !>". set auxD := dtysem σ s; set auxV := (vobj [(A, auxD)]). iAssert ([] s⊨p pv (vobj [(A, auxD)]) : - oMu (oTMemL A (shift T) (shift T)), 0) as ">#HwT". + oMu (oTMemL A (shift T) (shift T)), 0) as "#>#HwT". by iApply sP_Obj_I; iApply sD_Sing'; iApply (sD_Typ with "Hs"). - iIntros "!> %ρ %v #HT"; rewrite oProjN_eq. + iIntros "!> !> %ρ %v #HT"; rewrite oProjN_eq. iAssert (oTMemL A T T anil ρ auxV.[ρ])%I as "{HwT} #Hw". { rewrite -(path_wp_pv_eq auxV.[ρ]). by iApply "HwT". } @@ -371,10 +371,10 @@ Section type_proj. coveringσ σ T → ⊢ Γ s⊨ oLater T <:[i] oProj A (oTMemL A T T). Proof. - intros HclT. + iIntros "%HclT !>". iMod (leadsto_envD_equiv_alloc_shift HclT) as (s) "Hs". - iMod (oProj_oTMem A with "Hs") as "#Hs". - iIntros "!> %ρ _ !>". iApply "Hs". + iDestruct (oProj_oTMem A with "Hs") as "{Hs} #>#Hs". + iIntros "!>!> %ρ _ !>". iApply "Hs". Qed. Lemma Proj_Stp_TMem {Γ i A n} {T : ty} (HclT : nclosed T n) : diff --git a/theories/Dot/syntyp_lemmas/path_repl_lr_syn.v b/theories/Dot/syntyp_lemmas/path_repl_lr_syn.v index 0eccbfb7..dd193467 100644 --- a/theories/Dot/syntyp_lemmas/path_repl_lr_syn.v +++ b/theories/Dot/syntyp_lemmas/path_repl_lr_syn.v @@ -49,7 +49,7 @@ Section path_repl. Lemma P_Mu_E {Γ T T' p i} (Hrepl : T .Tp[ p /]~ T') : Γ ⊨p p : TMu T, i -∗ Γ ⊨p p : T', i. Proof. - rw. rewrite sP_Mu_E; iIntros ">#Hp !> %ρ Hg /=". + rw. rewrite sP_Mu_E. pupd; iIntros "#Hp !> %ρ Hg /=". iApply (strong_path_wp_wand with "(Hp Hg)"); iIntros "**". by rewrite (sem_psubst_one_eq Hrepl) ?alias_paths_pv_eq_1. Qed. @@ -57,7 +57,7 @@ Section path_repl. Lemma P_Mu_I {Γ T T' p i} (Hrepl : T .Tp[ p /]~ T') : Γ ⊨p p : T', i -∗ Γ ⊨p p : TMu T, i. Proof. - rw. rewrite -sP_Mu_I; iIntros ">#Hp !> %ρ Hg /=". + rw. rewrite -sP_Mu_I. pupd; iIntros "#Hp !> %ρ Hg /=". iApply (strong_path_wp_wand with "(Hp Hg)"); iIntros "**". by rewrite (sem_psubst_one_eq Hrepl) ?alias_paths_pv_eq_1. Qed. @@ -67,7 +67,7 @@ Section path_repl. Lemma P_Mu_E' {Γ T T' p i} (Hrepl : T .Tp[ p /]~ T') : Γ ⊨p p : TMu T, i -∗ Γ ⊨p p : T', i. Proof. - rw. iIntros ">#Hp !> %ρ Hg /=". + rw. pupd; iIntros "#Hp !> %ρ Hg /=". iApply (strong_path_wp_wand with "(Hp Hg)"); iIntros "**". by rewrite oMu_eq -(psubst_one_repl Hrepl) ?alias_paths_pv_eq_1. Qed. @@ -75,7 +75,7 @@ Section path_repl. Lemma P_Mu_I' {Γ T T' p i} (Hrepl : T .Tp[ p /]~ T') : Γ ⊨p p : T', i -∗ Γ ⊨p p : TMu T, i. Proof. - rw. iIntros ">#Hp !> %ρ Hg /=". + rw. pupd; iIntros "#Hp !> %ρ Hg /=". iApply (strong_path_wp_wand with "(Hp Hg)"); iIntros "**". by rewrite oMu_eq -(psubst_one_repl Hrepl) ?alias_paths_pv_eq_1. Qed. @@ -86,8 +86,8 @@ Section path_repl. (*────────────────────────────────────────────────────────────*) Γ ⊨ tapp e1 (path2tm p2) : T2'. Proof. - rw. iIntros ">He1 >#Hp2". - iDestruct (sT_All_E_p with "He1 Hp2") as ">Hep"; iIntros "!> %ρ #Hg". + rw. pupd'; iIntros "#He1 #Hp2 !>". + iDestruct (sT_All_E_p with "He1 Hp2") as "#>#Hep". iIntros "!> !> %ρ #Hg". iDestruct (path_wp_eq with "(Hp2 Hg)") as (pw Hal%alias_paths_pv_eq_1) "_ /=". iApply (wp_wand with "(Hep Hg)"); iIntros "{Hg} %v #Hv". iApply (sem_psubst_one_eq Hrepl Hal with "Hv"). From 7794da50122126a0094edece2214cf175a6759c2 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Mon, 29 Aug 2022 02:51:34 +0200 Subject: [PATCH 7/7] {Into,}Persistent instances --- .../Dot/examples/sem/semtyp_lemmas/sub_lr.v | 2 ++ theories/Dot/hkdot/hkdot.v | 25 ++++++++++++++++--- theories/Dot/hkdot/hkdot_syn.v | 2 -- theories/Dot/lr/dot_semtypes.v | 22 +++++++++++++++- theories/iris_extra/proofmode_extra.v | 3 +++ 5 files changed, 47 insertions(+), 7 deletions(-) diff --git a/theories/Dot/examples/sem/semtyp_lemmas/sub_lr.v b/theories/Dot/examples/sem/semtyp_lemmas/sub_lr.v index af64290c..621877e6 100644 --- a/theories/Dot/examples/sem/semtyp_lemmas/sub_lr.v +++ b/theories/Dot/examples/sem/semtyp_lemmas/sub_lr.v @@ -41,6 +41,8 @@ End Propers. Section judgment_lemmas. Context `{!dlangG Σ}. + #[global] Instance sstpi_persistent i j Γ τ1 τ2 : Persistent (sstpi i j Γ τ1 τ2) := _. + Lemma sstpi_app ρ Γ (T1 T2 : olty Σ) i j : sstpi' i j Γ T1 T2 -∗ sG⟦ Γ ⟧* ρ -∗ oClose (oLaterN i T1) ρ ⊆ oClose (oLaterN j T2) ρ. diff --git a/theories/Dot/hkdot/hkdot.v b/theories/Dot/hkdot/hkdot.v index 2248c28a..db66e5c1 100644 --- a/theories/Dot/hkdot/hkdot.v +++ b/theories/Dot/hkdot/hkdot.v @@ -58,6 +58,18 @@ Notation sf_sngl T := (sf_kintv T T). Section gen_lemmas. Context `{Hdlang : dlangG Σ} `{HswapProp : SwapPropI Σ}. + #[global] Instance sstpiK_persistent i Γ T1 T2 K : + Persistent (sstpiK i Γ T1 T2 K) := _. + + #[global] Instance sstpiK_into_persistent i Γ T1 T2 K : + IntoPersistent' (sstpiK i Γ T1 T2 K) := _. + + #[global] Instance sSkd_persistent i Γ K1 K2 : + Persistent (sSkd i Γ K1 K2) := _. + + #[global] Instance sSkd_into_persistent i Γ K1 K2 : + IntoPersistent' (sSkd i Γ K1 K2) := _. + #[global] Instance sstpiK_proper i : Proper4 (sstpiK (Σ := Σ) i). Proof. @@ -613,9 +625,9 @@ Section dot_types. s ↝[ σ ] T -∗ Γ s⊨ { l := dtysem σ s } : cTMemK l K. Proof. - rewrite sdtp_eq'. iIntros "#HTK (%φ & %Hγφ & #Hγ) !>". - iMod "HTK" as "#HTK". - iIntros "!>!>" (ρ Hpid) "Hg"; iExists (hoEnvD_inst (σ.|[ρ]) φ). + rewrite sdtp_eq'; iIntros "HTK #(%φ & %Hγφ & #Hγ)". + iRevert "HTK"; pupd; iIntros "#HTK !>". + iIntros (ρ Hpid) "Hg"; iExists (hoEnvD_inst (σ.|[ρ]) φ). iDestruct (dm_to_type_intro with "Hγ") as "-#$"; first done. iApply (sf_kind_proper' with "(HTK Hg)") => args v /=. do 1!f_equiv; symmetry. exact: Hγφ. @@ -704,6 +716,7 @@ Import defs_lr binding_lr examples_lr. Section derived. Context `{Hdlang : !dlangG Σ} `{HswapProp : SwapPropI Σ} `{!RecTyInterp Σ}. + Opaque sSkd sstpiK sptp sstpd sstpi. Lemma sT_New Γ l σ s (K : sf_kind Σ) T : @@ -850,7 +863,11 @@ Section derived. iApply (sStp_Singl_Widen with "HT"). Qed. - (* #[global] Instance : Params (@bi_wand b) 1 := {}. *) + (* #[global] Instance idstp_into_persistent Γ T ds : IntoPersistent' (idstp Γ T ds) | 0 := _. + #[global] Instance idtp_into_persistent Γ T l d : IntoPersistent' (idtp Γ T l d) | 0 := _. + #[global] Instance ietp_into_persistent Γ T e : IntoPersistent' (ietp Γ T e) | 0 := _. + #[global] Instance istpd_into_persistent Γ T1 T2 i : IntoPersistent' (istpd i Γ T1 T2) | 0 := _. + #[global] Instance iptp_into_persistent Γ T p i : IntoPersistent' (iptp Γ T p i) | 0 := _. *) (** Kind subsumption (for kinded subtyping). *) Lemma sKEq_Sub Γ (T1 T2 : oltyO Σ) (K1 K2 : sf_kind Σ) i : diff --git a/theories/Dot/hkdot/hkdot_syn.v b/theories/Dot/hkdot/hkdot_syn.v index 6a7adc64..ecf4cd6e 100644 --- a/theories/Dot/hkdot/hkdot_syn.v +++ b/theories/Dot/hkdot/hkdot_syn.v @@ -69,8 +69,6 @@ Section lemmas. apply sD_TypK_Abs_Syn. Qed. - #[local] Notation IntoPersistent' P := (IntoPersistent false P P). - #[global] Instance sstpiK_persistent i Γ T1 T2 K : IntoPersistent' (sstpiK i Γ T1 T2 K) := _. Lemma sT_New_Singl_Syn n Γ l (K : s_kind Σ n) T : oLater (oTMemK l (s_to_sf (ho_sing K (oLater V⟦T⟧)))) :: Γ s⊨ oLater V⟦T⟧ ∷[ 0 ] s_to_sf K -∗ Γ s⊨ vobj [ (l, dtysyn T) ] : oMu (oTMemK l (s_to_sf K)). diff --git a/theories/Dot/lr/dot_semtypes.v b/theories/Dot/lr/dot_semtypes.v index 580a76fd..334601ee 100644 --- a/theories/Dot/lr/dot_semtypes.v +++ b/theories/Dot/lr/dot_semtypes.v @@ -46,6 +46,24 @@ Section judgments. ∀ ρ, sG⟦Γ⟧* ρ → ▷^i path_wp p.|[ρ] (oClose τ ρ). #[global] Arguments sptp : simpl never. + + Section persistence. + Context `{!dlangG Σ}. + + (* + Avoid auto-dropping box (and unfolding) when introducing judgments persistently. + + We use cost 0 to take precedence over Iris. + + The instance for [sdtp] overlaps with [sdstp] and must take priority; since + there's no cost lower than 0, the instance for [sdtp] comes after the one for [sdstp]. + *) + #[global] Instance sdstp_into_persistent Γ Tds ds : IntoPersistent' (sdstp ds Γ Tds) | 0 := _. + #[global] Instance sdtp_into_persistent Γ Td l d : IntoPersistent' (sdtp l d Γ Td) | 0 := _. + #[global] Instance setp_into_persistent Γ T e : IntoPersistent' (setp e Γ T) | 0 := _. + #[global] Instance sstpd_into_persistent Γ T1 T2 i : IntoPersistent' (sstpd i Γ T1 T2) | 0 := _. + #[global] Instance sptp_into_persistent Γ T p i : IntoPersistent' (sptp p i Γ T) | 0 := _. + End persistence. End judgments. (** Expression typing *) @@ -280,7 +298,9 @@ Section misc_lemmas. Lemma ipwp_terminates {p T i} : [] s⊨p p : T , i ⊢ |==> ▷^i ⌜ terminates (path2tm p) ⌝. Proof. - iIntros "#>#H". + iIntros "#H". + rewrite /sptp. + iDestruct "H" as "#>#H". iSpecialize ("H" $! ids with "[//]"); rewrite hsubst_id. iApply (path_wp_terminates with "H"). Qed. diff --git a/theories/iris_extra/proofmode_extra.v b/theories/iris_extra/proofmode_extra.v index dc2b3c7f..957716f7 100644 --- a/theories/iris_extra/proofmode_extra.v +++ b/theories/iris_extra/proofmode_extra.v @@ -2,6 +2,9 @@ From iris.proofmode Require Import proofmode. From D Require Import prelude. Import bi. +(* Avoid auto-dropping box (and unfolding) when introducing judgments persistently. *) +#[global] Notation IntoPersistent' P := (IntoPersistent false P P). + Tactic Notation "iSplitWith" constr(H) "as" constr(H') := iApply (bi.and_parallel with H); iSplit; iIntros H'.