From 83fd962bf64cf044ec1a4a96e10940e1ba3eef47 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 23 Jul 2020 08:39:05 +0200
Subject: [PATCH] Bump Iris + get rid of iAlways.
---
opam | 2 +-
theories/lang/lock.v | 2 +-
theories/lifetime/frac_borrow.v | 8 ++++----
theories/lifetime/model/borrow_sep.v | 6 +++---
theories/lifetime/model/boxes.v | 8 ++++----
theories/lifetime/model/creation.v | 4 ++--
theories/lifetime/model/primitive.v | 4 ++--
theories/typing/function.v | 2 +-
theories/typing/lib/arc.v | 12 ++++++------
theories/typing/lib/cell.v | 2 +-
theories/typing/lib/mutex/mutex.v | 4 ++--
theories/typing/lib/mutex/mutexguard.v | 6 +++---
theories/typing/lib/rc/rc.v | 12 ++++++------
theories/typing/lib/rc/weak.v | 8 ++++----
theories/typing/lib/refcell/ref.v | 2 +-
theories/typing/lib/refcell/ref_code.v | 16 ++++++++--------
theories/typing/lib/refcell/refcell.v | 4 ++--
theories/typing/lib/refcell/refmut.v | 4 ++--
theories/typing/lib/refcell/refmut_code.v | 12 ++++++------
theories/typing/lib/rwlock/rwlockreadguard.v | 2 +-
theories/typing/lib/rwlock/rwlockwriteguard.v | 4 ++--
theories/typing/lib/spawn.v | 2 +-
theories/typing/own.v | 6 +++---
theories/typing/product.v | 2 +-
theories/typing/sum.v | 6 +++---
theories/typing/type.v | 6 +++---
theories/typing/uniq_bor.v | 8 ++++----
27 files changed, 77 insertions(+), 77 deletions(-)
diff --git a/opam b/opam
index 910aadf3..1d9bf8ec 100644
--- a/opam
+++ b/opam
@@ -16,7 +16,7 @@ This branch uses a proper weak memory model.
"""
depends: [
- "coq-gpfsl" { (= "dev.2020-07-15.0.654300d3") | (= "dev") }
+ "coq-gpfsl" { (= "dev.2020-07-22.1.6569264a") | (= "dev") }
]
build: [make "-j%{jobs}%"]
diff --git a/theories/lang/lock.v b/theories/lang/lock.v
index 5c7ad230..b3076cfc 100644
--- a/theories/lang/lock.v
+++ b/theories/lang/lock.v
@@ -67,7 +67,7 @@ Section proof.
Proof.
iIntros "#HR !#".
iSplit; iIntros "Hlck"; iApply (lock_proto_iff with "[HR] Hlck"); [done|].
- iAlways; iSplit; iIntros; by iApply "HR".
+ iModIntro; iSplit; iIntros; by iApply "HR".
Qed.
Lemma lock_interp_comparable l γ t s v R:
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index e4c6fb34..59a4ce45 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -55,7 +55,7 @@ Section frac_bor.
▷ □ (∀ q, φ q ↔ φ' q) -∗ &frac{κ}φ -∗ &frac{κ}φ'.
Proof.
iIntros "#Hφφ' H". iDestruct "H" as (γ κ' V0 φ0) "(? & ? & #Hφ0φ & ?)".
- iExists γ, κ', V0, φ0. iFrame. iNext. iAlways. iIntros (q).
+ iExists γ, κ', V0, φ0. iFrame. iNext. iModIntro. iIntros (q).
iSplit; iIntros "H".
- iApply "Hφφ'". by iApply "Hφ0φ".
- iApply "Hφ0φ". by iApply "Hφφ'".
@@ -74,7 +74,7 @@ Section frac_bor.
iMod ("Hclose" with "[] [-]") as "Hφ"; last first.
{ iExists γ, κ', V, φ. iFrame "#". iSplitR; [|iSplitR].
- iIntros "!>!>!#*". by iApply (bi.iff_refl True%I).
- - iModIntro. iNext. iAlways. iIntros (??).
+ - iModIntro. iNext. iModIntro. iIntros (??).
rewrite !bi.intuitionistically_elim. iApply ("Hfrac'" $! _ _).
- by iApply (in_at_bor_share with "[Hφ]"). }
{ iNext. iSplit. iDestruct "Hφ" as "[$ _]". iExists 1%Qp, 0, 0.
@@ -96,7 +96,7 @@ Section frac_bor.
iDestruct "H" as (κ') "(#? & #? & >_)". iExists γ, κ', V, φ. iFrame "#".
iSplitR; [|iSplitR].
+ iIntros "!> !> !# *". by iApply (bi.iff_refl True%I).
- + iModIntro. iNext. iAlways. iIntros (??).
+ + iModIntro. iNext. iModIntro. iIntros (??).
rewrite !bi.intuitionistically_elim. iApply ("Hfrac'" $! _ _).
+ by iApply in_at_bor_fake.
Qed.
@@ -217,7 +217,7 @@ Section frac_bor.
Lemma frac_bor_lft_incl `{LatBottom Lat} κ κ' q:
⎡lft_ctx⎤ -∗ &frac{κ}(λ q', (q * q').[κ']) -∗ κ ⊑ κ'.
Proof.
- iIntros "#LFT#Hbor". iApply lft_incl_intro. iAlways. iIntros (q') "Hκ'".
+ iIntros "#LFT#Hbor". iApply lft_incl_intro. iModIntro. iIntros (q') "Hκ'".
iMod (frac_bor_acc with "LFT Hbor Hκ'") as (q'') "[>Htok Hclose]". done.
iExists _. iIntros "{$Htok} !> Hκ'". by iApply "Hclose".
Qed.
diff --git a/theories/lifetime/model/borrow_sep.v b/theories/lifetime/model/borrow_sep.v
index a3fcd0ea..fdfbddf5 100644
--- a/theories/lifetime/model/borrow_sep.v
+++ b/theories/lifetime/model/borrow_sep.v
@@ -91,11 +91,11 @@ Proof.
rewrite !own_bor_op. iDestruct "Hbor" as "[[H● H◯Q] H◯P]".
iAssert (&{κ}P)%I with "[H◯P]" as "$".
{ rewrite /bor /raw_bor /idx_bor_own /=. iExists κ'. iFrame "Hκκ'". iExists γP.
- iSplitL; [by auto with iFrame|]. iExists _. iFrame "#". iNext. iAlways.
+ iSplitL; [by auto with iFrame|]. iExists _. iFrame "#". iNext. iModIntro.
iSplit; [|by auto]. iIntros "[_ H]". by iApply "H". }
iAssert (&{κ}Q)%I with "[H◯Q]" as "$".
{ rewrite /bor /raw_bor /idx_bor_own /=. iExists κ'. iFrame "Hκκ'". iExists γQ.
- iSplitL; [by auto with iFrame|]. iExists _. iFrame "#". iNext. iAlways.
+ iSplitL; [by auto with iFrame|]. iExists _. iFrame "#". iNext. iModIntro.
iSplit; [|by auto]. iIntros "[_ H]". by iApply "H". }
iMod ("Hclose" with "[-]"); [|done]. iModIntro ⎡_⎤%I. iExists A, I. iFrame.
rewrite big_sepS_later. iApply "Hclose'". iExists Vκ. iSplit; [done|].
@@ -179,7 +179,7 @@ Proof.
- iExists _. simpl. iFrame. iCombine "HV1 HV2" as "HV12".
iDestruct (monPred_in_intro with "HV12") as (V12) "(HV12' & % & %)".
iApply (monPred_in_elim _ V12). done. rewrite monPred_at_in. solve_lat.
- - iExists _. iFrame. iNext. iAlways.
+ - iExists _. iFrame. iNext. iModIntro.
by iSplit; iIntros "[HP HQ]"; iSplitL "HP"; (iApply "HPP'" || iApply "HQQ'"). }
iMod ("Hclose" with "[-]"); [|done]. iExists A, I. iFrame. rewrite big_sepS_later.
iApply "Hclose'". iExists _. iSplit; [done|]. iLeft. iSplit; [|done].
diff --git a/theories/lifetime/model/boxes.v b/theories/lifetime/model/boxes.v
index 7d42ddc2..772c9b7c 100644
--- a/theories/lifetime/model/boxes.v
+++ b/theories/lifetime/model/boxes.v
@@ -220,7 +220,7 @@ Proof.
iCombine "Hf" "HP'" as "Hf".
rewrite -big_sepM_sep big_sepM_fmap; iApply (big_sepM_fupd _ _ f).
iApply (@big_sepM_impl with "[$Hf]").
- iAlways; iIntros (γ b' ?) "[(Hγ' & #$ & #$) HΦ]".
+ iModIntro; iIntros (γ b' ?) "[(Hγ' & #$ & #$) HΦ]".
iInv N as (b) "[>Hγ _]" "Hclose".
iMod (box_own_auth_update γ with "[Hγ Hγ']") as "[Hγ $]"; first by iFrame.
iApply "Hclose". iNext; iExists (Some $ to_latT V). by iFrame.
@@ -236,7 +236,7 @@ Proof.
[∗ map] γ↦b ∈ f, box_own_auth γ (◯ Excl' None) ∗ box_own_prop γ (Φ γ) ∗
inv N (slice_inv γ (Φ γ)))%I with "[> Hf]" as "[HΦ ?]".
{ rewrite -big_sepM_sep -big_sepM_fupd. iApply (@big_sepM_impl with "[$Hf]").
- iAlways; iIntros (γ o ?) "(Hγ' & #HγΦ & #Hinv)".
+ iModIntro; iIntros (γ o ?) "(Hγ' & #HγΦ & #Hinv)".
assert (Ho : from_option (.⊑ V) False o) by eauto.
destruct o as [V'|]=>//. rewrite -Ho.
iInv N as (b) "[>Hγ HΦ]" "Hclose".
@@ -261,11 +261,11 @@ Proof.
- iMod (slice_delete_full with "Hs Hb") as (P') "(HQ & #Heq & Hb)"; try done.
iDestruct ("HQQ'" with "HQ") as "HQ'".
iMod (slice_insert_full with "HQ' Hb") as (γ') "(% & #Hs' & Hb)"; try done.
- iExists γ', _. iFrame "∗#%". iIntros "!>". do 2 iNext. iAlways. iIntros (V).
+ iExists γ', _. iFrame "∗#%". iIntros "!>". do 2 iNext. iModIntro. iIntros (V).
iRewrite "Heq". by iSplit; iIntros "[? $]"; iApply "HQQ'".
- iDestruct (slice_delete_empty with "Hs Hb") as (P') "(#Heq & Hb)"; [done|].
iMod (slice_insert_empty with "Hb") as (γ') "(% & #Hs' & Hb)"; try done.
- iExists γ', _. iFrame "∗#%". iIntros "!>". do 2 iNext. iAlways. iIntros (V).
+ iExists γ', _. iFrame "∗#%". iIntros "!>". do 2 iNext. iModIntro. iIntros (V).
iRewrite "Heq". by iSplit; iIntros "[? $]"; iApply "HQQ'".
Qed.
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index 6e71e3e0..c3525888 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -71,7 +71,7 @@ Proof.
pose (Kalive := filter (lft_alive_in A) K).
destruct (decide (Kalive = ∅)) as [HKalive|].
{ iModIntro. rewrite /Iinv. iFrame.
- iApply (@big_sepS_impl with "[$HK]"); iAlways.
+ iApply (@big_sepS_impl with "[$HK]"); iModIntro.
iIntros (κ Hκ) "[(_ & _ & %)|[$ _]]". set_solver. }
destruct (minimal_exists_L (⊂) Kalive)
as (κ & [Hκalive HκK]%elem_of_filter & Hκmin); first done.
@@ -146,7 +146,7 @@ Proof.
+ apply Hmono=>//; rewrite elem_of_difference elem_of_singleton; auto.
- rewrite (big_sepS_delete _ K) //. iSplitL "Hinv".
+ by rewrite functions.fn_lookup_insert -lat_join_sqsubseteq_l.
- + iApply (@big_sepS_impl with "[$HK]"). iAlways. iIntros (κ').
+ + iApply (@big_sepS_impl with "[$HK]"). iModIntro. iIntros (κ').
rewrite elem_of_difference elem_of_singleton. iIntros ([??]) "H".
rewrite functions.fn_lookup_insert_ne //.
Qed.
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 1d98bb66..bcda1f20 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -397,14 +397,14 @@ Lemma raw_bor_iff i P P' :
Proof.
iIntros "#HPP' HP". unfold raw_bor. iDestruct "HP" as (s) "[HiP HP]".
iExists s. iFrame. iDestruct "HP" as (P0) "[#Hiff ?]". iExists P0. iFrame.
- iNext. iAlways. iSplit; iIntros.
+ iNext. iModIntro. iSplit; iIntros.
by iApply "HPP'"; iApply "Hiff". by iApply "Hiff"; iApply "HPP'".
Qed.
Lemma idx_bor_iff κ i P P' : ▷ □ (P ↔ P') -∗ &{κ,i}P -∗ &{κ,i}P'.
Proof.
unfold idx_bor. iIntros "#HPP' [$ HP]". iDestruct "HP" as (P0) "[#HP0P Hs]".
- iExists P0. iFrame. iNext. iAlways. iSplit; iIntros.
+ iExists P0. iFrame. iNext. iModIntro. iSplit; iIntros.
by iApply "HPP'"; iApply "HP0P". by iApply "HP0P"; iApply "HPP'".
Qed.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 58801192..802638e6 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -281,7 +281,7 @@ Section typing.
+ iApply "HE'". iIntros "{$# Hf Hinh HE' LFT HE %}".
iInduction κs as [|κ κs] "IH"=> //=. iSplitL.
{ iApply lft_incl_trans; first done. iApply lft_intersect_incl_l. }
- iApply "IH". iAlways. iApply lft_incl_trans; first done.
+ iApply "IH". iModIntro. iApply lft_incl_trans; first done.
iApply lft_intersect_incl_r.
+ iSplitL; last done. iExists ϝ. iSplit; first by rewrite /= left_id.
iFrame "#∗".
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index c4335c6b..94937ba4 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -212,7 +212,7 @@ Section arc.
Next Obligation.
iIntros (ty κ κ' tid l) "#Hincl H". iDestruct "H" as (l') "[#Hl #Hshr]".
iExists _. iSplit; first by iApply frac_bor_shorten.
- iAlways. iIntros (F q) "% Htok".
+ iModIntro. iIntros (F q) "% Htok".
iMod (lft_incl_acc with "Hincl Htok") as (q'') "[Htok Hclose]"; first solve_ndisj.
iMod ("Hshr" with "[] Htok") as "Hshr2"; first done.
iModIntro. iNext. iMod "Hshr2" as "[Htok HX]".
@@ -239,7 +239,7 @@ Section arc.
type_incl ty1 ty2 -∗ type_incl (arc ty1) (arc ty2).
Proof.
iIntros "#Hincl". iPoseProof "Hincl" as "(#Hsz & #Hoincl & #Hsincl)".
- iSplit; first done. iSplit; iAlways.
+ iSplit; first done. iSplit; iModIntro.
- iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
iDestruct "Hvl" as "[(Hl1 & Hl2 & H† & Hc) | Hvl]".
{ iLeft. iFrame. iDestruct "Hsz" as %->.
@@ -338,7 +338,7 @@ Section arc.
Next Obligation.
iIntros (ty κ κ' tid l) "#Hincl H". iDestruct "H" as (l') "[#Hl #Hshr]".
iExists _. iSplit; first by iApply frac_bor_shorten.
- iAlways. iIntros (F q) "% Htok".
+ iModIntro. iIntros (F q) "% Htok".
iMod (lft_incl_acc with "Hincl Htok") as (q'') "[Htok Hclose]"; first solve_ndisj.
iMod ("Hshr" with "[] Htok") as "Hshr2"; first done.
iModIntro. iNext. iMod "Hshr2" as "[Htok HX]".
@@ -364,7 +364,7 @@ Section arc.
type_incl ty1 ty2 -∗ type_incl (weak ty1) (weak ty2).
Proof.
iIntros "#Hincl". iPoseProof "Hincl" as "(#Hsz & #Hoincl & #Hsincl)".
- iSplit; first done. iSplit; iAlways.
+ iSplit; first done. iSplit; iModIntro.
- iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
iDestruct "Hvl" as (???? ν ? ?) "(#Hpersist & Htk)".
iExists _, _, _, _, _, _, _. iFrame "#∗". by iApply arc_persist_type_incl.
@@ -884,9 +884,9 @@ Section arc.
{ iIntros "_". wp_if. unlock. iFrame. iExists (_::_). rewrite heap_mapsto_vec_cons.
iFrame. iExists 1%nat, _, []. rewrite /= right_id_L Max.max_0_r.
auto 10 with iFrame. }
- iIntros "([H† H1] & H2 & H3)". iDestruct "H1" as (vl') "[H1 Heq]".
+ iIntros "([H† H1] & H2 & H3)". iDestruct "H1" as (vl1) "[H1 Heq]".
iDestruct "Heq" as %<-. wp_if.
- wp_apply (wp_delete _ _ _ _ (_::_::vl') with "[H1 H2 H3 H†]"); [done|..].
+ wp_apply (wp_delete _ _ _ _ (_::_::vl1) with "[H1 H2 H3 H†]"); [done|..].
{ simpl. lia. }
{ rewrite 2!heap_mapsto_vec_cons shift_loc_assoc. auto with iFrame. }
iFrame. iIntros "_". iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame.
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index 352f6dc9..263bd1fa 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -39,7 +39,7 @@ Section cell.
iDestruct ("EQ" with "HE") as "(% & #Hown & #Hshr)".
iSplit; [done|iSplit; iIntros "!# * H"].
- iApply ("Hown" with "H").
- - iApply na_bor_iff; last done. iNext; iAlways; iSplit; iIntros "H";
+ - iApply na_bor_iff; last done. iNext; iModIntro; iSplit; iIntros "H";
iDestruct "H" as (vl) "[??]"; iExists vl; iFrame; by iApply "Hown".
Qed.
Lemma cell_mono' E L ty1 ty2 : eqtype E L ty1 ty2 → subtype E L (cell ty1) (cell ty2).
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index 64a09714..b82ba926 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -95,7 +95,7 @@ Section mutex.
iExists γ.
iApply lock_proto_iff_proper; [|iFrame].
iApply bor_iff_proper. iApply heap_mapsto_pred_iff_proper.
- iNext. iAlways; iIntros; iSplit; iIntros; by iApply "Howni".
+ iNext. iModIntro; iIntros; iSplit; iIntros; by iApply "Howni".
Qed.
Global Instance mutex_proper E L :
@@ -116,7 +116,7 @@ Section mutex.
iExists _. iFrame "Hincl". iDestruct "Hshr" as (γ) "Hproto".
iExists γ. iApply lock_proto_iff_proper; [|iFrame].
iApply bor_iff_proper. iApply heap_mapsto_pred_iff_proper.
- iNext. iAlways; iIntros; iSplit; iIntros; by iApply send_change_tid.
+ iNext. iModIntro; iIntros; iSplit; iIntros; by iApply send_change_tid.
Qed.
End mutex.
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index 28f36d79..de85d02c 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -89,7 +89,7 @@ Section mguard.
intros α1 α2 Hα ty1 ty2 Hty. generalize Hty. rewrite eqtype_unfold. iIntros (Hty' q) "HL".
iDestruct (Hty' with "HL") as "#Hty". clear Hty'. iDestruct (Hα with "HL") as "#Hα".
iIntros "!# #HE". iDestruct ("Hα" with "HE") as "{Hα} Hα".
- iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs) {HE Hty}". iSplit; [done|iSplit; iAlways].
+ iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs) {HE Hty}". iSplit; [done|iSplit; iModIntro].
- iIntros (tid [|[[]|][]]) "H"; try done. simpl.
iDestruct "H" as (β) "(#H⊑ & Hinv & Hown)".
iExists β. iFrame. iSplit; last iSplit.
@@ -98,10 +98,10 @@ Section mguard.
iExists γ. iApply (lock_proto_lft_mono with "Hα").
iApply lock_proto_iff_proper; [|iFrame].
iApply bor_iff_proper. iNext. iApply heap_mapsto_pred_iff_proper.
- iAlways; iIntros; iSplit; iIntros; by iApply "Ho".
+ iModIntro; iIntros; iSplit; iIntros; by iApply "Ho".
+ iApply bor_iff; last done. iIntros "!>".
iApply heap_mapsto_pred_iff_proper.
- iAlways; iIntros; iSplit; iIntros; by iApply "Ho".
+ iModIntro; iIntros; iSplit; iIntros; by iApply "Ho".
- iIntros (κ tid l) "H". iDestruct "H" as (l') "H". iExists l'.
iDestruct "H" as "[$ #H]". iIntros "!# * % Htok".
iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index e1f93314..a50131a6 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -191,7 +191,7 @@ Section rc.
Next Obligation.
iIntros (ty κ κ' tid l) "#Hincl H". iDestruct "H" as (l') "[#Hl #Hshr]".
iExists _. iSplit; first by iApply frac_bor_shorten.
- iAlways. iIntros (F q) "% Htok".
+ iModIntro. iIntros (F q) "% Htok".
iMod (lft_incl_acc with "Hincl Htok") as (q'') "[Htok Hclose]"; first solve_ndisj.
iMod ("Hshr" with "[] Htok") as "Hshr2"; first done.
iModIntro. iNext. iMod "Hshr2" as "[Htok HX]".
@@ -218,7 +218,7 @@ Section rc.
type_incl ty1 ty2 -∗ type_incl (rc ty1) (rc ty2).
Proof.
iIntros "#Hincl". iPoseProof "Hincl" as "(#Hsz & #Hoincl & #Hsincl)".
- iSplit; first done. iSplit; iAlways.
+ iSplit; first done. iSplit; iModIntro.
- iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
iDestruct "Hvl" as "[(Hl1 & Hl2 & H† & Hc) | Hvl]".
{ iLeft. iFrame. iDestruct "Hsz" as %->.
@@ -691,7 +691,7 @@ Section code.
iApply (type_cont [] [ϝ ⊑ₗ []]
(λ _, [rcx ◁ box (uninit 1); r ◁ box (Σ[ ty; rc ty ])])) ;
[solve_typing..| |]; last first.
- { simpl. iAlways. iIntros (k arg). inv_vec arg. simpl_subst.
+ { simpl. iModIntro. iIntros (k arg). inv_vec arg. simpl_subst.
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing. }
iIntros (k). simpl_subst.
@@ -786,7 +786,7 @@ Section code.
iApply (type_cont [] [ϝ ⊑ₗ []]
(λ _, [rcx ◁ box (uninit 1); r ◁ box (option ty)]));
[solve_typing..| |]; last first.
- { simpl. iAlways. iIntros (k arg). inv_vec arg. simpl_subst.
+ { simpl. iModIntro. iIntros (k arg). inv_vec arg. simpl_subst.
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing. }
iIntros (k). simpl_subst.
@@ -876,7 +876,7 @@ Section code.
iApply (type_cont [] [ϝ ⊑ₗ []]
(λ _, [rcx ◁ box (uninit 1); r ◁ box (option $ &uniq{α}ty)]));
[solve_typing..| |]; last first.
- { simpl. iAlways. iIntros (k arg). inv_vec arg. simpl_subst.
+ { simpl. iModIntro. iIntros (k arg). inv_vec arg. simpl_subst.
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing. }
iIntros (k). simpl_subst.
@@ -1008,7 +1008,7 @@ Section code.
iApply (type_cont [] [ϝ ⊑ₗ []]
(λ _, [rcx ◁ box (uninit 1); r ◁ box (&uniq{α}ty)]));
[solve_typing..| |]; last first.
- { simpl. iAlways. iIntros (k arg). inv_vec arg. simpl_subst.
+ { simpl. iModIntro. iIntros (k arg). inv_vec arg. simpl_subst.
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing. }
iIntros (k). simpl_subst.
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index 7f441063..798b16c7 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -63,7 +63,7 @@ Section weak.
Next Obligation.
iIntros (ty κ κ' tid l) "#Hincl H". iDestruct "H" as (l') "[#Hl #Hshr]".
iExists _. iSplit; first by iApply frac_bor_shorten.
- iAlways. iIntros (F q) "% Htok".
+ iModIntro. iIntros (F q) "% Htok".
iMod (lft_incl_acc with "Hincl Htok") as (q'') "[Htok Hclose]"; first solve_ndisj.
iMod ("Hshr" with "[] Htok") as "Hshr2"; first done.
iModIntro. iNext. iMod "Hshr2" as "[Htok HX]".
@@ -88,7 +88,7 @@ Section weak.
type_incl ty1 ty2 -∗ type_incl (weak ty1) (weak ty2).
Proof.
iIntros "#Hincl". iPoseProof "Hincl" as "(Hsz & #Hoincl & #Hsincl)".
- iSplit; first done. iSplit; iAlways.
+ iSplit; first done. iSplit; iModIntro.
- iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
iDestruct "Hvl" as (γ ν) "(#Hpersist & Htok)".
iExists _, _. iFrame "Htok". by iApply rc_persist_type_incl.
@@ -138,7 +138,7 @@ Section code.
iApply (type_cont [] [ϝ ⊑ₗ []]
(λ _, [w ◁ box (&shr{α}(weak ty)); r ◁ box (option (rc ty))])) ;
[solve_typing..| |]; last first.
- { simpl. iAlways. iIntros (k arg). inv_vec arg. simpl_subst.
+ { simpl. iModIntro. iIntros (k arg). inv_vec arg. simpl_subst.
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing. }
iIntros (k). simpl_subst.
@@ -386,7 +386,7 @@ Section code.
iIntros (_ ϝ ret arg). inv_vec arg=>w. simpl_subst.
iApply (type_cont [] [ϝ ⊑ₗ []] (λ _, [w ◁ box (uninit 1)]));
[solve_typing..| |]; last first.
- { simpl. iAlways. iIntros (k arg). inv_vec arg. simpl_subst.
+ { simpl. iModIntro. iIntros (k arg). inv_vec arg. simpl_subst.
iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing. }
diff --git a/theories/typing/lib/refcell/ref.v b/theories/typing/lib/refcell/ref.v
index 321feb64..d24833bf 100644
--- a/theories/typing/lib/refcell/ref.v
+++ b/theories/typing/lib/refcell/ref.v
@@ -82,7 +82,7 @@ Section ref.
iIntros (α1 α2 Hα ty1 ty2 Hty q) "HL".
iDestruct (Hty with "HL") as "#Hty". iDestruct (Hα with "HL") as "#Hα".
iIntros "!# #HE". iDestruct ("Hα" with "HE") as "Hα1α2".
- iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [|iSplit; iAlways].
+ iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [|iSplit; iModIntro].
- done.
- iIntros (tid [|[[]|][|[[]|][]]]) "H"=>//=.
iDestruct "H" as (ν q' γ β ty') "(#Hshr & #H⊑ & #Hinv & Htok & Hown)".
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 81ac8abd..c76a2634 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -316,8 +316,8 @@ Section ref_functions.
iDestruct ("Hclose3" with "Hαν") as "[Hα Hν]".
iMod ("Hclose2" with "Hϝ HL") as "HL".
wp_rec. iDestruct "Hr" as "[Hr Hr†]".
- iDestruct "Hr" as (?) "[Hr H]". iDestruct "H" as (vl1 ? ->) "[#Hr1' H]".
- iDestruct "H" as (vl2 ? ->) "[#Hr2' ->]".
+ iDestruct "Hr" as (?) "[Hr H]". iDestruct "H" as (vl1 vl1' ->) "[#Hr1' H]".
+ iDestruct "H" as (vl2 vl2' ->) "[#Hr2' ->]".
destruct vl1 as [|[[|lr1|]|] []], vl2 as [|[[|lr2|]|] []]=>//=.
rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
iDestruct "Hr" as "[Hr1 Hr2]". wp_read. wp_let. wp_op. wp_read. wp_let.
@@ -329,15 +329,15 @@ Section ref_functions.
iMod (na_bor_acc with "LFT Hinv Hβ Hna") as "(INV & Hna & Hclosena)"; [done..|].
wp_seq. wp_op. wp_read.
iDestruct (refcell_inv_reading_inv with "INV Hγ")
- as (q' n) "(H↦lrc & _ & [H● H◯] & H† & Hq' & Hshr')".
- iDestruct "Hq'" as (q'') "(Hq'q'' & Hν1 & Hν2)".
- iDestruct "Hq'q''" as %Hq'q''. iMod (own_update with "H●") as "[H● ?]".
+ as (q1 n) "(H↦lrc & _ & [H● H◯] & H† & Hq1 & Hshr')".
+ iDestruct "Hq1" as (q2) "(Hq1q2 & Hν1 & Hν2)".
+ iDestruct "Hq1q2" as %Hq1q2. iMod (own_update with "H●") as "[H● ?]".
{ apply auth_update_alloc,
- (op_local_update_discrete _ _ (reading_stR (q''/2)%Qp ν))=>-[Hagv _].
+ (op_local_update_discrete _ _ (reading_stR (q2/2)%Qp ν))=>-[Hagv _].
split; [split|done].
- by rewrite /= agree_idemp.
- - apply frac_valid'. rewrite -Hq'q'' comm -{2}(Qp_div_2 q'').
- apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (q''/2)%Qp).
+ - apply frac_valid'. rewrite -Hq1q2 comm -{2}(Qp_div_2 q2).
+ apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (q2/2)%Qp).
apply Qcplus_le_mono_r, Qp_ge_0. }
wp_let. wp_read. wp_let. wp_op. wp_write.
wp_apply (wp_delete _ _ _ _ [_; _] with "[Href↦1 Href↦2 Href†]")=>//.
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index ec39aa1f..98853741 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -80,7 +80,7 @@ Section refcell_inv.
iAssert (□ (&{α}((l +ₗ 1) ↦∗: ty_own ty1 tid) -∗
&{α}((l +ₗ 1) ↦∗: ty_own ty2 tid)))%I as "#Hb".
{ iIntros "!# H". iApply bor_iff; last done.
- iNext; iAlways; iSplit; iIntros "H"; iDestruct "H" as (vl) "[Hf H]"; iExists vl;
+ iNext; iModIntro; iSplit; iIntros "H"; iDestruct "H" as (vl) "[Hf H]"; iExists vl;
iFrame; by iApply "Hown". }
iDestruct "H" as (st) "H"; iExists st;
iDestruct "H" as "($&$&H)"; destruct st as [[[[ν rw] q' ] n]|]; try done;
@@ -191,7 +191,7 @@ Section refcell.
- iPureIntro. simpl. congruence.
- destruct vl as [|[[]|]]=>//=. by iApply "Hown".
- simpl. iDestruct "H" as (a γ) "[Ha H]". iExists a, γ. iFrame.
- iApply na_bor_iff; last done. iNext; iAlways; iSplit; iIntros "H".
+ iApply na_bor_iff; last done. iNext; iModIntro; iSplit; iIntros "H".
by iApply "Hty1ty2". by iApply "Hty2ty1".
Qed.
Lemma refcell_mono' E L ty1 ty2 :
diff --git a/theories/typing/lib/refcell/refmut.v b/theories/typing/lib/refcell/refmut.v
index 0f51cf44..3776c5e7 100644
--- a/theories/typing/lib/refcell/refmut.v
+++ b/theories/typing/lib/refcell/refmut.v
@@ -87,14 +87,14 @@ Section refmut.
intros α1 α2 Hα ty1 ty2. rewrite eqtype_unfold=>Hty. iIntros (q) "HL".
iDestruct (Hty with "HL") as "#Hty". iDestruct (Hα with "HL") as "#Hα".
iIntros "!# #HE". iDestruct ("Hα" with "HE") as "Hα1α2".
- iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [|iSplit; iAlways].
+ iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [|iSplit; iModIntro].
- done.
- iIntros (tid [|[[]|][|[[]|][]]]) "H"=>//=.
iDestruct "H" as (ν γ q' β ty') "(Hb & #H⊑ & #Hinv & Hν & Hown)".
iExists ν, γ, q', β, ty'. iFrame "∗#". iSplit.
+ iApply bor_shorten; last iApply bor_iff; last done.
* iApply lft_intersect_mono; first done. iApply lft_incl_refl.
- * iNext; iAlways; iSplit; iIntros "H"; iDestruct "H" as (vl) "[??]";
+ * iNext; iModIntro; iSplit; iIntros "H"; iDestruct "H" as (vl) "[??]";
iExists vl; iFrame; by iApply "Ho".
+ by iApply lft_incl_trans.
- iIntros (κ tid l) "H /=". iDestruct "H" as (lv lrc) "H". iExists lv, lrc.
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index 7b7b7785..d5488459 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -285,8 +285,8 @@ Section refmut_functions.
iDestruct ("Hclose3" with "Hαν") as "[Hα Hν]".
iMod ("Hclose2" with "Hϝ HL") as "HL".
wp_rec. iDestruct "Hr" as "[Hr Hr†]".
- iDestruct "Hr" as (?) "[Hr H]". iDestruct "H" as (vl1 ? ->) "[Hr1' H]".
- iDestruct "H" as (vl2 ? ->) "[Hr2' ->]".
+ iDestruct "Hr" as (?) "[Hr H]". iDestruct "H" as (vl1 vl1' ->) "[Hr1' H]".
+ iDestruct "H" as (vl2 vl2' ->) "[Hr2' ->]".
destruct vl1 as [|[[|lr1|]|] []], vl2 as [|[[|lr2|]|] []]=>//=.
rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
iDestruct "Hr" as "[Hr1 Hr2]". wp_read. wp_let. wp_op. wp_read. wp_let.
@@ -302,14 +302,14 @@ Section refmut_functions.
destruct st as [[[[??]?]?]|]; last by destruct Hst as [[?|] Hst]; inversion Hst.
move:Hst=>/Some_pair_included [/Some_pair_included_total_1
[/to_agree_included /(leibniz_equiv _ _) [= <- <-] _] _].
- iDestruct "Hst" as "(H† & Hq & _)". iDestruct "Hq" as (q' Hqq') "[Hν1 Hν2]".
+ iDestruct "Hst" as "(H† & Hq & _)". iDestruct "Hq" as (q1 Hqq1) "[Hν1 Hν2]".
iMod (own_update with "H●") as "[H● ?]".
{ apply auth_update_alloc,
- (op_local_update_discrete _ _ (writing_stR (q'/2)%Qp ν))=>-[Hagv _].
+ (op_local_update_discrete _ _ (writing_stR (q1/2)%Qp ν))=>-[Hagv _].
split; [split|done].
- by rewrite /= agree_idemp.
- - apply frac_valid'. rewrite -Hqq' comm -{2}(Qp_div_2 q').
- apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (q'/2)%Qp).
+ - apply frac_valid'. rewrite -Hqq1 comm -{2}(Qp_div_2 q1).
+ apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (q1/2)%Qp).
apply Qcplus_le_mono_r, Qp_ge_0. }
wp_let. wp_read. wp_let. wp_op. wp_write.
wp_apply (wp_delete _ _ _ _ [_; _] with "[Hrefmut↦1 Hrefmut↦2 Hrefmut†]")=>//.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index d7b5b5fd..0469dc74 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -82,7 +82,7 @@ Section rwlockreadguard.
iDestruct (proj1 Hty with "HL") as "#Hty". iDestruct (Hα with "HL") as "#Hα".
iDestruct (rwlock_proto_proper with "HL") as "#Hty1ty2"; first done.
iIntros "!# #HE". iDestruct ("Hα" with "HE") as "Hα1α2".
- iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [|iSplit; iAlways].
+ iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [|iSplit; iModIntro].
- done.
- iIntros (tid [|[[]|][]]) "H"; try done.
iDestruct "H" as (ν q' γs β) "(#Hshr & #H⊑ & Htok & Hown & Hinh & Hinv)".
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index baa57227..6cfd2e84 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -82,12 +82,12 @@ Section rwlockwriteguard.
iDestruct (Hty' with "HL") as "#Hty". iDestruct (Hα with "HL") as "#Hα".
iDestruct (rwlock_proto_proper with "HL") as "#Hty1ty2"; first done.
iIntros "!# #HE". iDestruct ("Hα" with "HE") as "Hα1α2".
- iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [done|iSplit; iAlways].
+ iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [done|iSplit; iModIntro].
- iIntros (tid [|[[]|][]]) "H"; try done.
iDestruct "H" as (γs β) "(Hb & #H⊑ & Hown & Hinv)".
iExists γs, β. iFrame "Hown". iSplitL "Hb"; last iSplitR "Hinv".
+ iApply bor_iff; last done.
- iNext; iAlways; iSplit; iIntros "H"; iDestruct "H" as (vl) "[??]";
+ iNext; iModIntro; iSplit; iIntros "H"; iDestruct "H" as (vl) "[??]";
iExists vl; iFrame; by iApply "Ho".
+ by iApply lft_incl_trans.
+ iDestruct "Hinv" as (γ tyO tyS) "(W & inv)".
diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index 772d602e..2da54c52 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -30,7 +30,7 @@ Section join_handle.
Lemma join_handle_subtype ty1 ty2 :
▷ type_incl ty1 ty2 -∗ type_incl (join_handle ty1) (join_handle ty2).
Proof.
- iIntros "#Hincl". iSplit; first done. iSplit; iAlways.
+ iIntros "#Hincl". iSplit; first done. iSplit; iModIntro.
- iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
simpl. iDestruct "Hvl" as (γc γe) "Hvl". iExists γc, γe.
iApply (join_handle_impl with "[] Hvl"). iIntros "!# * Hown" (tid').
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 0677b433..03080ae6 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -94,7 +94,7 @@ Section own.
Lemma own_type_incl n m ty1 ty2 :
▷ ⌜n = m⌝ -∗ ▷ type_incl ty1 ty2 -∗ type_incl (own_ptr n ty1) (own_ptr m ty2).
Proof.
- iIntros "#Heq (#Hsz & #Ho & #Hs)". iSplit; first done. iSplit; iAlways.
+ iIntros "#Heq (#Hsz & #Ho & #Hs)". iSplit; first done. iSplit; iModIntro.
- iIntros (?[|[[| |]|][]]) "H"; try done. simpl.
iDestruct "H" as "[Hmt H†]". iNext. iDestruct ("Hsz") as %<-.
iDestruct "Heq" as %->. iFrame. iApply (heap_mapsto_pred_wand with "Hmt").
@@ -141,7 +141,7 @@ Section own.
Sync ty → Sync (own_ptr n ty).
Proof.
iIntros (Hsync κ tid1 tid2 l) "H". iDestruct "H" as (l') "[Hm #Hshr]".
- iExists _. iFrame "Hm". iAlways. iIntros (F q) "% Htok".
+ iExists _. iFrame "Hm". iModIntro. iIntros (F q) "% Htok".
iMod ("Hshr" with "[] Htok") as "Hfin"; first done. iModIntro. iNext.
iMod "Hfin" as "{Hshr} [Hshr $]". by iApply Hsync.
Qed.
@@ -241,7 +241,7 @@ Section typing.
Lemma read_own_move E L ty n :
⊢ typed_read E L (own_ptr n ty) ty (own_ptr n $ uninit ty.(ty_size)).
Proof.
- rewrite typed_read_eq. iAlways.
+ rewrite typed_read_eq. iModIntro.
iIntros ([[]|] tid F qL ?) "_ _ $ $ Hown"; try done.
iDestruct "Hown" as "[H↦ H†]". iDestruct "H↦" as (vl) "[>H↦ Hown]".
iDestruct (ty_size_eq with "Hown") as "#>%".
diff --git a/theories/typing/product.v b/theories/typing/product.v
index 9abc418e..3bc52cac 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -94,7 +94,7 @@ Section product.
iClear "∗". iIntros "!# #HE".
iDestruct ("H1" with "HE") as "#(% & #Ho1 & #Hs1)". clear H1.
iDestruct ("H2" with "HE") as "#(% & #Ho2 & #Hs2)". clear H2.
- iSplit; first by (iPureIntro; simpl; f_equal). iSplit; iAlways.
+ iSplit; first by (iPureIntro; simpl; f_equal). iSplit; iModIntro.
- iIntros (??) "H". iDestruct "H" as (vl1 vl2) "(% & Hown1 & Hown2)".
iExists _, _. iSplit. done. iSplitL "Hown1".
+ by iApply "Ho1".
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index bbfa4ab4..8af91c2e 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -130,7 +130,7 @@ Section sum.
{ iInduction Htyl as [|???? Hsub] "IH".
{ iClear "∗". iIntros "!# _". done. }
iDestruct (Hsub with "HL") as "#Hsub". iDestruct ("IH" with "HL") as "{IH} #IH".
- iAlways. iIntros "#HE". iDestruct ("Hsub" with "HE") as "(% & _ & _)".
+ iModIntro. iIntros "#HE". iDestruct ("Hsub" with "HE") as "(% & _ & _)".
iDestruct ("IH" with "HE") as %IH. iPureIntro. simpl. inversion_clear IH. by f_equal. }
iDestruct (subtype_Forall2_llctx with "HL") as "#Htyl"; first done.
iClear "HL". iIntros "!# #HE".
@@ -146,11 +146,11 @@ Section sum.
rewrite (nth_lookup_Some tyl2 _ _ ty2) //. }
clear -Hleq. iClear "∗". iSplit; last iSplit.
- simpl. by rewrite Hleq.
- - iAlways. iIntros (tid vl) "H". iDestruct "H" as (i vl' vl'') "(% & % & Hown)".
+ - iModIntro. iIntros (tid vl) "H". iDestruct "H" as (i vl' vl'') "(% & % & Hown)".
iExists i, vl', vl''. iSplit; first done.
iSplit; first by rewrite -Hleq.
iDestruct ("Hty" $! i) as "(_ & #Htyi & _)". by iApply "Htyi".
- - iAlways. iIntros (κ tid l) "H". iDestruct "H" as (i) "(Hmt & Hshr)".
+ - iModIntro. iIntros (κ tid l) "H". iDestruct "H" as (i) "(Hmt & Hshr)".
iExists i. iSplitR "Hshr".
+ rewrite /is_pad -Hleq. iDestruct ("Hty" $! i) as "(Hlen & _)".
iDestruct "Hlen" as %<-. done.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 7515f0b3..b4fe9a2d 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -551,14 +551,14 @@ Section subtyping.
Global Instance type_incl_persistent ty1 ty2 : Persistent (type_incl ty1 ty2) := _.
Lemma type_incl_refl ty : ⊢ type_incl ty ty.
- Proof. iSplit; first done. iSplit; iAlways; iIntros; done. Qed.
+ Proof. iSplit; first done. iSplit; iModIntro; iIntros; done. Qed.
Lemma type_incl_trans ty1 ty2 ty3 :
type_incl ty1 ty2 -∗ type_incl ty2 ty3 -∗ type_incl ty1 ty3.
Proof.
iIntros "(% & #Ho12 & #Hs12) (% & #Ho23 & #Hs23)".
iSplit; first (iPureIntro; etrans; done).
- iSplit; iAlways; iIntros.
+ iSplit; iModIntro; iIntros.
- iApply "Ho23". iApply "Ho12". done.
- iApply "Hs23". iApply "Hs12". done.
Qed.
@@ -646,7 +646,7 @@ Section subtyping.
□ (∀ tid vl, st1.(st_own) tid vl -∗ st2.(st_own) tid vl) -∗
type_incl st1 st2.
Proof.
- iIntros "#Hst". iSplit; first done. iSplit; iAlways.
+ iIntros "#Hst". iSplit; first done. iSplit; iModIntro.
- iIntros. iApply "Hst"; done.
- iIntros (???). iDestruct 1 as (vl) "[Hf Hown]". iExists vl. iFrame "Hf".
by iApply "Hst".
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index e0cde6e6..2667230f 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -50,10 +50,10 @@ Section uniq_bor.
iDestruct (Hty with "HL") as "#Hty". iDestruct (Hκ with "HL") as "#Hκ".
iIntros "!# #HE". iSplit; first done.
iDestruct ("Hty" with "HE") as "(_ & #Ho & #Hs)"; [done..|clear Hty].
- iSpecialize ("Hκ" with "HE"). iSplit; iAlways.
+ iSpecialize ("Hκ" with "HE"). iSplit; iModIntro.
- iIntros (? [|[[]|][]]) "H"; try done.
iApply (bor_shorten with "Hκ"). iApply bor_iff; last done.
- iNext. iAlways. iSplit; iIntros "H"; iDestruct "H" as (vl) "[??]";
+ iNext. iModIntro. iSplit; iIntros "H"; iDestruct "H" as (vl) "[??]";
iExists vl; iFrame; by iApply "Ho".
- iIntros (κ ??) "H". iAssert (κ2 ⊓ κ ⊑ κ1 ⊓ κ)%I as "#Hincl'".
{ iApply lft_intersect_mono. done. iApply lft_incl_refl. }
@@ -80,7 +80,7 @@ Section uniq_bor.
Send ty → Send (uniq_bor κ ty).
Proof.
iIntros (Hsend tid1 tid2 [|[[]|][]]) "H"; try done.
- iApply bor_iff; last done. iNext. iAlways. iApply bi.equiv_iff.
+ iApply bor_iff; last done. iNext. iModIntro. iApply bi.equiv_iff.
do 3 f_equiv. iSplit; iIntros "."; by iApply Hsend.
Qed.
@@ -88,7 +88,7 @@ Section uniq_bor.
Sync ty → Sync (uniq_bor κ ty).
Proof.
iIntros (Hsync κ' tid1 tid2 l) "H". iDestruct "H" as (l') "[Hm #Hshr]".
- iExists l'. iFrame "Hm". iAlways. iIntros (F q) "% Htok".
+ iExists l'. iFrame "Hm". iModIntro. iIntros (F q) "% Htok".
iMod ("Hshr" with "[] Htok") as "Hfin"; first done. iClear "Hshr".
iModIntro. iNext. iMod "Hfin" as "[Hshr $]". iApply Hsync. done.
Qed.
--
GitLab