From 340e8204dfb690b918495b5dbe526ade8dec9c4c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 22 Jul 2020 21:09:01 +0200
Subject: [PATCH] Bump Iris + get rid of iAlways.
---
opam | 2 +-
theories/lang/lib/arc.v | 14 +++++-----
theories/lang/lib/lock.v | 2 +-
theories/lang/lifting.v | 28 +++++++++----------
theories/lifetime/frac_borrow.v | 4 +--
theories/lifetime/lifetime.v | 2 +-
theories/lifetime/model/borrow_sep.v | 2 +-
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/rwlock.v | 4 +--
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 +++---
30 files changed, 93 insertions(+), 93 deletions(-)
diff --git a/opam b/opam
index c0971646..fd87ed86 100644
--- a/opam
+++ b/opam
@@ -14,7 +14,7 @@ the type system, and safety proof for some Rust libraries.
"""
depends: [
- "coq-iris" { (= "dev.2020-07-15.1.6ae02201") | (= "dev") }
+ "coq-iris" { (= "dev.2020-07-22.0.1e8432a9") | (= "dev") }
]
build: [make "-j%{jobs}%"]
diff --git a/theories/lang/lib/arc.v b/theories/lang/lib/arc.v
index 203abf73..67b08374 100644
--- a/theories/lang/lib/arc.v
+++ b/theories/lang/lib/arc.v
@@ -268,25 +268,25 @@ Section arc.
iModIntro. wp_let. wp_op. wp_bind (CAS _ _ _). iInv N as (st) "[>Hâ— H]" "Hclose1".
iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]".
iDestruct (arc_tok_auth_val with "Hâ— Hown") as %(?&strong'&?&?&[-> _]).
- iDestruct "H" as (q) "(>#Hq & [HP1 HP1'] & Hl & Hw)". iDestruct "Hq" as %Hq.
+ iDestruct "H" as (qq) "(>#Hq & [HP1 HP1'] & Hl & Hw)". iDestruct "Hq" as %Hq.
destruct (decide (strong = strong')) as [->|?].
- wp_apply (wp_cas_int_suc with "Hl"). iIntros "Hl".
iMod (own_update with "Hâ—") as "[Hâ— Hown']".
{ apply auth_update_alloc, prod_local_update_1,
- (op_local_update_discrete _ _ (Some (Cinl ((q/2)%Qp, 1%positive, None))))
+ (op_local_update_discrete _ _ (Some (Cinl ((qq/2)%Qp, 1%positive, None))))
=>-[/= Hqa ?]. split;[split|]=>//=; last by rewrite left_id.
- apply frac_valid'. rewrite -Hq comm_L -{2}(Qp_div_2 q).
+ apply frac_valid'. rewrite -Hq comm_L -{2}(Qp_div_2 qq).
apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (_ / _)%Qp).
apply Qcplus_le_mono_r, Qp_ge_0. }
iMod ("Hclose2" with "Hown") as "HP". iModIntro.
iMod ("Hclose1" with "[Hl Hw Hâ— HP1']") as "_".
{ iExists _. iFrame. iExists _. rewrite /= [xH â‹… _]comm_L. iFrame.
- rewrite [(q / 2)%Qp â‹… _]comm frac_op' -[(_ + _)%Qp]assoc Qp_div_2 left_id_L. auto. }
+ rewrite [(qq / 2)%Qp â‹… _]comm frac_op' -[(_ + _)%Qp]assoc Qp_div_2 left_id_L. auto. }
iModIntro. wp_case. iApply "HΦ". iFrame.
- wp_apply (wp_cas_int_fail with "Hl"); [congruence|]. iIntros "Hl".
iMod ("Hclose2" with "Hown") as "HP". iModIntro.
iMod ("Hclose1" with "[-HP HΦ]") as "_".
- { iExists _. iFrame. iExists q. auto with iFrame. }
+ { iExists _. iFrame. iExists qq. auto with iFrame. }
iModIntro. wp_case. iApply ("IH" with "HP HΦ").
Qed.
@@ -309,7 +309,7 @@ Section arc.
iApply fupd_wp. iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]".
iDestruct (arc_tok_auth_val with "Hâ— Hown") as %(?&?& wlock & weak' &[-> _]).
iMod ("Hclose2" with "Hown") as "HP". iModIntro.
- iDestruct "H" as (q) "(>Heq & HP1 & Hl & Hl1)". iDestruct "Heq" as %Heq.
+ iDestruct "H" as (qq) "(>Heq & HP1 & Hl & Hl1)". iDestruct "Heq" as %Heq.
destruct (decide (weak = weak' ∧ wlock = None)) as [[<- ->]|Hw].
- wp_apply (wp_cas_int_suc with "Hl1"). iIntros "Hl1".
iMod (own_update with "Hâ—") as "[Hâ— Hown']".
@@ -509,7 +509,7 @@ Section arc.
iIntros "#INV !# * [Hown HP1] HΦ". iLöb as "IH".
wp_rec. wp_bind (!ˢᶜ_)%E. iInv N as (st) "[>H◠H]" "Hclose".
iDestruct (arc_tok_auth_val with "Hâ— Hown") as %(?& s &?&?&[-> _]).
- iDestruct "H" as (?) "(? & ? & ? & ?)". wp_read.
+ iDestruct "H" as (x') "(? & ? & ? & ?)". wp_read.
iMod ("Hclose" with "[-Hown HP1 HΦ]") as "_". { iExists _. auto with iFrame. }
iModIntro. wp_let. wp_op. wp_bind (CAS _ _ _). iInv N as (st) "[>Hâ— H]" "Hclose".
iDestruct (arc_tok_auth_val with "Hâ— Hown") as %(q' & s' & wl & w &[-> Hqq']).
diff --git a/theories/lang/lib/lock.v b/theories/lang/lib/lock.v
index 0d50e7ce..321a0789 100644
--- a/theories/lang/lib/lock.v
+++ b/theories/lang/lib/lock.v
@@ -36,7 +36,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.
(** The main proofs. *)
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index 3b0aa996..b6bff0b0 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -140,7 +140,7 @@ Lemma wp_alloc E (n : Z) :
{{{ l (sz: nat), RET LitV $ LitLoc l; ⌜n = sz⌠∗ †l…sz ∗ l ↦∗ repeat (LitV LitPoison) sz }}}.
Proof.
iIntros (? Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
- iIntros (σ1 ???) "Hσ !>"; iSplit; first by auto.
+ iIntros (σ1 κ κs n') "Hσ !>"; iSplit; first by auto.
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
iMod (heap_alloc with "Hσ") as "[Hσ Hl]"; [done..|].
iModIntro; iSplit=> //. iFrame.
@@ -154,7 +154,7 @@ Lemma wp_free E (n:Z) l vl :
{{{ RET LitV LitPoison; True }}}.
Proof.
iIntros (? Φ) "[>Hmt >Hf] HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
- iIntros (σ1 ???) "Hσ".
+ iIntros (σ1 κ κs n') "Hσ".
iMod (heap_free _ _ _ n with "Hσ Hmt Hf") as "(% & % & Hσ)"=>//.
iModIntro; iSplit; first by auto.
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
@@ -166,7 +166,7 @@ Lemma wp_read_sc E l q v :
{{{ RET v; l ↦{q} v }}}.
Proof.
iIntros (?) ">Hv HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
- iIntros (σ1 ???) "Hσ". iDestruct (heap_read with "Hσ Hv") as %[n ?].
+ iIntros (σ1 κ κs n) "Hσ". iDestruct (heap_read with "Hσ Hv") as %[m ?].
iModIntro; iSplit; first by eauto.
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
@@ -176,15 +176,15 @@ Lemma wp_read_na E l q v :
{{{ ▷ l ↦{q} v }}} Read Na1Ord (Lit $ LitLoc l) @ E
{{{ RET v; l ↦{q} v }}}.
Proof.
- iIntros (Φ) ">Hv HΦ". iApply wp_lift_head_step; auto. iIntros (σ1 ???) "Hσ".
- iMod (heap_read_na with "Hσ Hv") as (n) "(% & Hσ & Hσclose)".
+ iIntros (Φ) ">Hv HΦ". iApply wp_lift_head_step; auto. iIntros (σ1 κ κs n) "Hσ".
+ iMod (heap_read_na with "Hσ Hv") as (m) "(% & Hσ & Hσclose)".
iMod (fupd_intro_mask' _ ∅) as "Hclose"; first set_solver.
iModIntro; iSplit; first by eauto.
iNext; iIntros (e2 σ2 efs Hstep); inv_head_step. iMod "Hclose" as "_".
iModIntro. iFrame "Hσ". iSplit; last done.
clear dependent σ1 n.
iApply wp_lift_atomic_head_step_no_fork; auto.
- iIntros (σ1 ???) "Hσ". iMod ("Hσclose" with "Hσ") as (n) "(% & Hσ & Hv)".
+ iIntros (σ1 κ' κs' n') "Hσ". iMod ("Hσclose" with "Hσ") as (n) "(% & Hσ & Hv)".
iModIntro; iSplit; first by eauto.
iNext; iIntros (e2 σ2 efs Hstep) "!>"; inv_head_step.
iFrame "Hσ". iSplit; [done|]. by iApply "HΦ".
@@ -196,7 +196,7 @@ Lemma wp_write_sc E l e v v' :
{{{ RET LitV LitPoison; l ↦ v }}}.
Proof.
iIntros (<- Φ) ">Hv HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
- iIntros (σ1 ???) "Hσ". iDestruct (heap_read_1 with "Hσ Hv") as %?.
+ iIntros (σ1 κ κs n) "Hσ". iDestruct (heap_read_1 with "Hσ Hv") as %?.
iMod (heap_write _ _ _ v with "Hσ Hv") as "[Hσ Hv]".
iModIntro; iSplit; first by eauto.
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
@@ -209,14 +209,14 @@ Lemma wp_write_na E l e v v' :
{{{ RET LitV LitPoison; l ↦ v }}}.
Proof.
iIntros (<- Φ) ">Hv HΦ".
- iApply wp_lift_head_step; auto. iIntros (σ1 ???) "Hσ".
+ iApply wp_lift_head_step; auto. iIntros (σ1 κ κs n) "Hσ".
iMod (heap_write_na with "Hσ Hv") as "(% & Hσ & Hσclose)".
iMod (fupd_intro_mask' _ ∅) as "Hclose"; first set_solver.
iModIntro; iSplit; first by eauto.
iNext; iIntros (e2 σ2 efs Hstep); inv_head_step. iMod "Hclose" as "_".
iModIntro. iFrame "Hσ". iSplit; last done.
clear dependent σ1. iApply wp_lift_atomic_head_step_no_fork; auto.
- iIntros (σ1 ???) "Hσ". iMod ("Hσclose" with "Hσ") as "(% & Hσ & Hv)".
+ iIntros (σ1 κ' κs' n') "Hσ". iMod ("Hσclose" with "Hσ") as "(% & Hσ & Hv)".
iModIntro; iSplit; first by eauto.
iNext; iIntros (e2 σ2 efs Hstep) "!>"; inv_head_step.
iFrame "Hσ". iSplit; [done|]. by iApply "HΦ".
@@ -230,7 +230,7 @@ Lemma wp_cas_int_fail E l q z1 e2 lit2 zl :
Proof.
iIntros (<- ? Φ) ">Hv HΦ".
iApply wp_lift_atomic_head_step_no_fork; auto.
- iIntros (σ1 ???) "Hσ". iDestruct (heap_read with "Hσ Hv") as %[n ?].
+ iIntros (σ1 κ κs n) "Hσ". iDestruct (heap_read with "Hσ Hv") as %[m ?].
iModIntro; iSplit; first by eauto.
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step; inv_lit.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
@@ -244,7 +244,7 @@ Lemma wp_cas_suc E l lit1 e2 lit2 :
Proof.
iIntros (<- ? Φ) ">Hv HΦ".
iApply wp_lift_atomic_head_step_no_fork; auto.
- iIntros (σ1 ???) "Hσ". iDestruct (heap_read_1 with "Hσ Hv") as %?.
+ iIntros (σ1 κ κs n) "Hσ". iDestruct (heap_read_1 with "Hσ Hv") as %?.
iModIntro; iSplit; first (destruct lit1; by eauto).
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step; [inv_lit|].
iMod (heap_write with "Hσ Hv") as "[$ Hv]".
@@ -274,7 +274,7 @@ Lemma wp_cas_loc_fail E l q q' q1 l1 v1' e2 lit2 l' vl' :
Proof.
iIntros (<- ? Φ) "(>Hl & >Hl' & >Hl1) HΦ".
iApply wp_lift_atomic_head_step_no_fork; auto.
- iIntros (σ1 ???) "Hσ". iDestruct (heap_read with "Hσ Hl") as %[nl ?].
+ iIntros (σ1 κ κs n) "Hσ". iDestruct (heap_read with "Hσ Hl") as %[nl ?].
iDestruct (heap_read with "Hσ Hl'") as %[nl' ?].
iDestruct (heap_read with "Hσ Hl1") as %[nl1 ?].
iModIntro; iSplit; first by eauto.
@@ -292,7 +292,7 @@ Lemma wp_cas_loc_nondet E l l1 e2 l2 ll :
Proof.
iIntros (<- Φ) ">Hv HΦ".
iApply wp_lift_atomic_head_step_no_fork; auto.
- iIntros (σ1 ???) "Hσ". iDestruct (heap_read_1 with "Hσ Hv") as %?.
+ iIntros (σ1 κ κs n) "Hσ". iDestruct (heap_read_1 with "Hσ Hv") as %?.
iModIntro; iSplit; first (destruct (decide (ll = l1)) as [->|]; by eauto).
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step; last lia.
- inv_lit. iModIntro; iSplit; [done|]; iFrame "Hσ".
@@ -313,7 +313,7 @@ Proof.
[done|solve_exec_safe|solve_exec_puredet|].
iApply wp_value. by iApply Hpost.
- iApply wp_lift_atomic_head_step_no_fork; subst=>//.
- iIntros (σ1 ???) "Hσ1". iModIntro. inv_head_step.
+ iIntros (σ1 κ κs n') "Hσ1". iModIntro. inv_head_step.
iSplitR.
{ iPureIntro. repeat eexists. econstructor. eapply BinOpEqFalse. by auto. }
(* We need to do a little gymnastics here to apply Hne now and strip away a
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index e844bbda..e666a130 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -30,7 +30,7 @@ Section frac_bor.
▷ □ (∀ q, φ q ↔ φ' q) -∗ &frac{κ} φ -∗ &frac{κ} φ'.
Proof.
iIntros "#Hφφ' H". iDestruct "H" as (γ κ') "[? Hφ]". iExists γ, κ'. iFrame.
- iApply (at_bor_iff with "[Hφφ'] Hφ"). iNext. iAlways.
+ iApply (at_bor_iff with "[Hφφ'] Hφ"). iNext. iModIntro.
iSplit; iIntros "H"; iDestruct "H" as (q) "[H ?]"; iExists q; iFrame; by iApply "Hφφ'".
Qed.
@@ -137,7 +137,7 @@ End frac_bor.
Lemma frac_bor_lft_incl `{!invG Σ, !lftG Σ, !frac_borG Σ} κ κ' q:
lft_ctx -∗ &frac{κ}(λ q', (q * q').[κ']) -∗ κ ⊑ κ'.
Proof.
- iIntros "#LFT#Hbor". iApply lft_incl_intro. iAlways. iSplitR.
+ iIntros "#LFT#Hbor". iApply lft_incl_intro. iModIntro. iSplitR.
- iIntros (q') "Hκ'".
iMod (frac_bor_acc with "LFT Hbor Hκ'") as (q'') "[>? Hclose]". done.
iExists _. iFrame. iIntros "!>Hκ'". iApply "Hclose". auto.
diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index 13271eb5..ae9358d0 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -111,7 +111,7 @@ Qed.
Lemma bor_iff_proper κ P P': ▷ □ (P ↔ P') -∗ □ (&{κ}P ↔ &{κ}P').
Proof.
iIntros "#HP !#". iSplit; iIntros "?"; iApply bor_iff; try done.
- iNext. iAlways. iSplit; iIntros "?"; iApply "HP"; done.
+ iNext. iModIntro. iSplit; iIntros "?"; iApply "HP"; done.
Qed.
Lemma bor_later E κ P :
diff --git a/theories/lifetime/model/borrow_sep.v b/theories/lifetime/model/borrow_sep.v
index 61471b2b..3f17636a 100644
--- a/theories/lifetime/model/borrow_sep.v
+++ b/theories/lifetime/model/borrow_sep.v
@@ -120,7 +120,7 @@ Proof.
iAssert (&{κ}(P ∗ Q))%I with "[H◯ Hslice]" as "$".
{ rewrite /bor /raw_bor /idx_bor_own. iExists (κ1 ⊓ κ2).
iSplit; first by iApply (lft_incl_glb with "Hκ1 Hκ2").
- iExists γ. iFrame. iExists _. iFrame. iNext. iAlways.
+ iExists γ. iFrame. iExists _. iFrame. iNext. iModIntro.
by iSplit; iIntros "[HP HQ]"; iSplitL "HP"; (iApply "HPP'" || iApply "HQQ'"). }
iApply "Hclose". iExists A, I. iFrame. rewrite big_sepS_later.
iApply "Hclose'". iLeft. iFrame "%". iExists Pb, Pi. iFrame. iExists _.
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index b9b2fbee..f74160d1 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.
rewrite /lft_inv. iIntros (κ Hκ) "[[[_ %]|[$ _]] _]". set_solver. }
destruct (minimal_exists_L (⊂) Kalive)
as (κ & [Hκalive HκK]%elem_of_filter & Hκmin); first done.
@@ -122,7 +122,7 @@ Proof.
{ iNext. rewrite /lfts_inv /own_alft_auth.
iExists (<[Λ:=true]>A), I. rewrite /to_alftUR fmap_insert; iFrame.
iApply (@big_sepS_impl with "[$Hinv]").
- iAlways. rewrite /lft_inv. iIntros (κ ?) "[[Hκ %]|[Hκ %]]".
+ iModIntro. rewrite /lft_inv. iIntros (κ ?) "[[Hκ %]|[Hκ %]]".
- iLeft. iFrame "Hκ". iPureIntro. by apply lft_alive_in_insert.
- iRight. iFrame "Hκ". iPureIntro. by apply lft_dead_in_insert. }
iModIntro; iExists {[ Λ ]}.
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 8d7d0ddf..390bf7ae 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -386,14 +386,14 @@ Lemma raw_bor_iff i P P' : ▷ □ (P ↔ P') -∗ raw_bor i P -∗ raw_bor i 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 209a50a5..1dd2d629 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -276,7 +276,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 627bd6a4..b7ac9370 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -151,7 +151,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]".
@@ -178,7 +178,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 %->.
@@ -266,7 +266,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]".
@@ -291,7 +291,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.
@@ -783,9 +783,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†]").
+ wp_apply (wp_delete _ _ _ (_::_::vl1) with "[H1 H2 H3 H†]").
{ 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 1cdd3aab..ca2dc5ca 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 e1935d62..72e08c6d 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -101,7 +101,7 @@ Section mutex.
iExists _. iFrame "Hincl". iApply (at_bor_iff with "[] Hshr"). iNext.
iApply lock_proto_iff_proper. iApply bor_iff_proper. iNext.
iApply heap_mapsto_pred_iff_proper.
- iAlways; iIntros; iSplit; iIntros; by iApply "Howni".
+ iModIntro; iIntros; iSplit; iIntros; by iApply "Howni".
Qed.
Global Instance mutex_proper E L :
@@ -122,7 +122,7 @@ Section mutex.
iExists _. iFrame "Hincl". iApply (at_bor_iff with "[] Hshr"). iNext.
iApply lock_proto_iff_proper. iApply bor_iff_proper. iNext.
iApply heap_mapsto_pred_iff_proper.
- iAlways; iIntros; iSplit; iIntros; by iApply send_change_tid.
+ 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 d0f2e34e..cbd04b88 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -91,7 +91,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.
@@ -100,10 +100,10 @@ Section mguard.
iApply (at_bor_iff with "[] Hinv"). iNext.
iApply lock_proto_iff_proper. 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. iNext.
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 36eadb4f..e017caaf 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -184,7 +184,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]".
@@ -211,7 +211,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 %->.
@@ -689,7 +689,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.
@@ -784,7 +784,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.
@@ -874,7 +874,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.
@@ -1006,7 +1006,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 9680aee6..6c3e1e05 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -57,7 +57,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]".
@@ -82,7 +82,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.
@@ -132,7 +132,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.
@@ -380,7 +380,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 6f403685..108291c4 100644
--- a/theories/typing/lib/refcell/ref.v
+++ b/theories/typing/lib/refcell/ref.v
@@ -83,7 +83,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 25dc3ea2..172ae8ee 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -317,8 +317,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.
@@ -330,15 +330,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 d58a9b07..dd212d5d 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -81,7 +81,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;
@@ -192,7 +192,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 0ba4b8eb..4c92b64d 100644
--- a/theories/typing/lib/refcell/refmut.v
+++ b/theories/typing/lib/refcell/refmut.v
@@ -88,14 +88,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 621b03cd..46f484d6 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -287,8 +287,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.
@@ -304,14 +304,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/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index c57eea56..75a24847 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -71,7 +71,7 @@ Section rwlock_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 [[|[[agν ?]?]|]|]; try done;
@@ -178,7 +178,7 @@ Section rwlock.
- iPureIntro. simpl. congruence.
- destruct vl as [|[[]|]]; try done. iDestruct "H" as "[$ H]". by iApply "Hown".
- iDestruct "H" as (a γ) "[Ha H]". iExists a, γ. iFrame.
- iApply at_bor_iff; last done. iNext; iAlways; iSplit; iIntros "H".
+ iApply at_bor_iff; last done. iNext; iModIntro; iSplit; iIntros "H".
by iApply "Hty1ty2". by iApply "Hty2ty1".
Qed.
Lemma rwlock_mono' E L ty1 ty2 :
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index 7b468ca8..8cc6561c 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -83,7 +83,7 @@ Section rwlockreadguard.
iDestruct (rwlock_inv_proper with "HL") as "#Hty1ty2"; first done.
iDestruct (rwlock_inv_proper with "HL") as "#Hty2ty1"; first by symmetry.
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' γ β) "(#Hshr & #H⊑ & #Hinv & Htok & Hown)".
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index aabe30e7..7b8576d5 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -81,13 +81,13 @@ Section rwlockwriteguard.
iDestruct (rwlock_inv_proper with "HL") as "#Hty1ty2"; first done.
iDestruct (rwlock_inv_proper with "HL") as "#Hty2ty1"; first by symmetry.
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 (γ β) "(Hb & #H⊑ & #Hinv & Hown)".
iExists γ, β. iFrame "∗#". iSplit; last iSplit.
+ 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.
+ iApply at_bor_iff; try done.
diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index 53a3a252..f6caa8ea 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. iApply (join_handle_impl with "[] Hvl"). clear tid.
iIntros "!# * Hown" (tid).
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 22cfa025..2deec3a4 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -93,7 +93,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").
@@ -140,7 +140,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.
@@ -240,7 +240,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 42bed577..c0e28c9b 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 2e690507..2d8c32ad 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 9da92246..905b05c4 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -548,14 +548,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.
@@ -643,7 +643,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 d2c80811..95d7aaf4 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -51,10 +51,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. }
@@ -81,7 +81,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.
@@ -89,7 +89,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