diff --git a/theories/lang/arc.v b/theories/lang/arc.v
index 2018feec9168994162f1087e50fae4244b7477ad..0983259dbdc7cfc8d7aaebda96e7f11b01c6fa0d 100644
--- a/theories/lang/arc.v
+++ b/theories/lang/arc.v
@@ -7,7 +7,7 @@ From gpfsl.gps Require Import middleware protocols.
From gpfsl.logic Require Import view_invariants.
From lrust.lang Require Import notation new_delete arc_cmra.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
(* Rust Arc has a maximum number of clones to prevent overflow. We currently
don't support this. *)
@@ -242,7 +242,7 @@ Section ArcInv.
(∃ Dts, StrDowns γsw 1%Qp Dts ∗ SeenActs γw (l >> 1) Dts) ∗
StrWkTok γsw 1%Qp)%I.
- Global Instance strong_arc_timelesst t q l γi γs γw γsw : Timeless (strong_arc t q l γi γs γw γsw) := _.
+ Global Instance strong_arc_timeless t q l γi γs γw γsw : Timeless (strong_arc t q l γi γs γw γsw) := _.
Global Instance weak_arc_timeless t q l γi γs γw γsw : Timeless (weak_arc t q l γi γs γw γsw) := _.
Global Instance fake_arc_timeless l γi γs γw γsw : Timeless (fake_arc l γi γs γw γsw) := _.
@@ -326,10 +326,10 @@ Section arc.
by apply view_inv_proper, arc_inv_proper.
Qed.
- Instance strong_interp_read_persistent γi γw γsw l γs t s v :
+ Local Instance strong_interp_read_persistent γi γw γsw l γs t s v :
Persistent (strong_interp P1 (l >> 1) γi γw γsw false l γs t s v).
Proof. apply bi.exist_persistent. intros [[? []]|]; simpl; by apply _. Qed.
- Instance weak_interp_read_persistent i γs γsw l γw t s v :
+ Local Instance weak_interp_read_persistent i γs γsw l γw t s v :
Persistent (weak_interp P2 l i γs γsw false (l >> 1) γw t s v).
Proof.
intros. apply bi.exist_persistent.
@@ -730,8 +730,8 @@ Section arc.
iSplitR""; [iExists (Some (q',n))|iExists (Z.pos n)].
* iSplitL""; [done|]. by iFrame.
* iPureIntro. split; [done|split].
- + iDestruct (StrongTok_Auth_agree with "[$SA St]") as %(?&?&EQ&?).
- rewrite /StrongTok. iFrame "St". done. }
+ + iDestruct (StrongTok_Auth_agree with "[$SA St]") as %(?&?&EQ&?); [|done].
+ rewrite /StrongTok. iFrame "St". }
iIntros "!>" (t' [] v'). iDestruct 1 as "(_ & RR' & IS & Rs & St & SMA)".
iDestruct "Rs" as (z) "[% %]". subst v'.
iDestruct (GPS_SWSharedReaders_join with "SR2 RR'") as "SR". rewrite Qp_div_2.
@@ -1319,7 +1319,7 @@ Section arc.
{ rewrite /Dt'. case decide => ?; last first.
{ rewrite right_id_L /StrDowns. iFrame. by iIntros "!> !>". }
iMod (StrDowns_update _ _ _ {[t'']} with "[$SDA SD]") as "($ & $ & Cert)".
- by rewrite /StrDowns. iIntros "!> !>". by iFrame "Cert". }
+ - by rewrite /StrDowns. - iIntros "!> !>". by iFrame "Cert". }
iModIntro. iSplitL "Cert".
{ iIntros "!> _ !> !>". iExists (None, Some $ Cinl (q', n)).
do 2 (iSplit; [done|]). destruct n; simpl; [done..|].
@@ -1636,8 +1636,8 @@ Section arc.
first by iApply (WeakAuth_drop with "[$WA $Wt]").
by rewrite -Pplus_one_succ_l Pos.succ_pred. }
iIntros "!>". iSplitL "SDA".
- { rewrite /Q decide_False. by iFrame "SDA".
- rewrite Z2Pos.inj_add; by lia. }
+ { rewrite /Q decide_False.
+ - by iFrame "SDA". - rewrite Z2Pos.inj_add; by lia. }
iDestruct (GPS_SWSharedReaders_join with "R' R") as "R".
iDestruct (GPS_SWSharedWriter_Reader_update with "W' R") as "[W' R]".
iDestruct (WkUps_join with "[$WU $WU']") as "WU".
@@ -2493,9 +2493,8 @@ Section arc.
apply (irreflexive_eq (R:=Pos.lt) t4 t4); [done|].
eapply Pos.lt_le_trans; [|by apply Le7].
eapply Pos.le_lt_trans; [|by apply Ext7].
- etrans; [|by apply Ext']. case decide; case decide; [done..| |].
- move => ? /Pos.lt_nle ?. by eapply Pos.lt_le_incl, Pos.le_lt_trans.
- move => ? /Pos.lt_nle ?. by apply Pos.lt_le_incl.
+ etrans; [|by apply Ext'].
+ case decide; case decide; [done..| |]; clear; lia.
+ iDestruct (WeakUpAuth_Cert_include with "[$WUA $Cert]")
as %Le7%elem_of_subseteq_singleton%MAX5. exfalso.
apply (irreflexive_eq (R:=Pos.lt) t5 t5); [done|].
@@ -2567,9 +2566,10 @@ Section arc.
{ iApply (arc_inv_join with "SMA [SDA] WUA IS IW"); by iExists _. }
iModIntro. wp_seq. iApply "HΦ". iFrame "HP".
iExists _,_,_,_. iFrame "St tok SW SM SD oW". iSplitL "".
- iExists _,_. iFrame (MAX4) "SR4". iExists _,_. iFrame "WW".
- iPureIntro. move => ? /elem_of_union [/MAX1->|/elem_of_singleton -> //].
- by apply Pos.lt_le_incl.
+ + iExists _,_. iFrame (MAX4) "SR4".
+ + iExists _,_. iFrame "WW".
+ iPureIntro. move => ? /elem_of_union [/MAX1->|/elem_of_singleton -> //].
+ by apply Pos.lt_le_incl.
Qed.
Lemma try_unwrap_full_spec {HPn : HP2} γi γs γw γsw l q tid :
@@ -2714,7 +2714,8 @@ Section arc.
iIntros "(SDA & tok & tok' & VR)". iSplit; last iSplit.
- iDestruct 1 as ([iS st] Eq') "[WA WI]". inversion Eq' as [Eq1]. clear Eq'.
iDestruct (WeakAuth_strong with "[$WA $oW]") as %[qs ?]. subst iS.
- destruct st as [[[]| |]|]. exfalso. lia. by exfalso. by exfalso.
+ destruct st as [[[]| |]|].
+ { exfalso. lia. } { by exfalso. } { by exfalso. }
iDestruct "WI" as "(% & $ & WI)". iDestruct "WI" as (Ut) "(tokW&?&WU&?)".
iCombine "tok" "tok'" as "tok". rewrite -Qp_div_add_distr Eq.
iCombine "tok" "tokW" as "tok". iDestruct ("FR" with "tok VR") as "#$".
diff --git a/theories/lang/arc_cmra.v b/theories/lang/arc_cmra.v
index f12ad7aab7d81466f424e57e211bcc2369271bc7..237f230d3ae4ae713277865141a75e27e62006e1 100644
--- a/theories/lang/arc_cmra.v
+++ b/theories/lang/arc_cmra.v
@@ -6,7 +6,7 @@ From lrust.lang Require Import notation.
From gpfsl.gps Require Import middleware protocols.
From gpfsl.logic Require Import view_invariants.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
(** The CMRAs we need. *)
@@ -76,7 +76,7 @@ Class arcG Σ := {
Arc_viewInv :> view_invG Σ;
}.
Definition arcΣ : gFunctors := #[GFunctor arcUR; gpsΣ unitProtocol; atomicΣ; view_invΣ].
-Instance subG_arcΣ {Σ} : subG arcΣ Σ → arcG Σ.
+Global Instance subG_arcΣ {Σ} : subG arcΣ Σ → arcG Σ.
Proof. solve_inG. Qed.
Definition Z_of_arcweak_st (st : weak_stUR) : Z :=
@@ -159,7 +159,7 @@ Section ArcGhost.
Qed.
Global Instance StrMoves_asfractional γ q Mt :
AsFractional (StrMoves γ q Mt) (λ q, StrMoves γ q Mt) q.
- Proof. split. done. apply _. Qed.
+ Proof. split; [done|apply _]. Qed.
Global Instance StrDowns_fractional γ Dt : Fractional (λ q, StrDowns γ q Dt).
Proof.
rewrite /Fractional => p q. rewrite -embed_sep -own_op.
@@ -171,7 +171,7 @@ Section ArcGhost.
Qed.
Global Instance StrDowns_asfractional γ q Dt :
AsFractional (StrDowns γ q Dt) (λ q, StrDowns γ q Dt) q.
- Proof. split. done. apply _. Qed.
+ Proof. split; [done|apply _]. Qed.
Global Instance WkUps_fractional γ Ut : Fractional (λ q, WkUps γ q Ut).
Proof.
rewrite /Fractional => p q. rewrite -embed_sep -own_op.
@@ -182,7 +182,7 @@ Section ArcGhost.
Qed.
Global Instance WkUps_asfractional γ q Ut :
AsFractional (WkUps γ q Ut) (λ q, WkUps γ q Ut) q.
- Proof. split. done. apply _. Qed.
+ Proof. split; [done|apply _]. Qed.
(* move_self *)
Local Notation moveSAuth Mt
@@ -369,7 +369,7 @@ Section ArcGhost.
iDestruct (@own_valid _ arcUR with "WU")
as %[_ [_ [[VAL _]%auth_frag_valid_1 _]]].
iPureIntro. simpl in VAL.
- have Lt: (1 < 1 + q)%Qp. apply Qp_lt_sum. by eexists.
+ have Lt: (1 < 1 + q)%Qp. { apply Qp_lt_sum. by eexists. }
apply (irreflexive_eq (R:= Qp_lt) 1%Qp 1%Qp); [done|].
eapply Qp_lt_le_trans; [apply Lt|done].
Qed.
@@ -403,8 +403,9 @@ Section ArcGhost.
inversion Eq1. subst q1. exists q', n. split; [done|].
destruct Eq3 as [[Eq3 Eq4]|[[q'' Le1] Le2%pos_included]%prod_included].
- inversion Eq3. inversion Eq4. simpl in *. by subst.
- - simpl in *. rewrite decide_False. exists q''. by rewrite Le1 frac_op.
- move => ?. by subst n.
+ - simpl in *. rewrite decide_False.
+ + exists q''. by rewrite Le1 frac_op.
+ + move => ?. by subst n.
Qed.
Lemma WeakTok_Auth_agree γ st q :
@@ -426,7 +427,8 @@ Section ArcGhost.
subst qn. exists q', weak, st'. split; [done|]. inversion Eq2. subst.
apply prod_included in INCL as [[q'' Eq] INCLs%pos_included]. simpl in *.
rewrite decide_False.
- exists q''. by rewrite Eq frac_op. move => ?. by subst weak.
+ + exists q''. by rewrite Eq frac_op.
+ + move => ?. by subst weak.
Qed.
Lemma StrongAuth_first_tok γ :
@@ -571,7 +573,7 @@ Section ArcGhost.
iDestruct (@own_valid _ arcUR with "own") as %[[_ VAL] _]. simpl in VAL.
iPureIntro. move : VAL. rewrite -auth_frag_op -pair_op -Some_op frac_op.
move => /auth_frag_valid /= [/= ? _].
- have Lt: (1 < 1 + q)%Qp. apply Qp_lt_sum. by eexists.
+ have Lt: (1 < 1 + q)%Qp. { apply Qp_lt_sum. by eexists. }
apply (irreflexive_eq (R:= Qp_lt) 1%Qp 1%Qp); [done|].
eapply Qp_lt_le_trans; [apply Lt|done].
Qed.
@@ -584,7 +586,7 @@ Section ArcGhost.
iDestruct (StrMoves_fractional with "[$SM $SM']") as "SM".
iDestruct (@own_valid _ arcUR with "SM") as %[_ [[[[VAL _]%auth_frag_valid_1 _] _] _]].
iPureIntro. simpl in VAL.
- have Lt: (1 < 1 + q)%Qp. apply Qp_lt_sum. by eexists.
+ have Lt: (1 < 1 + q)%Qp. { apply Qp_lt_sum. by eexists. }
apply (irreflexive_eq (R:= Qp_lt) 1%Qp 1%Qp); [done|].
eapply Qp_lt_le_trans; [apply Lt|done].
Qed.
diff --git a/theories/lang/lock.v b/theories/lang/lock.v
index 097f97db2a11615c9c5949d5745cf559b41fd676..c5c6445c14f513ad3e1e2fa171bf54019ee53ed2 100644
--- a/theories/lang/lock.v
+++ b/theories/lang/lock.v
@@ -4,7 +4,8 @@ From lrust.lang Require Import notation.
From gpfsl.gps Require Import middleware protocols.
From lrust.logic Require Import gps.
From lrust.lifetime Require Import at_borrow.
-Set Default Proof Using "Type".
+
+From iris.prelude Require Import options.
Definition mklock_unlocked : val := λ: ["l"], "l" <- #false.
Definition mklock_locked : val := λ: ["l"], "l" <- #true.
@@ -22,7 +23,7 @@ Class lockG Σ := LockG {
Definition lockΣ : gFunctors := #[gpsΣ unitProtocol; atomicΣ].
-Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
+Global Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
Proof. solve_inG. Qed.
Section proof.
diff --git a/theories/lang/memcpy.v b/theories/lang/memcpy.v
index 9920e71bffdc3afe8266c445f708b226adc0d3ee..4df0f9c53206a57173a62d7a37c74b1ba73a5b96 100644
--- a/theories/lang/memcpy.v
+++ b/theories/lang/memcpy.v
@@ -1,6 +1,6 @@
From lrust.lang Require Export notation.
From gpfsl.logic Require Import proofmode.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Definition memcpy : val :=
rec: "memcpy" ["dst";"len";"src"] :=
diff --git a/theories/lang/spawn.v b/theories/lang/spawn.v
index 337873260e8e4a3b232ebe1f4f8099dfc5693a75..2dd03d3d71f265996a3178a2d87c17edf78857b9 100644
--- a/theories/lang/spawn.v
+++ b/theories/lang/spawn.v
@@ -5,7 +5,7 @@ From lrust.lang Require Import notation.
From gpfsl.logic Require Import view_invariants.
From gpfsl.gps Require Import surface protocols escrows.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Definition spawn : val :=
λ: ["f"],
@@ -38,7 +38,7 @@ Class spawnG Σ := SpawnG {
Definition spawnΣ : gFunctors :=
#[GFunctor (exclR unitO); gpsΣ unitProtocol; atomicΣ; view_invΣ].
-Instance subG_spawnΣ {Σ} : subG spawnΣ Σ → spawnG Σ.
+Global Instance subG_spawnΣ {Σ} : subG spawnΣ Σ → spawnG Σ.
Proof. solve_inG. Qed.
(** Now we come to the Iris part of the proof. *)
diff --git a/theories/lang/swap.v b/theories/lang/swap.v
index abef3ec3391e4091f2400511fa24afabc7dbac34..0178f7ee02ff0b1eb409c7bd8b10debd646ce454 100644
--- a/theories/lang/swap.v
+++ b/theories/lang/swap.v
@@ -1,6 +1,6 @@
From lrust.lang Require Export notation.
From gpfsl.logic Require Import proofmode.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Definition swap : val :=
rec: "swap" ["p1";"p2";"len"] :=
diff --git a/theories/lifetime/at_borrow.v b/theories/lifetime/at_borrow.v
index e0d685a2d0d3fa6fba99b7c1f3926149240d8364..54b4823d0ef6666dd9e293984db8987be412eeea 100644
--- a/theories/lifetime/at_borrow.v
+++ b/theories/lifetime/at_borrow.v
@@ -1,7 +1,7 @@
From iris.algebra Require Import gmap auth frac.
From iris.proofmode Require Import tactics.
From lrust.lifetime Require Export lifetime.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
(** Atomic persistent borrows *)
(* JH : at_bor has to depend on the view. Otherwise, we could open
@@ -48,7 +48,7 @@ Section atomic_bors.
iInv N as (V) ">Hi" "Hclose". iCombine "Hidx Htok" as "HH".
iDestruct (monPred_in_intro with "HH") as (V') "(#HV' & #Hidx' & Htok)".
iMod (idx_bor_acc with "LFT Hidx' Hi Htok") as (V'') "(% & HP & Hclose')".
- solve_ndisj. iExists V''. iModIntro. iSplitL "HP"; iIntros "H".
+ { solve_ndisj. } iExists V''. iModIntro. iSplitL "HP"; iIntros "H".
- iApply (monPred_in_elim with "H"). by iNext.
- iCombine "HV' H" as "HH".
iDestruct (monPred_in_intro with "HH") as (V''') "(#HV''' & % & HP)".
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index 997b4a726bfed60191d230f7dbaee2330d6f09b8..45cdfad1f2a84d52c7fef0019fc72da629f58f1f 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
From iris.bi Require Import fractional.
From iris.algebra Require Import frac.
From lrust.lifetime Require Export lifetime.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Class frac_borG Σ := frac_borG_inG :> inG Σ fracR.
@@ -67,8 +67,8 @@ Section frac_bor.
↑lftN ⊆ E → ⎡lft_ctx⎤ -∗
▷ □ (∀ q1 q2, φ (q1+q2)%Qp ↔ φ q1 ∗ φ q2) -∗ &{κ}(φ 1%Qp) ={E}=∗ &frac{κ}φ.
Proof.
- iIntros (?) "#LFT #Hfrac Hφ". iMod (own_alloc 1%Qp) as (γ) "Hown". done.
- iMod (bor_acc_atomic_strong with "LFT Hφ") as "[H|H]". done.
+ iIntros (?) "#LFT #Hfrac Hφ". iMod (own_alloc 1%Qp) as (γ) "Hown". { done. }
+ iMod (bor_acc_atomic_strong with "LFT Hφ") as "[H|H]". { done. }
- iDestruct "H" as (P' κ') "(#Hκκ' & Hφ & Hclose)". iCombine "Hfrac Hφ" as "HH".
iDestruct (monPred_in_intro with "HH") as (V) "(#HV & #Hfrac' & Hφ)".
iMod ("Hclose" with "[] [-]") as "Hφ"; last first.
@@ -77,7 +77,8 @@ Section frac_bor.
- 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, None, None; simpl.
+ { iNext. iSplit. { iDestruct "Hφ" as "[$ _]". }
+ iExists 1%Qp, None, None; simpl.
iDestruct "Hφ" as "[_ Hφ]". repeat (iSplit; [done|]). by iFrame. }
iIntros "!> Hφ H†!>". iNext.
iDestruct "Hφ" as (q q' q'' Hsum) "(Hφ1 & Htok & Hφ2 & _)".
@@ -110,7 +111,7 @@ Section frac_bor.
Proof.
iIntros (?) "#LFT Hfrac Hκ".
iDestruct "Hfrac" as (γ κ' V0 φ') "#(Hκκ' & HV0 & Hφ' & Hfrac & Hshr)".
- iMod (lft_incl_acc with "Hκκ' Hκ") as (qκ') "[Hκ Hclose]". done.
+ iMod (lft_incl_acc with "Hκκ' Hκ") as (qκ') "[Hκ Hclose]". { done. }
rewrite -{1}(Qp_div_2 qκ'). rewrite lft_tok_split_obj.
iDestruct "Hκ" as "[Hκ1 Hκ2]".
iMod (in_at_bor_acc with "LFT Hshr Hκ1") as (Vb) "[H Hclose']"; try done.
@@ -190,7 +191,7 @@ Section frac_bor.
⎡lft_ctx⎤ -∗ &frac{κ}(λ q', (q * q').[κ']) -∗ κ ⊑ κ'.
Proof.
iIntros "#LFT#Hbor". iApply lft_incl_intro. iModIntro. iIntros (q') "Hκ'".
- iMod (frac_bor_acc with "LFT Hbor Hκ'") as (q'') "[>Htok Hclose]". done.
+ iMod (frac_bor_acc with "LFT Hbor Hκ'") as (q'') "[>Htok Hclose]". { done. }
iExists _. iIntros "{$Htok} !> Hκ'". by iApply "Hclose".
Qed.
End frac_bor.
diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index e77f22f6ad0f353df96a3598f493f00456d0f76b..b9bd9420e02a8df520a2e93d021e59ea01e7d9ec 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -4,7 +4,7 @@ From lrust.lifetime.model Require definitions primitive accessors faking borrow
borrow_sep reborrow creation in_at_borrow.
From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Module Export lifetime : lifetime_sig.
Definition lft := gmultiset positive.
@@ -21,7 +21,7 @@ End lifetime.
Notation lft_intersect_list l := (foldr (⊓) static l).
-Instance lft_inhabited : Inhabited lft := populate static.
+Global Instance lft_inhabited : Inhabited lft := populate static.
Canonical lftO := leibnizO lft.
@@ -83,11 +83,13 @@ Proof.
iDestruct "H" as (P') "[HP Hclose]".
iDestruct (monPred_in_intro with "HP") as (V) "[#HV HP]".
iLeft. iExists (P' ∧ P V)%I. iSplitL "HP".
- - iModIntro. iSplit; [by iNext|]. iApply monPred_in_elim. done.
+ - iModIntro. iSplit; [by iNext|]. iApply monPred_in_elim. { done. }
iDestruct "HP" as "[_ HP]". by iNext.
- iIntros "!> HP". iMod ("Hclose" with "[] [HP]") as "$"; [by iIntros "!> $"| |done].
- iSplit. iDestruct "HP" as "[$ _]". iApply monPred_in_elim. done.
- iNext. iDestruct "HP" as "[_ $]".
+ iSplit.
+ + iDestruct "HP" as "[$ _]".
+ + iApply monPred_in_elim. { done. }
+ iNext. iDestruct "HP" as "[_ $]".
Qed.
Lemma bor_acc_cons E q κ P :
@@ -118,13 +120,13 @@ Lemma idx_bor_acc_sync E q κ i P :
Proof.
iIntros (?) "#LFT Hb Hown Htok". iCombine "Hb Hown Htok" as "HH".
iDestruct (monPred_in_intro with "HH") as (V) "(#HV & #Hb & Hown & Htok)".
- iMod (idx_bor_acc with "LFT Hb Hown Htok") as (V' HV') "(HP & Hclose)". done.
- revert HV'. rewrite lat_join_idem=>HV'. iSplitL "HP". iModIntro.
- - iApply monPred_in_elim; [|by iNext]. by rewrite HV'.
+ iMod (idx_bor_acc with "LFT Hb Hown Htok") as (V' HV') "(HP & Hclose)". { done. }
+ revert HV'. rewrite lat_join_idem=>HV'. iSplitL "HP".
+ - iModIntro. iApply monPred_in_elim; [|by iNext]. by rewrite HV'.
- iIntros "!> HP". iCombine "HV HP" as"HH".
iDestruct (monPred_in_intro with "HH") as (V'') "(#HV'' & % & HP)".
iMod ("Hclose" $! V'' with "[//] [$HP]") as "[Hown Htok]".
- iApply monPred_in_elim. done. by iFrame.
+ iApply monPred_in_elim; [done|]. by iFrame.
Qed.
Lemma bor_exists `{LatBottom Lat, !Inhabited A} (Φ : A → monPred _ _) E κ :
@@ -167,8 +169,7 @@ Proof.
iIntros (?) "#LFT Hb".
iMod (bor_acc_atomic_cons with "LFT Hb") as "[H|H]"; first done.
- iDestruct "H" as (P') "[HP Hclose]". iModIntro. iNext.
- iApply ("Hclose" with "[] [HP]"); [by iIntros "!> $"|].
- iSplit. iDestruct "HP" as "[$ _]". iDestruct "HP" as "[_ $]".
+ iApply ("Hclose" with "[] [HP]"); [by iIntros "!> $"|]. by iNext.
- iIntros "!> !>". iDestruct "H" as (κ') "(#? & #? & >_)".
by iApply bor_shorten; [|iApply bor_fake].
Qed.
@@ -219,7 +220,7 @@ Proof.
iMod (bor_create _ κ' with "LFT Hidx") as "[Hidx Hinh]"; first done.
iMod (idx_bor_unnest with "LFT Hbor Hidx") as "Hbor'"; first done.
iDestruct (bor_shorten with "[] Hbor'") as "$".
- { iApply lft_incl_glb. done. iApply lft_incl_refl. }
+ { iApply lft_incl_glb; [done|]. iApply lft_incl_refl. }
iIntros "!> H†". iMod ("Hinh" with "H†") as ">Hidx". auto.
Qed.
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index a2d99b71338828575cddabbce0f3a43f08011329..c41ee4ebd3c24d502daea7ee33af6af3c997b7ee 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -31,7 +31,7 @@ Module Type lifetime_sig.
Global Declare Instance lft_intersect : Meet lft.
Section defs.
- Notation monPred Σ Lat := (monPredI (lat_bi_index Lat) (uPredI (iResUR Σ))).
+ Notation monPred Σ Lat := (monPredI (lat_bi_index Lat) (iPropI Σ)).
Parameter lft_ctx : ∀ `{!invGS Σ, !lftG Σ Lat userE}, iProp Σ.
diff --git a/theories/lifetime/meta.v b/theories/lifetime/meta.v
index 331d3cf227cedf1de6bbb9f61c9c7d624cc09efe..ab6c88001de84c92a596a128cc37d7143bc9122c 100644
--- a/theories/lifetime/meta.v
+++ b/theories/lifetime/meta.v
@@ -1,7 +1,8 @@
From iris.algebra Require Import dyn_reservation_map agree.
From iris.proofmode Require Import tactics.
From lrust.lifetime Require Export lifetime.
-Set Default Proof Using "Type".
+
+From iris.prelude Require Import options.
(** This module provides support for attaching metadata (specifically, a
[gname]) to a lifetime (as is required for types using branding). *)
@@ -11,7 +12,7 @@ Class lft_metaG Σ := LftMetaG {
}.
Definition lft_metaΣ : gFunctors :=
#[GFunctor (dyn_reservation_mapR (agreeR gnameO))].
-Instance subG_lft_meta Σ :
+Global Instance subG_lft_meta Σ :
subG (lft_metaΣ) Σ → lft_metaG Σ.
Proof. solve_inG. Qed.
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index f37790563368a3b4db2e47358628d38b7164d9fb..6345d17ccceb39f10ab24fc7ce527fd7e20a4dbe 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -1,7 +1,8 @@
From lrust.lifetime Require Export primitive.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import csum auth excl frac gmap agree gset.
-Set Default Proof Using "Type".
+
+From iris.prelude Require Import options.
Section accessors.
Context `{!invGS Σ, !lftG Σ Lat userE}.
@@ -20,11 +21,12 @@ Proof.
iDestruct (own_bor_valid_2 with "Hown Hbor")
as %[EQB%to_borUR_included _]%auth_both_valid_discrete.
iMod (slice_empty _ _ true with "Hslice Hbox") as "[HP Hbox]".
- solve_ndisj. by rewrite lookup_fmap EQB.
+ { solve_ndisj. } { by rewrite lookup_fmap EQB. }
rewrite -(fmap_insert bor_filled _ _ (Bor_open q Vtok V')).
- iMod (own_bor_update_2 with "Hown Hbor") as "[Hown Hbor]". apply auth_update.
- { eapply singleton_local_update. by rewrite lookup_fmap EQB.
- by apply (exclusive_local_update _ (Excl (Bor_open q Vtok V'))). }
+ iMod (own_bor_update_2 with "Hown Hbor") as "[Hown Hbor]".
+ { apply auth_update. eapply singleton_local_update.
+ - by rewrite lookup_fmap EQB.
+ - by apply (exclusive_local_update _ (Excl (Bor_open q Vtok V'))). }
iExists V'. rewrite -fmap_insert. iFrame "∗%". iExists _. iFrame.
rewrite -insert_delete_insert big_sepM_insert ?lookup_delete // big_sepM_delete //=.
iIntros "/= !>". iNext. iDestruct "HB" as "[?$]". iFrame.
@@ -41,11 +43,12 @@ Proof.
iDestruct (own_bor_valid_2 with "Hown Hbor")
as %[EQB%to_borUR_included _]%auth_both_valid_discrete.
iMod (slice_fill _ _ true with "Hslice HP Hbox") as "Hbox".
- solve_ndisj. by rewrite lookup_fmap EQB.
+ { solve_ndisj. } { by rewrite lookup_fmap EQB. }
rewrite -(fmap_insert bor_filled _ _ (Bor_in (Vtok' ⊔ V))).
- iMod (own_bor_update_2 with "Hown Hbor") as "Hbor". apply auth_update.
- { eapply singleton_local_update. by rewrite lookup_fmap EQB.
- by apply (exclusive_local_update _ (Excl (Bor_in (Vtok' ⊔ V)))). }
+ iMod (own_bor_update_2 with "Hown Hbor") as "Hbor".
+ { apply auth_update. eapply singleton_local_update.
+ - by rewrite lookup_fmap EQB.
+ - by apply (exclusive_local_update _ (Excl (Bor_in (Vtok' ⊔ V)))). }
rewrite own_bor_op -fmap_insert /=. iDestruct "Hbor" as "[Hown Hbor]".
rewrite big_sepM_delete //. simpl. setoid_rewrite HVV'.
iDestruct "HB" as "[>[% $] HB]". iSplitR "Hbor"; last by iExists (Vtok' ⊔ V); auto.
@@ -86,12 +89,12 @@ Proof.
iMod (own_update_2 with "HA Htok") as "[$$]".
{ rewrite /to_alftUR fmap_insert. eapply auth_update, singleton_local_update.
{ by rewrite lookup_fmap HA. }
- apply csum_local_update_l, prod_local_update=>//=.
- etrans. apply (op_local_update_discrete _ _ (to_latT V))=>//.
- by rewrite !lat_op_join' (lat_le_join_l V V'). }
+ apply csum_local_update_l, prod_local_update=>//=. etrans.
+ - apply (op_local_update_discrete _ _ (to_latT V))=>//.
+ - by rewrite !lat_op_join' (lat_le_join_l V V'). }
iPureIntro; split.
+ intros Λ'. destruct (decide (Λ' = Λ)) as [->|?].
- by rewrite lookup_insert HA. by rewrite lookup_insert_ne.
+ * by rewrite lookup_insert HA. * by rewrite lookup_insert_ne.
+ intros κ' Vκ' Hκ' Λ' HΛ'. destruct (decide (Λ' = Λ)) as [->|?].
* rewrite lookup_insert /=. specialize (Hκ' Λ HΛ'). rewrite HA /= in Hκ'.
solve_lat.
@@ -131,7 +134,7 @@ Proof.
intros ?. unfold lft_inv. iDestruct 1 as (Vκ') "[% H]". iExists Vκ'.
iSplit; [by eauto using ame_hv|].
iDestruct "H" as "[[?%]|[?%]]"; [iLeft|iRight]; iFrame; iPureIntro.
- by eapply ame_lft_alive_in. by eapply ame_lft_dead_in.
+ - by eapply ame_lft_alive_in. - by eapply ame_lft_dead_in.
Qed.
(** Internal accessors *)
@@ -150,14 +153,14 @@ Proof.
rewrite big_sepS_later big_sepS_elem_of_acc //. rewrite [lft_inv _ κ]/lft_inv.
iDestruct "Hinv" as "[Hinv Hclose']".
iDestruct "Hinv" as (Vκ) "[>% [[Hinv >%]|[Hinv >%]]]"; last first.
- { iMod (lft_dead_in_tok with "HA") as "[_ H†]". done.
+ { iMod (lft_dead_in_tok with "HA") as "[_ H†]"; [done|].
iDestruct "H†" as (V) "H†".
set (V' := Vtok ⊔ V).
iDestruct (lft_tok_dead $! V' with "Htok H†") as "[]". }
rewrite [in _ Vκ]lft_inv_alive_unfold.
iDestruct "Hinv" as (Pb Pi) "(Halive & Hvs & Hinh)".
iMod (bor_open_internal with "Hs Halive Hbor Htok") as (V) "(% & Halive & Hf & HP)".
- solve_ndisj.
+ { solve_ndisj. }
iExists V. iFrame "HP %".
iMod ("Hclose" with "[-Hf]") as "_".
{ iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose'".
@@ -178,7 +181,7 @@ Proof.
rewrite lft_inv_alive_unfold.
iDestruct "Hinv" as (Pb Pi) "(Halive & Hvs & Hinh)".
iMod (bor_close_internal with "Hs Halive Hf HP") as "(Halive & $ & Htok)".
- solve_ndisj. done.
+ { solve_ndisj. } { done. }
iMod (extend_lft_view with "Htok HA") as (A') "($ & HA' & %)".
iApply "Hclose". iExists _, _. iFrame.
rewrite big_sepS_later (big_sepS_delete _ (dom _ I)) //. iSplitR "Hclose'".
@@ -198,7 +201,7 @@ Lemma idx_bor_acc E q κ i P Vtok Vbor:
Proof.
unfold idx_bor. iIntros (HE) "#LFT [#Hle #Hs] Hbor Htok".
iDestruct "Hs" as (P') "[#HPP' Hs]". destruct i as [κ' s].
- iMod (lft_incl_acc with "Hle Htok") as (q') "[Htok Hclose]". solve_ndisj.
+ iMod (lft_incl_acc with "Hle Htok") as (q') "[Htok Hclose]". { solve_ndisj. }
iMod (idx_bor_acc_internal with "LFT Hs Hbor Htok") as (V) "(% & HP & Hclose')";
[solve_ndisj|solve_ndisj|].
iExists (V ⊔ Vtok). iSplitR; [by iPureIntro; f_equiv|]. iModIntro. iSplitL "HP".
@@ -216,7 +219,7 @@ Proof.
iIntros "#HEQ Hvs HvsQ". iApply (lft_vs_cons with "[-Hvs] Hvs").
iIntros "[HQ HPb'] #H†".
iApply fupd_mask_mono; [|iMod ("HvsQ" with "HQ H†") as "HP"].
- set_solver.
+ { set_solver. }
iModIntro. iNext. iRewrite "HEQ". iFrame.
Qed.
@@ -240,7 +243,7 @@ Proof.
unfold bor, raw_bor. iIntros (HE) "#LFT Hbor Htok".
iDestruct "Hbor" as (κ'') "(#Hle & Htmp)". iDestruct "Htmp" as (s'') "(Hbor & #Hs)".
iDestruct "Hs" as (P') "[#HPP' Hs]".
- iMod (lft_incl_acc with "Hle Htok") as (q') "[Htok Hclose]". solve_ndisj.
+ iMod (lft_incl_acc with "Hle Htok") as (q') "[Htok Hclose]". { solve_ndisj. }
iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose'".
iAssert (⌜κ'' ∈ dom (gset _) IâŒ)%I as %Hκ'.
{ unfold idx_bor_own. iDestruct "Hbor" as (Vb) "[#HVb Hbor]".
@@ -248,7 +251,7 @@ Proof.
rewrite big_sepS_later big_sepS_elem_of_acc //. rewrite [lft_inv _ κ'']/lft_inv.
iDestruct "Hinv" as "[Hinv Hclose'']".
iDestruct "Hinv" as (Vκ) "[>% [[Hinv >%]|[Hinv >%]]]"; last first.
- { iMod (lft_dead_in_tok with "HA") as "[_ H†]". done.
+ { iMod (lft_dead_in_tok with "HA") as "[_ H†]". { done. }
iDestruct (monPred_in_intro with "Htok") as (Vtok) "[_ Htok]".
iDestruct "H†" as (V) "H†". iAssert ⎡False⎤%I as %[]. iModIntro.
set (V' := Vtok ⊔ V).
@@ -258,9 +261,9 @@ Proof.
iCombine "Hbor Htok" as "HborHtok".
iDestruct (monPred_in_intro with "HborHtok") as (V) "(#HV & Hbor & Htok)".
iMod (bor_open_internal with "Hs Halive Hbor Htok")
- as (V0 HVV0) "(Halive & Hbor & HP')". solve_ndisj.
+ as (V0 HVV0) "(Halive & Hbor & HP')". { solve_ndisj. }
iAssert (â–· P)%I with "[HP']" as "$".
- { iNext. iApply "HPP'". iApply monPred_in_elim. done. iFrame. }
+ { iNext. iApply "HPP'". iApply (monPred_in_elim with "HV"). iFrame. }
iMod ("Hclose'" with "[-Hbor Hclose]") as "_".
{ iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''".
iExists _. iFrame "%". iLeft. rewrite lft_inv_alive_unfold. iExists _, _. iFrame. }
@@ -283,7 +286,7 @@ Proof.
iDestruct (own_bor_valid_2 with "Hown Hbor")
as %[EQB%to_borUR_included _]%auth_both_valid_discrete.
iDestruct (slice_delete_empty _ true with "Hs Hbox") as (Pb') "[EQ Hbox]".
- by rewrite lookup_fmap EQB.
+ { by rewrite lookup_fmap EQB. }
iMod (slice_insert_empty _ _ true _ Q with "Hbox") as (j) "(% & #Hs' & Hbox)".
iMod (own_bor_update_2 with "Hown Hbor") as "Hown".
{ apply auth_update. etrans.
@@ -297,11 +300,11 @@ Proof.
iCombine "HV HQ HvsQ" as "HH".
iDestruct (monPred_in_intro with "HH") as (V') "(#HV' & % & HQ & HvsQ)".
iMod (bor_close_internal with "Hs' [Hbox Hown HB] Hbor [HQ]")
- as "(Halive & Hbor & Htok)". solve_ndisj. done.
+ as "(Halive & Hbor & Htok)". { solve_ndisj. } { done. }
{ rewrite -!fmap_delete -fmap_insert -(fmap_insert _ _ _ (Bor_open q' V V0))
/lft_bor_alive. iExists _. iFrame "Hbox Hown".
- rewrite big_sepM_insert. by rewrite big_sepM_delete.
- by rewrite -fmap_None -lookup_fmap fmap_delete. }
+ rewrite big_sepM_insert.
+ - by rewrite big_sepM_delete. - by rewrite -fmap_None -lookup_fmap fmap_delete. }
{ rewrite -(_ : V' ⊑ V' ⊔ V0) //. solve_lat. }
iMod (extend_lft_view with "Htok HA") as (A') "(Htok & HA' & %)".
iMod ("Hclose'" with "[-Hbor Htok Hclose]") as "_".
@@ -342,7 +345,7 @@ Proof.
rewrite big_sepS_later big_sepS_elem_of_acc //. rewrite [lft_inv _ (i.1)]/lft_inv.
iDestruct "Hinv" as "[Hinv Hclose'']".
iDestruct "Hinv" as (Vκ) "[>% [[Hinv >%]|[Hinv >%]]]"; last first.
- { iRight. iMod (lft_dead_in_tok with "HA") as "[HA #H†]". done.
+ { iRight. iMod (lft_dead_in_tok with "HA") as "[HA #H†]". { done. }
iMod ("Hclose'" with "[-Hbor]") as "_".
- iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''".
iExists _. iFrame "%". iRight. by iFrame.
@@ -355,11 +358,11 @@ Proof.
iDestruct (own_bor_valid_2 with "Hown Hbor")
as %[EQB%to_borUR_included _]%auth_both_valid_discrete.
iMod (slice_delete_full _ _ true with "Hs Hbox") as (Pb') "(HP' & EQ & Hbox)".
- solve_ndisj. by rewrite lookup_fmap EQB.
+ { solve_ndisj. } { by rewrite lookup_fmap EQB. }
iApply fupd_frame_l. iSplitL "HP'".
{ iNext. iSplit; [done|]. iApply "HPP'". by iApply monPred_in_elim. }
iMod fupd_mask_subseteq as "Hclose"; [|iModIntro; iIntros (Q) "HvsQ HQ"].
- solve_ndisj.
+ { solve_ndisj. }
iMod "Hclose" as "_".
iAssert (▷⌜Vb ⊑ VκâŒ)%I as "#>%".
{ rewrite monPred_at_big_sepM. rewrite -embed_pure. iNext. iModIntro.
@@ -368,7 +371,7 @@ Proof.
iDestruct (monPred_in_intro with "HH") as (V) "(#HV & HQ & HvsQ & #HPP'V)".
set (Q' := ((monPred_in V ∨ ⎡P' Vb⎤) ∧ (monPred_in V → Q))%I).
iMod (slice_insert_full _ _ true _ _ Q' Vb with "[HQ] Hbox")
- as (j) "(% & #Hs' & Hbox)". solve_ndisj.
+ as (j) "(% & #Hs' & Hbox)". { solve_ndisj. }
{ rewrite /Q' /=. iSplit.
- iDestruct "HQ" as "[? _]". iNext. by iRight.
- iDestruct "HQ" as "[_ ?]". iIntros (???). iFrame. }
@@ -395,7 +398,8 @@ Proof.
iExists _. iFrame "%". iLeft. rewrite lft_inv_alive_unfold. iExists _, _. iFrame.
iNext. rewrite -!fmap_delete -fmap_insert -(fmap_insert _ _ _ (Bor_in Vb)).
rewrite /lft_bor_alive. iExists _. iFrame "Hbox Hâ—".
- rewrite big_sepM_insert. by rewrite big_sepM_delete.
- by rewrite -fmap_None -lookup_fmap fmap_delete.
+ rewrite big_sepM_insert.
+ - by rewrite big_sepM_delete.
+ - by rewrite -fmap_None -lookup_fmap fmap_delete.
Qed.
End accessors.
diff --git a/theories/lifetime/model/borrow.v b/theories/lifetime/model/borrow.v
index 3c491d1c4ff910b839e46a1a41870dc0cc53afc7..5abdccb657dd53427a14dc3fdf922209d5b247a6 100644
--- a/theories/lifetime/model/borrow.v
+++ b/theories/lifetime/model/borrow.v
@@ -2,12 +2,14 @@ From lrust.lifetime Require Export primitive.
From lrust.lifetime Require Export faking.
From iris.algebra Require Import csum auth excl frac gmap agree gset.
From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type*".
+From iris.prelude Require Import options.
Section borrow.
Context `{!invGS Σ, !lftG Σ Lat userE, LatBottom Lat}.
Implicit Types κ : lft.
+Local Set Default Proof Using "Type*".
+
Lemma raw_bor_create E κ P :
↑lftN ⊆ E → ⎡lft_ctx⎤ -∗ ▷ P ={E}=∗ raw_bor κ P ∗ ([†κ] ={E}=∗ ▷ P).
Proof.
diff --git a/theories/lifetime/model/borrow_sep.v b/theories/lifetime/model/borrow_sep.v
index 8b7f5ced3c6b1ee0773ceff003bd54ae9d3c5900..b84379aaeb3e2d3f2e5a154d5b6ac2b9743bc4c0 100644
--- a/theories/lifetime/model/borrow_sep.v
+++ b/theories/lifetime/model/borrow_sep.v
@@ -2,7 +2,7 @@ From lrust.lifetime Require Export primitive.
From lrust.lifetime Require Export faking reborrow.
From iris.algebra Require Import csum auth excl frac gmap agree.
From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type*".
+From iris.prelude Require Import options.
Lemma uPred_and_split {M} (P Q1 Q2 : uPred M) :
P ∧ (Q1 ∗ Q2) -∗ ∃ P1 P2, bi_persistently (P1 ∗ P2 → P) ∗ (Q1 ∧ P1) ∗ (Q2 ∧ P2).
@@ -31,6 +31,8 @@ Section borrow.
Context `{!invGS Σ, !lftG Σ Lat userE, LatBottom Lat}.
Implicit Types κ : lft.
+Local Set Default Proof Using "Type*".
+
Lemma bor_sep E κ P Q :
↑lftN ⊆ E → ⎡lft_ctx⎤ -∗ &{κ}(P ∗ Q) ={E}=∗ &{κ}P ∗ &{κ}Q.
Proof.
@@ -69,11 +71,11 @@ Proof.
set (P1 := (((monPred_in V) ∨ ⎡P0⎤) ∧ (monPred_in V → P))%I).
set (Q1 := (((monPred_in V) ∨ ⎡Q0⎤) ∧ (monPred_in V → Q))%I).
iMod (slice_insert_full _ _ _ _ _ P1 V' with "[HP] Hbox") as (γP HγP) "[#? Hbox]".
- solve_ndisj.
+ { solve_ndisj. }
{ iSplit; [iRight; by iDestruct "HP" as "[_ $]"|].
iIntros (???); by iDestruct "HP" as "[$ _]". }
iMod (slice_insert_full _ _ _ _ _ Q1 V' with "[HQ] Hbox") as (γQ HγQ) "[#? Hbox]".
- solve_ndisj.
+ { solve_ndisj. }
{ iSplit; [iRight; by iDestruct "HQ" as "[_ $]"|].
iIntros (???); by iDestruct "HQ" as "[$ _]". }
iMod (own_bor_update_2 with "Hown Hbor") as "Hbor".
@@ -126,9 +128,9 @@ Proof.
iIntros (?) "#LFT HP HQ". rewrite {1 2}/bor.
iDestruct "HP" as (κ1) "[#Hκ1 Hbor1]". iDestruct "HQ" as (κ2) "[#Hκ2 Hbor2]".
iMod (raw_bor_shorten _ _ (κ1 ⊓ κ2) with "LFT Hbor1") as "Hbor1".
- done. by apply gmultiset_disj_union_subseteq_l.
+ { done. } { by apply gmultiset_disj_union_subseteq_l. }
iMod (raw_bor_shorten _ _ (κ1 ⊓ κ2) with "LFT Hbor2") as "Hbor2".
- done. by apply gmultiset_disj_union_subseteq_r.
+ { done. } { by apply gmultiset_disj_union_subseteq_r. }
iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose". unfold raw_bor, idx_bor_own.
iDestruct "Hbor1" as (j1) "[Hbor1 Hslice1]". iDestruct "Hbor2" as (j2) "[Hbor2 Hslice2]".
iDestruct "Hbor1" as (V1) "[#HV1 Hbor1]". iDestruct "Hbor2" as (V2) "[#HV2 Hbor2]".
@@ -179,7 +181,7 @@ Proof.
iExists γ. iSplit.
- 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.
+ iApply (monPred_in_elim _ V12). { done. } rewrite monPred_at_in. solve_lat.
- 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.
diff --git a/theories/lifetime/model/boxes.v b/theories/lifetime/model/boxes.v
index 2772a22a9e29e89db938f51c3d5379438c6b0eac..4fc6222b7370bf98a47d3840aa3da391c6b261dd 100644
--- a/theories/lifetime/model/boxes.v
+++ b/theories/lifetime/model/boxes.v
@@ -1,31 +1,31 @@
From iris.base_logic.lib Require Export invariants.
-From iris.algebra Require Import auth gmap agree excl.
+From iris.algebra Require Import auth gmap agree lib.excl_auth.
From iris.bi Require Import big_op.
From iris.proofmode Require Import tactics.
From gpfsl.base_logic Require Import vprop.
From gpfsl.algebra Require Import lattice_cmra.
-Set Default Proof Using "Type".
-Import uPred.
+
+From iris.prelude Require Import options.
Implicit Types Lat : latticeT.
(** The CMRAs we need. *)
Class boxG Lat Σ :=
boxG_inG :> inG Σ (prodR
- (authR (optionUR (exclR (optionO (latO Lat)))))
+ (excl_authR (optionO (latO Lat)))
(optionR (agreeR (laterO (Lat -d> iPropO Σ))))).
Definition boxΣ Lat : gFunctors := #[
- GFunctor (authR (optionUR (exclR (optionO (latO Lat)))) *
+ GFunctor (excl_authR (optionO (latO Lat)) *
optionRF (agreeRF (▶ (Lat -d> ∙))) ) ].
-Instance subG_stsΣ Lat Σ : subG (boxΣ Lat) Σ → boxG Lat Σ.
+Global Instance subG_stsΣ Lat Σ : subG (boxΣ Lat) Σ → boxG Lat Σ.
Proof. solve_inG. Qed.
Section box_defs.
Context `{invGS Σ, boxG Lat Σ} (N : namespace).
Notation iProp := (iProp Σ).
- Notation monPred := (monPred (lat_bi_index Lat) (uPredI (iResUR Σ))).
+ Notation monPred := (monPred (lat_bi_index Lat) (iPropI Σ)).
Definition slice_name := gname.
@@ -36,7 +36,7 @@ Section box_defs.
own γ (ε, Some (to_agree (Next (P : _ -d> _)))).
Definition slice_inv (γ : slice_name) (P : monPred) : iProp :=
- (∃ o, box_own_auth γ (◠Excl' o) ∗ from_option (P ∘ of_latT) True o)%I.
+ (∃ o, box_own_auth γ (â—E o) ∗ from_option (P ∘ of_latT) True o)%I.
Definition slice (γ : slice_name) (P : monPred) : iProp :=
(box_own_prop γ P ∗ inv N (slice_inv γ P))%I.
@@ -44,20 +44,20 @@ Section box_defs.
Definition box (f : gmap slice_name (option Lat)) (P : monPred) : iProp :=
(∃ Φ : slice_name → monPred,
▷ (P ≡ [∗ map] γ ↦ _ ∈ f, Φ γ) ∗
- [∗ map] γ ↦ o ∈ f, box_own_auth γ (◯ Excl' (to_latT <$> o)) ∗
+ [∗ map] γ ↦ o ∈ f, box_own_auth γ (◯E (to_latT <$> o)) ∗
box_own_prop γ (Φ γ) ∗ inv N (slice_inv γ (Φ γ)))%I.
End box_defs.
-Instance: Params (@box_own_prop) 4 := {}.
-Instance: Params (@box_own_auth) 4 := {}.
-Instance: Params (@slice_inv) 4 := {}.
-Instance: Params (@slice) 6 := {}.
-Instance: Params (@box) 6 := {}.
+Global Instance: Params (@box_own_prop) 4 := {}.
+Global Instance: Params (@box_own_auth) 4 := {}.
+Global Instance: Params (@slice_inv) 4 := {}.
+Global Instance: Params (@slice) 6 := {}.
+Global Instance: Params (@box) 6 := {}.
Section box.
Context `{invGS Σ, boxG Lat Σ} (N : namespace).
-Notation monPred := (monPred (lat_bi_index Lat) (uPredI (iResUR Σ))).
+Notation monPred := (monPred (lat_bi_index Lat) (iPropI Σ)).
Implicit Types P Q : monPred.
Global Instance box_own_prop_ne γ : NonExpansive (box_own_prop γ).
@@ -92,32 +92,33 @@ Global Instance box_proper f : Proper ((≡) ==> (≡)) (box N f).
Proof. apply ne_proper, _. Qed.
Lemma box_own_auth_agree γ o1 o2 :
- box_own_auth γ (◠Excl' o1) ∗ box_own_auth γ (◯ Excl' o2) ⊢ o1 ≡ o2.
+ box_own_auth γ (â—E o1) ∗ box_own_auth γ (â—¯E o2) ⊢ o1 ≡ o2.
Proof.
- rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_l.
- iDestruct 1 as %[[[[]|] EQ%(inj Some)] _]%auth_both_valid_discrete; by inversion_clear EQ.
+ rewrite /box_own_prop -own_op own_valid prod_validI /= bi.and_elim_l.
+ by iDestruct 1 as %?%excl_auth_agree.
Qed.
Lemma box_own_auth_update γ o1 o2 o3 :
- box_own_auth γ (◠Excl' o1) ∗ box_own_auth γ (◯ Excl' o2)
- ==∗ box_own_auth γ (◠Excl' o3) ∗ box_own_auth γ (◯ Excl' o3).
+ box_own_auth γ (â—E o1) ∗ box_own_auth γ (â—¯E o2)
+ ==∗ box_own_auth γ (â—E o3) ∗ box_own_auth γ (â—¯E o3).
Proof.
- rewrite /box_own_auth -!own_op. apply own_update, prod_update; last done.
- by apply auth_update, option_local_update, exclusive_local_update.
+ rewrite /box_own_auth -!own_op -pair_op left_id.
+ apply own_update, prod_update; last done.
+ by apply excl_auth_update.
Qed.
Lemma box_own_agree γ Q1 Q2 :
box_own_prop γ Q1 ∗ box_own_prop γ Q2 ⊢ ▷ (Q1 ≡ Q2).
Proof.
- rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_r.
+ rewrite /box_own_prop -own_op own_valid prod_validI /= bi.and_elim_r.
rewrite option_validI /= agree_validI agree_equivI later_equivI /=.
- iIntros "#HQ". iApply monPred_equivI. iIntros (V).
- rewrite discrete_fun_equivI. iNext. iApply "HQ".
+ by rewrite monPred_equivI discrete_fun_equivI.
Qed.
Lemma box_alloc : ⊢ box N ∅ True.
Proof.
- iIntros. iExists (λ _, True%I); iSplit; [|done]. by rewrite big_sepM_empty True_emp.
+ iIntros. iExists (λ _, True%I); iSplit; [|done].
+ by rewrite big_sepM_empty bi.True_emp.
Qed.
Lemma slice_insert_empty E q f Q P :
@@ -125,9 +126,9 @@ Lemma slice_insert_empty E q f Q P :
slice N γ Q ∗ ▷?q box N (<[γ:=None]> f) (Q ∗ P).
Proof.
iDestruct 1 as (Φ) "[#HeqP Hf]".
- iMod (own_alloc_cofinite (â— Excl' None â‹… â—¯ Excl' None,
+ iMod (own_alloc_cofinite (â—E None â‹… â—¯E None,
Some (to_agree (Next (Q : _ -d> _)))) (dom _ f))
- as (γ) "[Hdom Hγ]". { split; [by apply auth_both_valid_discrete|done]. }
+ as (γ) "[Hdom Hγ]". { split; [by apply excl_auth_valid|done]. }
rewrite pair_split. iDestruct "Hγ" as "[[Hγ Hγ'] #HγQ]".
iDestruct "Hdom" as % ?%not_elem_of_dom.
iMod (inv_alloc N _ (slice_inv γ Q) with "[Hγ]") as "#Hinv".
@@ -193,7 +194,7 @@ Proof.
iIntros (?) "HQ Hbox".
iMod (slice_insert_empty with "Hbox") as (γ) "(% & #Hslice & Hbox)".
iExists γ. iFrame "%#". iMod (slice_fill with "Hslice HQ Hbox"); first done.
- by apply lookup_insert. by rewrite insert_insert.
+ - by apply lookup_insert. - by rewrite insert_insert.
Qed.
Lemma slice_delete_full E q f P Q γ V :
@@ -234,7 +235,7 @@ Lemma box_empty E f P V :
Proof.
iDestruct 1 as (Φ) "[#HeqP Hf]".
iAssert (([∗ map] γ↦b ∈ f, ▷ Φ γ V) ∗
- [∗ map] γ↦b ∈ f, box_own_auth γ (◯ Excl' None) ∗ box_own_prop γ (Φ γ) ∗
+ [∗ map] γ↦b ∈ f, box_own_auth γ (◯E 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]").
iModIntro; iIntros (γ o ?) "(Hγ' & #HγΦ & #Hinv)".
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index 63919e380202a473dcf2d245c1ea804a273d4338..1cc711b46bfa36bbb284d1bfdf7ab56c6036315d 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -2,12 +2,14 @@ From lrust.lifetime Require Export primitive.
From lrust.lifetime Require Import faking.
From iris.algebra Require Import csum auth frac gmap agree gset numbers excl.
From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type*".
+From iris.prelude Require Import options.
Section creation.
Context `{!invGS Σ, !lftG Σ Lat userE, LatBottom Lat}.
Implicit Types κ : lft.
+Local Set Default Proof Using "Type*".
+
Lemma lft_kill (I : gmap lft lft_names) (K K' : gset lft) (κ : lft) (Vs : lft → Lat) :
(∀ κ', κ' ∈ dom (gset _) I → κ' ⊆ κ → Vs κ ⊑ Vs κ') →
let Iinv := (
@@ -114,7 +116,7 @@ Proof.
{ iExists (λ _, inhabitant). repeat (iSplit; [by auto|]). by rewrite !big_sepS_empty. }
destruct (minimal_exists_L (⊂) K) as (κ & HκK & Hκmin); first done.
rewrite big_sepS_delete //. iDestruct "HK" as "[Hinv HK]".
- iDestruct (IH with "HK") as (Vs) "(Hhv0 & Hmono & HK)". set_solver +HκK.
+ iDestruct (IH with "HK") as (Vs) "(Hhv0 & Hmono & HK)". { set_solver +HκK. }
iDestruct "Hmono" as %Hmono.
rewrite /lft_inv. iDestruct "Hinv" as (Vκ) "[Hhv Hinv]".
iDestruct "Hhv" as %Hhv. iDestruct "Hhv0" as %Hhv0.
@@ -198,8 +200,8 @@ Proof.
assert (EQAΛ : A !! Λ ≡ Some (true, V'0)).
{ rewrite lookup_fmap in Eqs. revert Eqs.
case: (A!!Λ)=>[[[]?]|]; (try by inversion 1); intros EQ%(inj Some).
- by apply (inj Cinl), (inj2 pair) in EQ; do 2 f_equiv; naive_solver.
- by inversion EQ. }
+ - by apply (inj Cinl), (inj2 pair) in EQ; do 2 f_equiv; naive_solver.
+ - by inversion EQ. }
iDestruct (exists_Vs with "Hinv") as (Vs) "(>% & >% & Hinv)".
iMod (own_update_2 with "HA HΛ") as "[HA HΛ]".
{ apply Some_equiv_eq in Eqs as (? & ? & ?).
@@ -213,7 +215,7 @@ Proof.
{ rewrite HI=>κ. rewrite elem_of_union elem_of_filter. split.
- intros HκK. split; [by auto|]. destruct (decide (Λ ∈ κ)) as [|HΛκ]; [by auto|left].
destruct (lft_alive_or_dead_in A κ) as [(Λ'&HΛ'&EQΛ')|[Hal|?]]=>//.
- + exfalso. assert (κ ∈ dom (gset _) I). by set_solver+HI HκK.
+ + exfalso. assert (κ ∈ dom (gset _) I). { by set_solver+HI HκK. }
assert (lft_has_view A κ (Vs κ)) as Hhv' by auto.
specialize (Hhv' Λ' HΛ'). by rewrite EQΛ' in Hhv'.
+ edestruct HK=>//. set_solver + Hal HΛκ HκK HI.
@@ -256,6 +258,6 @@ Proof.
- rewrite big_sepS_impl /lft_inv. iApply "HinvK".
iIntros "!>" (κ [? HκK]%elem_of_K) "Hdead". iExists (Vs κ). iSplitR; [by auto|].
iRight. iFrame. iPureIntro. destruct HκK.
- by apply lft_dead_in_insert_false. by apply lft_dead_in_insert_false'.
+ + by apply lft_dead_in_insert_false. + by apply lft_dead_in_insert_false'.
Qed.
End creation.
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index 5913de4abe9bffa63954fe86eaff1a5630b995b6..067b37e0ebd7245c586943ca7e08e88703373c94 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -2,8 +2,9 @@ From iris.algebra Require Import csum auth excl frac gmap agree gset numbers.
From lrust.lifetime.model Require Import boxes.
From lrust.lifetime Require Export lifetime_sig.
From gpfsl.algebra Require Export lattice_cmra.
-Set Default Proof Using "Type".
-Import uPred.
+
+From iris.prelude Require Import options.
+
Implicit Types (Lat : latticeT) (E : coPset).
Definition inhN : namespace := lftN .@ "inh".
@@ -19,7 +20,7 @@ Module Export lft_notation.
End lft_notation.
Definition static : lft := (∅ : gmultiset _).
-Instance lft_intersect : Meet lft := λ κ κ', κ ⊎ κ'.
+Global Instance lft_intersect : Meet lft := λ κ κ', κ ⊎ κ'.
Definition positive_to_lft (p : positive) : lft := {[+ p +]}.
Inductive bor_state {Lat} :=
@@ -68,7 +69,7 @@ Definition lftPreG' := lftPreG.
Definition lftΣ Lat : gFunctors :=
#[ boxΣ Lat; GFunctor (authR (alftUR Lat)); GFunctor (authR ilftUR);
GFunctor (authR (borUR Lat)); GFunctor (authR natUR); GFunctor (authR inhUR) ].
-Instance subG_lftPreG Lat Σ :
+Global Instance subG_lftPreG Lat Σ :
subG (lftΣ Lat) Σ → lftPreG Σ Lat.
Proof. solve_inG. Qed.
@@ -87,7 +88,7 @@ Section defs.
Context `{!invGS Σ, !lftG Σ Lat userE}.
Notation iProp := (iProp Σ).
- Notation monPred := (monPred (lat_bi_index Lat) (uPredI (iResUR Σ))).
+ Notation monPred := (monPred (lat_bi_index Lat) (iPropI Σ)).
Definition lft_tok (q : Qp) (κ : lft) : monPred :=
([∗ mset] Λ ∈ κ, ∃ V, monPred_in V ∗
@@ -213,11 +214,11 @@ Section defs.
(∃ κ', lft_incl κ κ' ∗ raw_bor κ' P)%I.
End defs.
-Instance: Params (@lft_bor_alive) 6 := {}.
-Instance: Params (@lft_inh) 6 := {}.
-Instance idx_bor_params : Params (@idx_bor) 6 := {}.
-Instance: Params (@raw_bor) 5 := {}.
-Instance bor_params : Params (@bor) 5 := {}.
+Global Instance: Params (@lft_bor_alive) 6 := {}.
+Global Instance: Params (@lft_inh) 6 := {}.
+Global Instance idx_bor_params : Params (@idx_bor) 6 := {}.
+Global Instance: Params (@raw_bor) 5 := {}.
+Global Instance bor_params : Params (@bor) 5 := {}.
Notation "q .[ κ ]" := (lft_tok q κ)
(format "q .[ κ ]", at level 2, left associativity) : bi_scope.
@@ -247,8 +248,8 @@ Lemma lft_vs_inv_go_ne κ (f f' : ∀ κ', κ' ⊂ κ → monPred) Vs I n :
(∀ κ' (Hκ : κ' ⊂ κ), f κ' Hκ ≡{n}≡ f' κ' Hκ) →
lft_vs_inv_go κ f Vs I ≡{n}≡ lft_vs_inv_go κ f' Vs I.
Proof.
- intros Hf. apply sep_ne, big_opS_ne=> // κ' ?.
- apply forall_ne=> Hκ. by rewrite Hf.
+ intros Hf. apply bi.sep_ne, big_opS_ne=> // κ' ?.
+ apply bi.forall_ne=> Hκ. by rewrite Hf.
Qed.
Lemma lft_vs_go_ne κ (f f' : ∀ κ', κ' ⊂ κ → monPred) Pb Pb' Pi Pi' n :
@@ -265,7 +266,7 @@ Lemma lft_inv_alive_go_ne κ (f f' : ∀ κ', κ' ⊂ κ → monPred) n :
(∀ κ' (Hκ : κ' ⊂ κ), f κ' Hκ ≡{n}≡ f' κ' Hκ) →
lft_inv_alive_go κ f ≡{n}≡ lft_inv_alive_go κ f'.
Proof.
- intros Hf. apply exist_ne=> Pb; apply exist_ne=> Pi. by rewrite lft_vs_go_ne.
+ intros Hf. apply bi.exist_ne=> Pb; apply bi.exist_ne=> Pi. by rewrite lft_vs_go_ne.
Qed.
Lemma lft_inv_alive_unfold κ :
@@ -282,7 +283,7 @@ Lemma lft_vs_inv_unfold κ (I : gmap lft lft_names) Vs :
own_ilft_auth I ∗
[∗ set] κ' ∈ dom _ I, ⌜κ' ⊂ κ⌠→ lft_inv_alive κ' (Vs κ').
Proof.
- rewrite /lft_vs_inv /lft_vs_inv_go. by setoid_rewrite pure_impl_forall.
+ rewrite /lft_vs_inv /lft_vs_inv_go. by setoid_rewrite bi.pure_impl_forall.
Qed.
Lemma lft_vs_unfold κ Pb Pi :
lft_vs κ Pb Pi ⊣⊢ ∃ (Vκ : Lat) (n : nat), monPred_in Vκ ∗
diff --git a/theories/lifetime/model/faking.v b/theories/lifetime/model/faking.v
index 37b488cc520ed3baaca3569ec28257727b1c9de3..b499f090b05ca7a4c30dd229f3966bb177bd00ff 100644
--- a/theories/lifetime/model/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -1,12 +1,15 @@
From lrust.lifetime.model Require Export primitive.
From iris.algebra Require Import csum auth excl frac gmap agree gset numbers.
From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type*".
+
+From iris.prelude Require Import options.
Section faking.
Context `{!invGS Σ, !lftG Σ Lat userE, LatBottom Lat bot}.
Implicit Types κ : lft.
+Local Set Default Proof Using "Type*".
+
Lemma ilft_create A I κ :
own_alft_auth A -∗ own_ilft_auth I -∗ ▷ ([∗ set] κ ∈ dom _ I, lft_inv A κ)
==∗ ∃ A' I', ⌜κ ∈ dom (gset _) I'⌠∗
@@ -38,8 +41,8 @@ Proof.
{ iSplit.
- rewrite /lft_inv_dead. iExists True%I, bot. iFrame "Hcnt".
iSplit; [done|]. iSplitL "Hbor"; last by iApply "Hinh". rewrite /lft_bor_dead.
- iExists ∅, True%I. rewrite !fmap_empty.
- iSplitL "Hbor". iExists γs. by iFrame. iApply box_alloc.
+ iExists ∅, True%I. rewrite !fmap_empty. iSplitL "Hbor".
+ + iExists γs. by iFrame. + iApply box_alloc.
- rewrite lft_inv_alive_unfold. iExists True%I, True%I. iSplitL "Hbor".
{ rewrite /lft_bor_alive. iExists ∅.
rewrite /to_borUR !fmap_empty big_sepM_empty monPred_at_emp (right_id ).
diff --git a/theories/lifetime/model/in_at_borrow.v b/theories/lifetime/model/in_at_borrow.v
index a7677e2e32a2dff40d0e54970e55ac1e4f9f487a..9c2e1f597370fdeb5f93f1d1f953fa542d1cb6dc 100644
--- a/theories/lifetime/model/in_at_borrow.v
+++ b/theories/lifetime/model/in_at_borrow.v
@@ -1,7 +1,8 @@
From iris.algebra Require Import auth.
From lrust.lifetime Require Import borrow accessors.
From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type".
+
+From iris.prelude Require Import options.
(** Internal atomic persistent borrows. *)
(* They are like atomic persistent borrows, but use lftN as their
@@ -21,7 +22,7 @@ Definition in_at_bor `{invGS Σ, lftG Σ Lat userE} κ P :=
∗ ▷ □ (P' ↔ P) ∗ ⎡slice borN (i.2) P'⎤
∗ ⎡inv in_atN (∃ V', idx_bor_own i V')⎤)%I.
Notation "&in_at{ κ }" := (in_at_bor κ) (format "&in_at{ κ }") : bi_scope.
-Instance in_at_bor_params : Params (@in_at_bor) 5 := {}.
+Global Instance in_at_bor_params : Params (@in_at_bor) 5 := {}.
Section in_at.
Context `{invGS Σ, lftG Σ Lat userE}.
@@ -57,12 +58,12 @@ Lemma in_at_bor_acc E q κ P :
(monPred_in Vb → ▷ P) ∗ ((monPred_in Vb → ▷ P) ={E∖↑lftN,E}=∗ q.[κ]).
Proof.
iIntros (?) "#LFT Hb Htok". iDestruct "Hb" as (P' [κ' s]) "#(? & HPP' & Hs & ?)".
- iMod (lft_incl_acc with "[//] Htok") as (q') "[Htok Hclose]". done.
+ iMod (lft_incl_acc with "[//] Htok") as (q') "[Htok Hclose]". { done. }
iInv in_atN as (V0) ">Hown" "Hclose'". simpl.
iDestruct (monPred_in_intro with "Htok") as (V) "[#HV Htok]".
iMod (idx_bor_acc_internal with "LFT Hs Hown Htok") as (Vb) "(% & HP & Hclose'')".
- solve_ndisj. solve_ndisj.
- iMod fupd_mask_subseteq as "Hclose'''"; last iModIntro. solve_ndisj.
+ { solve_ndisj. } { solve_ndisj. }
+ iMod fupd_mask_subseteq as "Hclose'''"; last iModIntro. { solve_ndisj. }
iExists Vb. iSplitL "HP".
{ iIntros "HVb". iApply "HPP'". iApply (monPred_in_elim with "HVb").
by rewrite monPred_at_later. }
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 8d2d064f34855b3ec81dd9c41b1021a0f5d853c0..b1d80bdf4fd01f5e640d402c29d1332a97d8ea7c 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -2,8 +2,8 @@ From iris.algebra Require Import csum auth excl frac gmap agree gset proofmode_c
From iris.bi Require Import big_op fractional.
From iris.proofmode Require Import tactics.
From lrust.lifetime.model Require Export definitions boxes.
-Set Default Proof Using "Type".
-Import uPred.
+
+From iris.prelude Require Import options.
Lemma lft_init `{!invGS Σ, !lftPreG Σ Lat} E userE :
↑lftN ⊆ E → ↑lftN ## userE → ⊢ |={E}=> ∃ _ : lftG Σ Lat userE, lft_ctx.
@@ -71,7 +71,7 @@ Proof.
iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs. move : Hγs.
rewrite auth_frag_valid singleton_op singleton_valid=> /to_agree_op_inv_L <-.
- iExists γs. iSplit. done. rewrite own_op; iFrame.
+ iExists γs. iSplit; [done|]. rewrite own_op; iFrame.
Qed.
Global Instance own_bor_into_sep κ x x1 x2 :
IsOp x x1 x2 → IntoSep (own_bor κ x) (own_bor κ x1) (own_bor κ x2).
@@ -79,7 +79,7 @@ Proof. rewrite /IsOp /IntoSep=>->. by rewrite own_bor_op. Qed.
Lemma own_bor_valid κ x : own_bor κ x -∗ ✓ x.
Proof. iDestruct 1 as (γs) "[#? Hx]". by iApply own_valid. Qed.
Lemma own_bor_valid_2 κ x y : own_bor κ x -∗ own_bor κ y -∗ ✓ (x ⋅ y).
-Proof. apply wand_intro_r. rewrite -own_bor_op. apply own_bor_valid. Qed.
+Proof. apply bi.wand_intro_r. rewrite -own_bor_op. apply own_bor_valid. Qed.
Lemma own_bor_update κ x y : x ~~> y → own_bor κ x ==∗ own_bor κ y.
Proof.
iDestruct 1 as (γs) "[#Hκ Hx]"; iExists γs. iFrame "Hκ". by iApply own_update.
@@ -87,7 +87,7 @@ Qed.
Lemma own_bor_update_2 κ x1 x2 y :
x1 ⋅ x2 ~~> y → own_bor κ x1 ⊢ own_bor κ x2 ==∗ own_bor κ y.
Proof.
- intros. apply wand_intro_r. rewrite -own_bor_op. by apply own_bor_update.
+ intros. apply bi.wand_intro_r. rewrite -own_bor_op. by apply own_bor_update.
Qed.
Lemma own_cnt_auth I κ x : own_ilft_auth I -∗ own_cnt κ x -∗ ⌜κ ∈ dom (gset _) IâŒ.
@@ -113,7 +113,7 @@ Qed.
Lemma own_cnt_valid κ x : own_cnt κ x -∗ ✓ x.
Proof. iDestruct 1 as (γs) "[#? Hx]". by iApply own_valid. Qed.
Lemma own_cnt_valid_2 κ x y : own_cnt κ x -∗ own_cnt κ y -∗ ✓ (x ⋅ y).
-Proof. apply wand_intro_r. rewrite -own_cnt_op. apply own_cnt_valid. Qed.
+Proof. apply bi.wand_intro_r. rewrite -own_cnt_op. apply own_cnt_valid. Qed.
Lemma own_cnt_update κ x y : x ~~> y → own_cnt κ x ==∗ own_cnt κ y.
Proof.
iDestruct 1 as (γs) "[#Hκ Hx]"; iExists γs. iFrame "Hκ". by iApply own_update.
@@ -121,7 +121,7 @@ Qed.
Lemma own_cnt_update_2 κ x1 x2 y :
x1 ⋅ x2 ~~> y → own_cnt κ x1 -∗ own_cnt κ x2 ==∗ own_cnt κ y.
Proof.
- intros. apply wand_intro_r. rewrite -own_cnt_op. by apply own_cnt_update.
+ intros. apply bi.wand_intro_r. rewrite -own_cnt_op. by apply own_cnt_update.
Qed.
Lemma own_inh_auth I κ x : own_ilft_auth I -∗ own_inh κ x -∗ ⌜κ ∈ dom (gset _) IâŒ.
@@ -137,7 +137,7 @@ Proof.
iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs. move : Hγs.
rewrite -auth_frag_op auth_frag_valid singleton_op singleton_valid=> /to_agree_op_inv_L <-.
- iExists γs. iSplit. done. rewrite own_op; iFrame.
+ iExists γs. iSplit; [done|]. rewrite own_op; iFrame.
Qed.
Global Instance own_inh_into_sep κ x x1 x2 :
IsOp x x1 x2 → IntoSep (own_inh κ x) (own_inh κ x1) (own_inh κ x2).
@@ -147,7 +147,7 @@ Qed.
Lemma own_inh_valid κ x : own_inh κ x -∗ ✓ x.
Proof. iDestruct 1 as (γs) "[#? Hx]". by iApply own_valid. Qed.
Lemma own_inh_valid_2 κ x y : own_inh κ x -∗ own_inh κ y -∗ ✓ (x ⋅ y).
-Proof. apply wand_intro_r. rewrite -own_inh_op. apply own_inh_valid. Qed.
+Proof. apply bi.wand_intro_r. rewrite -own_inh_op. apply own_inh_valid. Qed.
Lemma own_inh_update κ x y : x ~~> y → own_inh κ x ==∗ own_inh κ y.
Proof.
iDestruct 1 as (γs) "[#Hκ Hx]"; iExists γs. iFrame "Hκ". by iApply own_update.
@@ -155,7 +155,7 @@ Qed.
Lemma own_inh_update_2 κ x1 x2 y :
x1 ⋅ x2 ~~> y → own_inh κ x1 ⊢ own_inh κ x2 ==∗ own_inh κ y.
Proof.
- intros. apply wand_intro_r. rewrite -own_inh_op. by apply own_inh_update.
+ intros. apply bi.wand_intro_r. rewrite -own_inh_op. by apply own_inh_update.
Qed.
(** Alive and dead *)
@@ -264,30 +264,30 @@ Proof.
Qed.
(** Basic rules about lifetimes *)
-Instance lft_inhabited : Inhabited lft := _.
-Instance bor_idx_inhabited : Inhabited bor_idx := _.
-Instance lft_intersect_comm : Comm (A:=lft) eq (⊓) := _.
-Instance lft_intersect_assoc : Assoc (A:=lft) eq (⊓) := _.
-Instance lft_intersect_inj_1 κ : Inj eq eq (κ ⊓.) := _.
-Instance lft_intersect_inj_2 κ : Inj eq eq (.⊓ κ) := _.
-Instance lft_intersect_left_id : LeftId eq static (⊓) := _.
-Instance lft_intersect_right_id : RightId eq static (⊓) := _.
+Local Instance lft_inhabited : Inhabited lft := _.
+Local Instance bor_idx_inhabited : Inhabited bor_idx := _.
+Local Instance lft_intersect_comm : Comm (A:=lft) eq (⊓) := _.
+Local Instance lft_intersect_assoc : Assoc (A:=lft) eq (⊓) := _.
+Local Instance lft_intersect_inj_1 κ : Inj eq eq (κ ⊓.) := _.
+Local Instance lft_intersect_inj_2 κ : Inj eq eq (.⊓ κ) := _.
+Local Instance lft_intersect_left_id : LeftId eq static (⊓) := _.
+Local Instance lft_intersect_right_id : RightId eq static (⊓) := _.
Lemma lft_tok_sep q κ1 κ2 : q.[κ1] ∗ q.[κ2] ⊣⊢ q.[κ1 ⊓ κ2].
Proof. by rewrite /lft_tok -big_sepMS_disj_union. Qed.
Lemma lft_dead_or κ1 κ2 : [†κ1] ∨ [†κ2] ⊣⊢ [†κ1 ⊓ κ2].
Proof.
- rewrite /lft_dead -or_exist. apply exist_proper=> Λ.
- rewrite -or_exist. apply exist_proper=> V'.
- rewrite -sep_or_r -pure_or. do 2 f_equiv. set_solver.
+ rewrite /lft_dead -bi.or_exist. apply bi.exist_proper=> Λ.
+ rewrite -bi.or_exist. apply bi.exist_proper=> V'.
+ rewrite -bi.sep_or_r -bi.pure_or. do 2 f_equiv. set_solver.
Qed.
Lemma lft_tok_dead q κ : q.[κ] -∗ [†κ] -∗ False.
Proof.
rewrite /lft_tok /lft_dead. iIntros "H".
iDestruct 1 as (Λ' V') "(% & #? & H')".
- iDestruct (@big_sepMS_elem_of _ _ _ _ _ _ Λ' with "H") as "H"=> //.
+ iDestruct (big_sepMS_elem_of _ _ Λ' with "H") as "H"=> //.
iDestruct "H" as (V'') "[#? H]". iDestruct (own_valid_2 with "H H'") as %Hvalid.
move: Hvalid=> /auth_frag_valid /=; by rewrite singleton_op singleton_valid.
Qed.
@@ -324,7 +324,7 @@ Proof.
Qed.
Global Instance lft_tok_as_fractional κ q :
AsFractional (q.[κ]) (λ q, q.[κ])%I q.
-Proof. split. done. apply _. Qed.
+Proof. split; [done|apply _]. Qed.
Global Instance frame_lft_tok p κ q1 q2 RES :
FrameFractionalHyps p q1.[κ] (λ q, q.[κ])%I RES q1 q2 →
Frame p q1.[κ] q2.[κ] RES | 5.
@@ -410,14 +410,14 @@ 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. iModIntro. iSplit; iIntros.
- by iApply "HPP'"; iApply "Hiff". by iApply "Hiff"; iApply "HPP'".
+ - 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. iModIntro. iSplit; iIntros.
- by iApply "HPP'"; iApply "HP0P". by iApply "HP0P"; iApply "HPP'".
+ iExists P0. iFrame. iIntros "!> !>". iSplit; iIntros.
+ - by iApply "HPP'"; iApply "HP0P". - by iApply "HP0P"; iApply "HPP'".
Qed.
Lemma bor_unfold_idx κ P : (&{κ}P)%I ⊣⊢ ∃ i, &{κ,i}P ∗ idx_bor_own i.
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index e3fdee53c8e0a3ccc63efc29afe87ca8aa3794fb..19111cb59b329ba2923de91d1d21a21b41caba7e 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -1,7 +1,8 @@
From lrust.lifetime Require Import borrow accessors.
From iris.algebra Require Import csum auth excl frac gmap agree gset numbers.
From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type*".
+
+From iris.prelude Require Import options.
Lemma and_extract_ownM {M} σ (P : uPred M) :
uPred_ownM σ ∧ P -∗ uPred_ownM σ ∗ (uPred_ownM σ -∗ P).
@@ -32,6 +33,8 @@ Section reborrow.
Context `{!invGS Σ, !lftG Σ Lat userE, LatBottom Lat}.
Implicit Types κ : lft.
+Local Set Default Proof Using "Type*".
+
(* Notice that taking lft_inv for both κ and κ' already implies
κ ≠κ'. Still, it is probably more instructing to require
κ ⊂ κ' in this lemma (as opposed to just κ ⊆ κ'), and it
@@ -172,7 +175,7 @@ Proof.
iDestruct (own_bor_valid_2 with "Hâ— Hbor")
as %[EQB%to_borUR_included _]%auth_both_valid_discrete.
iMod (slice_empty _ _ true with "Hs' Hbox") as "[Hidx Hbox]".
- solve_ndisj. by rewrite lookup_fmap EQB.
+ { solve_ndisj. } { by rewrite lookup_fmap EQB. }
iAssert (â–· ⌜κ ∈ dom (gset lft) IâŒ)%I with "[#]" as ">%".
{ iNext. iDestruct (monPred_in_elim with "HV' Hidx") as "Hidx".
iDestruct "HP'" as "[HP' _]". rewrite /idx_bor_own.
@@ -199,7 +202,7 @@ Proof.
iIntros "%% [??] %% _ !>". iNext. iRewrite "HeqPb'". iFrame. }
iDestruct "HH" as "([HI Hinvκ] & Hb & Halive & Hvs)".
iMod ("Hclose" with "[-Hb]"); last first.
- { iApply monPred_in_elim. done. by iFrame. }
+ { iApply (monPred_in_elim with "HV"). by iFrame. }
iExists _, _. iFrame. rewrite (big_sepS_delete _ (dom _ _) κ') //.
iDestruct ("Hclose'" with "Hinvκ") as "$".
rewrite /lft_inv. iExists Vκ. iSplit; [done|].
diff --git a/theories/lifetime/na_borrow.v b/theories/lifetime/na_borrow.v
index a5ed5cd9d84c99c412c2844a6a3bf95bc5ac447c..3b192a69e7da4d4c9e6b8810374b6b5a28994bda 100644
--- a/theories/lifetime/na_borrow.v
+++ b/theories/lifetime/na_borrow.v
@@ -1,7 +1,7 @@
From lrust.lifetime Require Export lifetime.
From gpfsl.logic Require Export na_invariants.
From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Definition na_bor `{!invGS Σ, !lftG Σ View userE, na_invG View bot Σ}
(κ : lft) (tid : na_inv_pool_name) (N : namespace) (P : monPred _ _) :=
@@ -45,7 +45,7 @@ Section na_bor.
iIntros (???) "#LFT#HP Hκ Hnaown".
iDestruct "HP" as (i) "(#Hpers&#Hinv)".
iMod (na_inv_acc with "Hinv Hnaown") as "(>Hown&Hnaown&Hclose)"; try done.
- iMod (idx_bor_acc_sync with "LFT Hpers Hown Hκ") as "[HP Hclose']". done.
+ iMod (idx_bor_acc_sync with "LFT Hpers Hown Hκ") as "[HP Hclose']"; [done|].
iIntros "{$HP $Hnaown} !> HP Hnaown".
iMod ("Hclose'" with "HP") as "[Hown $]". iApply "Hclose". by iFrame.
Qed.
diff --git a/theories/logic/gps.v b/theories/logic/gps.v
index f4bf46be77042abaf759f806990de6326e372aa1..9a0c6e92ad9992ffd25cf20117077b84ee10ded4 100644
--- a/theories/logic/gps.v
+++ b/theories/logic/gps.v
@@ -2,6 +2,7 @@ From iris.proofmode Require Import tactics.
From lrust.lang Require Import notation.
From lrust.lifetime Require Import at_borrow.
From gpfsl.gps Require Import middleware.
+From iris.prelude Require Import options.
Section gps_at_bor_SP.
Context `{!noprolG Σ, !atomicG Σ, !gpsG Σ Prtcl, !lftG Σ view_Lat lft_userE}
diff --git a/theories/typing/base.v b/theories/typing/base.v
index 547d7a2b2d9b900d83db6923c748e16203b819c2..8340847ef27fbff658aea05d73043e7ac36a516b 100644
--- a/theories/typing/base.v
+++ b/theories/typing/base.v
@@ -4,6 +4,7 @@ From gpfsl.base_logic Require Import na.
(* Last, so that we make sure we shadow the definition of delete for
sets coming from the prelude. *)
From lrust.lang Require Export new_delete.
+From iris.prelude Require Import options.
Open Scope Z_scope.
diff --git a/theories/typing/bool.v b/theories/typing/bool.v
index 436691de6bc6542b0ad0aa22dd8d088daec72653..e3141115ecaa2614b3cfa2ce49933734239c7cbf 100644
--- a/theories/typing/bool.v
+++ b/theories/typing/bool.v
@@ -1,6 +1,6 @@
From lrust.typing Require Export type.
From lrust.typing Require Import programs.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section bool.
Context `{!typeG Σ}.
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index 91971e0521e340bd766f0a4e89665d6ed6cbe5da..602de0b818200a14cffbb454a621dde74ea0a93f 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
From gpfsl.logic Require Import proofmode.
From lrust.typing Require Export uniq_bor shr_bor own.
From lrust.typing Require Import lft_contexts type_context programs.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
(** The rules for borrowing and derferencing borrowed non-Copy pointers are in
a separate file so make sure that own.v and uniq_bor.v can be compiled
@@ -16,10 +16,10 @@ Section borrow.
Proof.
iIntros (tid ??) "#LFT _ $ [H _]".
iDestruct "H" as ([[]|]) "[% Hown]"; try done. iDestruct "Hown" as "[Hmt ?]".
- iMod (bor_create with "LFT Hmt") as "[Hbor Hext]". done.
+ iMod (bor_create with "LFT Hmt") as "[Hbor Hext]". { done. }
iModIntro. rewrite /tctx_interp /=. iSplitL "Hbor"; last iSplit; last done.
- iExists _. auto.
- - iExists _. iSplit. done. by iFrame.
+ - iExists _. iSplit; [done|]. by iFrame.
Qed.
Lemma tctx_share E L p κ ty :
@@ -69,7 +69,7 @@ Section borrow.
((p â—{κ} own_ptr n ty)::T).
Proof.
intros. apply (tctx_incl_frame_r _ [_] [_;_]). rewrite subtype_tctx_incl.
- by apply tctx_borrow. by f_equiv.
+ - by apply tctx_borrow. - by f_equiv.
Qed.
(* See the comment above [tctx_extract_hasty_share]. *)
@@ -91,13 +91,13 @@ Section borrow.
iDestruct (llctx_interp_acc_noend with "HL") as "[HL HLclose]".
iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; first solve_ndisj.
wp_apply (wp_hasty with "Hp"); [done|]. iIntros ([[]|]) "_ Hown"; try done.
- iMod (bor_acc_cons with "LFT Hown Htok") as "[H↦ Hclose']". done.
+ iMod (bor_acc_cons with "LFT Hown Htok") as "[H↦ Hclose']". { done. }
iDestruct "H↦" as ([|[[|l'|]|][]]) "[>H↦ Hown]"; try iDestruct "Hown" as ">[]".
iDestruct "Hown" as "[Hown H†]". rewrite heap_mapsto_vec_singleton -wp_fupd. wp_read.
iMod ("Hclose'" $! (l↦#l' ∗ ⎡freeable_sz n (ty_size ty) l'⎤ ∗ _)%I
with "[] [H↦ Hown H†]") as "[Hbor Htok]"; last 1 first.
- - iMod (bor_sep with "LFT Hbor") as "[_ Hbor]". done.
- iMod (bor_sep with "LFT Hbor") as "[_ Hbor]". done.
+ - iMod (bor_sep with "LFT Hbor") as "[_ Hbor]". { done. }
+ iMod (bor_sep with "LFT Hbor") as "[_ Hbor]". { done. }
iMod ("Hclose" with "Htok") as "HL".
iDestruct ("HLclose" with "HL") as "$".
by rewrite tctx_interp_singleton tctx_hasty_val' //=.
@@ -124,7 +124,7 @@ Section borrow.
iMod (Hκ with "HE HL") as (q) "[[Htok1 Htok2] Hclose]"; first solve_ndisj.
wp_apply (wp_hasty with "Hp"); [done|]. iIntros ([[]|]) "_ Hown"; try done.
iDestruct "Hown" as (l') "#[H↦b #Hown]".
- iMod (frac_bor_acc with "LFT H↦b Htok1") as (q''') "[>H↦ Hclose']". done.
+ iMod (frac_bor_acc with "LFT H↦b Htok1") as (q''') "[>H↦ Hclose']". { done. }
iApply (wp_step_fupd _ _ (_∖_) with "[Hown Htok2]"); try done.
- iApply ("Hown" with "[%] Htok2"); first solve_ndisj.
- iApply wp_fupd. wp_read. iIntros "!>[#Hshr Htok2]".
@@ -152,11 +152,11 @@ Section borrow.
iDestruct (Hincl with "HL HE") as "%".
iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; first solve_ndisj.
wp_apply (wp_hasty with "Hp"); [done|]. iIntros ([[]|]) "_ Hown"; try done.
- iMod (bor_exists with "LFT Hown") as (vl) "Hbor". done.
- iMod (bor_sep with "LFT Hbor") as "[H↦ Hbor]". done.
+ iMod (bor_exists with "LFT Hown") as (vl) "Hbor". { done. }
+ iMod (bor_sep with "LFT Hbor") as "[H↦ Hbor]". { done. }
destruct vl as [|[[]|][]];
try by iMod (bor_persistent with "LFT Hbor Htok") as "[>[] _]".
- iMod (bor_acc with "LFT H↦ Htok") as "[>H↦ Hclose']". done.
+ iMod (bor_acc with "LFT H↦ Htok") as "[>H↦ Hclose']". { done. }
rewrite heap_mapsto_vec_singleton.
iMod (bor_unnest with "LFT Hbor") as "Hbor"; [done|].
iApply wp_fupd. wp_read.
@@ -165,7 +165,7 @@ Section borrow.
iDestruct ("HLclose" with "HL") as "$".
rewrite tctx_interp_singleton tctx_hasty_val' //.
iApply (bor_shorten with "[] Hbor").
- iApply lft_incl_glb. by iApply lft_incl_syn_sem. iApply lft_incl_refl.
+ iApply lft_incl_glb. - by iApply lft_incl_syn_sem. - iApply lft_incl_refl.
Qed.
Lemma type_deref_uniq_uniq {E L} κ κ' x p e ty C T T' :
@@ -186,7 +186,7 @@ Section borrow.
iMod (Hκ with "HE HL") as (q) "[[Htok1 Htok2] Hclose]"; first solve_ndisj.
wp_apply (wp_hasty with "Hp"); [done|]. iIntros ([[]|]) "_ Hshr"; try done.
iDestruct "Hshr" as (l') "[H↦ Hown]".
- iMod (frac_bor_acc with "LFT H↦ Htok1") as (q'') "[>H↦ Hclose']". done.
+ iMod (frac_bor_acc with "LFT H↦ Htok1") as (q'') "[>H↦ Hclose']". { done. }
iAssert (κ ⊑ κ' ⊓ κ)%I as "#Hincl'".
{ iApply lft_incl_glb.
+ by iApply lft_incl_syn_sem.
diff --git a/theories/typing/cont.v b/theories/typing/cont.v
index bbcf9c017015b4515f48473033998ac5b78bf9f6..302ab45bbfed40f59db00f29167d66c0f6820841 100644
--- a/theories/typing/cont.v
+++ b/theories/typing/cont.v
@@ -1,6 +1,6 @@
From lrust.typing Require Export type.
From lrust.typing Require Import programs.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section typing.
Context `{!typeG Σ}.
diff --git a/theories/typing/cont_context.v b/theories/typing/cont_context.v
index 6ce090e36765ea0d031fd1d3c962c0af913a4538..83704edb18ca47d36a92e513603dde8f545cc28f 100644
--- a/theories/typing/cont_context.v
+++ b/theories/typing/cont_context.v
@@ -1,6 +1,6 @@
From iris.proofmode Require Import tactics.
From lrust.typing Require Import type lft_contexts type_context.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section cont_context_def.
Context `{!typeG Σ}.
diff --git a/theories/typing/examples/get_x.v b/theories/typing/examples/get_x.v
index 5da7c4cd07efc311f8d9ccb0ade00c2ed9794a80..13a13f775bbae948a0385c5ce7c3cc2c957999f1 100644
--- a/theories/typing/examples/get_x.v
+++ b/theories/typing/examples/get_x.v
@@ -1,5 +1,5 @@
From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section get_x.
Context `{!typeG Σ}.
diff --git a/theories/typing/examples/init_prod.v b/theories/typing/examples/init_prod.v
index 2756e4fc161b7d7ae46b14ea9269db44fd251689..0aefa05040dc4f4ec9daf4d302ae8a7a26642068 100644
--- a/theories/typing/examples/init_prod.v
+++ b/theories/typing/examples/init_prod.v
@@ -1,5 +1,5 @@
From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section init_prod.
Context `{!typeG Σ}.
diff --git a/theories/typing/examples/lazy_lft.v b/theories/typing/examples/lazy_lft.v
index 8203e58019476b372aeabf7e4dbe2e38b0bd252d..d2434d4a141b11a14e04e5bcb412f0dec0f4bc9f 100644
--- a/theories/typing/examples/lazy_lft.v
+++ b/theories/typing/examples/lazy_lft.v
@@ -1,5 +1,5 @@
From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section lazy_lft.
Context `{!typeG Σ}.
diff --git a/theories/typing/examples/nonlexical.v b/theories/typing/examples/nonlexical.v
index de890d8b74d37871eacb3ae4db29d120a8705b61..76c961afbb27234c2e5cb31c344ba327c55116aa 100644
--- a/theories/typing/examples/nonlexical.v
+++ b/theories/typing/examples/nonlexical.v
@@ -1,4 +1,5 @@
From lrust.typing Require Import typing lib.option.
+From iris.prelude Require Import options.
(* Typing "problem case #3" from:
http://smallcultfollowing.com/babysteps/blog/2016/04/27/non-lexical-lifetimes-introduction/
@@ -73,7 +74,7 @@ Section non_lexical.
Lemma get_default_type :
typed_val get_default (fn(∀ m, ∅; &uniq{m} hashmap, K) → &uniq{m} V).
- Proof.
+ Proof using Type*.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>".
iIntros (m Ï ret p). inv_vec p=>map key. simpl_subst.
iApply type_let; [iApply get_mut_type|solve_typing|].
diff --git a/theories/typing/examples/rebor.v b/theories/typing/examples/rebor.v
index d9498d4565fb7ec15f7ea6a4bb6a962304df2408..958a34561cd70e1c600d23aaedd72aba5a21e422 100644
--- a/theories/typing/examples/rebor.v
+++ b/theories/typing/examples/rebor.v
@@ -1,5 +1,5 @@
From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section rebor.
Context `{!typeG Σ}.
diff --git a/theories/typing/examples/unbox.v b/theories/typing/examples/unbox.v
index f681022c887dd285912f2d32079672a65e2e5af9..05c510aef0969915db0f9a76bb22f53d00c1ce4a 100644
--- a/theories/typing/examples/unbox.v
+++ b/theories/typing/examples/unbox.v
@@ -1,5 +1,5 @@
From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section unbox.
Context `{!typeG Σ}.
diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index fa8f989e1849bb2c653c1c7c80a7614194a431ea..4262b17c62f5650dbc137e687443faa17f83e620 100644
--- a/theories/typing/fixpoint.v
+++ b/theories/typing/fixpoint.v
@@ -1,6 +1,6 @@
From gpfsl.logic Require Import proofmode.
From lrust.typing Require Export lft_contexts type bool.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Import uPred.
Section fixpoint_def.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 246d4334eef34bb62909b11b1679659df097d4bb..32472fbf770a4226dbaf6aee66c6561268d42a30 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -1,7 +1,7 @@
From iris.algebra Require Import vector list.
From lrust.typing Require Export type.
From lrust.typing Require Import own programs cont.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Implicit Types tid : thread_id.
@@ -140,7 +140,7 @@ Notation "'fn(' E ')' '→' R" :=
(at level 99, R at level 200,
format "'fn(' E ')' '→' R") : lrust_type_scope.
-Instance elctx_empty : Empty (lft → elctx) := λ Ï, [].
+Global Instance elctx_empty : Empty (lft → elctx) := λ Ï, [].
Section typing.
Context `{!typeG Σ}.
diff --git a/theories/typing/int.v b/theories/typing/int.v
index 595dcd76141295cfeaa4c5ccfd2677de4475b82e..b4e6fc4d525d9683aca98f4bf772ee0ae1b9a6e3 100644
--- a/theories/typing/int.v
+++ b/theories/typing/int.v
@@ -1,7 +1,7 @@
From iris.proofmode Require Import tactics.
From lrust.typing Require Export type.
From lrust.typing Require Import bool programs.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section int.
Context `{!typeG Σ}.
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index f0b1ce590d63d3675a3bcb8be2c40059b18c12aa..8195b3e06398a8c37613c17c984095dd6b18db76 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -3,7 +3,7 @@ From iris.bi Require Import fractional.
From lrust.typing Require Export base.
From lrust.lifetime Require Import frac_borrow.
From gpfsl.base_logic Require Import history.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Definition elctx_elt : Type := lft * lft.
Notation elctx := (list elctx_elt).
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index d844b74516c494d47d40b06aeda6051031fd8f8c..a545202b26d75c61ef753f7a73ed3570cb2fd3ed 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -9,7 +9,7 @@ From lrust.lifetime Require Import at_borrow.
From lrust.typing Require Export type.
From lrust.typing Require Import typing option.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Definition arcN := lrustN .@ "arc".
Definition arc_invN := arcN .@ "inv".
@@ -40,7 +40,7 @@ Section arc.
Proof.
unfold arc_persist, P1, P2. move => ???.
apply bi.sep_ne.
- - apply is_arc_contractive; eauto. done.
+ - apply is_arc_contractive; eauto; [done|].
solve_proper_core ltac:(fun _ => f_type_equiv || f_equiv).
- solve_proper_core ltac:(fun _ => exact: type_dist2_S || exact: type_dist2_dist ||
f_type_equiv || f_contractive || f_equiv).
@@ -564,7 +564,7 @@ Section arc.
{ iIntros "!> Hα".
iMod (at_bor_acc with "LFT Hrctokb Hα") as (Vb) "[Htok Hclose1]"; [solve_ndisj..|].
iExists Vb, q'. iFrame. iMod fupd_mask_subseteq as "Hclose2"; last iModIntro.
- solve_ndisj.
+ { solve_ndisj. }
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
iIntros (c) "[Hα _]". iMod ("Hclose1" with "Hα HL") as "HL".
(* Finish up the proof. *)
@@ -610,7 +610,7 @@ Section arc.
{ iIntros "!> Hα".
iMod (at_bor_acc with "LFT Hrctokb Hα") as (Vb) "[Htok Hclose1]"; [solve_ndisj..|].
iExists Vb, q'. iFrame. iMod fupd_mask_subseteq as "Hclose2"; last iModIntro.
- solve_ndisj. iFrame.
+ { solve_ndisj. } iFrame.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
iIntros (c) "[Hα _]". iMod ("Hclose1" with "Hα HL") as "HL".
(* Finish up the proof. *)
@@ -659,7 +659,7 @@ Section arc.
{ iIntros "!> Hα".
iMod (at_bor_acc with "LFT Hrctokb Hα") as (Vb) "[Htok Hclose1]"; [solve_ndisj..|].
iExists Vb, q'. iFrame. iMod fupd_mask_subseteq as "Hclose2"; last iModIntro.
- solve_ndisj. iFrame.
+ { solve_ndisj. } iFrame.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
iIntros (t'' q'') "[Hα Hown]". wp_seq. iMod ("Hclose1" with "Hα HL") as "HL".
(* Finish up the proof. *)
@@ -708,7 +708,7 @@ Section arc.
{ iIntros "!> Hα".
iMod (at_bor_acc with "LFT Hrctokb Hα") as (Vb) "[Htok Hclose1]"; [solve_ndisj..|].
iExists Vb, q'. iFrame. iMod fupd_mask_subseteq as "Hclose2"; last iModIntro.
- solve_ndisj. iFrame.
+ { solve_ndisj. } iFrame.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
iIntros (??) "[Hα Hown]". wp_seq. iMod ("Hclose1" with "Hα HL") as "HL".
(* Finish up the proof. *)
@@ -755,7 +755,7 @@ Section arc.
{ iIntros "!> Hα".
iMod (at_bor_acc with "LFT Hrctokb Hα") as (Vb) "[Htok Hclose1]"; [solve_ndisj..|].
iExists Vb, q'. iFrame. iMod fupd_mask_subseteq as "Hclose2"; last iModIntro.
- solve_ndisj. iFrame.
+ { solve_ndisj. } iFrame.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
iIntros (??) "[Hα Hown]". wp_seq. iMod ("Hclose1" with "Hα HL") as "HL".
(* Finish up the proof. *)
@@ -806,7 +806,7 @@ Section arc.
{ iIntros "!> Hα".
iMod (at_bor_acc with "LFT Hrctokb Hα") as (Vb) "[Htok Hclose1]"; [solve_ndisj..|].
iExists Vb, q0. iFrame. iMod fupd_mask_subseteq as "Hclose2"; last iModIntro.
- solve_ndisj. iFrame.
+ { solve_ndisj. } iFrame.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
iIntros ([] q') "[Hα Hown]"; wp_if; iMod ("Hclose1" with "Hα HL") as "HL".
- (* Finish up the proof (sucess). *)
@@ -921,7 +921,7 @@ Section arc.
rewrite !tctx_hasty_val [[rcx]]lock [[r]]lock. destruct rc' as [[|rc'|]|]=>//=.
iDestruct "Hrc'" as (γi γs γw γsw ν t q) "[#Hpersist Htok]". wp_bind (drop_weak _).
iApply (drop_weak_spec with "[] [Htok]");
- [|by iDestruct "Hpersist" as "[$?]"|by iExists _|]. solve_ndisj.
+ [|by iDestruct "Hpersist" as "[$?]"|by iExists _|]. { solve_ndisj. }
iIntros "!> * Hdrop". wp_bind (if: _ then _ else _)%E.
iApply (wp_wand _ _ _ (λ _, True)%I with "[Hdrop]").
{ destruct b; wp_if=>//. iDestruct "Hdrop" as "((? & H↦) & ? & ?)".
@@ -1202,7 +1202,8 @@ Section arc.
iDestruct "Hcl" as "[Hcl Hcl†]". iDestruct "Hcl" as (vl) "[Hcl↦ Hown]".
iDestruct (ty_size_eq with "Hown") as %Hsz.
iDestruct ("Hclose3" with "Hαν") as "[Hα2 Hν]".
- wp_apply wp_new=>//. lia. iIntros (l') "(Hl'†& Hl' & Hm')". wp_let. wp_op.
+ wp_apply wp_new=>//. { lia. }
+ iIntros (l') "(Hl'†& Hl' & Hm')". wp_let. wp_op.
rewrite shift_loc_0. rewrite -!lock Nat2Z.id.
rewrite !heap_mapsto_vec_cons shift_loc_assoc shift_loc_0.
iDestruct "Hl'" as "(Hl' & Hl'1 & Hl'2)". wp_write. wp_op. wp_write. wp_op.
@@ -1226,7 +1227,8 @@ Section arc.
!tctx_hasty_val' //. unlock. iFrame. iRight.
iExists _, _, _, _, _, _, _. iFrame "∗#". }
iApply type_letalloc_1; [solve_typing..|]. iIntros (rcold). simpl_subst.
- iApply type_let. apply arc_drop_type. solve_typing. iIntros (drop). simpl_subst.
+ iApply type_let. { apply arc_drop_type. } { solve_typing. }
+ iIntros (drop). simpl_subst.
iApply (type_letcall ()); [solve_typing..|]. iIntros (content). simpl_subst.
iApply type_delete; [solve_typing..|].
iApply type_assign; [solve_typing..|].
diff --git a/theories/typing/lib/brandedvec.v b/theories/typing/lib/brandedvec.v
index 677d1e25dea510143b79a65eb01c8f7855f0bc59..819648eb82ea375c91a533de5031ed4b9449af71 100644
--- a/theories/typing/lib/brandedvec.v
+++ b/theories/typing/lib/brandedvec.v
@@ -4,7 +4,7 @@ From lrust.lang Require Import notation new_delete.
From lrust.lifetime Require Import meta at_borrow.
From lrust.typing Require Import typing.
From lrust.typing.lib Require Import option.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Definition brandidx_stR := max_natUR.
Class brandidxG Σ := BrandedIdxG {
@@ -14,7 +14,7 @@ Class brandidxG Σ := BrandedIdxG {
Definition brandidxΣ : gFunctors
:= #[GFunctor (authR brandidx_stR); lft_metaΣ].
-Instance subG_brandidxΣ {Σ} : subG brandidxΣ Σ → brandidxG Σ.
+Global Instance subG_brandidxΣ {Σ} : subG brandidxΣ Σ → brandidxG Σ.
Proof. solve_inG. Qed.
Definition brandidxN := lrustN .@ "brandix".
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index 514fbd75ad2c85b25d45055c2129ed9d6b69af20..a1408fa414e438d0291975ef07e85cf3032f517f 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -3,7 +3,7 @@ From lrust.lang Require Import memcpy.
From lrust.lifetime Require Import na_borrow.
From lrust.typing Require Export type.
From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section cell.
Context `{!typeG Σ}.
diff --git a/theories/typing/lib/diverging_static.v b/theories/typing/lib/diverging_static.v
index 1c985a36742b5f30668cad9db79d47bd486c5662..5685986d7d84404d8a0a8dffe46d6601f6b28cc6 100644
--- a/theories/typing/lib/diverging_static.v
+++ b/theories/typing/lib/diverging_static.v
@@ -1,7 +1,7 @@
From iris.proofmode Require Import tactics.
From lrust.typing Require Export type.
From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section diverging_static.
Context `{!typeG Σ}.
diff --git a/theories/typing/lib/fake_shared.v b/theories/typing/lib/fake_shared.v
index 0b3db02beed2185a7989b9c84594963b53f295ae..4efaf32f616baa1dd44b4b1ddd8b7b1dac08dad5 100644
--- a/theories/typing/lib/fake_shared.v
+++ b/theories/typing/lib/fake_shared.v
@@ -1,6 +1,6 @@
From iris.proofmode Require Import tactics.
From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section fake_shared.
Context `{!typeG Σ}.
@@ -24,7 +24,8 @@ Section fake_shared.
iNext. destruct vl as [|[[|l'|]|][]]; try done. iExists l'. iSplit.
{ iApply frac_bor_iff; last done. iIntros "!>!> *".
rewrite heap_mapsto_vec_singleton. iSplit; auto. }
- iDestruct "H" as "#H". iIntros "!> * % $". iApply step_fupd_intro. set_solver.
+ iDestruct "H" as "#H". iIntros "!> * % $".
+ iApply step_fupd_intro. { set_solver. }
simpl. iApply ty_shr_mono; last done.
by iApply lft_incl_syn_sem. }
do 2 wp_seq.
@@ -55,7 +56,8 @@ Section fake_shared.
iNext. destruct vl as [|[[|l'|]|][]]; try done. iExists l'. iSplit.
{ iApply frac_bor_iff; last done. iIntros "!>!> *".
rewrite heap_mapsto_vec_singleton. iSplit; auto. }
- iDestruct "H" as "#H". iIntros "!> * % $". iApply step_fupd_intro. set_solver.
+ iDestruct "H" as "#H". iIntros "!> * % $".
+ iApply step_fupd_intro. { set_solver. }
simpl. iApply ty_shr_mono; last done.
by iApply lft_intersect_incl_l.
}
diff --git a/theories/typing/lib/join.v b/theories/typing/lib/join.v
index ef6a979e5464efa2e01d386caf4aadd4e87565d1..1ca6c637ed44da470983c820d161b9af99e9daca 100644
--- a/theories/typing/lib/join.v
+++ b/theories/typing/lib/join.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
From lrust.lang Require Import spawn.
From lrust.typing Require Export type.
From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Definition joinN := lrustN .@ "join".
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index 6d4f19975e42c318af099d1002df85d936e44f49..980f71a070aaac426893b0c1fe60b1c3e355f031 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -3,7 +3,7 @@ From lrust.lang Require Import memcpy lock.
From lrust.lifetime Require Import at_borrow.
From lrust.typing Require Export type.
From lrust.typing Require Import typing option.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Definition mutexN := lrustN .@ "mutex".
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index 6cb50d7220a96dfb749c56430c8d387966043475..c4fac885c1456fcea41172adbe4d55243f9765ce 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -3,7 +3,7 @@ From lrust.lang Require Import memcpy lock.
From lrust.lifetime Require Import at_borrow.
From lrust.typing Require Export type.
From lrust.typing Require Import typing util option mutex.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
(* This type is an experiment in defining a Rust type on top of a non-typesysten-specific
interface, like the one provided by lang.lock.
@@ -57,7 +57,7 @@ Section mguard.
iExists _. iFrame "H↦". iApply delay_sharing_nested; try done.
(* FIXME: "iApply lft_intersect_mono" only preserves the later on the last
goal, as does "iApply (lft_intersect_mono with ">")". *)
- iNext. iApply lft_intersect_mono. done. iApply lft_incl_refl.
+ iNext. iApply lft_intersect_mono; [done|]. iApply lft_incl_refl.
Qed.
Next Obligation.
iIntros (??????) "#? H". iDestruct "H" as (l') "[#Hf #H]".
@@ -65,10 +65,11 @@ Section mguard.
- by iApply frac_bor_shorten.
- iIntros "!> * % Htok".
iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
- { iApply lft_intersect_mono. iApply lft_incl_refl. done. }
- iMod ("H" with "[] Htok") as "Hshr". done. iModIntro. iNext.
+ { iApply lft_intersect_mono. - iApply lft_incl_refl. - done. }
+ iMod ("H" with "[] Htok") as "Hshr"; [done|]. iModIntro. iNext.
iMod "Hshr" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
- iApply ty_shr_mono; try done. iApply lft_intersect_mono. iApply lft_incl_refl. done.
+ iApply ty_shr_mono; try done. iApply lft_intersect_mono.
+ + iApply lft_incl_refl. + done.
Qed.
Global Instance mutexguard_wf α ty `{!TyWf ty} : TyWf (mutexguard α ty) :=
@@ -107,7 +108,7 @@ Section mguard.
iDestruct "H" as "[$ #H]". iIntros "!> * % Htok".
iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
{ iApply lft_intersect_mono; first by iApply lft_incl_syn_sem. iApply lft_incl_refl. }
- iMod ("H" with "[] Htok") as "Hshr". done. iModIntro. iNext.
+ iMod ("H" with "[] Htok") as "Hshr"; [done|]. iModIntro. iNext.
iMod "Hshr" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
iApply ty_shr_mono; try done.
+ iApply lft_intersect_mono; first by iApply lft_incl_syn_sem.
diff --git a/theories/typing/lib/option.v b/theories/typing/lib/option.v
index 66c6d79b7d91b64756aede9d73f14505b48eddb6..7fa43b4686ef00af5cfd9dbf48f49eecc6eda6fe 100644
--- a/theories/typing/lib/option.v
+++ b/theories/typing/lib/option.v
@@ -1,6 +1,6 @@
From iris.proofmode Require Import tactics.
From lrust.typing Require Import typing lib.panic.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section option.
Context `{!typeG Σ}.
diff --git a/theories/typing/lib/panic.v b/theories/typing/lib/panic.v
index f5564c57ba904fc61ff64bd69d2c24a4ca63cc48..67d3f232b0b724aa7969e879858b812a139bd696 100644
--- a/theories/typing/lib/panic.v
+++ b/theories/typing/lib/panic.v
@@ -1,6 +1,6 @@
From iris.proofmode Require Import tactics.
From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
(* Minimal support for panic. Lambdarust does not support unwinding the
stack. Instead, we just end the current thread by not calling any
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 193629bbdea230290561a9c4b33d2e9b941a47f3..fc119a2e86121a0d03b16c0b709edf9fc4fcc93c 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -3,14 +3,14 @@ From lrust.lang Require Import memcpy.
From lrust.lifetime Require Import na_borrow.
From lrust.typing Require Export type.
From lrust.typing Require Import typing option.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Definition rc_stR :=
prodUR (optionUR (csumR (prodR fracR positiveR) (exclR unitO))) natUR.
Class rcG Σ :=
RcG :> inG Σ (authR rc_stR).
Definition rcΣ : gFunctors := #[GFunctor (authR rc_stR)].
-Instance subG_rcΣ {Σ} : subG rcΣ Σ → rcG Σ.
+Global Instance subG_rcΣ {Σ} : subG rcΣ Σ → rcG Σ.
Proof. solve_inG. Qed.
Definition rc_tok q : authR rc_stR :=
@@ -278,7 +278,7 @@ Section code.
}}}.
Proof.
iIntros (? Φ) "[Hna [(Hl1 & Hl2 & H†& Hown)|Hown]] HΦ".
- - wp_read. iApply "HΦ". iFrame "Hl1". iLeft. iSplit. done. iSplit.
+ - wp_read. iApply "HΦ". iFrame "Hl1". iLeft. iSplit. { done. } iSplit.
+ iExists _. iFrame "Hl2". iLeft. iFrame. iSplit; first done.
iApply step_fupd_intro; auto.
+ iIntros "Hl1". iFrame. iApply step_fupd_intro; first done.
@@ -425,8 +425,8 @@ Section code.
iDestruct (own_valid_2 with "Hrcâ— Hrctok") as %[[[[=]|(?&[[q0 s0]| |]&[=<-]&?&Hincl)]
%option_included _]%prod_included [Hval _]]%auth_both_valid_discrete;
setoid_subst; try done; last first.
- { exfalso. destruct Hincl as [Hincl|Hincl]. by inversion Hincl.
- apply csum_included in Hincl. naive_solver. }
+ { exfalso. destruct Hincl as [Hincl|Hincl].
+ - by inversion Hincl. - apply csum_included in Hincl. naive_solver. }
iDestruct "Hrcst" as (qb) "(Hl'1 & Hl'2 & Hl'†& >% & Hνtok & Hν†)".
wp_read. wp_let.
(* And closing it again. *)
@@ -484,8 +484,9 @@ Section code.
iDestruct (own_valid_2 with "Hrcâ— Hrctok") as %[[[[=]|(?&[[q0 weak0]| |]&[=<-]&?&Hincl)]
%option_included _]%prod_included [Hval _]]%auth_both_valid_discrete;
setoid_subst; try done; last first.
- { exfalso. destruct Hincl as [Hincl|Hincl]. by inversion Hincl.
- apply csum_included in Hincl. naive_solver. }
+ { exfalso. destruct Hincl as [Hincl|Hincl].
+ - by inversion Hincl.
+ - apply csum_included in Hincl. naive_solver. }
iDestruct "Hrcst" as (qb) "(Hl'1 & Hl'2 & Hl'†& >% & Hνtok & Hν†)".
wp_read. wp_let.
(* And closing it again. *)
@@ -589,8 +590,9 @@ Section code.
iDestruct (own_valid_2 with "Hrcâ— Hrctok") as %[[[[=]|(?&[[q0 s0]| |]&[=<-]&?&Hincl)]
%option_included _]%prod_included [Hval _]]%auth_both_valid_discrete;
setoid_subst; try done; last first.
- { exfalso. destruct Hincl as [Hincl|Hincl]. by inversion Hincl.
- apply csum_included in Hincl. naive_solver. }
+ { exfalso. destruct Hincl as [Hincl|Hincl].
+ - by inversion Hincl.
+ - apply csum_included in Hincl. naive_solver. }
iDestruct "Hrcst" as (qb) "(Hl'1 & Hl'2 & Hl'†& >% & Hνtok & Hν†)".
wp_read. wp_let. wp_op. rewrite shift_loc_0. wp_op. wp_write. wp_write.
(* And closing it again. *)
@@ -1093,7 +1095,7 @@ Section code.
iDestruct "Hs" as "[Hs|Hν']"; last by iDestruct (lft_tok_dead with "Hν Hν'") as "[]".
wp_bind (of_val clone). iApply (wp_wand with "[Hna]").
{ iApply (Hclone _ [] $! _ 1%Qp with "LFT HE Hna").
- by rewrite /llctx_interp. by rewrite /tctx_interp. }
+ - by rewrite /llctx_interp. - by rewrite /tctx_interp. }
clear clone Hclone. iIntros (clone) "(Hna & _ & Hclone)".
wp_let. wp_let. rewrite tctx_interp_singleton tctx_hasty_val.
iDestruct (lft_intersect_acc with "Hα2 Hν") as (q'') "[Hαν Hclose3]".
@@ -1107,7 +1109,8 @@ Section code.
iDestruct "Hcl" as "[Hcl Hcl†]". iDestruct "Hcl" as (vl) "[Hcl↦ Hown]".
iDestruct (ty_size_eq with "Hown") as %Hsz.
iDestruct ("Hclose3" with "Hαν") as "[Hα2 Hν]".
- wp_apply wp_new=>//. lia. iIntros (l') "(Hl'†& Hl' & Hm')". wp_let. wp_op.
+ wp_apply wp_new=>//. { lia. }
+ iIntros (l') "(Hl'†& Hl' & Hm')". wp_let. wp_op.
rewrite shift_loc_0. rewrite -!lock Nat2Z.id.
rewrite !heap_mapsto_vec_cons shift_loc_assoc shift_loc_0.
iDestruct "Hl'" as "(Hl' & Hl'1 & Hl'2)". wp_write. wp_op. wp_write. wp_op.
@@ -1130,7 +1133,7 @@ Section code.
!tctx_hasty_val' //. unlock. iFrame. iRight. iExists γ, ν, _.
unfold rc_persist, tc_opaque. iFrame "∗#". eauto. }
iApply type_letalloc_1; [solve_typing..|]. iIntros (rcold). simpl_subst.
- iApply type_let. apply rc_drop_type. solve_typing. iIntros (drop). simpl_subst.
+ iApply type_let. { apply rc_drop_type. } { solve_typing. } iIntros (drop). simpl_subst.
iApply (type_letcall ()); [solve_typing..|]. iIntros (content). simpl_subst.
iApply type_delete; [solve_typing..|].
iApply type_assign; [solve_typing..|].
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index b6c6befbd6f010c078b98fb7af556af8931dea74..8632c8e50914a8b0253fa1a09a43765ed6bc8f10 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -5,7 +5,7 @@ From lrust.lifetime Require Import na_borrow.
From lrust.typing Require Export type.
From lrust.typing Require Import typing option.
From lrust.typing.lib Require Export rc.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section weak.
Context `{!typeG Σ, !rcG Σ}.
@@ -266,8 +266,8 @@ Section code.
iDestruct (own_valid_2 with "Hrcâ— Hrctok") as %[[[[=]|(?&[[q0 weak0]| |]&[=<-]&?&Hincl)]
%option_included _]%prod_included [Hval _]]%auth_both_valid_discrete;
setoid_subst; try done; last first.
- { exfalso. destruct Hincl as [Hincl|Hincl]. by inversion Hincl.
- apply csum_included in Hincl. naive_solver. }
+ { exfalso. destruct Hincl as [Hincl|Hincl].
+ - by inversion Hincl. - apply csum_included in Hincl. naive_solver. }
iDestruct "Hrcst" as (qb) "(Hl'1 & Hl'2 & Hrcst)".
wp_read. wp_let. wp_op. wp_op. wp_write. wp_write.
(* And closing it again. *)
diff --git a/theories/typing/lib/refcell/ref.v b/theories/typing/lib/refcell/ref.v
index 7de2d42616e85a042c8a33b35f6f86ed299f271e..f36c6f676ba56c154391952a51ac4de7a87ace97 100644
--- a/theories/typing/lib/refcell/ref.v
+++ b/theories/typing/lib/refcell/ref.v
@@ -3,7 +3,7 @@ From iris.bi Require Import fractional.
From lrust.lifetime Require Import na_borrow.
From lrust.typing Require Import typing.
From lrust.typing.lib.refcell Require Import refcell.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Definition refcell_refN := refcellN .@ "ref".
@@ -38,26 +38,26 @@ Section ref.
Next Obligation. iIntros (???[|[[]|][|[[]|][]]]) "?"; auto. Qed.
Next Obligation.
iIntros (α ty E κ l tid q ?) "#LFT Hb Htok".
- iMod (bor_exists with "LFT Hb") as (vl) "Hb". done.
- iMod (bor_sep with "LFT Hb") as "[H↦ Hb]". done.
- iMod (bor_fracture _ (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦". done.
+ iMod (bor_exists with "LFT Hb") as (vl) "Hb". { done. }
+ iMod (bor_sep with "LFT Hb") as "[H↦ Hb]". { done. }
+ iMod (bor_fracture _ (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦". { done. }
destruct vl as [|[[|lv|]|][|[[|lrc|]|][]]];
try by iMod (bor_persistent with "LFT Hb Htok") as "[>[] _]".
- iMod (bor_exists with "LFT Hb") as (ν) "Hb". done.
- iMod (bor_exists with "LFT Hb") as (q') "Hb". done.
- iMod (bor_exists with "LFT Hb") as (γ) "Hb". done.
- iMod (bor_exists with "LFT Hb") as (β) "Hb". done.
- iMod (bor_exists with "LFT Hb") as (ty') "Hb". done.
- iMod (bor_sep with "LFT Hb") as "[Hshr Hb]". done.
- iMod (bor_persistent with "LFT Hshr Htok") as "[#Hshr Htok]". done.
- iMod (bor_sep with "LFT Hb") as "[Hαβ Hb]". done.
- iMod (bor_persistent with "LFT Hαβ Htok") as "[#Hαβ Htok]". done.
- iMod (bor_sep with "LFT Hb") as "[Hinv Hb]". done.
- iMod (bor_persistent with "LFT Hinv Htok") as "[#Hinv $]". done.
- iMod (bor_sep with "LFT Hb") as "[Hκν Hb]". done.
+ iMod (bor_exists with "LFT Hb") as (ν) "Hb". { done. }
+ iMod (bor_exists with "LFT Hb") as (q') "Hb". { done. }
+ iMod (bor_exists with "LFT Hb") as (γ) "Hb". { done. }
+ iMod (bor_exists with "LFT Hb") as (β) "Hb". { done. }
+ iMod (bor_exists with "LFT Hb") as (ty') "Hb". { done. }
+ iMod (bor_sep with "LFT Hb") as "[Hshr Hb]". { done. }
+ iMod (bor_persistent with "LFT Hshr Htok") as "[#Hshr Htok]". { done. }
+ iMod (bor_sep with "LFT Hb") as "[Hαβ Hb]". { done. }
+ iMod (bor_persistent with "LFT Hαβ Htok") as "[#Hαβ Htok]". { done. }
+ iMod (bor_sep with "LFT Hb") as "[Hinv Hb]". { done. }
+ iMod (bor_persistent with "LFT Hinv Htok") as "[#Hinv $]". { done. }
+ iMod (bor_sep with "LFT Hb") as "[Hκν Hb]". { done. }
iDestruct (frac_bor_lft_incl with "LFT [> Hκν]") as "#Hκν".
- { iApply bor_fracture; try done. split. by rewrite Qp_mul_1_r. apply _. }
- iMod (bor_na with "Hb") as "#Hb". done. eauto 20.
+ { iApply bor_fracture; try done. split. - by rewrite Qp_mul_1_r. - apply _. }
+ iMod (bor_na with "Hb") as "#Hb". { done. } eauto 20.
Qed.
Next Obligation.
iIntros (??????) "#? H". iDestruct "H" as (ν q γ β ty' lv lrc) "H".
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 6d7bb9c4c12f62b7bd59d45467298515e6708305..06d306a1f9935e3611864c422e69e76770e7f312 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -3,7 +3,7 @@ From iris.bi Require Import fractional.
From lrust.lifetime Require Import lifetime na_borrow.
From lrust.typing Require Import typing.
From lrust.typing.lib.refcell Require Import refcell ref.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section ref_functions.
Context `{!typeG Σ, !refcellG Σ}.
@@ -56,10 +56,10 @@ Section ref_functions.
iDestruct "Hx'" as (ν q γ δ ty' lv lrc) "#(Hαν & Hfrac & Hshr & Hβδ & Hinv & H◯inv)".
wp_op.
iMod (lctx_lft_alive_tok β with "HE HL") as (qβ) "(Hβ & HL & Hclose)"; [solve_typing..|].
- iMod (lft_incl_acc with "Hβδ Hβ") as (qδ) "[Hδ Hcloseβ]". done.
+ iMod (lft_incl_acc with "Hβδ Hβ") as (qδ) "[Hδ Hcloseβ]". { done. }
iMod (lctx_lft_alive_tok_noend α with "HE HL") as (qα) "([Hα1 Hα2] & HL & Hclose')";
[solve_typing..|].
- iMod (frac_bor_acc with "LFT Hfrac Hα1") as (qlx') "[H↦ Hcloseα1]". done.
+ iMod (frac_bor_acc with "LFT Hfrac Hα1") as (qlx') "[H↦ Hcloseα1]". { done. }
iMod (na_bor_acc with "LFT Hinv Hδ Hna") as "(INV & Hna & Hcloseδ)"; [done..|].
iMod (na_bor_acc with "LFT H◯inv Hα2 Hna") as "(H◯ & Hna & Hcloseα2)"; [solve_ndisj..|].
rewrite {1}heap_mapsto_vec_cons heap_mapsto_vec_singleton.
@@ -115,7 +115,7 @@ Section ref_functions.
iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]=>//=.
iDestruct "Hx'" as (ν q γ δ ty' lv lrc) "#(Hαν & Hfrac & Hshr & Hx')".
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
- iMod (frac_bor_acc with "LFT Hfrac Hα") as (qlx') "[H↦ Hcloseα]". done.
+ iMod (frac_bor_acc with "LFT Hfrac Hα") as (qlx') "[H↦ Hcloseα]". { done. }
rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
iMod "H↦" as "[H↦1 H↦2]". wp_read. wp_let.
iMod ("Hcloseα" with "[$H↦1 $H↦2]") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
@@ -154,7 +154,7 @@ Section ref_functions.
iDestruct "Hx" as "[[Hx↦1 Hx↦2] Hx]". wp_op. wp_read. wp_let.
iDestruct "Hx" as (ν q γ β ty') "(_ & #Hαβ & #Hinv & Hν & H◯)".
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
- iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβ Hcloseα]". done.
+ iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβ Hcloseα]". { done. }
iMod (na_bor_acc with "LFT Hinv Hβ Hna") as "(INV & Hna & Hcloseβ)"; [done..|].
iDestruct (refcell_inv_reading_inv with "INV [$Hâ—¯]")
as (q' n) "(H↦lrc & >% & Hâ—â—¯ & H†& Hq' & Hshr)".
@@ -326,7 +326,7 @@ Section ref_functions.
{ rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton /= freeable_sz_full.
iFrame. }
iIntros "_".
- iMod (lft_incl_acc with "Hαβ Hα") as (?) "[Hβ Hβclose]". done.
+ iMod (lft_incl_acc with "Hαβ Hα") as (?) "[Hβ Hβclose]". { done. }
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γ")
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index 413bb764ac3700828f83f3582de15bf1e1e133f8..f96ffeffb48b58dd9c1fd4a11f3f94de35cbf3ce 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -2,7 +2,7 @@ From iris.algebra Require Import auth csum frac agree numbers.
From iris.bi Require Import fractional.
From lrust.lifetime Require Import na_borrow.
From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Definition refcell_stR :=
optionUR (prodR (prodR
@@ -12,7 +12,7 @@ Definition refcell_stR :=
Class refcellG Σ :=
RefCellG :> inG Σ (authR refcell_stR).
Definition refcellΣ : gFunctors := #[GFunctor (authR refcell_stR)].
-Instance subG_refcellΣ {Σ} : subG refcellΣ Σ → refcellG Σ.
+Global Instance subG_refcellΣ {Σ} : subG refcellΣ Σ → refcellG Σ.
Proof. solve_inG. Qed.
Definition refcell_st := option ((lft * Datatypes.bool) * frac * positive).
@@ -117,7 +117,7 @@ Section refcell.
Qed.
Next Obligation.
iIntros (ty E κ l tid q ?) "#LFT Hb Htok".
- iMod (bor_acc_cons with "LFT Hb Htok") as "[H Hclose]". done.
+ iMod (bor_acc_cons with "LFT Hb Htok") as "[H Hclose]". { done. }
iDestruct "H" as ([|[[| |n]|]vl]) "[H↦ H]"; try iDestruct "H" as ">[]".
iDestruct "H" as "Hown".
iMod ("Hclose" $! ((∃ n:Z, l ↦ #n) ∗
@@ -127,34 +127,35 @@ Section refcell.
iExists (#n'::vl'). rewrite heap_mapsto_vec_cons. iFrame. }
{ iNext. rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[Hn Hvl]".
iSplitL "Hn"; eauto with iFrame. }
- iMod (bor_sep with "LFT H") as "[Hn Hvl]". done.
- iMod (bor_acc_cons with "LFT Hn Htok") as "[H Hclose]". done.
+ iMod (bor_sep with "LFT H") as "[Hn Hvl]". { done. }
+ iMod (bor_acc_cons with "LFT Hn Htok") as "[H Hclose]". { done. }
iAssert ((q / 2).[κ] ∗ ▷ ∃ γ, refcell_inv tid l γ κ ty)%I with "[> -Hclose]"
as "[$ HQ]"; last first.
{ iMod ("Hclose" with "[] HQ") as "[Hb $]".
- iIntros "!> H !>". iNext. iDestruct "H" as (γ st) "(H & _ & _)". eauto.
- - iMod (bor_exists with "LFT Hb") as (γ) "Hb". done.
- iExists κ, γ. iSplitR. by iApply lft_incl_refl. by iApply bor_na. }
+ - iMod (bor_exists with "LFT Hb") as (γ) "Hb". { done. }
+ iExists κ, γ. iSplitR. + by iApply lft_incl_refl. + by iApply bor_na. }
clear dependent n. iDestruct "H" as ([|n|n]) "Hn"; try lia.
- iFrame. iMod (own_alloc (◠None)) as (γ) "Hst"; first by apply auth_auth_valid.
iExists γ, None. by iFrame.
- - iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". done.
+ - iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". { done. }
iMod (own_alloc (◠(refcell_st_to_R $ Some (ν, false, (1/2)%Qp, n)))) as (γ) "Hst".
{ by apply auth_auth_valid. }
iApply (fupd_mask_mono (↑lftN)); first done.
- iMod (rebor _ _ (κ ⊓ ν) with "LFT [] Hvl") as "[Hvl Hh]". done.
+ iMod (rebor _ _ (κ ⊓ ν) with "LFT [] Hvl") as "[Hvl Hh]". { done. }
{ iApply lft_intersect_incl_l. }
iDestruct (lft_intersect_acc with "Htok' Htok1") as (q') "[Htok Hclose]".
- iMod (ty_share with "LFT Hvl Htok") as "[Hshr Htok]". done.
+ iMod (ty_share with "LFT Hvl Htok") as "[Hshr Htok]". { done. }
iDestruct ("Hclose" with "Htok") as "[$ Htok]".
iExists γ, _. iFrame "Hst Hn Hshr".
iSplitR "Htok2"; last by iExists _; iFrame; rewrite Qp_div_2.
iIntros "!> !> Hν". iMod ("Hhν" with "Hν") as "Hν". iModIntro. iNext. iMod "Hν".
- iApply fupd_mask_mono; last iApply "Hh". set_solver+. rewrite -lft_dead_or. auto.
+ iApply fupd_mask_mono; last iApply "Hh". { set_solver+. }
+ rewrite -lft_dead_or. auto.
- iMod (own_alloc (◠(refcell_st_to_R $ Some (static, true, (1/2)%Qp, n)))) as (γ) "Hst".
{ by apply auth_auth_valid. }
iFrame "Htok'". iExists γ, _. iFrame. iSplitR.
- { rewrite -step_fupd_intro. auto. set_solver+. }
+ { rewrite -step_fupd_intro. - auto. - set_solver+. }
iSplitR; [|done]. iExists (1/2)%Qp. rewrite Qp_div_2. iSplitR; [done|].
iApply lft_tok_static.
Qed.
@@ -192,7 +193,7 @@ Section refcell.
- destruct vl as [|[[]|]]=>//=. by iApply "Hown".
- simpl. iDestruct "H" as (a γ) "[Ha H]". iExists a, γ. iFrame.
iApply na_bor_iff; last done. iNext; iModIntro; iSplit; iIntros "H".
- by iApply "Hty1ty2". by iApply "Hty2ty1".
+ + by iApply "Hty1ty2". + by iApply "Hty2ty1".
Qed.
Lemma refcell_mono' E L ty1 ty2 :
eqtype E L ty1 ty2 → subtype E L (refcell ty1) (refcell ty2).
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index ff38fa7655215943f494af7a0f4de910605bf514..961e4d958811c191410c97d77532f785b9f2246e 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -4,7 +4,7 @@ From lrust.lang Require Import memcpy.
From lrust.lifetime Require Import na_borrow.
From lrust.typing Require Import typing option.
From lrust.typing.lib.refcell Require Import refcell ref refmut.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section refcell_functions.
Context `{!typeG Σ, !refcellG Σ}.
@@ -153,7 +153,7 @@ Section refcell_functions.
iDestruct "HT" as "(Hx & Hx' & Hr)". destruct x' as [[|lx|]|]=>//=.
iDestruct "Hx'" as (β γ) "#[Hαβ Hinv]".
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
- iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[[Hβtok1 Hβtok2] Hclose']". done.
+ iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[[Hβtok1 Hβtok2] Hclose']". { done. }
iMod (na_bor_acc with "LFT Hinv Hβtok1 Hna") as "(INV & Hna & Hclose'')"; try done.
iDestruct "INV" as (st) "(Hlx & Hownst & Hst)". wp_read. wp_let. wp_op; case_bool_decide; wp_if.
- iMod ("Hclose''" with "[Hlx Hownst Hst] Hna") as "[Hβtok1 Hna]";
@@ -189,15 +189,15 @@ Section refcell_functions.
iFrame "∗#". iExists (Some (ν, false, _, _)). iFrame "∗#".
rewrite [_ â‹… _]comm -Some_op -!pair_op agree_idemp. iFrame.
iExists _. iFrame. rewrite -(assoc Qp_add) Qp_div_2 //.
- - iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". done.
+ - iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". { done. }
iMod (own_update with "Hownst") as "[Hownst Hreading]"; first by apply
auth_update_alloc, (op_local_update_discrete _ _ (reading_stR (1/2)%Qp ν)).
rewrite (right_id None). iExists _, _. iFrame "Htok1 Hreading".
iDestruct (lft_intersect_acc with "Hβtok2 Htok2") as (q) "[Htok Hclose]".
iApply (fupd_mask_mono (↑lftN)); first done.
- iMod (rebor _ _ (β ⊓ ν) with "LFT [] Hst") as "[Hst Hh]". done.
+ iMod (rebor _ _ (β ⊓ ν) with "LFT [] Hst") as "[Hst Hh]". { done. }
{ iApply lft_intersect_incl_l. }
- iMod (ty_share with "LFT Hst Htok") as "[#Hshr Htok]". done. iFrame "Hshr".
+ iMod (ty_share with "LFT Hst Htok") as "[#Hshr Htok]". { done. } iFrame "Hshr".
iDestruct ("Hclose" with "Htok") as "[$ Htok2]". iExists _. iFrame "∗#".
iSplitR "Htok2".
+ iIntros "!> Hν". iMod ("Hhν" with "Hν") as "Hν". iModIntro.
@@ -217,7 +217,7 @@ Section refcell_functions.
rewrite tctx_hasty_val' //. rewrite /= freeable_sz_full. iFrame.
iExists [_; _]. rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
iFrame. simpl. iExists _, _, _, _, _. iFrame "∗#". iApply ty_shr_mono; try by auto.
- iApply lft_intersect_mono. done. iApply lft_incl_refl. }
+ iApply lft_intersect_mono; [done|]. iApply lft_incl_refl. }
iApply (type_sum_memcpy (option $ ref α ty)); [solve_typing..|].
simpl. iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
@@ -263,7 +263,7 @@ Section refcell_functions.
iDestruct "HT" as "(Hx & Hx' & Hr)". destruct x' as [[|lx|]|]=>//=.
iDestruct "Hx'" as (β γ) "#[Hαβ Hinv]".
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
- iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβtok Hclose']". done.
+ iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβtok Hclose']". { done. }
iMod (na_bor_acc with "LFT Hinv Hβtok Hna") as "(INV & Hna & Hclose'')"; try done.
iDestruct "INV" as (st) "(Hlx & Hownst & Hb)". wp_read. wp_let. wp_op; case_bool_decide; wp_if.
- wp_write. wp_apply wp_new; [done..|].
@@ -271,13 +271,13 @@ Section refcell_functions.
rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
iDestruct "Hlref" as "[Hlref0 Hlref1]". wp_op. wp_write. wp_op. wp_write.
destruct st as [[[[ν []] s] n]|]; try done.
- iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". done.
+ iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". { done. }
iMod (own_update with "Hownst") as "[Hownst ?]".
{ by eapply auth_update_alloc,
(op_local_update_discrete _ _ (refcell_st_to_R $ Some (ν, true, (1/2)%Qp, xH))). }
rewrite (right_id None).
iApply fupd_wp. iApply (fupd_mask_mono (↑lftN)); first done.
- iMod (rebor _ _ (β ⊓ ν) with "LFT [] Hb") as "[Hb Hbh]". done.
+ iMod (rebor _ _ (β ⊓ ν) with "LFT [] Hb") as "[Hb Hbh]". { done. }
{ iApply lft_intersect_incl_l. }
iModIntro. iMod ("Hclose''" with "[Hlx Hownst Hbh Htok1] Hna") as "[Hβtok Hna]".
{ iExists _. iFrame. iNext. iSplitL "Hbh".
diff --git a/theories/typing/lib/refcell/refmut.v b/theories/typing/lib/refcell/refmut.v
index 57402d42bb78ec8070e10f630ec0280827a4a323..4898ebc7c9a4e5087f93fb8733301387c78182b6 100644
--- a/theories/typing/lib/refcell/refmut.v
+++ b/theories/typing/lib/refcell/refmut.v
@@ -3,7 +3,7 @@ From iris.bi Require Import fractional.
From lrust.lifetime Require Import na_borrow.
From lrust.typing Require Import typing util.
From lrust.typing.lib.refcell Require Import refcell.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section refmut.
Context `{!typeG Σ, !refcellG Σ}.
@@ -39,23 +39,23 @@ Section refmut.
Qed.
Next Obligation.
iIntros (α ty E κ l tid q HE) "#LFT Hb Htok".
- iMod (bor_exists with "LFT Hb") as (vl) "Hb". done.
- iMod (bor_sep with "LFT Hb") as "[H↦ Hb]". done.
- iMod (bor_fracture _ (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦". done.
+ iMod (bor_exists with "LFT Hb") as (vl) "Hb". { done. }
+ iMod (bor_sep with "LFT Hb") as "[H↦ Hb]". { done. }
+ iMod (bor_fracture _ (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦". { done. }
destruct vl as [|[[|lv|]|][|[[|lrc|]|][]]];
try by iMod (bor_persistent with "LFT Hb Htok") as "[>[] _]".
- iMod (bor_exists with "LFT Hb") as (ν) "Hb". done.
- iMod (bor_exists with "LFT Hb") as (q') "Hb". done.
- iMod (bor_exists with "LFT Hb") as (γ) "Hb". done.
- iMod (bor_exists with "LFT Hb") as (β) "Hb". done.
- iMod (bor_exists with "LFT Hb") as (ty') "Hb". done.
- iMod (bor_sep with "LFT Hb") as "[Hb H]". done.
- iMod (bor_sep with "LFT H") as "[Hαβ H]". done.
- iMod (bor_persistent with "LFT Hαβ Htok") as "[#Hαβ $]". done.
- iMod (bor_sep with "LFT H") as "[_ H]". done.
- iMod (bor_sep with "LFT H") as "[H _]". done.
+ iMod (bor_exists with "LFT Hb") as (ν) "Hb". { done. }
+ iMod (bor_exists with "LFT Hb") as (q') "Hb". { done. }
+ iMod (bor_exists with "LFT Hb") as (γ) "Hb". { done. }
+ iMod (bor_exists with "LFT Hb") as (β) "Hb". { done. }
+ iMod (bor_exists with "LFT Hb") as (ty') "Hb". { done. }
+ iMod (bor_sep with "LFT Hb") as "[Hb H]". { done. }
+ iMod (bor_sep with "LFT H") as "[Hαβ H]". { done. }
+ iMod (bor_persistent with "LFT Hαβ Htok") as "[#Hαβ $]". { done. }
+ iMod (bor_sep with "LFT H") as "[_ H]". { done. }
+ iMod (bor_sep with "LFT H") as "[H _]". { done. }
unshelve (iMod (bor_fracture _ (λ q, (q' * q).[ν])%I with "LFT H") as "H"=>//); try apply _; [|].
- { split. by rewrite Qp_mul_1_r. apply _. }
+ { split. - by rewrite Qp_mul_1_r. - apply _. }
iDestruct (frac_bor_lft_incl with "LFT H") as "#Hκν". iClear "H".
iExists _, _. iFrame "H↦". iApply delay_sharing_nested; try done.
rewrite -assoc. iApply lft_intersect_mono; first by iApply lft_incl_refl.
@@ -67,10 +67,11 @@ Section refmut.
- by iApply frac_bor_shorten.
- iIntros "!> * % Htok".
iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
- { iApply lft_intersect_mono. iApply lft_incl_refl. done. }
- iMod ("H" with "[] Htok") as "Hshr". done. iModIntro. iNext.
+ { iApply lft_intersect_mono. - iApply lft_incl_refl. - done. }
+ iMod ("H" with "[] Htok") as "Hshr". { done. } iModIntro. iNext.
iMod "Hshr" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
- iApply ty_shr_mono; try done. iApply lft_intersect_mono. iApply lft_incl_refl. done.
+ iApply ty_shr_mono; try done. iApply lft_intersect_mono.
+ + iApply lft_incl_refl. + done.
Qed.
Global Instance refmut_wf α ty `{!TyWf ty} : TyWf (refmut α ty) :=
@@ -105,7 +106,8 @@ Section refmut.
iMod ("H" with "[] Htok") as "Hshr"; first done. iModIntro. iNext.
iMod "Hshr" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
iApply ty_shr_mono; try done.
- + iApply lft_intersect_mono. by iApply lft_incl_syn_sem. iApply lft_incl_refl.
+ + iApply lft_intersect_mono.
+ * by iApply lft_incl_syn_sem. * iApply lft_incl_refl.
+ by iApply "Hs".
Qed.
Global Instance refmut_mono_flip E L :
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index 893d3a099c6a05e071dc436c4a2652c9e0bb2ddd..d6d019f794a6127e51b8b2291f664373fbf4b287 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -3,7 +3,7 @@ From iris.bi Require Import fractional.
From lrust.lifetime Require Import na_borrow.
From lrust.typing Require Import typing.
From lrust.typing.lib.refcell Require Import refcell refmut.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section refmut_functions.
Context `{!typeG Σ, !refcellG Σ}.
@@ -28,7 +28,7 @@ Section refmut_functions.
iDestruct "Hx'" as (lv lrc) "#(Hfrac & #Hshr)".
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "([Hα1 Hα2] & HL & Hclose')";
[solve_typing..|].
- iMod (frac_bor_acc with "LFT Hfrac Hα1") as (qlx') "[H↦ Hcloseα1]". done.
+ iMod (frac_bor_acc with "LFT Hfrac Hα1") as (qlx') "[H↦ Hcloseα1]". { done. }
rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
iMod (lctx_lft_alive_tok_noend β with "HE HL") as (qβ) "(Hβ & HL & Hclose'')";
[solve_typing..|].
@@ -63,27 +63,27 @@ Section refmut_functions.
iIntros (tid qmax) "#LFT #HE Hna HL Hk HT". simpl_subst.
rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]; try done.
- iMod (bor_exists with "LFT Hx'") as (vl) "H". done.
- iMod (bor_sep with "LFT H") as "[H↦ H]". done.
+ iMod (bor_exists with "LFT Hx'") as (vl) "H". { done. }
+ iMod (bor_sep with "LFT H") as "[H↦ H]". { done. }
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose')";
[solve_typing..|].
destruct vl as [|[[|lv|]|][|[[|lrc|]|][]]]; simpl;
try by iMod (bor_persistent with "LFT H Hα") as "[>[] _]".
- iMod (bor_exists with "LFT H") as (ν) "H". done.
- iMod (bor_exists with "LFT H") as (q) "H". done.
- iMod (bor_exists with "LFT H") as (γ) "H". done.
- iMod (bor_exists with "LFT H") as (δ) "H". done.
- iMod (bor_exists with "LFT H") as (ty') "H". done.
- iMod (bor_sep with "LFT H") as "[Hb H]". done.
- iMod (bor_sep with "LFT H") as "[Hβδ H]". done.
- iMod (bor_persistent with "LFT Hβδ Hα") as "[#Hβδ Hα]". done.
- iMod (bor_sep with "LFT H") as "[_ H]". done.
- iMod (bor_sep with "LFT H") as "[H _]". done.
+ iMod (bor_exists with "LFT H") as (ν) "H". { done. }
+ iMod (bor_exists with "LFT H") as (q) "H". { done. }
+ iMod (bor_exists with "LFT H") as (γ) "H". { done. }
+ iMod (bor_exists with "LFT H") as (δ) "H". { done. }
+ iMod (bor_exists with "LFT H") as (ty') "H". { done. }
+ iMod (bor_sep with "LFT H") as "[Hb H]". { done. }
+ iMod (bor_sep with "LFT H") as "[Hβδ H]". { done. }
+ iMod (bor_persistent with "LFT Hβδ Hα") as "[#Hβδ Hα]". { done. }
+ iMod (bor_sep with "LFT H") as "[_ H]". { done. }
+ iMod (bor_sep with "LFT H") as "[H _]". { done. }
unshelve (iMod (bor_fracture _ (λ q', (q * q').[ν])%I with "LFT H") as "H"=>//); try apply _; try done.
- { split. by rewrite Qp_mul_1_r. apply _. }
+ { split. - by rewrite Qp_mul_1_r. - apply _. }
iDestruct (frac_bor_lft_incl _ _ q with "LFT H") as "#Hαν". iClear "H".
- rewrite heap_mapsto_vec_cons. iMod (bor_sep with "LFT H↦") as "[H↦ _]". done.
- iMod (bor_acc with "LFT H↦ Hα") as "[H↦ Hcloseα]". done.
+ rewrite heap_mapsto_vec_cons. iMod (bor_sep with "LFT H↦") as "[H↦ _]". { done. }
+ iMod (bor_acc with "LFT H↦ Hα") as "[H↦ Hcloseα]". { done. }
wp_bind (!#lx')%E. iMod (bor_unnest with "LFT Hb") as "Hb"; first done.
wp_read. wp_let. iMod "Hb".
iMod ("Hcloseα" with "[$H↦]") as "[_ Hα]". iMod ("Hclose'" with "Hα HL") as "HL".
@@ -123,7 +123,7 @@ Section refmut_functions.
iDestruct "Hx" as (ν q γ β ty') "(Hb & #Hαβ & #Hinv & Hν & H◯)".
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)";
[solve_typing..|].
- iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβ Hcloseα]". done.
+ iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβ Hcloseα]". { done. }
iMod (na_bor_acc with "LFT Hinv Hβ Hna") as "(INV & Hna & Hcloseβ)"; [done..|].
iDestruct "INV" as (st) "(H↦lrc & H◠& INV)". wp_read. wp_let. wp_op. wp_write.
iAssert (|={↑lftN ∪ lft_userE}[lft_userE]▷=> refcell_inv tid lrc γ β ty')%I
@@ -192,7 +192,7 @@ Section refmut_functions.
rewrite {1}heap_mapsto_vec_cons heap_mapsto_vec_singleton.
iDestruct "Href" as "[[Href↦1 Href↦2] Href]".
iDestruct "Href" as (ν q γ β ty') "(Hbor & #Hαβ & #Hinv & >Hν & Hγ)".
- wp_read. wp_let. wp_apply wp_new; first done. done. done.
+ wp_read. wp_let. wp_apply wp_new; [done..|].
iIntros (lx) "(H†& Hlx & ?)". rewrite heap_mapsto_vec_singleton.
wp_let. wp_write. wp_let. rewrite tctx_hasty_val.
iMod (lctx_lft_alive_tok α with "HE HL") as (?) "(Hα & HL & Hclose1)";[solve_typing..|].
@@ -297,7 +297,7 @@ Section refmut_functions.
{ rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton /= freeable_sz_full.
iFrame. }
iIntros "_".
- iMod (lft_incl_acc with "Hαβ Hα") as (?) "[Hβ Hβclose]". done.
+ iMod (lft_incl_acc with "Hαβ Hα") as (?) "[Hβ Hβclose]". { done. }
iMod (na_bor_acc with "LFT Hinv Hβ Hna") as "(INV & Hna & Hclosena)"; [done..|].
wp_seq. wp_op. wp_read.
iDestruct "INV" as (st) "(Hlrc & Hâ— & Hst)".
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index d7e916651c5ae42fefe7a771345d3be44a3a4e70..ec6c4eba61599e965150207957cd21a5d2720f4f 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -5,7 +5,7 @@ From gpfsl.gps Require Import middleware protocols.
From lrust.lifetime Require Import at_borrow.
From lrust.typing Require Import typing.
From lrust.logic Require Import gps.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Definition rwlock_st := option (() + lft * frac * positive).
@@ -19,7 +19,7 @@ Class rwlockG Σ := RwLockG {
}.
Definition rwlockΣ : gFunctors := #[GFunctor rwlockR; gpsΣ unitProtocol; atomicΣ].
-Instance subG_rwlockΣ {Σ} : subG rwlockΣ Σ → rwlockG Σ.
+Global Instance subG_rwlockΣ {Σ} : subG rwlockΣ Σ → rwlockG Σ.
Proof. solve_inG. Qed.
Definition rwlock_to_st (st : rwlock_st) : rwlock_stR :=
@@ -396,7 +396,7 @@ Section rwlock.
Qed.
Next Obligation.
iIntros (ty E κ l tid q ?) "#LFT Hb Htok".
- iMod (bor_acc_cons with "LFT Hb Htok") as "[H Hclose]". done.
+ iMod (bor_acc_cons with "LFT Hb Htok") as "[H Hclose]". { done. }
iDestruct "H" as ([|[[| |n]|]vl]) "[H↦ [#hInv H]]"; try iDestruct "H" as ">[]".
iDestruct "H" as "[>% Hown]".
iMod ("Hclose" $! ((∃ n:Z, l ↦ #n ∗ ⌜-1 ≤ nâŒ) ∗
@@ -406,8 +406,8 @@ Section rwlock.
iExists (#n'::vl'). rewrite heap_mapsto_vec_cons. iFrame "∗% hInv". }
{ iNext. rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[Hn Hvl]".
iSplitL "Hn"; [eauto|iExists _; iFrame]. }
- iMod (bor_sep with "LFT H") as "[Hn Hvl]". done.
- iMod (rwlock_proto_create with "LFT Htok hInv Hvl Hn") as "[$ Hproto]". done.
+ iMod (bor_sep with "LFT H") as "[Hn Hvl]". { done. }
+ iMod (rwlock_proto_create with "LFT Htok hInv Hvl Hn") as "[$ Hproto]". { done. }
iExists κ. iFrame "Hproto". by iApply lft_incl_refl.
Qed.
Next Obligation.
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index d34eb9ccfd3d9afbbd0c9392958920bd44e5eb1e..db82f8519501eccb20538b8ddb492c42f8753466 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -7,7 +7,7 @@ From lrust.lang Require Import memcpy.
From lrust.lifetime Require Import at_borrow.
From lrust.typing Require Import typing option.
From lrust.typing.lib.rwlock Require Import rwlock rwlockreadguard rwlockwriteguard.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
(** SYNCHRONIZATION CONDITIONS of rwlock *)
(* ---> stands for Release-Acquire synchronization.
@@ -176,7 +176,7 @@ Section rwlock_functions.
iDestruct "Hx'" as (β) "#[Hαβ Hinv]".
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)";
[solve_typing..|].
- iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβtok Hclose']". done.
+ iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβtok Hclose']". { done. }
iDestruct (lft_tok_split_obj (qβ/2) (qβ/2) β with "[Hβtok]")
as "[Hβtok1 Hβtok2]". { by rewrite Qp_div_2. }
iDestruct "Hinv" as (γ γs tyO tyS) "(EqO & EqS & R)".
@@ -262,14 +262,15 @@ Section rwlock_functions.
iExists (). iSplitL ""; [done|]. iIntros (t2 Ext2) "W' !>". iSplitL "".
{ rewrite /Q1 Eqst2. by iIntros "!> $". } iIntros "!> !>".
iDestruct (GPS_SWSharedWriter_Reader_update with "W' R") as "[W' [R1 R2]]".
- iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #H†]". solve_ndisj.
+ iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #H†]". { solve_ndisj. }
iMod (rwown_update_write_read ν γs with "g") as "[g rst]".
iDestruct (lft_intersect_acc with "Hβtok2 Htok2") as (q) "[Htok Hclose]".
iApply (fupd_mask_mono (↑lftN ∪ lft_userE)).
{ apply union_subseteq; split; solve_ndisj. }
iMod (rebor _ _ (β ⊓ ν) with "LFT [] Hown") as "[Hst Hh]";
[apply union_subseteq_l|iApply lft_intersect_incl_l|].
- iMod ("Share" with "[%] Hst Htok") as "[#Hshr Htok]". apply union_subseteq_l.
+ iMod ("Share" with "[%] Hst Htok") as "[#Hshr Htok]".
+ { apply union_subseteq_l. }
iDestruct ("Hclose" with "Htok") as "[Hβtok2 Htok2]".
iModIntro. iSplitL "Htok2 rst R1 Hβtok2".
+ iFrame "Hβtok2". iExists _,_. rewrite Eqst2.
@@ -307,7 +308,7 @@ Section rwlock_functions.
iSpecialize ("Hk" with "[]"); first solve_typing.
iApply ("Hk" $! [#] with "Hna HL").
rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame.
- iExists _. iSplit. done. iExists _. iFrame "Hαβ".
+ iExists _. iSplit; [done|]. iExists _. iFrame "Hαβ".
iExists _,_,_,_. iFrame "EqO EqS". by iExists _,_.
Qed.
@@ -346,7 +347,7 @@ Section rwlock_functions.
iDestruct "Hinv" as (γ γs tyO tyS) "(EqO & EqS & R)".
iDestruct "R" as (tP vP) "R".
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
- iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβtok Hclose']". done.
+ iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβtok Hclose']". { done. }
wp_bind (CAS _ _ _ _ _ _).
set Q : time → () → vProp Σ :=
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index af08b2af9c2acdf0b7d2dd43202d4a77f1600cdc..d2d965a5b6317acd2355a106ca2c17c419bd113a 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -5,7 +5,7 @@ From lrust.lifetime Require Import at_borrow.
From lrust.typing Require Import typing.
From lrust.typing.lib.rwlock Require Import rwlock.
From gpfsl.gps Require Import middleware.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section rwlockreadguard.
Context `{!typeG Σ, !rwlockG Σ}.
@@ -35,21 +35,21 @@ Section rwlockreadguard.
Next Obligation. intros α ty tid [|[[]|] []]; auto. Qed.
Next Obligation.
iIntros (α ty E κ l tid q ?) "#LFT Hb Htok".
- iMod (bor_exists with "LFT Hb") as (vl) "Hb". done.
- iMod (bor_sep with "LFT Hb") as "[H↦ Hb]". done.
- iMod (bor_fracture _ (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦". done.
+ iMod (bor_exists with "LFT Hb") as (vl) "Hb". { done. }
+ iMod (bor_sep with "LFT Hb") as "[H↦ Hb]". { done. }
+ iMod (bor_fracture _ (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦". { done. }
destruct vl as [|[[|l'|]|][]];
try by iMod (bor_persistent with "LFT Hb Htok") as "[>[] _]".
- iMod (bor_exists with "LFT Hb") as (ν) "Hb". done.
- iMod (bor_exists with "LFT Hb") as (q') "Hb". done.
- iMod (bor_exists with "LFT Hb") as (γs) "Hb". done.
- iMod (bor_exists with "LFT Hb") as (β) "Hb". done.
- iMod (bor_exists with "LFT Hb") as (tid_own) "Hb". done.
- iMod (bor_sep with "LFT Hb") as "[Hshr Hb]". done.
- iMod (bor_persistent with "LFT Hshr Htok") as "[#Hshr Htok]". done.
- iMod (bor_sep with "LFT Hb") as "[Hαβ Hb]". done.
- iMod (bor_persistent with "LFT Hαβ Htok") as "[#Hαβ $]". done.
- iMod (bor_sep with "LFT Hb") as "[Hκν _]". done.
+ iMod (bor_exists with "LFT Hb") as (ν) "Hb". { done. }
+ iMod (bor_exists with "LFT Hb") as (q') "Hb". { done. }
+ iMod (bor_exists with "LFT Hb") as (γs) "Hb". { done. }
+ iMod (bor_exists with "LFT Hb") as (β) "Hb". { done. }
+ iMod (bor_exists with "LFT Hb") as (tid_own) "Hb". { done. }
+ iMod (bor_sep with "LFT Hb") as "[Hshr Hb]". { done. }
+ iMod (bor_persistent with "LFT Hshr Htok") as "[#Hshr Htok]". { done. }
+ iMod (bor_sep with "LFT Hb") as "[Hαβ Hb]". { done. }
+ iMod (bor_persistent with "LFT Hαβ Htok") as "[#Hαβ $]". { done. }
+ iMod (bor_sep with "LFT Hb") as "[Hκν _]". { done. }
iDestruct (frac_bor_lft_incl with "LFT [> Hκν]") as "#Hκν".
{ iApply bor_fracture; try done. constructor; [by rewrite Qp_mul_1_r|apply _]. }
iExists _. iFrame "#". iApply ty_shr_mono; last done.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index 3df7e309e3fed3ed9ec32e081049bfddb8d7396f..56cfca652c14ce992f4a50369608c2cb06e4d831 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -6,7 +6,7 @@ From lrust.logic Require Import gps.
From lrust.lifetime Require Import at_borrow.
From lrust.typing Require Import typing.
From lrust.typing.lib.rwlock Require Import rwlock rwlockreadguard.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section rwlockreadguard_functions.
Context `{!typeG Σ, !rwlockG Σ}.
@@ -31,7 +31,7 @@ Section rwlockreadguard_functions.
iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]; try done.
iDestruct "Hx'" as (l') "#[Hfrac Hshr]".
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
- iMod (frac_bor_acc with "LFT Hfrac Hα") as (qlx') "[H↦ Hcloseα]". done.
+ iMod (frac_bor_acc with "LFT Hfrac Hα") as (qlx') "[H↦ Hcloseα]". { done. }
rewrite heap_mapsto_vec_singleton. wp_read. wp_op. wp_let.
iMod ("Hcloseα" with "[$H↦]") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
iDestruct (lctx_lft_incl_incl α β with "HL HE") as %?; [solve_typing..|].
@@ -78,7 +78,7 @@ Section rwlockreadguard_functions.
iDestruct "Hinv" as (γ tyO tyS) "(R & #EqO & #EqS & R')".
iDestruct "R'" as (tR vR) "R'".
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
- iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβ Hcloseα]". done.
+ iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβ Hcloseα]". { done. }
wp_bind (!ʳˡˣ#lx')%E.
iApply (GPS_aSP_Read rwlockN _ _ _ β qβ
(λ _ _ v, ∃ st, ⌜v = #(Z_of_rwlock_st st)âŒ)%I with "[$LFT $Hβ $R']");
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index 368a7b603bb9c5cec9735fc077afe3a5b6169f19..68196e985488b102e8e04f87609ada0139eafaa0 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -5,7 +5,7 @@ From lrust.lifetime Require Import at_borrow.
From lrust.typing Require Import util typing.
From lrust.typing.lib.rwlock Require Import rwlock.
From gpfsl.gps Require Import middleware.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section rwlockwriteguard.
Context `{!typeG Σ, !rwlockG Σ}.
@@ -36,21 +36,21 @@ Section rwlockwriteguard.
Next Obligation. by iIntros (???[|[[]|][]]) "?". Qed.
Next Obligation.
iIntros (α ty E κ l tid q HE) "#LFT Hb Htok".
- iMod (bor_exists with "LFT Hb") as (vl) "Hb". done.
- iMod (bor_sep with "LFT Hb") as "[H↦ Hb]". done.
- iMod (bor_fracture _ (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦". done.
+ iMod (bor_exists with "LFT Hb") as (vl) "Hb". { done. }
+ iMod (bor_sep with "LFT Hb") as "[H↦ Hb]". { done. }
+ iMod (bor_fracture _ (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦". { done. }
destruct vl as [|[[|l'|]|][]];
try by iMod (bor_persistent with "LFT Hb Htok") as "[>[] _]".
- iMod (bor_exists with "LFT Hb") as (γs) "Hb". done.
- iMod (bor_exists with "LFT Hb") as (β) "Hb". done.
- iMod (bor_exists with "LFT Hb") as (tid_shr) "Hb". done.
- iMod (bor_sep with "LFT Hb") as "[Hb H]". done.
- iMod (bor_sep with "LFT H") as "[Hαβ _]". done.
- iMod (bor_persistent with "LFT Hαβ Htok") as "[#Hαβ $]". done.
+ iMod (bor_exists with "LFT Hb") as (γs) "Hb". { done. }
+ iMod (bor_exists with "LFT Hb") as (β) "Hb". { done. }
+ iMod (bor_exists with "LFT Hb") as (tid_shr) "Hb". { done. }
+ iMod (bor_sep with "LFT Hb") as "[Hb H]". { done. }
+ iMod (bor_sep with "LFT H") as "[Hαβ _]". { done. }
+ iMod (bor_persistent with "LFT Hαβ Htok") as "[#Hαβ $]". { done. }
iExists _. iFrame "H↦". iApply delay_sharing_nested; try done.
(* FIXME: "iApply lft_intersect_mono" only preserves the later on the last
goal, as does "iApply (lft_intersect_mono with ">")". *)
- iNext. iApply lft_intersect_mono. done. iApply lft_incl_refl.
+ iNext. iApply lft_intersect_mono; [done|]. iApply lft_incl_refl.
Qed.
Next Obligation.
iIntros (??????) "#? H". iDestruct "H" as (l') "[#Hf #H]".
@@ -58,10 +58,11 @@ Section rwlockwriteguard.
- by iApply frac_bor_shorten.
- iIntros "!> * % Htok".
iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
- { iApply lft_intersect_mono. iApply lft_incl_refl. done. }
- iMod ("H" with "[] Htok") as "Hshr". done. iModIntro. iNext.
+ { iApply lft_intersect_mono. - iApply lft_incl_refl. - done. }
+ iMod ("H" with "[] Htok") as "Hshr". { done. } iModIntro. iNext.
iMod "Hshr" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
- iApply ty_shr_mono; try done. iApply lft_intersect_mono. iApply lft_incl_refl. done.
+ iApply ty_shr_mono; try done. iApply lft_intersect_mono.
+ + iApply lft_incl_refl. + done.
Qed.
Global Instance rwlockwriteguard_wf α ty `{!TyWf ty} : TyWf (rwlockwriteguard α ty) :=
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index e5dcb3fdf3cb5ab41d356be4b7398da0d898a146..ddf79195f615b72d2874e11991e0f504bf187728 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -6,7 +6,7 @@ From lrust.logic Require Import gps.
From lrust.lifetime Require Import at_borrow.
From lrust.typing Require Import typing.
From lrust.typing.lib.rwlock Require Import rwlock rwlockwriteguard.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section rwlockwriteguard_functions.
Context `{!typeG Σ, !rwlockG Σ}.
@@ -32,7 +32,7 @@ Section rwlockwriteguard_functions.
iDestruct "Hx'" as (l') "#[Hfrac Hshr]".
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "([Hα1 Hα2] & HL & Hclose)";
[solve_typing..|].
- iMod (frac_bor_acc with "LFT Hfrac Hα1") as (qlx') "[H↦ Hcloseα1]". done.
+ iMod (frac_bor_acc with "LFT Hfrac Hα1") as (qlx') "[H↦ Hcloseα1]". { done. }
rewrite heap_mapsto_vec_singleton.
iMod (lctx_lft_alive_tok_noend β with "HE HL") as (qβ) "(Hβ & HL & Hclose')";
[solve_typing..|].
@@ -74,19 +74,19 @@ Section rwlockwriteguard_functions.
iIntros (tid qmax) "#LFT #HE Hna HL Hk HT". simpl_subst.
rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]; try done.
- iMod (bor_exists with "LFT Hx'") as (vl) "H". done.
- iMod (bor_sep with "LFT H") as "[H↦ H]". done.
+ iMod (bor_exists with "LFT Hx'") as (vl) "H". { done. }
+ iMod (bor_sep with "LFT H") as "[H↦ H]". { done. }
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
destruct vl as [|[[|l|]|][]];
try by iMod (bor_persistent with "LFT H Hα") as "[>[] _]".
rewrite heap_mapsto_vec_singleton.
- iMod (bor_exists with "LFT H") as (γ) "H". done.
- iMod (bor_exists with "LFT H") as (δ) "H". done.
- iMod (bor_exists with "LFT H") as (tid_shr) "H". done.
- iMod (bor_sep with "LFT H") as "[Hb H]". done.
- iMod (bor_sep with "LFT H") as "[Hβδ _]". done.
- iMod (bor_persistent with "LFT Hβδ Hα") as "[#Hβδ Hα]". done.
- iMod (bor_acc with "LFT H↦ Hα") as "[H↦ Hcloseα]". done.
+ iMod (bor_exists with "LFT H") as (γ) "H". { done. }
+ iMod (bor_exists with "LFT H") as (δ) "H". { done. }
+ iMod (bor_exists with "LFT H") as (tid_shr) "H". { done. }
+ iMod (bor_sep with "LFT H") as "[Hb H]". { done. }
+ iMod (bor_sep with "LFT H") as "[Hβδ _]". { done. }
+ iMod (bor_persistent with "LFT Hβδ Hα") as "[#Hβδ Hα]". { done. }
+ iMod (bor_acc with "LFT H↦ Hα") as "[H↦ Hcloseα]". { done. }
wp_bind (!(LitV lx'))%E. iMod (bor_unnest with "LFT Hb") as "Hb"; first done.
wp_read. wp_op. wp_let. iMod "Hb".
iMod ("Hcloseα" with "[$H↦]") as "[_ Hα]". iMod ("Hclose" with "Hα HL") as "HL".
@@ -95,8 +95,8 @@ Section rwlockwriteguard_functions.
with "[] LFT HE Hna HL Hk"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
iFrame. iApply (bor_shorten with "[] Hb"). iApply lft_incl_glb.
- iApply lft_incl_trans; last done. by iApply lft_incl_syn_sem.
- by iApply lft_incl_refl. }
+ - iApply lft_incl_trans; last done. by iApply lft_incl_syn_sem.
+ - by iApply lft_incl_refl. }
iApply (type_letalloc_1 (&uniq{α}ty)); [solve_typing..|].
iIntros (r). simpl_subst. iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
@@ -126,7 +126,7 @@ Section rwlockwriteguard_functions.
iDestruct "W" as (t) "W".
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)";
[solve_typing..|].
- iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβ Hcloseα]". done.
+ iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβ Hcloseα]". { done. }
wp_bind (#lx' <-ʳᵉˡ #0)%E.
iApply (GPS_aSP_SWWrite_rel rwlockN (rwlock_interp γs β tyO tyS)
rwlock_noCAS _ β qβ (λ _, True)%I True%I
diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index c88073a91ed0f9d73abcdac12fdf77073ad96754..b84ae8b6523fd2762a0491083357397b783bb21d 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
From lrust.lang Require Import spawn.
From lrust.typing Require Export type.
From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Definition spawnN := lrustN .@ "spawn".
diff --git a/theories/typing/lib/swap.v b/theories/typing/lib/swap.v
index c8bf802d69ddfa4d06857e8f844ce6abd2ac4e83..0d3cf3166e78c3c3cc9b3e30db39cb49818fb20c 100644
--- a/theories/typing/lib/swap.v
+++ b/theories/typing/lib/swap.v
@@ -1,6 +1,6 @@
From lrust.lang Require Import swap.
From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section swap.
Context `{!typeG Σ}.
diff --git a/theories/typing/lib/take_mut.v b/theories/typing/lib/take_mut.v
index bcd9e596689529dcecb53ecccfde6738c24a6212..c36ab18f4951e4dafd2924db2f3deba8ab7c5665 100644
--- a/theories/typing/lib/take_mut.v
+++ b/theories/typing/lib/take_mut.v
@@ -2,7 +2,7 @@ From lrust.lang Require Import memcpy.
From lrust.lifetime Require Import na_borrow.
From lrust.typing Require Export type.
From lrust.typing Require Import typing.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section code.
Context `{!typeG Σ}.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 27dbbb06c0a44414fdce8707409116779d3808d8..f3a80f6127a31310a1802df8c633cf2772b1ed2c 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
From lrust.lang Require Import memcpy.
From lrust.typing Require Export type.
From lrust.typing Require Import util uninit type_context programs.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section own.
Context `{!typeG Σ}.
@@ -37,7 +37,7 @@ Section own.
destruct sz1; [|destruct sz2;[|rewrite /freeable_sz plus_Sn_m; destruct n]].
- by rewrite left_id shift_loc_0.
- by rewrite right_id Nat.add_0_r.
- - iSplit. by iIntros "[[]?]". by iIntros "[]".
+ - iSplit. + by iIntros "[[]?]". + by iIntros "[]".
- rewrite hist_freeable_op_eq. f_equiv; [|done..].
by rewrite -Qp_div_add_distr pos_to_Qp_add -Nat2Pos.inj_add.
Qed.
@@ -79,7 +79,8 @@ Section own.
Next Obligation.
intros _ ty κ κ' tid l. iIntros "#Hκ #H".
iDestruct "H" as (l') "[Hfb #Hvs]".
- iExists l'. iSplit. by iApply (frac_bor_shorten with "[]"). iIntros "!> *% Htok".
+ iExists l'. iSplit. { by iApply (frac_bor_shorten with "[]"). }
+ iIntros "!> *% Htok".
iApply (step_fupd_mask_mono F _ (F∖↑shrN)); [solve_ndisj..|].
iMod (lft_incl_acc with "Hκ Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
iMod ("Hvs" with "[%] Htok") as "Hvs'"; first solve_ndisj. iModIntro. iNext.
@@ -100,7 +101,7 @@ Section own.
iApply "Ho".
- iIntros (???) "H". iDestruct "H" as (l') "[Hfb #Hvs]".
iExists l'. iFrame. iIntros "!>". iIntros (F' q) "% Htok".
- iMod ("Hvs" with "[%] Htok") as "Hvs'". done. iModIntro. iNext.
+ iMod ("Hvs" with "[%] Htok") as "Hvs'"; [done|]. iModIntro. iNext.
iMod "Hvs'" as "[Hshr $]". iApply ("Hs" with "Hshr").
Qed.
@@ -323,7 +324,7 @@ Section typing.
{ (* TODO : simpl_subst should be able to do this. *)
unfold subst=>/=. repeat f_equal.
- by rewrite bool_decide_true.
- - eapply is_closed_subst. done. set_solver. }
+ - eapply is_closed_subst; [done|set_solver]. }
iApply type_assign; [|solve_typing|by eapply write_own|solve_typing].
apply subst_is_closed; last done. apply is_closed_of_val.
Qed.
@@ -346,9 +347,9 @@ Section typing.
(xv <-{ty.(ty_size)} !p ;; subst x xv e)%E) as ->.
{ (* TODO : simpl_subst should be able to do this. *)
unfold subst=>/=. repeat f_equal.
- - eapply (is_closed_subst []). apply is_closed_of_val. set_solver.
+ - eapply (is_closed_subst []). + apply is_closed_of_val. + set_solver.
- by rewrite bool_decide_true.
- - eapply is_closed_subst. done. set_solver. }
+ - eapply is_closed_subst; [done|set_solver]. }
rewrite Nat2Z.id. iApply type_memcpy.
+ apply subst_is_closed; last done. apply is_closed_of_val.
+ solve_typing.
diff --git a/theories/typing/product.v b/theories/typing/product.v
index 0b1bc8e40bc6608ff6330549e11de2f4e1c06aa6..ebf54324c18a8facb4edc76588e3d332e9c0be4b 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
From iris.algebra Require Import list numbers.
From lrust.typing Require Import lft_contexts.
From lrust.typing Require Export type.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section product.
Context `{!typeG Σ}.
@@ -22,7 +22,7 @@ Section product.
Global Instance unit0_copy : Copy unit0.
Proof.
- split. by apply _. iIntros (????????) "_ _ Htok $".
+ split. { by apply _. } iIntros (????????) "_ _ Htok $".
iDestruct (na_own_acc with "Htok") as "[$ Htok]"; first solve_ndisj.
iExists 1%Qp. iModIntro. iSplitR.
{ iExists []. iSplitL; last by auto. rewrite heap_mapsto_vec_nil. auto. }
@@ -96,7 +96,7 @@ Section product.
iDestruct ("H2" with "HE") as "#(% & #Ho2 & #Hs2)". clear H2.
iSplit; first by (iPureIntro; simpl; f_equal). iSplit; iModIntro.
- iIntros (??) "H". iDestruct "H" as (vl1 vl2) "(% & Hown1 & Hown2)".
- iExists _, _. iSplit. done. iSplitL "Hown1".
+ iExists _, _. iSplit; [done|]. iSplitL "Hown1".
+ by iApply "Ho1".
+ by iApply "Ho2".
- iIntros (???) "#[Hshr1 Hshr2]". iSplit.
@@ -128,15 +128,18 @@ Section product.
iDestruct (ty_size_eq with "H2") as "#>%".
iDestruct "H↦1" as "[H↦1 H↦1f]". iDestruct "H↦2" as "[H↦2 H↦2f]".
iIntros "!>". iSplitL "H↦1 H1 H↦2 H2".
- - iNext. iSplitL "H↦1 H1". iExists vl1. by iFrame. iExists vl2. by iFrame.
+ - iNext. iSplitL "H↦1 H1".
+ + iExists vl1. by iFrame. + iExists vl2. by iFrame.
- iIntros "Htl [H1 H2]". iDestruct ("Htlclose" with "Htl") as "Htl".
iDestruct "H1" as (vl1') "[H↦1 H1]". iDestruct "H2" as (vl2') "[H↦2 H2]".
iDestruct (ty_size_eq with "H1") as "#>%".
iDestruct (ty_size_eq with "H2") as "#>%".
iDestruct (heap_mapsto_vec_combine with "H↦1 H↦1f") as "H↦1"; [congruence|].
iDestruct (heap_mapsto_vec_combine with "H↦2 H↦2f") as "H↦2"; [congruence|].
- iMod ("Hclose2" with "Htl [H2 H↦2]") as "[Htl $]". by iExists _; iFrame.
- iMod ("Hclose1" with "Htl [H1 H↦1]") as "[$$]". by iExists _; iFrame. done.
+ iMod ("Hclose2" with "Htl [H2 H↦2]") as "[Htl $]".
+ { by iExists _; iFrame. }
+ iMod ("Hclose1" with "Htl [H1 H↦1]") as "[$$]".
+ + by iExists _; iFrame. + done.
Qed.
Global Instance product2_send `{!Send ty1} `{!Send ty2} :
@@ -202,10 +205,10 @@ Section typing.
iSplit; first by rewrite /= assoc. iSplit; iIntros "!> *"; iSplit; iIntros "H".
- iDestruct "H" as (vl1 vl') "(% & Ho1 & H)".
iDestruct "H" as (vl2 vl3) "(% & Ho2 & Ho3)". subst.
- iExists _, _. iSplit. by rewrite assoc. iFrame. iExists _, _. by iFrame.
+ iExists _, _. iSplit. { by rewrite assoc. } iFrame. iExists _, _. by iFrame.
- iDestruct "H" as (vl1 vl') "(% & H & Ho3)".
iDestruct "H" as (vl2 vl3) "(% & Ho1 & Ho2)". subst.
- iExists _, _. iSplit. by rewrite -assoc. iFrame. iExists _, _. by iFrame.
+ iExists _, _. iSplit. { by rewrite -assoc. } iFrame. iExists _, _. by iFrame.
- iDestruct "H" as "(Hs1 & Hs2 & Hs3)". rewrite shift_loc_assoc_nat.
by iFrame.
- iDestruct "H" as "[[Hs1 Hs2] Hs3]". rewrite /= shift_loc_assoc_nat.
@@ -238,7 +241,7 @@ Section typing.
eqtype E L (Î (tyl1 ++ Î tyl2 :: tyl3)) (Î (tyl1 ++ tyl2 ++ tyl3)).
Proof.
unfold product. induction tyl1; simpl; last by f_equiv.
- induction tyl2. by rewrite left_id. by rewrite /= -assoc; f_equiv.
+ induction tyl2. - by rewrite left_id. - by rewrite /= -assoc; f_equiv.
Qed.
Lemma prod_flatten_l E L tyl1 tyl2 :
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index 3027a1a8fac6d1176e098dd7a658cc3b7a3edac3..0b5beabe4435fd5d4f4fe51d25eabe79f8e8415f 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -3,7 +3,7 @@ From iris.proofmode Require Import tactics.
From lrust.typing Require Export type.
From lrust.typing Require Import type_context lft_contexts product own uniq_bor.
From lrust.typing Require Import shr_bor.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section product_split.
Context `{!typeG Σ}.
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 999858e7f99e9373d0b5915f83df42b0eeb374b4..9ec82d6163b17f2485259a68a09aeb8d6f5123fc 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -1,7 +1,7 @@
From gpfsl.logic Require Import proofmode.
From lrust.lang Require Export memcpy.
From lrust.typing Require Export lft_contexts type_context cont_context type.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Implicit Types tid : thread_id.
@@ -73,7 +73,7 @@ Section typing.
∃ (l : loc) vl, ⌜length vl = ty.(ty_size) ∧ v = #l⌠∗ l ↦∗ vl ∗
(▷ l ↦∗: ty.(ty_own) tid ={F}=∗
llctx_interp_noend qmax L qL ∗ ty2.(ty_own) tid [v]))%I.
- Definition typed_write_aux : seal (@typed_write_def). by eexists. Qed.
+ Definition typed_write_aux : seal (@typed_write_def). Proof. by eexists. Qed.
Definition typed_write := typed_write_aux.(unseal).
Definition typed_write_eq : @typed_write = @typed_write_def := typed_write_aux.(seal_eq).
Global Arguments typed_write _ _ _%T _%T _%T.
@@ -94,7 +94,7 @@ Section typing.
∃ (l : loc) vl q, ⌜v = #l⌠∗ l ↦∗{q} vl ∗ ▷ ty.(ty_own) tid vl ∗
(l ↦∗{q} vl ={F}=∗ na_own tid F ∗
llctx_interp_noend qmax L qL ∗ ty2.(ty_own) tid [v]))%I.
- Definition typed_read_aux : seal (@typed_read_def). by eexists. Qed.
+ Definition typed_read_aux : seal (@typed_read_def). Proof. by eexists. Qed.
Definition typed_read := typed_read_aux.(unseal).
Definition typed_read_eq : @typed_read = @typed_read_def := typed_read_aux.(seal_eq).
Global Arguments typed_read _ _ _%T _%T _%T.
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index 1b723d933e571bb3ec13be9d4918b4682d88b146..bc2b4eaeb88bdd52f3e225b13973a889bb6d8678 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -1,7 +1,7 @@
From iris.proofmode Require Import tactics.
From lrust.typing Require Export type.
From lrust.typing Require Import lft_contexts type_context programs.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section shr_bor.
Context `{!typeG Σ}.
@@ -78,7 +78,7 @@ Section typing.
iIntros (Hκκ' tid ??) "#LFT #HE HL [H _]". iDestruct (Hκκ' with "HL HE") as "%".
iFrame. rewrite /tctx_interp /=.
iDestruct "H" as ([[]|]) "[% #Hshr]"; try done. iModIntro. iSplit.
- - iExists _. iSplit. done. iApply (ty_shr_mono with "[] Hshr").
+ - iExists _. iSplit; [done|]. iApply (ty_shr_mono with "[] Hshr").
by iApply lft_incl_syn_sem.
- iSplit=> //. iExists _. auto.
Qed.
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index e1e398f1ca463953cdcc839b13508dd30def832e..5cd4307df385d444627417e6b73d440689d45124 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -5,8 +5,7 @@ From gpfsl.logic Require Import na_invariants.
From lrust.lang Require Import notation.
From lrust.lifetime Require Import lifetime frac_borrow.
From lrust.typing Require Import typing.
-
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Class typePreG Σ := PreTypeG {
type_preG_heapG :> noprolGpreS Σ;
@@ -17,7 +16,7 @@ Class typePreG Σ := PreTypeG {
Definition typeΣ : gFunctors :=
#[noprolΣ; lftΣ view_Lat; na_invΣ view_Lat; GFunctor (constRF fracR)].
-Instance subG_typePreG {Σ} : subG typeΣ Σ → typePreG Σ.
+Global Instance subG_typePreG {Σ} : subG typeΣ Σ → typePreG Σ.
Proof. solve_inG. Qed.
Section type_soundness.
@@ -45,10 +44,10 @@ Section type_soundness.
iMod na_alloc as (tid2) "Htl". set (Htype := TypeG _ _ _ _ _).
set (tid := {| tid_na_inv_pool := tid2; tid_tid := tid1 |}).
wp_bind (of_val main). iApply (wp_wand with "[Htl]").
- iApply (Hmain Htype [] [] $! tid 1%Qp with "LFT [] Htl [] []").
- { by rewrite /elctx_interp big_sepL_nil. }
- { by rewrite /llctx_interp big_sepL_nil. }
- { by rewrite tctx_interp_nil. }
+ { iApply (Hmain Htype [] [] $! tid 1%Qp with "LFT [] Htl [] []").
+ - by rewrite /elctx_interp big_sepL_nil.
+ - by rewrite /llctx_interp big_sepL_nil.
+ - by rewrite tctx_interp_nil. }
clear Hrtc Hmain main. iIntros (main) "(Htl & _ & Hmain & _)".
iDestruct "Hmain" as (?) "[EQ Hmain]".
rewrite eval_path_of_val. iDestruct "EQ" as %[= <-].
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index df33cd6d8a7c550c5513899713cdcdc8a30104d9..e21de128913e8a7258ebb2f7f2b27ec9d05abe64 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -3,7 +3,7 @@ From iris.algebra Require Import list.
From iris.bi Require Import fractional.
From lrust.typing Require Import lft_contexts.
From lrust.typing Require Export type.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section sum.
Context `{!typeG Σ}.
@@ -74,7 +74,7 @@ Section sum.
iMod (bor_sep with "LFT Hown") as "[Hmt Hown]"; first solve_ndisj.
iMod ((nth i tyl emp0).(ty_share) with "LFT Hown Htok") as "[#Hshr $]"; try done.
iMod (bor_fracture with "LFT Hmt") as "H'"; [|done|by eauto].
- split. done. apply _.
+ split; [done|apply _].
Qed.
Next Obligation.
iIntros (tyl κ κ' tid l) "#Hord H".
@@ -178,8 +178,8 @@ Section sum.
Proof.
intros HFA. split.
- intros tid vl.
- cut (∀ i vl', Persistent (ty_own (nth i tyl emp0) tid vl')). by apply _.
- intros. apply @copy_persistent.
+ cut (∀ i vl', Persistent (ty_own (nth i tyl emp0) tid vl')). { by apply _. }
+ intros. apply : copy_persistent.
edestruct nth_in_or_default as [| ->]; [by eapply List.Forall_forall| ].
split; first by apply _. iIntros (????????) "? []".
- intros κ tid E F l q ? HF.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index f1d22fad901f74830476ab77d4b7fe9cd47ef1b8..14289e38a5cdeef535e4ef03d09c4bdcf6f56316 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -5,7 +5,7 @@ From gpfsl.logic Require Export na_invariants.
From lrust.lifetime Require Export frac_borrow.
From lrust.typing Require Export base.
From lrust.typing Require Import lft_contexts.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Class typeG Σ := TypeG {
type_noprolG :> noprolG Σ;
@@ -20,7 +20,7 @@ Definition shrN := lrustN .@ "shr".
Record thread_id :=
{ tid_na_inv_pool :> na_inv_pool_name;
tid_tid :> history.thread_id }.
-Instance thread_id_inhabited : Inhabited thread_id.
+Global Instance thread_id_inhabited : Inhabited thread_id.
Proof. repeat constructor. Qed.
Record type `{!typeG Σ} :=
@@ -50,10 +50,10 @@ Record type `{!typeG Σ} :=
ty_shr_mono κ κ' tid l :
κ' ⊑ κ -∗ ty_shr κ tid l -∗ ty_shr κ' tid l
}.
-Existing Instance ty_shr_persistent.
-Instance: Params (@ty_size) 2 := {}.
-Instance: Params (@ty_own) 2 := {}.
-Instance: Params (@ty_shr) 2 := {}.
+Global Existing Instance ty_shr_persistent.
+Global Instance: Params (@ty_size) 2 := {}.
+Global Instance: Params (@ty_own) 2 := {}.
+Global Instance: Params (@ty_shr) 2 := {}.
Arguments ty_own {_ _} !_ _ _ / : simpl nomatch.
@@ -82,7 +82,7 @@ Inductive ListTyWf `{!typeG Σ} : list type → Type :=
| list_ty_wf_nil : ListTyWf []
| list_ty_wf_cons ty tyl `{!TyWf ty, !ListTyWf tyl} : ListTyWf (ty::tyl).
Existing Class ListTyWf.
-Existing Instances list_ty_wf_nil list_ty_wf_cons.
+Global Existing Instances list_ty_wf_nil list_ty_wf_cons.
Fixpoint tyl_lfts `{!typeG Σ} tyl {WF : ListTyWf tyl} : list lft :=
match WF with
@@ -121,8 +121,8 @@ Record simple_type `{!typeG Σ} :=
{ st_own : thread_id → list val → vProp Σ;
st_size_eq tid vl : st_own tid vl -∗ ⌜length vl = 1%natâŒ;
st_own_persistent tid vl : Persistent (st_own tid vl) }.
-Existing Instance st_own_persistent.
-Instance: Params (@st_own) 2 := {}.
+Global Existing Instance st_own_persistent.
+Global Instance: Params (@st_own) 2 := {}.
Program Definition ty_of_st `{!typeG Σ} (st : simple_type) : type :=
{| ty_size := 1; ty_own := st.(st_own);
@@ -162,14 +162,14 @@ Section ofe.
(∀ tid vs, ty1.(ty_own) tid vs ≡ ty2.(ty_own) tid vs) →
(∀ κ tid l, ty1.(ty_shr) κ tid l ≡ ty2.(ty_shr) κ tid l) →
type_equiv' ty1 ty2.
- Instance type_equiv : Equiv type := type_equiv'.
+ Local Instance type_equiv : Equiv type := type_equiv'.
Inductive type_dist' (n : nat) (ty1 ty2 : type) : Prop :=
Type_dist :
ty1.(ty_size) = ty2.(ty_size) →
(∀ tid vs, ty1.(ty_own) tid vs ≡{n}≡ ty2.(ty_own) tid vs) →
(∀ κ tid l, ty1.(ty_shr) κ tid l ≡{n}≡ ty2.(ty_shr) κ tid l) →
type_dist' n ty1 ty2.
- Instance type_dist : Dist type := type_dist'.
+ Local Instance type_dist : Dist type := type_dist'.
Let T := prodO
(prodO natO (thread_id -d> list val -d> vPropO Σ))
@@ -221,7 +221,7 @@ Section ofe.
- (* TODO: automate this *)
repeat apply limit_preserving_and; repeat (apply limit_preserving_forall; intros ?).
+ apply bi.limit_preserving_Persistent=> n ty1 ty2 Hty; apply Hty.
- + apply bi.limit_preserving_entails=> n ty1 ty2 Hty. apply Hty. by rewrite Hty.
+ + apply bi.limit_preserving_entails=> n ty1 ty2 Hty; [apply Hty|by rewrite Hty].
+ apply bi.limit_preserving_entails=> n ty1 ty2 Hty; repeat f_equiv; apply Hty.
+ apply bi.limit_preserving_entails=> n ty1 ty2 Hty; repeat f_equiv; apply Hty.
Qed.
@@ -230,12 +230,12 @@ Section ofe.
St_equiv :
(∀ tid vs, ty1.(ty_own) tid vs ≡ ty2.(ty_own) tid vs) →
st_equiv' ty1 ty2.
- Instance st_equiv : Equiv simple_type := st_equiv'.
+ Local Instance st_equiv : Equiv simple_type := st_equiv'.
Inductive st_dist' (n : nat) (ty1 ty2 : simple_type) : Prop :=
St_dist :
(∀ tid vs, ty1.(ty_own) tid vs ≡{n}≡ (ty2.(ty_own) tid vs)) →
st_dist' n ty1 ty2.
- Instance st_dist : Dist simple_type := st_dist'.
+ Local Instance st_dist : Dist simple_type := st_dist'.
Definition st_unpack (ty : simple_type) : thread_id -d> list val -d> vPropO Σ :=
λ tid vl, ty.(ty_own) tid vl.
@@ -256,8 +256,8 @@ Section ofe.
Global Instance ty_of_st_ne : NonExpansive ty_of_st.
Proof.
- intros n ?? EQ. constructor; try apply EQ. done.
- - simpl. intros; repeat f_equiv. apply EQ.
+ intros n ?? EQ. constructor; try apply EQ; [done|].
+ simpl. intros; repeat f_equiv. apply EQ.
Qed.
Global Instance ty_of_st_proper : Proper ((≡) ==> (≡)) ty_of_st.
Proof. apply (ne_proper _). Qed.
@@ -292,7 +292,7 @@ Section type_dist2.
Global Instance type_dist2_later_equivalence n :
Equivalence (type_dist2_later n).
- Proof. destruct n as [|n]. by split. apply type_dist2_equivalence. Qed.
+ Proof. destruct n as [|n]. - by split. - apply type_dist2_equivalence. Qed.
(* The hierarchy of metrics:
dist n → type_dist2 n → dist_later n → type_dist2_later. *)
@@ -404,31 +404,31 @@ Class Copy `{!typeG Σ} (t : type) := {
(na_own tid (F ∖ shr_locsE l t.(ty_size)) -∗ ▷l ↦∗{q'}: t.(ty_own) tid
={E}=∗ na_own tid F ∗ q.[κ])
}.
-Existing Instances copy_persistent.
-Instance: Params (@Copy) 2 := {}.
+Global Existing Instances copy_persistent.
+Global Instance: Params (@Copy) 2 := {}.
Class ListCopy `{!typeG Σ} (tys : list type) := lst_copy : Forall Copy tys.
-Instance: Params (@ListCopy) 2 := {}.
+Global Instance: Params (@ListCopy) 2 := {}.
Global Instance lst_copy_nil `{!typeG Σ} : ListCopy [] := List.Forall_nil _.
Global Instance lst_copy_cons `{!typeG Σ} ty tys :
Copy ty → ListCopy tys → ListCopy (ty :: tys) := List.Forall_cons _ _ _.
Class Send `{!typeG Σ} (t : type) :=
send_change_tid tid1 tid2 vl : t.(ty_own) tid1 vl -∗ t.(ty_own) tid2 vl.
-Instance: Params (@Send) 2 := {}.
+Global Instance: Params (@Send) 2 := {}.
Class ListSend `{!typeG Σ} (tys : list type) := lst_send : Forall Send tys.
-Instance: Params (@ListSend) 2 := {}.
+Global Instance: Params (@ListSend) 2 := {}.
Global Instance lst_send_nil `{!typeG Σ} : ListSend [] := List.Forall_nil _.
Global Instance lst_send_cons `{!typeG Σ} ty tys :
Send ty → ListSend tys → ListSend (ty :: tys) := List.Forall_cons _ _ _.
Class Sync `{!typeG Σ} (t : type) :=
sync_change_tid κ tid1 tid2 l : t.(ty_shr) κ tid1 l -∗ t.(ty_shr) κ tid2 l.
-Instance: Params (@Sync) 2 := {}.
+Global Instance: Params (@Sync) 2 := {}.
Class ListSync `{!typeG Σ} (tys : list type) := lst_sync : Forall Sync tys.
-Instance: Params (@ListSync) 2 := {}.
+Global Instance: Params (@ListSync) 2 := {}.
Global Instance lst_sync_nil `{!typeG Σ} : ListSync [] := List.Forall_nil _.
Global Instance lst_sync_cons `{!typeG Σ} ty tys :
Sync ty → ListSync tys → ListSync (ty :: tys) := List.Forall_cons _ _ _.
@@ -541,23 +541,23 @@ Definition type_incl `{!typeG Σ} (ty1 ty2 : type) : vPropI Σ :=
(⌜ty1.(ty_size) = ty2.(ty_size)⌠∗
(□ ∀ tid vl, ty1.(ty_own) tid vl -∗ ty2.(ty_own) tid vl) ∗
(□ ∀ κ tid l, ty1.(ty_shr) κ tid l -∗ ty2.(ty_shr) κ tid l))%I.
-Instance: Params (@type_incl) 2 := {}.
+Global Instance: Params (@type_incl) 2 := {}.
(* Typeclasses Opaque type_incl. *)
Definition type_equal `{!typeG Σ} (ty1 ty2 : type) : vProp Σ :=
(⌜ty1.(ty_size) = ty2.(ty_size)⌠∗
(□ ∀ tid vl, ty1.(ty_own) tid vl ∗-∗ ty2.(ty_own) tid vl) ∗
(□ ∀ κ tid l, ty1.(ty_shr) κ tid l ∗-∗ ty2.(ty_shr) κ tid l))%I.
-Instance: Params (@type_equal) 2 := {}.
+Global Instance: Params (@type_equal) 2 := {}.
Definition subtype `{!typeG Σ} (E : elctx) (L : llctx) (ty1 ty2 : type) : Prop :=
∀ qmax qL, llctx_interp_noend qmax L qL -∗ □ (elctx_interp E -∗ type_incl ty1 ty2).
-Instance: Params (@subtype) 4 := {}.
+Global Instance: Params (@subtype) 4 := {}.
(* TODO: The prelude should have a symmetric closure. *)
Definition eqtype `{!typeG Σ} (E : elctx) (L : llctx) (ty1 ty2 : type) : Prop :=
subtype E L ty1 ty2 ∧ subtype E L ty2 ty1.
-Instance: Params (@eqtype) 4 := {}.
+Global Instance: Params (@eqtype) 4 := {}.
Section subtyping.
Context `{!typeG Σ}.
@@ -592,7 +592,7 @@ Section subtyping.
iDestruct (H12 with "HL") as "#H12".
iDestruct (H23 with "HL") as "#H23".
iClear "∗". iIntros "!> #HE".
- iApply (type_incl_trans with "[#]"). by iApply "H12". by iApply "H23".
+ iApply (type_incl_trans with "[#]"). - by iApply "H12". - by iApply "H23".
Qed.
Lemma subtype_Forall2_llctx_noend E L tys1 tys2 qmax qL :
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index 2cf6c9db2687f458b12125bd29174266075e516b..9f82fffa4695bc3118707f45c6d888881ffea6ba 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -1,7 +1,7 @@
From gpfsl.logic Require Export proofmode.
From iris.proofmode Require Import tactics.
From lrust.typing Require Import type lft_contexts.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Definition path := expr.
Bind Scope expr_scope with path.
@@ -36,7 +36,7 @@ Section type_context.
Lemma eval_path_of_val (v : val) :
eval_path v = Some v.
- Proof. destruct v. done. simpl. rewrite (decide_True_pi _). done. Qed.
+ Proof. destruct v; [done|]. simpl. rewrite (decide_True_pi _). done. Qed.
Lemma wp_eval_path E tid p v (SUB : ↑histN ⊆ E) :
eval_path p = Some v → ⊢ WP p @ tid; E {{ v', ⌜v' = v⌠}}.
@@ -213,8 +213,9 @@ Section type_context.
Proof.
remember (p â— ty). induction 1 as [|???? IH]; subst.
- apply (tctx_incl_frame_r _ [_] [_;_]), copy_tctx_incl, _.
- - etrans. by apply (tctx_incl_frame_l [_]), IH, reflexivity.
- apply contains_tctx_incl, submseteq_swap.
+ - etrans.
+ + by apply (tctx_incl_frame_l [_]), IH, reflexivity.
+ + apply contains_tctx_incl, submseteq_swap.
Qed.
Lemma type_incl_tctx_incl tid p ty1 ty2 :
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index 1bd53a5299aeb1f0ebb5122d59c799ab53491652..a01ed2c21f416027de595149b7574bce8dd61394 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
From lrust.lang Require Import memcpy.
From lrust.typing Require Import uninit uniq_bor shr_bor own sum.
From lrust.typing Require Import lft_contexts type_context programs product.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section case.
Context `{!typeG Σ}.
@@ -68,8 +68,8 @@ Section case.
iApply (wp_hasty with "Hp"); [done|].
iIntros ([[]|] Hv) "Hp"; try iDestruct "Hp" as "[]".
iDestruct (llctx_interp_acc_noend with "HL") as "[HL HLclose]".
- iMod (Halive with "HE HL") as (q) "[Htok Hclose]". done.
- iMod (bor_acc_cons with "LFT Hp Htok") as "[H↦ Hclose']". done.
+ iMod (Halive with "HE HL") as (q) "[Htok Hclose]". { done. }
+ iMod (bor_acc_cons with "LFT Hp Htok") as "[H↦ Hclose']". { done. }
iDestruct "H↦" as (vl) "[H↦ Hown]".
iDestruct "Hown" as (i vl' vl'') "(>% & >EQlen & Hown)". subst.
iDestruct "EQlen" as %[=EQlen].
@@ -86,7 +86,7 @@ Section case.
iExists (#i::vl'2++vl''). iIntros "!>". iNext.
iDestruct (ty.(ty_size_eq) with "Hown") as %EQlenvl'2.
rewrite heap_mapsto_vec_cons heap_mapsto_vec_app EQlenvl' EQlenvl'2.
- iFrame. iExists _, _, _. iSplit. by auto.
+ iFrame. iExists _, _, _. iSplit. { by auto. }
rewrite /= -EQlen !app_length EQlenvl' EQlenvl'2 nth_lookup EQty /=. auto. }
{ iExists vl'. iFrame. }
iMod ("Hclose" with "Htok") as "HL".
@@ -125,8 +125,8 @@ Section case.
iApply (wp_hasty with "Hp"); [done|]. iIntros ([[]|] Hv) "Hp"; try done.
iDestruct "Hp" as (i) "[#Hb Hshr]".
iDestruct (llctx_interp_acc_noend with "HL") as "[HL HLclose]".
- iMod (Halive with "HE HL") as (q) "[Htok Hclose]". done.
- iMod (frac_bor_acc with "LFT Hb Htok") as (q') "[[H↦i H↦vl''] Hclose']". done.
+ iMod (Halive with "HE HL") as (q) "[Htok Hclose]". { done. }
+ iMod (frac_bor_acc with "LFT Hb Htok") as (q') "[[H↦i H↦vl''] Hclose']". { done. }
rewrite nth_lookup.
destruct (tyl !! i) as [ty|] eqn:EQty; last done.
edestruct @Forall2_lookup_l as (e & He & Hety); eauto.
@@ -203,7 +203,7 @@ Section case.
wp_bind p. iApply (wp_hasty with "Hp"); [done|]. iIntros (v Hv) "Hty".
rewrite typed_write_eq in Hw.
iDestruct (llctx_interp_acc_noend with "HL") as "[HL HLclose]".
- iMod (Hw with "[] LFT HE HL Hty") as (l vl) "(H & H↦ & Hw)". done.
+ iMod (Hw with "[] LFT HE HL Hty") as (l vl) "(H & H↦ & Hw)". { done. }
simpl. destruct vl as [|? vl]; iDestruct "H" as %[[= Hlen] ->].
rewrite heap_mapsto_vec_cons -wp_fupd. iDestruct "H↦" as "[H↦0 H↦vl]".
wp_write. rewrite tctx_interp_singleton tctx_hasty_val' //.
diff --git a/theories/typing/uninit.v b/theories/typing/uninit.v
index e45318a9f54c9ed7b254e11c4122fc2b9800e55f..a2a3a0a0b5c1ca4166f78089834ebca280a844db 100644
--- a/theories/typing/uninit.v
+++ b/theories/typing/uninit.v
@@ -1,7 +1,7 @@
From iris.proofmode Require Import tactics.
From lrust.typing Require Export type.
From lrust.typing Require Import product.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section uninit.
Context `{!typeG Σ}.
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 40f68513971f9d3611e89975410d03f12514b14f..ae61678d8cac6345300bea76e1ff00277c9cc690 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -1,7 +1,7 @@
From iris.proofmode Require Import tactics.
From lrust.typing Require Export type.
From lrust.typing Require Import util lft_contexts type_context programs.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section uniq_bor.
Context `{!typeG Σ}.
@@ -31,8 +31,8 @@ Section uniq_bor.
Next Obligation.
intros κ0 ty κ κ' tid l. iIntros "#Hκ #H".
iDestruct "H" as (l') "[Hfb Hvs]". iAssert (κ0⊓κ' ⊑ κ0⊓κ)%I as "#Hκ0".
- { iApply lft_intersect_mono. iApply lft_incl_refl. done. }
- iExists l'. iSplit. by iApply (frac_bor_shorten with "[]").
+ { iApply lft_intersect_mono. - iApply lft_incl_refl. - done. }
+ iExists l'. iSplit. { by iApply (frac_bor_shorten with "[]"). }
iIntros "!> * % Htok". iApply (step_fupd_mask_mono F _ (F∖↑shrN)); try solve_ndisj.
iMod (lft_incl_acc with "Hκ0 Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
iMod ("Hvs" with "[%] Htok") as "Hvs'"; first solve_ndisj. iModIntro. iNext.
@@ -80,7 +80,7 @@ Section uniq_bor.
Qed.
Global Instance uniq_mono_flip E L :
Proper (lctx_lft_incl E L ==> eqtype E L ==> flip (subtype E L)) uniq_bor.
- Proof. intros ??????. apply uniq_mono. done. by symmetry. Qed.
+ Proof. intros ??????. apply uniq_mono; [done|]. by symmetry. Qed.
Global Instance uniq_proper E L :
Proper (lctx_lft_eq E L ==> eqtype E L ==> eqtype E L) uniq_bor.
Proof. intros ??[]; split; by apply uniq_mono. Qed.
@@ -130,7 +130,7 @@ Section typing.
iDestruct (lft_incl_syn_sem κ' κ H) as "Hκκ'".
iFrame. rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
iDestruct "H" as ([[]|]) "[% Hb]"; try done.
- iMod (rebor with "LFT Hκκ' Hb") as "[Hb Hext]". done. iModIntro.
+ iMod (rebor with "LFT Hκκ' Hb") as "[Hb Hext]"; [done|]. iModIntro.
iSplitL "Hb"; iExists _; auto.
Qed.
@@ -153,7 +153,7 @@ Section typing.
iDestruct "H↦" as (vl) "[>H↦ #Hown]".
iDestruct (ty_size_eq with "Hown") as "#>%". iIntros "!>".
iExists _, _, _. iSplit; first done. iFrame "∗#". iIntros "H↦".
- iMod ("Hclose'" with "[H↦]") as "[$ Htok]". by iExists _; iFrame.
+ iMod ("Hclose'" with "[H↦]") as "[$ Htok]". { by iExists _; iFrame. }
by iMod ("Hclose" with "Htok") as "($ & $ & $)".
Qed.
@@ -167,7 +167,7 @@ Section typing.
iDestruct "H↦" as (vl) "[>H↦ Hown]". rewrite ty.(ty_size_eq).
iDestruct "Hown" as ">%". iModIntro. iExists _, _. iSplit; first done.
iFrame. iIntros "Hown". iDestruct "Hown" as (vl') "[H↦ Hown]".
- iMod ("Hclose'" with "[H↦ Hown]") as "[$ Htok]". by iExists _; iFrame.
+ iMod ("Hclose'" with "[H↦ Hown]") as "[$ Htok]". { by iExists _; iFrame. }
by iMod ("Hclose" with "Htok") as "($ & $ & $)".
Qed.
End typing.
diff --git a/theories/typing/util.v b/theories/typing/util.v
index 793773224b5e9c9d3d4c6c174f25c1aca9aa7838..eff9fb5ef9a066bd49a78c5596234261f2c63f5f 100644
--- a/theories/typing/util.v
+++ b/theories/typing/util.v
@@ -1,5 +1,5 @@
From lrust.typing Require Export type.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
Section util.
Context `{!typeG Σ}.