diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index bd06b9058a06e5dc2c073595cd7f46ca714ef237..cd88dc1f5d8e11409f58d08d857614f80c93999c 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -15,7 +15,7 @@ This branch uses a proper weak memory model.
"""
depends: [
- "coq-gpfsl" { (= "dev.2022-08-12.0.fd801c97") | (= "dev") }
+ "coq-gpfsl" { (= "dev.2022-08-12.1.964b326d") | (= "dev") }
]
build: [make "-j%{jobs}%"]
diff --git a/theories/lang/arc.v b/theories/lang/arc.v
index 863a962560516d3c824a94732f1c9016dbf0abba..13bbf9295b5fd5a96af6707f14825cb948ac479c 100644
--- a/theories/lang/arc.v
+++ b/theories/lang/arc.v
@@ -586,7 +586,7 @@ Section arc.
Proof.
iIntros "Hl1 Hl2 HP1".
iDestruct (HPn (1/2)%Qp (1/2)%Qp with "[HP1]") as "[HP1 HP1']";
- [by rewrite Qp_div_2|rewrite monPred_objectively_elim].
+ [by rewrite Qp.div_2|rewrite monPred_objectively_elim].
set stS : strong_stUR := Some ((1/2)%Qp, xH).
set stW : weak_stUR := (Some 1%Qp, None).
iAssert (|==> ∃ γ, StrongAuth γ stS ∗ StrongTok γ (1/2)%Qp ∗
@@ -608,7 +608,7 @@ Section arc.
iDestruct "Own" as (γsw)
"(SA & St & WA & SMA & [SM1 SM2] & SDA & [SD1 SD2] & WUA & WU & [S1 S2])".
iMod (view_inv_alloc_frac N _ (1/2 + 1/2/2) (1/2/2)) as (γi) "[[tok2 tok1] VI]";
- first by rewrite -Qp_add_assoc 2!Qp_div_2.
+ first by rewrite -Qp.add_assoc 2!Qp.div_2.
set Qs : time → time → gname → gname → vProp :=
(λ ts tw γs γw,
GPS_SWSharedReader l ts (() : unitProtocol) #1 (1/2)%Qp γs ∗
@@ -626,7 +626,7 @@ Section arc.
iDestruct (GPS_SWSharedReader_Reader with "Rw2") as "#R2".
iModIntro. iSplitL "SA SM1 SD1 Ws Rs1 HP1 S1 tok1"; last iSplitR "Rs2".
- iNext. iExists stS. iSplitL ""; [done|]. iFrame "SA Ws".
- iExists (1/2)%Qp. rewrite Qp_div_2. iSplitL ""; [done|]. iFrame "HP1".
+ iExists (1/2)%Qp. rewrite Qp.div_2. iSplitL ""; [done|]. iFrame "HP1".
iExists ∅,∅. iFrame "tok1 Rs1 SM1 SD1 S1".
iSplitL ""; iExists _, _; [by iFrame "R1"|by iFrame "R2"].
- iNext. iExists stW. iSplitL ""; [done|]. iFrame "WA". iSplitL ""; [done|].
@@ -664,7 +664,7 @@ Section arc.
[|rewrite left_id]; by apply auth_auth_valid. }
iDestruct "Own" as (γsw) "(SA & WA & Wt & SMA & SM & SDA & SD & WUA & [WU1 WU2])".
iMod (view_inv_alloc_frac N _ (1/2 + 1/2/2) (1/2/2)) as (γi) "[[tok2 tok1] VI]";
- first by rewrite -Qp_add_assoc 2!Qp_div_2.
+ first by rewrite -Qp.add_assoc 2!Qp.div_2.
set Qs : time → time → gname → gname → vProp :=
(λ ts tw γs γw,
GPS_SWSharedReader (l >> 1) tw (() : unitProtocol) #1 (1 / 2)%Qp γw ∗
@@ -682,7 +682,7 @@ Section arc.
- iNext. iExists stS. iSplitL ""; [done|]. by iFrame "SA".
- iNext. iExists stW. iSplitL ""; [done|].
iFrame "WA HP2 Ww". iSplitL "tok1 Rw1 WU1".
- + iExists (1/2)%Qp,∅. rewrite Qp_div_2. iSplitL ""; [done|].
+ + iExists (1/2)%Qp,∅. rewrite Qp.div_2. iSplitL ""; [done|].
iFrame "tok1 Rw1 WU1". iExists _, _; by iFrame "R1".
+ iFrame "tok2". iSplitL "Ws"; [by iExists _|]. iSplitL "SM"; iExists _; by iFrame.
- by iFrame "Rw2 R1 R2". }
@@ -734,7 +734,7 @@ Section arc.
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.
+ iDestruct (GPS_SWSharedReaders_join with "SR2 RR'") as "SR". rewrite Qp.div_2.
iSpecialize ("Hclose1" with "tok [SMA MDU IW IS]").
{ iDestruct "MDU" as "[SDA WUA]".
iApply (arc_inv_join with "[SMA] SDA WUA IS IW"). by iExists _. }
@@ -841,7 +841,7 @@ Section arc.
iModIntro. iSplitR ""; [iExists _; by iFrame "SI"|by iExists _]. }
iIntros "!>" (t' [] v'). iDestruct 1 as "(_ & SR1 & IS & Rs)".
iDestruct "Rs" as (z) "%". subst v'.
- iDestruct (GPS_SWSharedReaders_join with "SR2 SR1") as "SR". rewrite Qp_div_2.
+ iDestruct (GPS_SWSharedReaders_join with "SR2 SR1") as "SR". rewrite Qp.div_2.
(* closing invariant *)
iSpecialize ("Hclose1" with "tok [MA IW IS]").
@@ -904,13 +904,13 @@ Section arc.
inversion Eq. subst z. clear Eq. iDestruct "SI" as "[$ SI]".
iDestruct "SI" as (q'') "(>Eq'' & HP & SI)". iDestruct "Eq''" as %Eq''.
iAssert (▷ (P1 (q''/2) ∗ <obj> P1 (q''/2)))%I with "[HP]" as "[HP1 HP2]".
- { iNext. iApply HPn. by rewrite Qp_div_2. }
+ { iNext. iApply HPn. by rewrite Qp.div_2. }
iDestruct "SI" as (Mt' Dt') "(>tok & R & SM' & RestS)". rewrite /StrMoves.
iDestruct "SM'" as ">SM'".
iDestruct (StrongMoveAuth_agree with "[$SMA SM']") as %?;
[by rewrite /StrMoves|]. subst Mt'.
iDestruct (view_tok_split_unit γi (q''/2/2) (q''/2/2) with "[tok]")
- as "[tok1 tok2]"; first by rewrite Qp_div_2.
+ as "[tok1 tok2]"; first by rewrite Qp.div_2.
iModIntro. iExists (). iSplitL""; [done|]. iIntros (t'' Lt'') "W' _".
set Mt' : gset time := if decide (n = 1%positive) then (Mt ∪ {[t'']}) else Mt.
@@ -946,14 +946,14 @@ Section arc.
iMod (StrongAuth_new_tok _ q' q'' _ Eq'' with "SA") as "[SA St']".
iAssert (StrDowns γsw (q'' / 2) Dt' ∗ StrDowns γsw (q'' / 2) ∅)%I
with "[SD]" as "[SD1 SD2]".
- { rewrite -(right_id_L ∅ union Dt') -{1}(Qp_div_2 q'').
+ { rewrite -(right_id_L ∅ union Dt') -{1}(Qp.div_2 q'').
by iApply (StrDowns_forget with "SD"). }
iModIntro. iSplitR "SA W' tok1 R1 SM1 OS1 SD1 HP1 SeenM'".
- rewrite /Q Pos2Z.id. iFrame "SMA SM". iSplitL "St"; [by rewrite /StrongTok|].
iExists _. by iFrame "St' tok2 R2 SM2 HP2 MAX SD2 OS2".
- iExists (Some ((q' + q'' / 2)%Qp, (n + 1)%positive)). iSplitL ""; [done|].
iFrame "SA W'". iExists (q''/2)%Qp.
- iSplitL "". { iPureIntro. by rewrite -Qp_add_assoc Qp_div_2. }
+ iSplitL "". { iPureIntro. by rewrite -Qp.add_assoc Qp.div_2. }
iFrame "HP1". iExists Mt', Dt'. iFrame "tok1 R1 SM1 SeenM' SD1 SeenD OS1". }
(* finally done with the CAS *)
@@ -969,7 +969,7 @@ Section arc.
{ iExists _, _. iFrame (MAX'') "RR'". }
iDestruct (GPS_SWSharedReaders_join with "SR2 R'") as "SR".
(* tedious removal of acq_mod *)
- rewrite Qp_div_2 2!acq_objectively_elim 2!monPred_objectively_elim.
+ rewrite Qp.div_2 2!acq_objectively_elim 2!monPred_objectively_elim.
rewrite 7!acq_embed_elim.
(* closing *)
@@ -993,7 +993,7 @@ Section arc.
iDestruct "WR" as (??) "WR". iExists _, _. by iFrame "WR".
- subst b.
iDestruct "Rs" as "(St & SMA & SM)". rewrite 3!acq_embed_elim.
- iDestruct (GPS_SWSharedReaders_join with "SR2 R'") as "SR". rewrite Qp_div_2.
+ iDestruct (GPS_SWSharedReaders_join with "SR2 R'") as "SR". rewrite Qp.div_2.
(* closing *)
iSpecialize ("Hclose1" with "tok [SMA MDU IW IS]").
{ iDestruct "MDU" as "[SDA WUA]".
@@ -1128,7 +1128,7 @@ Section arc.
iMod (WeakAuth_new_tok _ _ q' q'' _ Eq'' with "WA") as "[WA St']".
iAssert (WkUps γsw (q'' / 2) Ut' ∗ WkUps γsw (q'' / 2) ∅)%I
with "[WU]" as "[WU1 WU2]".
- { rewrite -(right_id_L ∅ union Ut') -{1}(Qp_div_2 q'').
+ { rewrite -(right_id_L ∅ union Ut') -{1}(Qp.div_2 q'').
by iApply (WkUps_forget with "WU"). }
iDestruct (GPS_SWSharedWriter_Reader_update with "W' R") as "[W' [R1 R2]]".
iModIntro. iSplitR "WA W' tok1 R1 WU1 SeenU".
@@ -1139,7 +1139,7 @@ Section arc.
+ iExists (Some 1%Qp, Some $ Cinl ((q' + q'' / 2)%Qp, (n + 1)%positive)).
iSplitL ""; [done|]. iFrame "WA W'". iSplit; [done|].
iExists (q''/2)%Qp, Ut'. iFrame "tok1 R1 WU1 SeenU".
- iPureIntro. by rewrite -Qp_add_assoc Qp_div_2.
+ iPureIntro. by rewrite -Qp.add_assoc Qp.div_2.
- iDestruct "WI" as "(>Eq & $ & WI)". iDestruct "Eq" as %?. subst qs.
iDestruct "WI" as (Ut') "([tok1 tok2] & R & WU & #SeenU)".
iModIntro. iExists (). iSplitL""; [done|]. iIntros (t'' Lt'') "W'".
@@ -1151,7 +1151,7 @@ Section arc.
iMod (WeakAuth_first_tok with "WA") as "[WA Wt']".
iAssert (WkUps γsw (1 / 2) Ut' ∗ WkUps γsw (1 / 2) ∅)%I
with "[WU]" as "[WU1 WU2]".
- { rewrite -(right_id_L ∅ union Ut') -{1}(Qp_div_2 1).
+ { rewrite -(right_id_L ∅ union Ut') -{1}(Qp.div_2 1).
by iApply (WkUps_forget with "WU"). }
iDestruct (GPS_SWSharedWriter_Reader_update with "W' R") as "[W' [R1 R2]]".
iModIntro. iSplitR "WA W' tok1 R1 WU1 SeenU".
@@ -1160,7 +1160,7 @@ Section arc.
iDestruct "SeenU" as (t4 v4) "[Rs _]". iExists _, _. by iFrame "Rs".
+ iExists (Some 1%Qp, Some $ Cinl ((1/2)%Qp, 1%positive)).
iSplitL ""; [done|]. iFrame "WA W'". iSplitL""; [done|].
- iExists (1/2)%Qp, Ut'. iSplitL ""; [iPureIntro; by rewrite Qp_div_2|].
+ iExists (1/2)%Qp, Ut'. iSplitL ""; [iPureIntro; by rewrite Qp.div_2|].
iFrame "tok1 R1 WU1 SeenU". }
iIntros "!>" (b t' [] v') "(IW &%& [([%[%%]]&R'&Q) | ([%[_ %]] &_&Rs&_)])".
- subst b v'.
@@ -1293,17 +1293,17 @@ Section arc.
iMod (WeakAuth_new_tok _ _ q' q'' _ Eq'' with "WA") as "[WA St']".
iAssert (WkUps γsw (q'' / 2) Ut' ∗ WkUps γsw (q'' / 2) ∅)%I
with "[WU]" as "[WU1 WU2]".
- { rewrite -(right_id_L ∅ union Ut') -{1}(Qp_div_2 q'').
+ { rewrite -(right_id_L ∅ union Ut') -{1}(Qp.div_2 q'').
by iApply (WkUps_forget with "WU"). }
iDestruct (GPS_SWSharedWriter_Reader_update with "W' R") as "[W' [R1 R2]]".
iDestruct (view_tok_split_unit γi (q''/2/2) (q''/2/2) with "[tok]")
- as "[tok1 tok2]"; first by rewrite Qp_div_2.
+ as "[tok1 tok2]"; first by rewrite Qp.div_2.
iModIntro. iSplitR "WA W' tok1 R1 WU1 SeenU".
+ rewrite /Q Pos2Z.id decide_False; last by lia. rewrite /WeakTok right_id_L.
iFrame "Wt SDA". iExists _. iFrame "St' tok2 R2 WU2".
+ iExists (Some iS, Some $ Cinl ((q' + q'' / 2)%Qp, (n + 1)%positive)).
iSplitL ""; [done|]. iFrame (iSI) "WA W'". iExists (q''/2)%Qp, Ut'.
- iFrame "tok1 R1 WU1 SeenU". iPureIntro. by rewrite -Qp_add_assoc Qp_div_2.
+ iFrame "tok1 R1 WU1 SeenU". iPureIntro. by rewrite -Qp.add_assoc Qp.div_2.
- iDestruct "WI" as "($ & WI & HP2 & tokM & SW & SM & SD)".
iDestruct "WI" as (q'' Ut') "(>Eq'' & tok & R & WU & #SeenU)".
iDestruct "Eq''" as %Eq''. rewrite /StrDowns. iDestruct "SD" as (Dt') ">SD".
@@ -1329,10 +1329,10 @@ Section arc.
iMod (WeakAuth_new_tok _ _ q' q'' _ Eq'' with "WA") as "[WA Wt']".
iAssert (WkUps γsw (q'' / 2) Ut' ∗ WkUps γsw (q'' / 2) ∅)%I
with "[WU]" as "[WU1 WU2]".
- { rewrite -(right_id_L ∅ union Ut') -{1}(Qp_div_2 q'').
+ { rewrite -(right_id_L ∅ union Ut') -{1}(Qp.div_2 q'').
by iApply (WkUps_forget with "WU"). }
iDestruct (view_tok_split_unit γi (q''/2/2) (q''/2/2) with "[tok]")
- as "[tok1 tok2]"; first by rewrite Qp_div_2.
+ as "[tok1 tok2]"; first by rewrite Qp.div_2.
iModIntro. iSplitR "WA W' tok1 R1 WU1 HP2 tokM SW SM SD".
+ rewrite /Q Pos2Z.id /WeakTok. iFrame "SDA Wt".
iExists _. iFrame "Wt' tok2 R2 WU2".
@@ -1340,7 +1340,7 @@ Section arc.
iSplitL ""; [done|]. iFrame "WA W' HP2 tokM SW SM".
iSplitR "SD"; [|by iExists _].
iExists (q''/2)%Qp, Ut'. iFrame "tok1 R1 WU1 SeenU".
- iPureIntro. by rewrite -Qp_add_assoc Qp_div_2. }
+ iPureIntro. by rewrite -Qp.add_assoc Qp.div_2. }
(* finally done with the CAS *)
iIntros "!>" (b t' [] v') "(IW &%& [([%[%%]]&R'&Q) | ([%[_ %]] &R'&Rs&_)])".
@@ -1352,7 +1352,7 @@ Section arc.
iDestruct (GPS_SWSharedReaders_join_subjectively _ _ _ _ _ _ _ _ q''
with "R' [R'']") as "[R' R'']". { by iApply acq_subjective. }
iDestruct (GPS_SWSharedReader_Reader with "R'") as "#RR".
- iDestruct (GPS_SWSharedReaders_join with "WR2 R'") as "WRq". rewrite Qp_div_2.
+ iDestruct (GPS_SWSharedReaders_join with "WR2 R'") as "WRq". rewrite Qp.div_2.
(* closing *)
iSpecialize ("Hclose1" with "tok [SMA SDA WUA IW IS]").
@@ -1368,7 +1368,7 @@ Section arc.
- subst b.
iDestruct "Rs" as "(Wt & SDA)". rewrite 2!acq_embed_elim.
iDestruct (GPS_SWSharedReaders_join with "WR2 R'") as "WRq".
- rewrite Qp_div_2.
+ rewrite Qp.div_2.
(* closing *)
iSpecialize ("Hclose1" with "tok [SMA SDA WUA IW IS]").
@@ -1468,7 +1468,7 @@ Section arc.
iDestruct "SI" as "[$ SI]".
iDestruct "SI" as (q'') "(>Eq'' & HP & SI)". iDestruct "Eq''" as %Eq''.
iAssert (▷ (P1 (q''/2) ∗ <obj> P1 (q''/2)))%I with "[HP]" as "[HP1 HP2]".
- { iNext. iApply HPn. by rewrite Qp_div_2. }
+ { iNext. iApply HPn. by rewrite Qp.div_2. }
iModIntro. iExists (). iSplitL""; [done|]. iIntros (t'' Lt'') "W'".
set Ut' : gset time := if decide (n = 1%positive) then {[t'']} else ∅.
iMod (WkUps_update _ UtA Ut Ut' q with "[$WUA WU]")
@@ -1483,19 +1483,19 @@ Section arc.
iDestruct (GPS_SWSharedWriter_Reader_update with "W' SR") as "[W' [SR1 SR2]]".
iAssert (StrDowns γsw (q'' / 2) Dt' ∗ StrDowns γsw (q'' / 2) ∅)%I
with "[SD]" as "[SD1 SD2]".
- { rewrite -(right_id_L ∅ union Dt') -{1}(Qp_div_2 q'').
+ { rewrite -(right_id_L ∅ union Dt') -{1}(Qp.div_2 q'').
by iApply (StrDowns_forget with "SD"). }
iDestruct "SeenM" as (t4 v4) "[SR4 MAX4]".
iDestruct (GPS_SWSharedWriter_latest_time_1 with "W' SR4") as %Ext4.
iDestruct (view_tok_split_unit γi (q''/2/2) (q''/2/2) with "[tok]")
- as "[tok1 tok2]"; first by rewrite Qp_div_2.
+ as "[tok1 tok2]"; first by rewrite Qp.div_2.
iModIntro. iSplitR "tok1 SM1 oW1 HP1 SA W' SR1 SD1".
- rewrite /Q /=. iFrame "WUA WU".
iExists (q''/2)%Qp, Mt'. iFrame "St' HP2 tok2 SR2 SM2 SD2 oW2".
iDestruct "MAX4" as %MAX. iPureIntro. move => ? /MAX ->. by rewrite Ext4.
- iExists (Some ((q' + q'' / 2)%Qp, (n + 1)%positive)).
iSplitL ""; [done|]. iFrame "SA W'". iExists (q''/2)%Qp.
- iSplitL ""; [by rewrite -Qp_add_assoc Qp_div_2|].
+ iSplitL ""; [by rewrite -Qp.add_assoc Qp.div_2|].
iFrame "HP1". iExists Mt', Dt'. iFrame "tok1 SR1 SM1 SD1 SeenD oW1".
iExists _,_. by iFrame "SR4 MAX4". }
@@ -1631,7 +1631,7 @@ Section arc.
- subst n. simpl in Eq'. subst q'.
by iApply (WeakAuth_drop_last with "[$WA $Wt]").
- rewrite (decide_False _ _ NEq) in Eq'. destruct Eq' as [q3 Eq3].
- iExists q3. iFrame (Eq3). rewrite Eq3 Qp_add_comm.
+ iExists q3. iFrame (Eq3). rewrite Eq3 Qp.add_comm.
rewrite {1}(_: n = (1 + Pos.pred n)%positive);
first by iApply (WeakAuth_drop with "[$WA $Wt]").
by rewrite -Pplus_one_succ_l Pos.succ_pred. }
@@ -1644,7 +1644,7 @@ Section arc.
iCombine "SeenU" "SeenU'" as "SeenU'".
iDestruct (SeenActs_join with "SeenU'") as "SeenU'".
rewrite decide_False; last lia.
- iCombine "tok" "tok'" as "tok". rewrite -Qp_div_add_distr.
+ iCombine "tok" "tok'" as "tok". rewrite -Qp.div_add_distr.
case (decide (n = 1%positive)) => nEq.
+ subst n. simpl in Eq'. subst q'. iExists (Some 1%Qp, None).
iSplitL""; [done|]. iFrame "WA W'". iSplitL ""; [done|]. iExists _.
@@ -1655,7 +1655,7 @@ Section arc.
by rewrite Z.add_1_r -Pos2Z.inj_succ Pos.succ_pred. }
iFrame "WA W'". iSplitL ""; [done|]. iExists (q + q'')%Qp,_.
iFrame "tok R WU SeenU'".
- iPureIntro. by rewrite Qp_add_assoc (Qp_add_comm q2).
+ iPureIntro. by rewrite Qp.add_assoc (Qp.add_comm q2).
- iDestruct "WI" as "($ & WI & HP & tokS & SW & SM & SD)".
iDestruct "WI" as (q'' Ut') "(Eq'' & tok' & R & WU' & SeenU')".
iDestruct "Eq''" as %Eq''. rewrite /StrDowns.
@@ -1687,7 +1687,7 @@ Section arc.
- subst n. simpl in Eq'. subst q'.
by iApply (WeakAuth_drop_last with "[$WA $Wt]").
- rewrite (decide_False _ _ NEq) in Eq'. destruct Eq' as [q3 Eq3].
- iExists q3. iFrame (Eq3). rewrite Eq3 Qp_add_comm.
+ iExists q3. iFrame (Eq3). rewrite Eq3 Qp.add_comm.
rewrite {1}(_: n = (1 + Pos.pred n)%positive);
first by iApply (WeakAuth_drop with "[$WA $Wt]").
by rewrite -Pplus_one_succ_l Pos.succ_pred. }
@@ -1713,7 +1713,7 @@ Section arc.
{ iPureIntro. f_equal. by rewrite Z.sub_1_r -Pos2Z.inj_pred. }
iFrame "WA W' HP tokS SW SM". subst q'. iSplitR "SD"; [|by iExists _].
iExists (q + q'')%Qp, _.
- iCombine "tok" "tok'" as "tok". rewrite -Qp_div_add_distr.
+ iCombine "tok" "tok'" as "tok". rewrite -Qp.div_add_distr.
iFrame "R' tok WU SeenU'". by rewrite assoc_L (comm_L _ q2). }
(* finally done with the CAS *)
@@ -1771,7 +1771,7 @@ Section arc.
iIntros "!> (WW & WR & tok' & WU & P2 & tokh & SW & SM & SD)".
iDestruct "WU" as (Uw) "[WU _]". iDestruct "SM" as (Ms) "SM".
iDestruct "tok'" as (q'' Eq'') "tok'".
- iCombine "tok" "tok'" as "tok". rewrite -Qp_div_add_distr Eq''.
+ iCombine "tok" "tok'" as "tok". rewrite -Qp.div_add_distr Eq''.
iCombine "tokh" "tok" as "tok".
iApply wp_fupd. iApply wp_hist_inv; [done|]. iIntros "#HINV". wp_let.
@@ -2115,7 +2115,7 @@ Section arc.
- subst n. simpl in Eq'. subst q'.
by iApply (StrongAuth_drop_last with "[$SA $St]").
- rewrite (decide_False _ _ NEq) in Eq'. destruct Eq' as [q3 Eq3].
- iExists q3. iFrame (Eq3). rewrite Eq3 Qp_add_comm.
+ iExists q3. iFrame (Eq3). rewrite Eq3 Qp.add_comm.
rewrite {1}(_: n = (1 + Pos.pred n)%positive);
first by iApply (StrongAuth_drop with "[$SA $St]").
by rewrite -Pplus_one_succ_l Pos.succ_pred. }
@@ -2143,11 +2143,11 @@ Section arc.
iExists (Some (q2, Pos.pred n)). iSplitL "".
{ iPureIntro. f_equal. by rewrite Z.sub_1_r -Pos2Z.inj_pred. }
iFrame "SA W'". subst q'. iExists (q + q'')%Qp. iSplitL "".
- { by rewrite Qp_add_assoc (Qp_add_comm q2). } iFrame "HP".
+ { by rewrite Qp.add_assoc (Qp.add_comm q2). } iFrame "HP".
iExists _,_. iFrame "R' SM SD SeenD' oW".
rewrite /Mt' (decide_False _ _ nEq). iFrame "SeenM'".
rewrite decide_False; last first. { simpl. by destruct n; try lia. }
- rewrite Qp_div_add_distr. by iFrame "tok tok'". }
+ rewrite Qp.div_add_distr. by iFrame "tok tok'". }
(* finally done with the CAS *)
iIntros "!>" (b t2 [] v2) "(_ & [((%&%&%)&QI) | ((%&_&%)&IS&R'&_&P&IW)])";
@@ -2216,7 +2216,7 @@ Section arc.
iMod ("Hclose1" with "tok [SMA SDA WUA IW IS]") as "tok".
{ by iApply (arc_inv_join with "SMA SDA WUA IS IW"). }
- iCombine "tok" "tok'" as "tok". rewrite -Qp_div_add_distr Eq''.
+ iCombine "tok" "tok'" as "tok". rewrite -Qp.div_add_distr Eq''.
iModIntro. iApply "HΦ". iFrame "HP tok". iSplitL "SW"; [by iExists _|].
iSplitL "SM SeenM'"; [iExists _; by iFrame|].
iSplitL "SD SeenD'"; [iExists _; by iFrame|]. by iFrame "oW".
@@ -2329,7 +2329,7 @@ Section arc.
iIntros "!> (SW & HP & tok' & SR & SM & SD & oW)".
iDestruct "SM" as (Mt2) "[SM SeenM']". iDestruct "SD" as (Dt2) "[SD SeenD']".
iDestruct "tok'" as (q'' Eq'') "tok'".
- iCombine "tok" "tok'" as "tok". rewrite -Qp_div_add_distr Eq''.
+ iCombine "tok" "tok'" as "tok". rewrite -Qp.div_add_distr Eq''.
iApply wp_fupd. wp_let.
(* open invariant to revert shared writer to strong writer *)
@@ -2480,7 +2480,7 @@ Section arc.
iDestruct (GPS_SWSharedReaders_join with "SR' SR") as "SR'".
iDestruct (StrMoves_agree with "[$SM $SM']") as %?. subst Mt2.
iCombine "SM" "SM'" as "SM". iCombine "HP1" "HP2" as "HP".
- iCombine "tok" "tok'" as "tok". rewrite HPn Qp_add_comm -Qp_div_add_distr Eq''.
+ iCombine "tok" "tok'" as "tok". rewrite HPn Qp.add_comm -Qp.div_add_distr Eq''.
iCombine "tok" "tokW" as "tok". iDestruct ("FR" with "tok VR") as "#$".
by iFrame "SR' SMA WUA SM HP tok VR".
- (* it's impossible to read 1 with only F_read *)
@@ -2717,7 +2717,7 @@ Section arc.
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" "tok'" as "tok". rewrite -Qp.div_add_distr Eq.
iCombine "tok" "tokW" as "tok". iDestruct ("FR" with "tok VR") as "#$".
iModIntro. by iFrame "tok VR".
- iDestruct 1 as (st Eq') "[_ WI]". inversion Eq' as [Eq1]. clear Eq'.
@@ -2741,7 +2741,7 @@ Section arc.
iDestruct "Rs" as "[Rs oW]". iDestruct "Rs" as (z) "%". subst v2.
iModIntro. wp_op. rewrite bool_decide_false; [|move => ?; exfalso; by subst z].
wp_case. iApply ("HΦ" $! 1%fin). simpl. iFrame "HP1".
- iCombine "tok" "tok'" as "tok". rewrite -Qp_div_add_distr Eq. iFrame "tok".
+ iCombine "tok" "tok'" as "tok". rewrite -Qp.div_add_distr Eq. iFrame "tok".
iSplitL "SW"; [by iExists _|]. iSplitL "SM". { iExists _. iFrame "SM SeenM". }
iFrame "oW". iExists _. iFrame "SD". iExists _, _. iFrame (MAX) "WR". }
diff --git a/theories/lang/arc_cmra.v b/theories/lang/arc_cmra.v
index e945fae52f40859271ac050a979233efc9dd1b17..866f5e88db292f673ef7495277701c4dc5704d8f 100644
--- a/theories/lang/arc_cmra.v
+++ b/theories/lang/arc_cmra.v
@@ -369,9 +369,9 @@ 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. }
- apply (irreflexive_eq (R:= Qp_lt) 1%Qp 1%Qp); [done|].
- eapply Qp_lt_le_trans; [apply Lt|done].
+ 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.
Lemma WkUps_update γ Ut1 Ut2 Ut' q :
@@ -451,11 +451,11 @@ Section ArcGhost.
iMod (@own_update _ arcUR with "own") as "$"; [|done].
apply prod_update; simpl; [|by rewrite right_id].
apply prod_update; simpl; [|done]. apply auth_update_alloc.
- rewrite Pos.add_comm Qp_add_comm -pos_op_add /= -frac_op pair_op Some_op.
+ rewrite Pos.add_comm Qp.add_comm -pos_op_add /= -frac_op pair_op Some_op.
rewrite -{2}(right_id None op (Some ((q' /2)%Qp, _))).
apply op_local_update_discrete => _ /=. split; simpl; [|done].
- apply frac_valid. rewrite -Hqq' comm -{2}(Qp_div_2 q').
- apply Qp_add_le_mono_l. apply Qp_le_add_r.
+ apply frac_valid. rewrite -Hqq' comm -{2}(Qp.div_2 q').
+ apply Qp.add_le_mono_l. apply Qp.le_add_r.
Qed.
Lemma WeakAuth_first_tok γ iS :
@@ -480,12 +480,12 @@ Section ArcGhost.
apply prod_update; simpl; [|by rewrite right_id].
apply prod_update; simpl; [done|]. apply auth_update_alloc.
apply prod_local_update; simpl; [done|].
- rewrite Pos.add_comm Qp_add_comm -pos_op_add /=
+ rewrite Pos.add_comm Qp.add_comm -pos_op_add /=
-frac_op pair_op Cinl_op Some_op.
rewrite -{2}(right_id None op (Some $ Cinl ((q' /2)%Qp, _))).
apply op_local_update_discrete => _ /=. split; simpl; [|done].
- apply frac_valid. rewrite -Hqq' comm -{2}(Qp_div_2 q').
- apply Qp_add_le_mono_l. apply Qp_le_add_r.
+ apply frac_valid. rewrite -Hqq' comm -{2}(Qp.div_2 q').
+ apply Qp.add_le_mono_l. apply Qp.le_add_r.
Qed.
Lemma StrongAuth_drop_last γ q:
@@ -573,9 +573,9 @@ 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. }
- apply (irreflexive_eq (R:= Qp_lt) 1%Qp 1%Qp); [done|].
- eapply Qp_lt_le_trans; [apply Lt|done].
+ 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.
Lemma StrMoves_full_exclusive γ q Mt' :
@@ -586,9 +586,9 @@ 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. }
- apply (irreflexive_eq (R:= Qp_lt) 1%Qp 1%Qp); [done|].
- eapply Qp_lt_le_trans; [apply Lt|done].
+ 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.
Lemma WeakAuth_new_lock γ iS q:
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index 05e4d0c1a20612f4b51f6477890c3b3a748e69a8..67bf1b2dfeeea8f25c5f8e6fb1d7e146bf429441 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -112,7 +112,7 @@ Section frac_bor.
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. }
- rewrite -{1}(Qp_div_2 qκ'). rewrite lft_tok_split_obj.
+ 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.
iCombine "H HV0" as "HH".
@@ -120,23 +120,23 @@ Section frac_bor.
iAssert ⎡monPred_in Vb (Vb ⊔ V)⎤%I as "HVVb"; [solve_lat|].
iDestruct ("H" with "HVVb")
as (qφ0 qtok qφ1) "(>% & Hφ0 & >Htok' & Hφ1 & >Hown)".
- destruct (Qp_lower_bound (qκ'/2) (qφ0/2)) as (qq & qκ'0 & qφ0' & Hqκ' & Hqφ).
+ destruct (Qp.lower_bound (qκ'/2) (qφ0/2)) as (qq & qκ'0 & qφ0' & Hqκ' & Hqφ).
iExists qq.
iAssert (▷ φ qq ∗ ⎡▷ φ' (qφ0' + qφ0 / 2) V0⎤)%Qp%I with "[Hφ0]" as "[$ Hqφ]".
- { rewrite -{1}(Qp_div_2 qφ0) {1}Hqφ -assoc_L !embed_later -bi.later_sep. iNext.
+ { rewrite -{1}(Qp.div_2 qφ0) {1}Hqφ -assoc_L !embed_later -bi.later_sep. iNext.
iDestruct ("Hfrac" with "Hφ0") as "[Hφ0 $]". iApply "Hφ'".
by iApply (monPred_in_elim with "HV0"). }
iAssert (▷ ⎡own γ qq⎤ ∗
▷ ⎡own γ (qφ0' + qφ0 / 2 ⋅? qφ1)%Qp⎤)%I with "[Hown]" as "[>Hown1 Hown2]".
{ rewrite -bi.later_sep -embed_sep -own_op. iNext.
- by rewrite -!frac_op -!cmra_op_opM_assoc_L assoc_L !frac_op -Hqφ Qp_div_2. }
+ by rewrite -!frac_op -!cmra_op_opM_assoc_L assoc_L !frac_op -Hqφ Qp.div_2. }
rewrite monPred_objectively_unfold Hqκ'. iDestruct ("Hκ2" $! V0) as "[Hκ2 Hκ2']".
iMod ("Hclose'" with "[-Hown1 Hclose Hκ2']") as "Hκ1".
{ iIntros "#HVb". iExists (qφ0' + qφ0 / 2)%Qp, (qtok ⋅ Some qq)%Qp, qφ1.
iNext. iFrame. iSplit; [|iSplitR "Hφ1"].
- iPureIntro.
rewrite (comm_L _ qtok) cmra_opM_opM_assoc_L -assoc_L Some_op_opM /=.
- rewrite -cmra_op_opM_assoc_L frac_op -(comm_L _ qq) assoc_L -Hqφ Qp_div_2.
+ rewrite -cmra_op_opM_assoc_L frac_op -(comm_L _ qq) assoc_L -Hqφ Qp.div_2.
by rewrite -cmra_opM_opM_assoc_L.
- rewrite comm_L Some_op_opM. destruct qtok as [qtok|]; simpl; [|done].
by iSplitL "Hκ2".
@@ -151,14 +151,14 @@ Section frac_bor.
iAssert ⎡monPred_in Vb (Vb ⊔ V)⎤%I as "HVVb"; [solve_lat|].
iDestruct ("H" with "HVVb")
as (qφ0 qtok qφ1) "(>% & Hφ0 & >Htok' & Hφ1 & >Hown)".
- iEval (rewrite -(Qp_div_2 qκ') {1}Hqκ').
+ iEval (rewrite -(Qp.div_2 qκ') {1}Hqκ').
iClear "Hshr".
iCombine "Hown1" "Hown" as "Hown". iDestruct (own_valid with "Hown") as %Hval.
destruct qtok as [qtok|]; simplify_eq/=; last first.
- { destruct (Qp_not_add_le_r qq 1). by rewrite {1}(_ : 1 = qφ0 ⋅? qφ1)%Qp. }
+ { destruct (Qp.not_add_le_r qq 1). by rewrite {1}(_ : 1 = qφ0 ⋅? qφ1)%Qp. }
assert (∃ qm, qtok = qq ⋅? qm)%Qp as [qm ->].
- { assert (qq ≤ qtok)%Qp as [[qm ->]%Qp_lt_sum| ->]%Qp_le_lteq.
- - rewrite (Qp_add_le_mono_r _ _ (qφ0 ⋅? qφ1)). trans 1%Qp; [done|].
+ { assert (qq ≤ qtok)%Qp as [[qm ->]%Qp.lt_sum| ->]%Qp.le_lteq.
+ - rewrite (Qp.add_le_mono_r _ _ (qφ0 ⋅? qφ1)). trans 1%Qp; [done|].
apply reflexive_eq. by rewrite -frac_op -cmra_op_opM_assoc_L comm_L.
- by exists (Some qm).
- by exists None. }
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 2c28f67679f682a03ca3ecc481db5e5529c878aa..73491d98d893fec15b1b6606b85f68a4096056a4 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -379,7 +379,7 @@ Qed.
Lemma lft_intersect_acc κ κ' q q' :
q.[κ] -∗ q'.[κ'] -∗ ∃ q'', q''.[κ ⊓ κ'] ∗ (q''.[κ ⊓ κ'] -∗ q.[κ] ∗ q'.[κ']).
Proof.
- iIntros "Hκ Hκ'". destruct (Qp_lower_bound q q') as (qq & q0 & q'0 & -> & ->).
+ iIntros "Hκ Hκ'". destruct (Qp.lower_bound q q') as (qq & q0 & q'0 & -> & ->).
iExists qq. rewrite -lft_tok_sep.
iDestruct "Hκ" as "[$$]". iDestruct "Hκ'" as "[$$]". auto.
Qed.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 6bf57750cfd7ad4e3ea45e6675ba99b80d088e51..8c7903132ff9418f06f4eac4422db16624ee4327 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -274,9 +274,9 @@ Section typing.
iMod (lft_create with "LFT") as (Ï_inner) "[Htk #Hend]"; first done.
set (Ï := Ï_inner ⊓ lft_intersect_list κs).
iSpecialize ("Hf" $! x Ï _ vl). iDestruct (HE Ï with "HL") as "#HE'".
- destruct (Qp_lower_bound qκs 1) as (q0 & q'1 & q'2 & -> & Hsum1).
+ destruct (Qp.lower_bound qκs 1) as (q0 & q'1 & q'2 & -> & Hsum1).
rewrite Hsum1. assert (q0 < 1)%Qp as Hq0.
- { apply Qp_lt_sum. eauto. }
+ { apply Qp.lt_sum. eauto. }
clear Hsum1.
iDestruct "Htk" as "[Htk1 Htk2]".
iDestruct "Hκs" as "[Hκs1 Hκs2]".
@@ -291,7 +291,7 @@ Section typing.
done.
+ iSplitL; last done. iExists Ï. rewrite left_id. iSplit; first done.
rewrite decide_False; last first.
- { apply Qp_lt_nge. done. }
+ { apply Qp.lt_nge. done. }
subst Ï. rewrite -!lft_tok_sep. iFrame. iIntros "[Htk1 _]".
rewrite -lft_dead_or. rewrite -bi.or_intro_l. iApply "Hend". iFrame.
+ iIntros (y) "IN {Hend}". iDestruct "IN" as %->%elem_of_list_singleton.
@@ -299,7 +299,7 @@ Section typing.
iDestruct "HÏ" as (κ') "(EQ & Htk & _)". iDestruct "EQ" as %EQ.
rewrite /= left_id in EQ. subst κ' Ï.
rewrite decide_False; last first.
- { apply Qp_lt_nge. done. }
+ { apply Qp.lt_nge. done. }
rewrite -lft_tok_sep. iDestruct "Htk" as "[_ Hκs1]". wp_rec.
iApply ("Hk" with "Htl HL [$Hκs1 $Hκs2]"). rewrite tctx_hasty_val. done.
+ rewrite /tctx_interp vec_to_list_map !zip_with_fmap_r
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 8195b3e06398a8c37613c17c984095dd6b18db76..494c6b5c4ef0d1c2ba1165a9d0c7f2c9bd94207b 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -64,14 +64,14 @@ Section lft_contexts.
Proof.
destruct x as [κ κs]. iIntros (q q'). iSplit; iIntros "H".
- iDestruct "H" as (κ0) "(% & Hq)".
- rewrite Qp_mul_add_distr_l.
+ rewrite Qp.mul_add_distr_l.
iDestruct "Hq" as "[Hq Hq']".
iSplitL "Hq"; iExists _; by iFrame "∗%".
- iDestruct "H" as "[Hq Hq']".
iDestruct "Hq" as (κ0) "(% & Hq)".
iDestruct "Hq'" as (κ0') "(% & Hq')". simpl in *.
rewrite (inj ((lft_intersect_list κs) ⊓.) κ0' κ0); last congruence.
- iExists κ0. rewrite Qp_mul_add_distr_l. by iFrame "∗%".
+ iExists κ0. rewrite Qp.mul_add_distr_l. by iFrame "∗%".
Qed.
Lemma llctx_elt_interp_acc_noend qmax x :
@@ -80,10 +80,10 @@ Section lft_contexts.
Proof.
destruct x as [κ κs].
iIntros "H". iDestruct "H" as (κ0) "(% & Hq & Hend)". iSplitL "Hq".
- { iExists κ0. rewrite Qp_mul_1_r. by iFrame "∗%". }
+ { iExists κ0. rewrite Qp.mul_1_r. by iFrame "∗%". }
iIntros "H". iDestruct "H" as (κ0') "(% & Hq')". simpl in *.
rewrite (inj ((lft_intersect_list κs) ⊓.) κ0' κ0); last congruence.
- iExists κ0. rewrite Qp_mul_1_r. by iFrame "∗%".
+ iExists κ0. rewrite Qp.mul_1_r. by iFrame "∗%".
Qed.
Definition llctx_interp (qmax : Qp) (L : llctx) : vProp Σ :=
@@ -269,7 +269,7 @@ Section lft_contexts.
Proof.
iIntros (? Hal) "#HE [HL1 HL2]".
iMod (Hal with "HE HL1") as (q') "[Htok Hclose]"; first done.
- destruct (Qp_lower_bound (q/2) q') as (qq & q0 & q'0 & Hq & ->). rewrite Hq.
+ destruct (Qp.lower_bound (q/2) q') as (qq & q0 & q'0 & Hq & ->). rewrite Hq.
iExists qq. iDestruct "HL2" as "[$ HL]". iDestruct "Htok" as "[$ Htok]".
iIntros "!> Htok' HL'". iCombine "HL'" "HL" as "HL". rewrite -Hq. iFrame.
iApply "Hclose". iFrame.
@@ -300,7 +300,7 @@ Section lft_contexts.
inversion_clear Hκs.
iIntros "HL". iMod (lctx_lft_alive_tok_noend κ with "HE HL")as (q') "(Hκ & HL & Hclose1)"; [solve_typing..|].
iMod ("IH" with "[//] HL") as (q'') "(Hκs & HL & Hclose2)".
- destruct (Qp_lower_bound q' q'') as (qq & q0 & q'0 & -> & ->).
+ destruct (Qp.lower_bound q' q'') as (qq & q0 & q'0 & -> & ->).
iExists qq. iDestruct "HL" as "[$ HL2]". iDestruct "Hκ" as "[Hκ1 Hκ2]".
iDestruct "Hκs" as "[Hκs1 Hκs2]". iModIntro. simpl. rewrite -lft_tok_sep. iSplitL "Hκ1 Hκs1".
{ by iFrame. }
@@ -343,13 +343,13 @@ Section lft_contexts.
- iDestruct "HL1" as "[HL1 HL2]".
iMod (Hκ with "HE HL1") as (q') "[Htok' Hclose]"; first done.
iMod ("IH" with "HL2") as (q'') "[Htok'' Hclose']".
- destruct (Qp_lower_bound q' q'') as (q0 & q'2 & q''2 & -> & ->).
+ destruct (Qp.lower_bound q' q'') as (q0 & q'2 & q''2 & -> & ->).
iExists q0. rewrite -lft_tok_sep. iDestruct "Htok'" as "[$ Hr']".
iDestruct "Htok''" as "[$ Hr'']". iIntros "!>[Hκ Hfold]".
iMod ("Hclose" with "[$Hκ $Hr']") as "$". iApply "Hclose'". iFrame. }
- iDestruct "H" as (q') "[Htok' Hclose']". rewrite -{5}(Qp_div_2 qL).
+ iDestruct "H" as (q') "[Htok' Hclose']". rewrite -{5}(Qp.div_2 qL).
set (qeff := (if decide (1 ≤ qmax) then 1 else qmax)%Qp).
- destruct (Qp_lower_bound q' (qeff * (qL/2))) as (q0 & q'2 & q''2 & -> & Hmax).
+ destruct (Qp.lower_bound q' (qeff * (qL/2))) as (q0 & q'2 & q''2 & -> & Hmax).
iExists q0. rewrite -(lft_tok_sep q0). rewrite Hmax.
iDestruct "Htok" as "[$ Htok]".
iDestruct "Htok'" as "[$ Htok']". iIntros "!>[Hfold Hκ0]".
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index a545202b26d75c61ef753f7a73ed3570cb2fd3ed..9215c2514cbc8ec6765c82dde37a83ff233c22fe 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -179,7 +179,7 @@ Section arc.
- iAssert (⎡(&{κ} _) V⎤)%I with "[Hbtok]" as "Hb".
{ rewrite bor_unfold_idx. iExists _. by iFrame. }
iClear "H↦ Hinv Hpb".
- rewrite -(Qp_div_2 q0). iDestruct (lft_tok_split_obj with "Htok") as "[$ Htok]".
+ rewrite -(Qp.div_2 q0). iDestruct (lft_tok_split_obj with "Htok") as "[$ Htok]".
remember ((full_arc_own _ _ _ ∨ shared_arc_own _ _ _)%I) as X.
iApply (monPred_in_elim with "Hin"). iModIntro. iSpecialize ("Htok" $! V V).
iMod (bor_acc_cons with "LFT Hb Htok") as "[HP Hclose2]"; first solve_ndisj.
@@ -200,7 +200,7 @@ Section arc.
iMod (bor_sep with "LFT HX") as "[Hrc Hlft]"; first solve_ndisj.
iDestruct (frac_bor_lft_incl with "LFT [> Hlft]") as "$".
{ iApply (bor_fracture with "LFT Hlft"); [|solve_ndisj].
- constructor; [by rewrite Qp_mul_1_r|apply _]. }
+ constructor; [by rewrite Qp.mul_1_r|apply _]. }
iExists _,_,_. iFrame "lc". iApply (bor_share with "Hrc"); solve_ndisj. }
iMod ("Hclose1" with "[]"); [|done]. by auto.
- iMod ("Hclose1" with "[]") as "_"; first by iRight; iNext.
@@ -318,7 +318,7 @@ Section arc.
- iAssert (⎡(&{κ} _) V⎤)%I with "[Hbtok]" as "Hb".
{ rewrite bor_unfold_idx. iExists _. by iFrame. }
iClear "H↦ Hinv Hpb".
- rewrite -(Qp_div_2 q0). iDestruct (lft_tok_split_obj with "Htok") as "[$ Htok]".
+ rewrite -(Qp.div_2 q0). iDestruct (lft_tok_split_obj with "Htok") as "[$ Htok]".
iApply (monPred_in_elim with "Hin"). iModIntro. iSpecialize ("Htok" $! V V).
iMod (bor_acc_cons with "LFT Hb Htok") as "[HP Hclose2]"; first solve_ndisj.
iDestruct "HP" as (γi γs γw γsw ν tw q') "[#Hpersist H]".
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 478fc41f3e87034631aa8ca1b6c807ec7fb0cf15..2439c8f4a65b11390531a02cb1001020eafd6b04 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -148,7 +148,7 @@ Section rc.
- iAssert (⎡(&{κ} _) V⎤)%I with "[Hbtok]" as "Hb".
{ rewrite bor_unfold_idx. iExists _. by iFrame. }
iClear "H↦ Hinv Hpb".
- rewrite -(Qp_div_2 q'). iDestruct (lft_tok_split_obj with "Htok") as "[$ Htok]".
+ rewrite -(Qp.div_2 q'). iDestruct (lft_tok_split_obj with "Htok") as "[$ Htok]".
remember ((∃ _ _ _, rc_persist _ _ _ _ _ ∗ _)%I) as X.
iApply (monPred_in_elim with "Hin"). iModIntro. iSpecialize ("Htok" $! V V).
iMod (bor_acc_cons with "LFT Hb Htok") as "[HP Hclose2]"; [solve_ndisj|].
@@ -167,7 +167,7 @@ Section rc.
iMod (na_inv_alloc tid _ _ (rc_inv tid ν γ l' ty)
with "[Ha Hν2 Hl'1 Hl'2 H†HPend]") as "#?".
{ rewrite /rc_inv. iExists (Some $ Cinl (_, _), _). iFrame "Ha". iExists _.
- iFrame "H†Hl'1 Hl'2 Hν2 HPend". rewrite Qp_div_2; auto. }
+ iFrame "H†Hl'1 Hl'2 Hν2 HPend". rewrite Qp.div_2; auto. }
iMod (ty_share with "LFT HP Hν1") as "[??]"; first solve_ndisj.
subst X. iExists _, _, _. iFrame. iExists ty. iFrame "#". iSplitR; last by auto.
by iApply type_incl_refl. }
@@ -180,7 +180,7 @@ Section rc.
iMod (bor_sep with "LFT HX") as "[Hrc Hlft]"; first solve_ndisj.
iDestruct (frac_bor_lft_incl with "LFT [> Hlft]") as "$".
{ iApply (bor_fracture with "LFT Hlft");
- [split; [by rewrite Qp_mul_1_r|apply _]|solve_ndisj]. }
+ [split; [by rewrite Qp.mul_1_r|apply _]|solve_ndisj]. }
iApply (bor_na with "Hrc"); solve_ndisj. }
iApply ("Hclose1" with "[]"). by auto.
- iMod ("Hclose1" with "[]") as "_"; first by iRight.
@@ -600,12 +600,12 @@ Section code.
{ apply auth_update_alloc, prod_local_update_1,
(op_local_update_discrete _ _ (Some (Cinl ((qb/2)%Qp, 1%positive))))=>-[/= Hqa _].
split; simpl; last done. apply frac_valid. rewrite /= -H comm_L.
- by apply Qp_add_le_mono_l, Qp_div_le. }
+ by apply Qp.add_le_mono_l, Qp.div_le. }
rewrite right_id -Some_op -Cinl_op -pair_op. iDestruct "Hνtok" as "[Hνtok1 Hνtok2]".
iMod ("Hclose3" with "[$Hrctok] Hna") as "[Hα1 Hna]".
iMod ("Hclose2" with "[Hrc◠Hl'1 Hl'2 Hl'†Hνtok2 Hν†$Hna]") as "Hna".
{ iExists _. iFrame "Hrcâ—". iExists _. rewrite Z.add_comm. iFrame.
- rewrite [_ â‹… _]comm frac_op -[(_ + _)%Qp]assoc Qp_div_2. auto. }
+ rewrite [_ â‹… _]comm frac_op -[(_ + _)%Qp]assoc Qp.div_2. auto. }
iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
(* Finish up the proof. *)
iApply (type_type _ _ _ [ x ◠box (&shr{α}(rc ty)); #lr ◠box (rc ty)]
@@ -1090,7 +1090,7 @@ Section code.
iSplitR; first by iApply type_incl_refl.
iMod (ty_share with "LFT Hb Hν1") as "[Hty Hν]"=>//.
iSplitR "Hty"; last by auto. iApply na_inv_alloc. iExists _. do 2 iFrame.
- iExists _. iFrame. by rewrite Qp_div_2. }
+ iExists _. iFrame. by rewrite Qp.div_2. }
iDestruct "Hty" as (ty') "#(Hty'ty & Hinv & Hs & Hν†)".
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]").
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index 8632c8e50914a8b0253fa1a09a43765ed6bc8f10..38ce536849fcc36725c6b41b60043286d1616cbc 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -45,7 +45,7 @@ Section weak.
- iAssert (⎡(&{κ} _) V⎤)%I with "[Hbtok]" as "Hb".
{ rewrite bor_unfold_idx. iExists _. by iFrame. }
iClear "H↦ Hinv Hpb".
- rewrite -(Qp_div_2 q'). iDestruct (lft_tok_split_obj with "Htok") as "[$ Htok]".
+ rewrite -(Qp.div_2 q'). iDestruct (lft_tok_split_obj with "Htok") as "[$ Htok]".
iApply (monPred_in_elim with "Hin"). iModIntro. iSpecialize ("Htok" $! V V).
iMod (bor_acc_cons with "LFT Hb Htok") as "[HP Hclose2]"; first solve_ndisj.
iDestruct "HP" as (γ ν) "(#Hpersist & Hweak)".
@@ -174,12 +174,12 @@ Section code.
{ apply auth_update_alloc, prod_local_update_1,
(op_local_update_discrete _ _ (Some (Cinl ((qb/2)%Qp, 1%positive))))=>-[/= Hqa _].
split; simpl; last done. apply frac_valid.
- rewrite /= -Hq''q0 comm_L. by apply Qp_add_le_mono_l, Qp_div_le. }
+ rewrite /= -Hq''q0 comm_L. by apply Qp.add_le_mono_l, Qp.div_le. }
rewrite right_id -Some_op -Cinl_op -pair_op.
iMod ("Hclose3" with "[$Hwtok] Hna") as "[Hα1 Hna]".
iMod ("Hclose2" with "[Hrc◠Hl'1 Hl'2 Hl'†Hν2 Hν†$Hna]") as "Hna".
{ iExists _. iFrame "Hrcâ—". iExists _. rewrite Z.add_comm. iFrame.
- rewrite [_ â‹… _]comm frac_op -[(_ + _)%Qp]assoc Qp_div_2. auto. }
+ rewrite [_ â‹… _]comm frac_op -[(_ + _)%Qp]assoc Qp.div_2. auto. }
iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
(* Finish up the proof. *)
iApply (type_type _ _ _ [ w ◠box (&shr{α}(weak ty)); #lr ◠box (uninit 2);
diff --git a/theories/typing/lib/refcell/ref.v b/theories/typing/lib/refcell/ref.v
index f36c6f676ba56c154391952a51ac4de7a87ace97..3c900fef2c402c12b74216971499a3e85ffe5e4d 100644
--- a/theories/typing/lib/refcell/ref.v
+++ b/theories/typing/lib/refcell/ref.v
@@ -56,7 +56,7 @@ Section ref.
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 _. }
+ { 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.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index f14d2a774f9e1f27130f190f9171154b106cfdca..ba589a064fa4c94f2a8bcb4f2e443d46148cdb8a 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -73,7 +73,7 @@ Section ref_functions.
split; [split|done].
- by rewrite /= agree_idemp.
- apply frac_valid. rewrite /= -Hq'q'' comm_L.
- by apply Qp_add_le_mono_l, Qp_div_le. }
+ by apply Qp.add_le_mono_l, Qp.div_le. }
wp_apply wp_new; [done..|]. iIntros (lr) "(?&Hlr&?)".
iAssert (lx' ↦∗{qlx'} [ #lv; #lrc])%I with "[H↦1 H↦2]" as "H↦".
{ rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton. iFrame. }
@@ -82,7 +82,7 @@ Section ref_functions.
iMod ("Hcloseδ" with "[H↦lrc H◠Hν1 Hshr' H†] Hna") as "[Hδ Hna]".
{ iExists (Some (_, false, _, _)). rewrite Z.add_comm -Some_op -!pair_op agree_idemp.
iFrame. iExists _. iFrame.
- rewrite (comm Qp_add) (assoc Qp_add) Qp_div_2 (comm Qp_add). auto. }
+ rewrite (comm Qp.add) (assoc Qp.add) Qp.div_2 (comm Qp.add). auto. }
iMod ("Hcloseβ" with "Hδ") as "Hβ". iMod ("Hcloseα1" with "[$H↦]") as "Hα2".
iMod ("Hclose'" with "[$Hα1 $Hα2] HL") as "HL". iMod ("Hclose" with "Hβ HL") as "HL".
iApply (type_type _ _ _
@@ -338,7 +338,7 @@ Section ref_functions.
split; [split|done].
- by rewrite /= agree_idemp.
- apply frac_valid. rewrite /= -Hq1q2 comm_L.
- by apply Qp_add_le_mono_l, Qp_div_le. }
+ by apply Qp.add_le_mono_l, Qp.div_le. }
wp_let. wp_read. wp_let. wp_op. wp_write.
wp_apply (wp_delete _ _ _ _ [_; _] with "[Href↦1 Href↦2 Href†]")=>//.
{ rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton /= freeable_sz_full.
@@ -350,7 +350,7 @@ Section ref_functions.
iMod ("Hclosena" with "[H↦lrc H◠Hν1 Hshr' H†] Hna") as "[Hβ Hna]".
{ iExists (Some (_, false, _, _)). rewrite Z.add_comm -Some_op -!pair_op agree_idemp.
iFrame. iExists _. iFrame.
- rewrite (comm Qp_add) (assoc Qp_add) Qp_div_2 (comm Qp_add). auto. }
+ rewrite (comm Qp.add) (assoc Qp.add) Qp.div_2 (comm Qp.add). auto. }
iMod ("Hβclose" with "Hβ") as "Hα". iMod ("Hclose1" with "Hα HL") as "HL".
iApply (type_type _ [_] _ [ #lrefs ◠box (Π[ref α ty1; ref α ty2]) ]
with "[] LFT HE Hna HL Hk"); first last.
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index f96ffeffb48b58dd9c1fd4a11f3f94de35cbf3ce..6a3cc8ce6b93263df41ad577267a0571dcd574b0 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -148,7 +148,7 @@ Section refcell.
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.
+ 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.
@@ -156,7 +156,7 @@ Section refcell.
{ by apply auth_auth_valid. }
iFrame "Htok'". iExists γ, _. iFrame. iSplitR.
{ rewrite -step_fupd_intro. - auto. - set_solver+. }
- iSplitR; [|done]. iExists (1/2)%Qp. rewrite Qp_div_2. iSplitR; [done|].
+ iSplitR; [|done]. iExists (1/2)%Qp. rewrite Qp.div_2. iSplitR; [done|].
iApply lft_tok_static.
Qed.
Next Obligation.
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index 961e4d958811c191410c97d77532f785b9f2246e..e745680a76f267e7823ab909d98e3a1cfce33c99 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -184,11 +184,11 @@ Section refcell_functions.
split; [split|].
- by rewrite /= agree_idemp.
- apply frac_valid. rewrite /= -Hqq' comm_L.
- by apply Qp_add_le_mono_l, Qp_div_le.
+ by apply Qp.add_le_mono_l, Qp.div_le.
- done. }
iFrame "∗#". iExists (Some (ν, false, _, _)). iFrame "∗#".
rewrite [_ â‹… _]comm -Some_op -!pair_op agree_idemp. iFrame.
- iExists _. iFrame. rewrite -(assoc Qp_add) Qp_div_2 //.
+ iExists _. iFrame. rewrite -(assoc Qp.add) Qp.div_2 //.
- 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 ν)).
@@ -206,7 +206,7 @@ Section refcell_functions.
{ set_solver+. }
* rewrite -lft_dead_or. auto.
* iMod "Hclose". done.
- + iExists _. iFrame. by rewrite Qp_div_2. }
+ + iExists _. iFrame. by rewrite Qp.div_2. }
iMod ("Hclose''" with "[$INV] Hna") as "[Hβtok1 Hna]".
iMod ("Hclose'" with "[$Hβtok1 $Hβtok2]") as "Hα".
iMod ("Hclose" with "Hα HL") as "HL".
@@ -286,7 +286,7 @@ Section refcell_functions.
{ set_solver+. }
* rewrite -lft_dead_or. auto.
* iMod "Hclose". done.
- - iSplitL; [|done]. iExists _. iFrame. by rewrite Qp_div_2. }
+ - iSplitL; [|done]. iExists _. iFrame. by rewrite Qp.div_2. }
iMod ("Hclose'" with "Hβtok") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
iApply (type_type _ _ _
[ x ◠box (&shr{α}(refcell ty)); r ◠box (uninit 3); #lref ◠box (refmut α ty)]
diff --git a/theories/typing/lib/refcell/refmut.v b/theories/typing/lib/refcell/refmut.v
index 4898ebc7c9a4e5087f93fb8733301387c78182b6..1ebcf5fde529893711d815b5d9b17a84c0ec9385 100644
--- a/theories/typing/lib/refcell/refmut.v
+++ b/theories/typing/lib/refcell/refmut.v
@@ -55,7 +55,7 @@ Section refmut.
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.
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index b4faa81abb0a5215ac0a55402ed70bdbbf2c346d..af534737450548070e4051a098dd22edd6396ba9 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -80,7 +80,7 @@ Section refmut_functions.
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. }
@@ -312,7 +312,7 @@ Section refmut_functions.
split; [split|done].
- by rewrite /= agree_idemp.
- apply frac_valid. rewrite /= -Hqq1 comm_L.
- by apply Qp_add_le_mono_l, Qp_div_le. }
+ by apply Qp.add_le_mono_l, Qp.div_le. }
wp_let. wp_read. wp_let. wp_op. wp_write.
wp_apply (wp_delete _ _ _ _ [_; _] with "[Hrefmut↦1 Hrefmut↦2 Hrefmut†]")=>//.
{ rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton /= freeable_sz_full.
@@ -325,7 +325,7 @@ Section refmut_functions.
{ iExists (Some (_, true, _, _)).
rewrite -Some_op -!pair_op agree_idemp /= (comm _ xH _).
iFrame. iSplitL; [|done]. iExists _. iFrame.
- rewrite (comm Qp_add) (assoc Qp_add) Qp_div_2 (comm Qp_add). auto. }
+ rewrite (comm Qp.add) (assoc Qp.add) Qp.div_2 (comm Qp.add). auto. }
iMod ("Hβclose" with "Hβ") as "Hα". iMod ("Hclose1" with "Hα HL") as "HL".
iApply (type_type _ [_] _ [ #lrefmuts ◠box (Π[refmut α ty1; refmut α ty2]) ]
with "[] LFT HE Hna HL Hk"); first last.
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 73ed9c4e104e5c6ac5a54d854bfa6102ebf1a152..48d6273754013809c48630ebf54adeb332e9defa 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -71,14 +71,14 @@ Section rwlock_inv.
Proof.
iIntros (st') "g". rewrite -embed_sep -own_op.
iMod (own_update with "g") as "$"; [|done]. apply auth_update_alloc.
- rewrite Pos.add_comm Qp_add_comm -pos_op_add /=
+ rewrite Pos.add_comm Qp.add_comm -pos_op_add /=
-{2}(agree_idemp (to_agree _)) -frac_op
2!pair_op Cinr_op Some_op.
rewrite -{2}(right_id None op (Some (Cinr (_, (q' /2)%Qp, _)))).
apply op_local_update_discrete =>-[Hagv _]. split; [split|done].
- by rewrite /= agree_idemp.
- - apply frac_valid. rewrite -Hqq' comm -{2}(Qp_div_2 q') /=.
- apply Qp_add_le_mono_l. apply Qp_le_add_r.
+ - apply frac_valid. rewrite -Hqq' comm -{2}(Qp.div_2 q') /=.
+ apply Qp.add_le_mono_l. apply Qp.le_add_r.
Qed.
Lemma rwown_update_write γs :
@@ -311,7 +311,7 @@ Section rwlock_inv.
iIntros "!> !> !%". destruct st as [[|[[]]]|]; simpl; lia.
+ iExists _. iFrame "Hn". iExists (Some $ inr (ν, (1/2)%Qp, n)).
iSplitL ""; [done|]. iFrame "Hst". iExists _.
- iFrame "Hshr Htok2 Hhν". iSplitR ""; [|by rewrite Qp_div_2].
+ iFrame "Hshr Htok2 Hhν". iSplitR ""; [|by rewrite Qp.div_2].
iIntros "!> Hν". iDestruct (lft_tok_dead with "Htok Hν") as "[]".
- iMod (own_alloc (st_global (Some $ inl ()))) as (γs) "Hst".
{ by apply auth_auth_valid. }
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index db82f8519501eccb20538b8ddb492c42f8753466..39d39a629e732c97a63769087102f6c2b86a7990 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -178,7 +178,7 @@ Section rwlock_functions.
[solve_typing..|].
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. }
+ as "[Hβtok1 Hβtok2]". { by rewrite Qp.div_2. }
iDestruct "Hinv" as (γ γs tyO tyS) "(EqO & EqS & R)".
iDestruct "R" as (tR vR) "R".
wp_bind (!ʳˡˣ(LitV lx))%E.
@@ -257,7 +257,7 @@ Section rwlock_functions.
by iFrame "Htok2 Hshr rst H†R1".
+ iExists (Some (inr (ν, (q + q' / 2)%Qp, (n + 1)%positive))).
iSplitL ""; [done|]. iFrame "Share g W'". iExists _.
- iFrame "H†Hh Hshr Htok1 R2". by rewrite -Qp_add_assoc Qp_div_2.
+ iFrame "H†Hh Hshr Htok1 R2". by rewrite -Qp.add_assoc Qp.div_2.
- rewrite Eqst2. iDestruct "INT" as "(Hown & $ & R)".
iExists (). iSplitL ""; [done|]. iIntros (t2 Ext2) "W' !>". iSplitL "".
{ rewrite /Q1 Eqst2. by iIntros "!> $". } iIntros "!> !>".
@@ -277,7 +277,7 @@ Section rwlock_functions.
by iFrame "Htok2 Hshr rst H†R1".
+ iExists (Some (inr (ν, (1 / 2)%Qp, 1%positive))). iSplitL ""; [done|].
iFrame "Share g W'". iExists _. iFrame "H†Hshr Htok1 R2".
- rewrite Qp_div_2. iSplitR ""; [|done].
+ rewrite Qp.div_2. iSplitR ""; [|done].
iIntros "!> Hν". iApply "Hh". rewrite -lft_dead_or. auto. }
iNext. simpl.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index d2d965a5b6317acd2355a106ca2c17c419bd113a..42ee0b627039c763c39bccd5cedbb9fe2fb4a861 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -51,7 +51,7 @@ Section rwlockreadguard.
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 _]. }
+ { iApply bor_fracture; try done. constructor; [by rewrite Qp.mul_1_r|apply _]. }
iExists _. iFrame "#". iApply ty_shr_mono; last done.
iApply lft_intersect_mono; last done. iApply lft_incl_refl.
Qed.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index 56cfca652c14ce992f4a50369608c2cb06e4d831..df763433722b22cb0f181117384cac54dbe5ac5f 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -131,14 +131,14 @@ Section rwlockreadguard_functions.
iExists None. iSplitL ""; [done|]. iFrame "Share Hâ— Hb W".
iDestruct (GPS_SWSharedReaders_join with "R Rm") as "R".
by rewrite Hqrq'.
- - inversion Eqst as [Eqst1]. rewrite Eqn Qp_add_comm Eqst1.
+ - inversion Eqst as [Eqst1]. rewrite Eqn Qp.add_comm Eqst1.
iMod (rwown_update_read_dealloc with "Hâ— Hâ—¯") as "Hâ—".
iApply step_fupd_intro; [solve_ndisj|]. iIntros "!>". iSplitL ""; [done|].
have Eqn': (Z.pos n - 1) = Z.pos (Pos.pred n).
{ rewrite Pos2Z.inj_pred => // ?. by subst n. } rewrite Eqn'.
iExists (Some (inr (ν, q0, Pos.pred n))). iSplitL ""; [done|].
iFrame "Share H◠W". iExists (q + qr)%Qp. iFrame "H†Hh Hshr Hν".
- iSplitR "R Rm"; [by rewrite Qp_add_assoc (Qp_add_comm q0)|].
+ iSplitR "R Rm"; [by rewrite Qp.add_assoc (Qp.add_comm q0)|].
by iApply (GPS_SWSharedReaders_join with "R Rm"). } }
iIntros "!>" (b t [] v') "(Hβ & _ & CASE)".
diff --git a/theories/typing/own.v b/theories/typing/own.v
index f3a80f6127a31310a1802df8c633cf2772b1ed2c..241daeef628c44539a8b657ab6264f83d68b2b00 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -24,7 +24,7 @@ Section own.
destruct n as [|n].
- iSplit; iIntros "H /="; auto.
- assert (Z.of_nat (S n) = 0 ↔ False) as -> by done. rewrite right_id.
- by rewrite /freeable_sz Qp_div_diag.
+ by rewrite /freeable_sz Qp.div_diag.
Qed.
Lemma freeable_sz_full_S n l : ⎡freeable_sz (S n) (S n) l⎤%I ≡@{vProp _} ⎡†{1}l…(S n)⎤%I.
@@ -39,7 +39,7 @@ Section own.
- by rewrite right_id Nat.add_0_r.
- 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.
+ by rewrite -Qp.div_add_distr pos_to_Qp_add -Nat2Pos.inj_add.
Qed.
(* Make sure 'simpl' doesn't unfold. *)
diff --git a/theories/typing/product.v b/theories/typing/product.v
index ebf54324c18a8facb4edc76588e3d332e9c0be4b..11d525b0d1888b4a8e8d175fd0c8bc4df9a1b014 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -121,7 +121,7 @@ Section product.
set_solver. }
iDestruct (na_own_acc with "Htl") as "[$ Htlclose]".
{ generalize (shr_locsE_shift l ty1.(ty_size) ty2.(ty_size)). simpl. set_solver+. }
- destruct (Qp_lower_bound q1 q2) as (qq & q'1 & q'2 & -> & ->). iExists qq.
+ destruct (Qp.lower_bound q1 q2) as (qq & q'1 & q'2 & -> & ->). iExists qq.
iDestruct "H1" as (vl1) "[H↦1 H1]". iDestruct "H2" as (vl2) "[H↦2 H2]".
rewrite !split_prod_mt.
iDestruct (ty_size_eq with "H1") as "#>%".
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 9ec82d6163b17f2485259a68a09aeb8d6f5123fc..295463e8f8daf236738b6b40455920ff797e9054 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -207,9 +207,9 @@ Section typing_rules.
iApply ("He" $! (κ' ⊓ Λ) with "LFT HE Htl [HL Htk] HC HT").
rewrite /llctx_interp /=. iFrame "HL".
iExists Λ. iSplit; first done.
- destruct (decide (1 ≤ qmax)%Qp) as [_|Hlt%Qp_lt_nge].
+ destruct (decide (1 ≤ qmax)%Qp) as [_|Hlt%Qp.lt_nge].
- by iFrame "#∗".
- - apply Qp_lt_sum in Hlt as [q' ->]. iDestruct "Htk" as "[$ Htk]".
+ - apply Qp.lt_sum in Hlt as [q' ->]. iDestruct "Htk" as "[$ Htk]".
iIntros "Htk'". iApply "Hinh". iFrame.
Qed.
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index e21de128913e8a7258ebb2f7f2b27ec9d05abe64..e5f5b3acd5f1ba33df58e077d492334381ecad29 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -200,7 +200,7 @@ Section sum.
trans (shr_locsE (l +â‚— 1) (max_list_with ty_size tyl)).
- apply shr_locsE_subseteq. lia.
- set_solver+. }
- destruct (Qp_lower_bound q'1 q'2) as (q' & q'01 & q'02 & -> & ->).
+ destruct (Qp.lower_bound q'1 q'2) as (q' & q'01 & q'02 & -> & ->).
rewrite -(heap_mapsto_pred_combine _ q' q'02); last (by intros; apply ty_size_eq).
rewrite (fractional (Φ := λ q, _ ↦{q} _ ∗ _ ↦∗{q}: _)%I).
iDestruct "HownC" as "[HownC1 HownC2]". iDestruct "Hown" as "[Hown1 Hown2]".
@@ -210,7 +210,7 @@ Section sum.
iDestruct ("Htlclose" with "Htl") as "Htl".
iDestruct (heap_mapsto_agree with "[Hown1] [Hown2]") as "#Heq".
{ iDestruct "Hown1" as "[$ _]". } { iDestruct "Hown2" as "[$ _]". }
- iDestruct "Heq" as %[= ->%Z_of_nat_inj].
+ iDestruct "Heq" as %[= ->%Nat2Z.inj].
iMod ("Hclose'" with "Htl [$HownC1 $HownC2]") as "[$ ?]".
iMod ("Hclose" with "[$Hown1 $Hown2]") as "$". by iFrame.
Qed.
diff --git a/theories/typing/uninit.v b/theories/typing/uninit.v
index a2a3a0a0b5c1ca4166f78089834ebca280a844db..18032c941dccf8f7caf7523ae0ab42fb1ec9f331 100644
--- a/theories/typing/uninit.v
+++ b/theories/typing/uninit.v
@@ -84,7 +84,7 @@ Section uninit.
subtype E L (uninit n) (Î (ty :: tyl)).
Proof.
intros ?%Nat2Z.inj_le. rewrite -!uninit_uninit0_eqtype /uninit0=>Hty Htyl.
- rewrite (le_plus_minus ty.(ty_size) n) // replicate_plus
+ rewrite (le_plus_minus ty.(ty_size) n) // replicate_add
-(prod_flatten_r _ _ [_]) /= -prod_app. repeat (done || f_equiv).
Qed.
Lemma uninit_product_subtype_cons_l {E L} (n : nat) ty tyl :
@@ -94,7 +94,7 @@ Section uninit.
subtype E L (Î (ty :: tyl)) (uninit n).
Proof.
intros ?%Nat2Z.inj_le. rewrite -!uninit_uninit0_eqtype /uninit0=>Hty Htyl.
- rewrite (le_plus_minus ty.(ty_size) n) // replicate_plus
+ rewrite (le_plus_minus ty.(ty_size) n) // replicate_add
-(prod_flatten_r _ _ [_]) /= -prod_app. repeat (done || f_equiv).
Qed.
Lemma uninit_product_eqtype_cons_r {E L} (n : nat) ty tyl :
diff --git a/theories/typing/util.v b/theories/typing/util.v
index eff9fb5ef9a066bd49a78c5596234261f2c63f5f..b84333791005fe297e9a1d6d947a78215c61640d 100644
--- a/theories/typing/util.v
+++ b/theories/typing/util.v
@@ -38,7 +38,7 @@ Section util.
iIntros "!> !> * % Htok".
iMod (inv_acc with "Hinv") as "[INV Hclose]"; first solve_ndisj.
iDestruct "INV" as "[>Hbtok|#Hshr]".
- - rewrite -(Qp_div_2 q).
+ - rewrite -(Qp.div_2 q).
iDestruct (lft_tok_split_obj with "Htok") as "[$ Htok]".
rewrite monPred_objectively_unfold. iSpecialize ("Htok" $! V).
iApply (monPred_in_elim with "Hin"). iModIntro.
@@ -69,7 +69,7 @@ Section util.
iIntros "!> !> * % Htok".
iMod (inv_acc with "Hinv") as "[INV Hclose]"; first solve_ndisj.
iDestruct "INV" as "[>Hbtok|#Hshr]".
- - rewrite -(Qp_div_2 q).
+ - rewrite -(Qp.div_2 q).
iDestruct (lft_tok_split_obj with "Htok") as "[$ Htok]".
rewrite monPred_objectively_unfold. iSpecialize ("Htok" $! V).
iApply (monPred_in_elim with "Hin"). iModIntro.