From 22bbf305812ff6a6f7a4b34cca90bf075b45a50d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 21 Oct 2020 09:27:39 +0200
Subject: [PATCH] Bump std++ (Qp changes).
---
opam | 2 +-
theories/lang/arc.v | 49 +++----
theories/lang/arc_cmra.v | 33 ++---
theories/lifetime/frac_borrow.v | 138 +++++++-----------
theories/typing/function.v | 2 +-
theories/typing/lib/arc.v | 4 +-
theories/typing/lib/rc/rc.v | 7 +-
theories/typing/lib/rc/weak.v | 5 +-
theories/typing/lib/refcell/ref.v | 2 +-
theories/typing/lib/refcell/ref_code.v | 21 ++-
theories/typing/lib/refcell/refcell_code.v | 8 +-
theories/typing/lib/refcell/refmut.v | 2 +-
theories/typing/lib/refcell/refmut_code.v | 10 +-
theories/typing/lib/rwlock/rwlock.v | 8 +-
theories/typing/lib/rwlock/rwlock_code.v | 2 +-
theories/typing/lib/rwlock/rwlockreadguard.v | 2 +-
.../typing/lib/rwlock/rwlockreadguard_code.v | 5 +-
.../typing/lib/rwlock/rwlockwriteguard_code.v | 1 -
theories/typing/own.v | 17 +--
theories/typing/product_split.v | 1 -
theories/typing/util.v | 1 -
21 files changed, 130 insertions(+), 190 deletions(-)
diff --git a/opam b/opam
index e41b3f1e..094bd18e 100644
--- a/opam
+++ b/opam
@@ -16,7 +16,7 @@ This branch uses a proper weak memory model.
"""
depends: [
- "coq-gpfsl" { (= "dev.2020-10-21.0.e29403ca") | (= "dev") }
+ "coq-gpfsl" { (= "dev.2020-10-30.0.93f5a686") | (= "dev") }
]
build: [make "-j%{jobs}%"]
diff --git a/theories/lang/arc.v b/theories/lang/arc.v
index bfc7200d..a085a017 100644
--- a/theories/lang/arc.v
+++ b/theories/lang/arc.v
@@ -1,4 +1,3 @@
-From Coq.QArith Require Import Qcanon.
From iris.bi Require Import fractional.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import excl csum frac auth agree.
@@ -270,10 +269,6 @@ End ArcInv.
Typeclasses Opaque StrongTok WeakTok StrMoves StrDowns WkUps.
-Lemma Qp_plus_div (x y : Qp) n:
- (x/n + y/n)%Qp = ((x+y) / n)%Qp.
-Proof. apply Qp_eq; simpl. by rewrite -Qcmult_plus_distr_l. Qed.
-
Section arc.
(* P1 is the thing that is shared by strong reference owners (in practice,
this is the lifetime token), and P2 is the thing that is owned by the
@@ -614,7 +609,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_plus_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 ∗
@@ -670,7 +665,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_plus_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 ∗
@@ -959,7 +954,7 @@ Section arc.
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_plus_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 *)
@@ -1148,7 +1143,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_plus_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'".
@@ -1313,7 +1308,7 @@ Section arc.
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_plus_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".
@@ -1350,7 +1345,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_plus_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&_)])".
@@ -1507,7 +1502,7 @@ Section arc.
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_plus_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". }
@@ -1648,7 +1643,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_plus_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. }
@@ -1661,7 +1656,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_plus_div.
+ 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 _.
@@ -1672,7 +1667,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_plus_assoc (Qp_plus_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.
@@ -1704,7 +1699,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_plus_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. }
@@ -1730,8 +1725,8 @@ 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_plus_div.
- iFrame "R' tok WU SeenU'". by rewrite Qp_plus_assoc (Qp_plus_comm q2). }
+ 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 *)
iIntros "!>" (b t2 [] v2) "(_ & [((%&%&%)&QI) | ((%&_&%)&IW&R'&_&P&IS)])";
@@ -1793,7 +1788,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_plus_div 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.
@@ -2144,7 +2139,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_plus_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. }
@@ -2172,11 +2167,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_plus_assoc (Qp_plus_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_plus_div. 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)])";
@@ -2252,7 +2247,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_plus_div 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".
@@ -2367,7 +2362,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_plus_div 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 *)
@@ -2518,7 +2513,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_plus_comm Qp_plus_div 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 *)
@@ -2754,7 +2749,7 @@ Section arc.
iDestruct (WeakAuth_strong with "[$WA $oW]") as %[qs ?]. subst iS.
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_plus_div 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'.
@@ -2778,7 +2773,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_plus_div 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 81a09112..596986c8 100644
--- a/theories/lang/arc_cmra.v
+++ b/theories/lang/arc_cmra.v
@@ -1,4 +1,3 @@
-From Coq.QArith Require Import Qcanon.
From iris.base_logic.lib Require Import invariants.
From iris.proofmode Require Import tactics.
From iris.bi Require Import fractional.
@@ -368,9 +367,9 @@ Section ArcGhost.
iDestruct (@own_valid _ arcUR with "WU")
as %[_ [_ [[VAL _]%auth_frag_valid_1 _]]].
iPureIntro. simpl in VAL.
- have Lt: (1%Qp < (1%Qp + q)%Qp)%Qc. apply Qp_lt_sum. by eexists.
- apply (irreflexive_eq (R:= Qclt) 1%Qp 1%Qp); [done|].
- eapply Qclt_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 :
@@ -441,19 +440,18 @@ Section ArcGhost.
Lemma StrongAuth_new_tok γ (q q': frac) n (Hqq' : (q + q')%Qp = 1%Qp):
StrongAuth γ (Some (q,n)) ==∗
- StrongAuth γ (Some ((q + (q'/2)%Qp)%Qp, (n + 1)%positive)) ∗
+ StrongAuth γ (Some ((q + q'/2)%Qp, (n + 1)%positive)) ∗
StrongTok γ (q'/2)%Qp.
Proof.
iIntros "own". rewrite -embed_sep -own_op.
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_plus_comm -pos_op_plus /= -frac_op' pair_op Some_op.
+ rewrite Pos.add_comm Qp_add_comm -pos_op_plus /= -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 Qcplus_le_mono_l. rewrite -{1}(Qcanon.Qcplus_0_l (q'/2)%Qp).
- apply Qcplus_le_mono_r, Qp_ge_0.
+ apply Qp_add_le_mono_l. apply Qp_le_add_r.
Qed.
Lemma WeakAuth_first_tok γ iS :
@@ -470,7 +468,7 @@ Section ArcGhost.
Lemma WeakAuth_new_tok γ iS (q q': frac) n (Hqq' : (q + q')%Qp = 1%Qp):
WeakAuth γ (iS, Some (Cinl (q, n))) ==∗
- WeakAuth γ (iS, Some (Cinl ((q + (q'/2)%Qp)%Qp, (n + 1)%positive))) ∗
+ WeakAuth γ (iS, Some (Cinl ((q + q'/2)%Qp, (n + 1)%positive))) ∗
WeakTok γ (q'/2)%Qp.
Proof.
iIntros "own". rewrite -embed_sep -own_op.
@@ -478,13 +476,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_plus_comm -pos_op_plus /=
+ rewrite Pos.add_comm Qp_add_comm -pos_op_plus /=
-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 Qcplus_le_mono_l. rewrite -{1}(Qcanon.Qcplus_0_l (q'/2)%Qp).
- apply Qcplus_le_mono_r, Qp_ge_0.
+ apply Qp_add_le_mono_l. apply Qp_le_add_r.
Qed.
Lemma StrongAuth_drop_last γ q:
@@ -572,9 +569,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%Qp < (1%Qp + q)%Qp)%Qc. apply Qp_lt_sum. by eexists.
- apply (irreflexive_eq (R:= Qclt) 1%Qp 1%Qp); [done|].
- eapply Qclt_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' :
@@ -585,9 +582,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%Qp < (1%Qp + q)%Qp)%Qc. apply Qp_lt_sum. by eexists.
- apply (irreflexive_eq (R:= Qclt) 1%Qp 1%Qp); [done|].
- eapply Qclt_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 59a4ce45..b0fec12b 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -1,4 +1,3 @@
-From Coq Require Import Qcanon.
From iris.proofmode Require Import tactics.
From iris.bi Require Import fractional.
From iris.algebra Require Import frac.
@@ -16,25 +15,22 @@ Definition frac_bor `{!invG Σ, !lftG Lat E0 Σ, !frac_borG Σ} κ
▷ □ ⎡(∀ q1 q2, φ' (q1+q2)%Qp ↔ φ' q1 ∗ φ' q2) V0⎤ ∗
(* Then we use an (internal) atomic persistent borrow. *)
- &in_at{κ'} (∃ (qfresh : Qp) (qdep qused : Qc),
+ &in_at{κ'} (∃ (qfresh : Qp) (qdep qused : option Qp),
(* We divide the 1 fraction into 3 parts... *)
- ⌜0 ≤ qdep⌝%Qc ∗ ⌜0 ≤ qused⌝%Qc ∗ ⌜(qfresh + qdep + qused = 1)%Qc⌝ ∗
+ ⌜(qfresh ⋅? qdep ⋅? qused = 1)%Qp⌝ ∗
(* First part: the piece of φ' which is still fresh. *)
⎡φ' qfresh V0⎤ ∗
(* Second part: some tokens have been left in deposit while the
fractured borrow is accessed. *)
- (if decide (0 < qdep)%Qc is left H return _
- then ⎡(mk_Qp qdep H).[κ'] V0⎤ else True) ∗
+ ⎡from_option (λ qdep', qdep'.[κ']) True qdep V0⎤ ∗
(* Third part: the piece of φ' that is "already used". It can be given
back when the lifetime ends, but cannot be used when accessing the
fractured borrow. *)
- (if decide (0 < qused)%Qc is left H return _
- then φ' (mk_Qp qused H) else True) ∗
+ from_option φ' True%I qused ∗
(* We keep a set of "receipts", to prove that we will always have
enough fractions of the lifetime in deposit. *)
- (if decide (0 < qfresh+qused)%Qc is left H return _
- then ⎡own γ (mk_Qp (qfresh+qused) H)⎤
- else True (* Dummy, never happens *))))%I.
+ ⎡own γ (qfresh ⋅? qused)⎤))%I.
+
Notation "&frac{ κ }" := (frac_bor κ) (format "&frac{ κ }") : bi_scope.
Section frac_bor.
@@ -77,21 +73,18 @@ 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, 0, 0.
- iDestruct "Hφ" as "[_ Hφ]". repeat (iSplit; [done|]).
- rewrite /= -(proj2 (Qp_eq 1 (mk_Qp (1+0) _))) //. iFrame. }
+ { 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 & _)".
- destruct (decide (0 < q')%Qc).
+ iDestruct "Hφ" as (q q' q'' Hsum) "(Hφ1 & Htok & Hφ2 & _)".
+ destruct q' as [q'|]; simplify_eq/=.
{ iExFalso. rewrite -(embed_pure False). iModIntro ⎡_⎤%I.
iApply (lft_tok_dead_subj with "Htok [H†]"). iApply "H†". }
- destruct (Qcle_lt_or_eq 0 q') as [|<-]; [done|done|].
- rewrite Qcplus_0_r in Hsum. destruct (decide (0 < q'')%Qc).
+ destruct q'' as [q''|]; simplify_eq/=.
{ iDestruct ("Hfrac" with "[Hφ1 Hφ2]") as "H".
- iSplitL "Hφ1"; [|done]. by iApply monPred_in_elim.
- - by rewrite (proj2 (Qp_eq (q + mk_Qp q'' _) 1) Hsum). }
- destruct (Qcle_lt_or_eq 0 q'') as [|<-]; [done|done|]. rewrite Qcplus_0_r in Hsum.
- rewrite (proj2 (Qp_eq q 1) Hsum). by iApply monPred_in_elim.
+ - by iEval (rewrite -Hsum). }
+ by iApply monPred_in_elim.
- iDestruct (monPred_in_intro with "Hfrac") as (V) "[HV Hfrac']".
iDestruct "H" as (κ') "(#? & #? & >_)". iExists γ, κ', V, φ. iFrame "#".
iSplitR; [|iSplitR].
@@ -111,7 +104,6 @@ Section frac_bor.
↑lftN ⊆ E →
⎡lft_ctx⎤ -∗ &frac{κ}φ -∗ q.[κ] ={E}=∗ ∃ q', ▷ φ q' ∗ (▷ φ q' ={E}=∗ q.[κ]).
Proof.
- assert (Inhabited Qc) by exact (populate 0%Qc).
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.
@@ -122,7 +114,7 @@ Section frac_bor.
iDestruct (monPred_in_intro with "HH") as (V) "(#HV & H & %)".
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)".
+ 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φ).
iExists qq.
iAssert (▷ φ qq ∗ ⎡▷ φ' (qφ0' + qφ0 / 2) V0⎤)%Qp%I with "[Hφ0]" as "[$ Hqφ]".
@@ -130,32 +122,20 @@ Section frac_bor.
iDestruct ("Hfrac" with "Hφ0") as "[Hφ0 $]". iApply "Hφ'".
by iApply (monPred_in_elim with "HV0"). }
iAssert (▷ ⎡own γ qq⎤ ∗
- ▷ if decide (0 < qφ0' + qφ0 / 2 + qφ1)%Qc is left H
- then ⎡own γ (mk_Qp _ H)⎤ else True)%I with "[Hown]" as "[>Hown1 Hown2]".
- { destruct (decide (0 < qφ0 + qφ1)%Qc) as [|[]]; last by apply Qcplus_pos_nonneg.
- destruct decide as [|[]]; first last.
- { assert (0 < / 2)%Qc by reflexivity. unfold Qcdiv.
- auto using Qcplus_pos_nonneg, Qcplus_pos_pos, Qcmult_pos_pos. }
- rewrite -bi.later_sep -embed_sep -own_op frac_op' monPred_at_embed. iNext.
- rewrite [(_ + _)%Qp](_ : _ = {| Qp_car := qφ0 + qφ1 |}) //.
- apply Qp_eq. apply Qp_eq in Hqφ. simpl in Hqφ.
- rewrite /= !Qcplus_assoc -Hqφ (Qcplus_diag (qφ0/2)) Qcmult_div_r //. }
+ ▷ ⎡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. }
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 + qq)%Qc, qφ1. iNext. iFrame.
- iSplit; [|iSplit; [done|iSplit; [|iSplitR "Hφ1"]]].
- - iPureIntro. apply Qcplus_nonneg_nonneg, Qclt_le_weak=>//.
- - iPureIntro. simpl.
- replace (qφ0' + qφ0 / 2%Z + (qtok + qq))%Qc
- with (qq + qφ0' + qφ0 / 2%Z + qtok)%Qc by ring.
- apply Qp_eq in Hqφ. simpl in Hqφ. rewrite -Hqφ Qcplus_diag Qcmult_div_r //.
- - destruct (decide (0 < qtok)%Qc), (decide (0 < qtok + qq)%Qc)=>//.
- + erewrite (proj2 (Qp_eq (mk_Qp (_ + _) _) (_ + qq))).
- rewrite lft_tok_fractional monPred_at_embed. by iFrame "Htok'". done.
- + destruct (Qcle_lt_or_eq 0 qtok) as [|<-]=>//.
- erewrite (proj2 (Qp_eq (mk_Qp (_ + _) _) qq)). iFrame.
- simpl. apply Qcplus_0_l.
- - destruct (decide (0 < qφ1)%Qc); [|done]. iCombine "HV HVb" as "HH".
+ { 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.
+ by rewrite -cmra_opM_opM_assoc_L.
+ - rewrite comm_L Some_op_opM. destruct qtok as [qtok|]; simpl; [|done].
+ by iSplitL "Hκ2".
+ - destruct qφ1 as [qφ1|]; [|done]. iCombine "HV HVb" as "HH".
iDestruct (monPred_in_intro with "HH") as (VV) "(HVV & % & %)".
iApply (monPred_in_elim with "HVV"). iFrame. }
rewrite -Hqκ'. iClear "Hκκ' HV HVVb". clear dependent qφ0' qtok qφ1 Vb qφ0 V.
@@ -165,47 +145,35 @@ Section frac_bor.
iDestruct (monPred_in_intro with "HH") as (V) "(#HV & H & %)".
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 (decide (0 < qφ0 + qφ1)%Qc) as [|[]]; last by auto using Qcplus_pos_nonneg.
- iClear "Hshr". rewrite monPred_at_embed. iDestruct "Hown" as ">Hown".
+ as (qφ0 qtok qφ1) "(>% & Hφ0 & >Htok' & Hφ1 & >Hown)".
+ iEval (rewrite -(Qp_div_2 qκ') {1}Hqκ').
+ iClear "Hshr".
iCombine "Hown1" "Hown" as "Hown". iDestruct (own_valid with "Hown") as %Hval.
- assert (qq + qφ0 + qφ1 ≤ 1)%Qc. {
- destruct (decide (0 < qφ0 + qφ1)%Qc) as [|[]]; [|by apply Qcplus_pos_nonneg].
- by rewrite -Qcplus_assoc. }
- assert (0 ≤ qtok - qq)%Qc. {
- replace (qtok - qq)%Qc with ((qφ0 + qtok + qφ1) - (qq + qφ0 + qφ1))%Qc by ring.
- change 0%Qc with (1 - 1)%Qc. apply Qcplus_le_compat.
- by apply reflexive_eq. by apply Qcopp_le_compat. }
- replace qtok with (qtok - qq + qq)%Qc by ring.
- destruct (decide (0 < qtok - qq + qq)%Qc) as [|[]]; last by apply Qcplus_nonneg_pos.
- assert (∀ H,
- (mk_Qp (qtok - qq + qq) H).[κ'] V0 ⊣⊢
- (if decide (0 < qtok - qq)%Qc is left H return _ then (mk_Qp _ H).[κ'] V0 else True)
- ∗ qq.[κ'] V0) as ->.
- { intros ?. destruct (decide (0 < qtok - qq)%Qc) as [|EQ%Qcnot_lt_le%Qcle_antisym]=>//.
- - rewrite -monPred_at_sep -lft_tok_fractional. by erewrite (proj2 (Qp_eq _ _)).
- - erewrite (proj2 (Qp_eq _ _)), (left_id _ _)=>//=. by rewrite -EQ Qcplus_0_l. }
- iDestruct "Htok'" as "[Htok1 >Htok2]". iCombine "Htok2" "Hκ2'" as "Htok2".
- rewrite -monPred_at_sep -lft_tok_fractional -Hqκ'.
+ 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. }
+ 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|].
+ apply reflexive_eq. by rewrite -frac_op' -cmra_op_opM_assoc_L comm_L.
+ - by exists (Some qm).
+ - by exists None. }
+ iAssert (⎡from_option (λ qm', qm'.[κ']) True qm V0⎤ ∗ ⎡ monPred_at qq.[κ'] V0 ⎤)%I
+ with "[Htok']" as "[Htok1 Htok2]".
+ { destruct qm as [qm|]; simplify_eq/=; [|by auto].
+ iDestruct "Htok'" as "[$$]". }
+ iCombine "Htok2 Hκ2'" as "Htok2"; rewrite -monPred_at_sep -lft_tok_fractional.
iDestruct (monPred_in_elim with "HV0 Htok2") as "$".
- iApply "Hclose'". iIntros "#HVb". iExists qφ0, (qtok - qq)%Qc, (qφ1 + qq)%Qc.
- replace (qφ0 + (qtok - qq) + (qφ1 + qq))%Qc with (qφ0 + qtok + qφ1)%Qc by ring.
- iNext. iFrame "Hφ0 %". iSplit; [|iSplitL "Htok1"; [|iSplitR "Hown"]].
- - iPureIntro. apply Qcplus_nonneg_nonneg, Qclt_le_weak=>//.
- - by destruct (decide (0 < qtok - qq))%Qc.
- - destruct (decide (0 < qφ1 + qq))%Qc as [|[]]; last by apply Qcplus_nonneg_pos.
- destruct (decide (0 < qφ1)%Qc) as [|<-%Qcnot_lt_le%Qcle_antisym]=>//.
- + erewrite (proj2 (Qp_eq (mk_Qp (_ + _) _) _)).
- * rewrite !bi.intuitionistically_elim.
- iDestruct (monPred_in_elim with "HV0 Hfrac") as "Hfrac'".
- iApply "Hfrac'". iSplitL "Hφ"; [by iApply "Hφ'"|]. iCombine "HV HVb" as "HH".
- iDestruct (monPred_in_intro with "HH") as (VV) "(HVV & % & %)".
- iApply (monPred_in_elim with "HVV"). iFrame.
- * simpl. ring.
- + erewrite (proj2 (Qp_eq (mk_Qp _ _) qq)). by iApply "Hφ'". simpl; ring.
- - destruct decide as [|[]].
- + erewrite ->(proj2 (Qp_eq _ _)). iFrame. simpl. ring.
- + auto using Qcplus_pos_pos, Qcplus_nonneg_pos.
+ iApply "Hclose'". iIntros "#HVb". iExists qφ0, qm, (Some (qq ⋅? qφ1)); simpl.
+ iNext. iFrame "Hφ0 %". iSplit; [|iSplitL "Htok1"; [done|iSplitR "Hown"]].
+ - iPureIntro. by rewrite -cmra_op_opM_assoc_L -(comm_L _ qq)
+ -cmra_op_opM_assoc_L (comm_L _ qq) cmra_op_opM_assoc_L.
+ - destruct qφ1 as [qφ1|]; simpl; [|by iApply "Hφ'"].
+ rewrite !bi.intuitionistically_elim.
+ iDestruct (monPred_in_elim with "HV0 Hfrac") as "Hfrac'".
+ iApply "Hfrac'". iSplitL "Hφ"; [by iApply "Hφ'"|]. iCombine "HV HVb" as "HH".
+ iDestruct (monPred_in_intro with "HH") as (VV) "(HVV & % & %)".
+ iApply (monPred_in_elim with "HVV"). iFrame.
+ - by rewrite -cmra_op_opM_assoc_L -(comm_L _ qq) cmra_op_opM_assoc_L.
Qed.
Lemma frac_bor_shorten φ κ κ' : κ ⊑ κ' -∗ &frac{κ'}φ -∗ &frac{κ}φ.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 802638e6..782dd346 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -276,7 +276,7 @@ Section typing.
iMod (bor_create _ ϝ with "LFT Hκs") as "[Hκs HκsI]"; first done.
iDestruct (frac_bor_lft_incl with "LFT [>Hκs]") as "#Hκs".
{ iApply (bor_fracture with "LFT Hκs"); [|done].
- split; [by rewrite Qp_mult_1_r|]. apply _. }
+ split; [by rewrite Qp_mul_1_r|]. apply _. }
iApply ("Hf" with "LFT [] Htl [Htk] [Hk HκsI HL]").
+ iApply "HE'". iIntros "{$# Hf Hinh HE' LFT HE %}".
iInduction κs as [|κ κs] "IH"=> //=. iSplitL.
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index 94937ba4..663e1e21 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -1,5 +1,3 @@
-From Coq.QArith Require Import Qcanon.
-
From iris.bi Require Import fractional.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import auth csum frac agree.
@@ -202,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_mult_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.
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 6fa28d52..86e8e3cc 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -181,7 +181,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_mult_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.
@@ -593,9 +593,8 @@ Section code.
iMod (own_update with "Hrc●") as "[Hrc● Hrctok2]".
{ 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 -{2}(Qp_div_2 qb).
- apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (_ / _)%Qp).
- apply Qcplus_le_mono_r, Qp_ge_0. }
+ split; simpl; last done. apply frac_valid'. rewrite /= -H comm_L.
+ 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".
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index eadb9ca5..21072063 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -1,4 +1,3 @@
-From Coq.QArith Require Import Qcanon.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import auth csum frac agree numbers.
From lrust.lang Require Import memcpy.
@@ -175,9 +174,7 @@ 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 -{2}(Qp_div_2 qb).
- apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (_ / _)%Qp).
- apply Qcplus_le_mono_r, Qp_ge_0. }
+ 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".
diff --git a/theories/typing/lib/refcell/ref.v b/theories/typing/lib/refcell/ref.v
index d24833bf..4028a108 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_mult_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 f8d64e9f..62f4a49f 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -1,4 +1,3 @@
-From Coq.QArith Require Import Qcanon.
From iris.algebra Require Import auth csum frac agree numbers.
From iris.bi Require Import fractional.
From lrust.lifetime Require Import lifetime na_borrow.
@@ -12,7 +11,7 @@ Section ref_functions.
Lemma refcell_inv_reading_inv tid l γ α ty q ν :
refcell_inv tid l γ α ty -∗
⎡own γ (◯ reading_stR q ν)⎤ -∗
- ∃ (q' : Qp) n, l ↦ #(Zpos n) ∗ ⌜(q ≤ q')%Qc⌝ ∗
+ ∃ (q' : Qp) n, l ↦ #(Zpos n) ∗ ⌜(q ≤ q')%Qp⌝ ∗
⎡own γ (● (refcell_st_to_R $ Some (ν, false, q', n)) ⋅ ◯ reading_stR q ν)⎤ ∗
((1).[ν] ={↑lftN ∪ ↑histN}[↑histN]▷=∗ &{α}((l +ₗ 1) ↦∗: ty_own ty tid)) ∗
(∃ q'', ⌜(q' + q'' = 1)%Qp⌝ ∗ q''.[ν]) ∗
@@ -20,7 +19,7 @@ Section ref_functions.
Proof.
iIntros "INV H◯".
iDestruct "INV" as (st) "(H↦lrc & H● & INV)".
- iAssert (∃ q' n, st ≡ Some (ν, false, q', n) ∗ ⌜q ≤ q'⌝%Qc)%I with
+ iAssert (∃ q' n, st ≡ Some (ν, false, q', n) ∗ ⌜q ≤ q'⌝%Qp)%I with
"[#]" as (q' n) "[%%]".
{ destruct st as [[[[??]?]?]|];
iDestruct (own_valid_2 with "H● H◯")
@@ -73,10 +72,9 @@ Section ref_functions.
(op_local_update_discrete _ _ (reading_stR (q''/2)%Qp ν))=>-[Hagv _].
split; [split|done].
- by rewrite /= agree_idemp.
- - apply frac_valid'. rewrite -Hq'q'' comm -{2}(Qp_div_2 q'').
- apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (q''/2)%Qp).
- apply Qcplus_le_mono_r, Qp_ge_0. }
- wp_apply wp_new; [done..|]. iIntros (lr) "(H†lr&Hlr)".
+ - apply frac_valid'. rewrite /= -Hq'q'' comm_L.
+ 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. }
wp_let. wp_apply (wp_memcpy with "[$Hlr $H↦]"); [done..|].
@@ -84,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_plus) (assoc Qp_plus) Qp_div_2 (comm Qp_plus). 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 _ _ _
@@ -336,9 +334,8 @@ Section ref_functions.
(op_local_update_discrete _ _ (reading_stR (q2/2)%Qp ν))=>-[Hagv _].
split; [split|done].
- by rewrite /= agree_idemp.
- - apply frac_valid'. rewrite -Hq1q2 comm -{2}(Qp_div_2 q2).
- apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (q2/2)%Qp).
- apply Qcplus_le_mono_r, Qp_ge_0. }
+ - apply frac_valid'. rewrite /= -Hq1q2 comm_L.
+ 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 +347,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_plus) (assoc Qp_plus) Qp_div_2 (comm Qp_plus). 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_code.v b/theories/typing/lib/refcell/refcell_code.v
index 81d8b73a..21e4ca17 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -1,4 +1,3 @@
-From Coq.QArith Require Import Qcanon.
From iris.algebra Require Import auth csum frac agree.
From iris.bi Require Import fractional.
From lrust.lang Require Import memcpy.
@@ -184,13 +183,12 @@ Section refcell_functions.
(op_local_update_discrete _ _ (reading_stR (q'/2)%Qp ν)) => ?.
split; [split|].
- by rewrite /= agree_idemp.
- - apply frac_valid'. rewrite -Hqq' comm -{2}(Qp_div_2 q').
- apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (q'/2)%Qp).
- apply Qcplus_le_mono_r, Qp_ge_0.
+ - apply frac_valid'. rewrite /= -Hqq' comm_L.
+ 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_plus) 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 ν)).
diff --git a/theories/typing/lib/refcell/refmut.v b/theories/typing/lib/refcell/refmut.v
index 3776c5e7..6a2cecc4 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_mult_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 57f781da..424ab2ba 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -1,4 +1,3 @@
-From Coq.QArith Require Import Qcanon.
From iris.algebra Require Import auth csum frac agree numbers.
From iris.bi Require Import fractional.
From lrust.lifetime Require Import na_borrow.
@@ -81,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_mult_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.
@@ -308,9 +307,8 @@ Section refmut_functions.
(op_local_update_discrete _ _ (writing_stR (q1/2)%Qp ν))=>-[Hagv _].
split; [split|done].
- by rewrite /= agree_idemp.
- - apply frac_valid'. rewrite -Hqq1 comm -{2}(Qp_div_2 q1).
- apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (q1/2)%Qp).
- apply Qcplus_le_mono_r, Qp_ge_0. }
+ - apply frac_valid'. rewrite /= -Hqq1 comm_L.
+ 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.
@@ -323,7 +321,7 @@ Section refmut_functions.
{ iExists (Some (_, true, _, _)).
rewrite -Some_op -!pair_op agree_idemp /= (comm _ xH _).
iFrame. iSplitL; [|done]. iExists _. iFrame.
- rewrite (comm Qp_plus) (assoc Qp_plus) Qp_div_2 (comm Qp_plus). 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 de3da62e..d2cf2420 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -1,4 +1,3 @@
-From Coq.QArith Require Import Qcanon.
From iris.bi Require Import fractional.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import auth excl csum frac agree numbers.
@@ -71,15 +70,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_plus_comm -pos_op_plus /=
+ rewrite Pos.add_comm Qp_add_comm -pos_op_plus /=
-{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 Qcplus_le_mono_l. rewrite -{1}(Qcanon.Qcplus_0_l (q'/2)%Qp).
- apply Qcplus_le_mono_r, Qp_ge_0.
+ - 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 :
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 17576c1b..0e9e4c64 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -259,7 +259,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_plus_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 "!> !>".
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index 0469dc74..432dc938 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -50,7 +50,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_mult_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 f76e7f02..acb8d15d 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -1,4 +1,3 @@
-From Coq.QArith Require Import Qcanon.
From iris.bi Require Import fractional.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import auth csum frac agree numbers.
@@ -133,14 +132,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_plus_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_plus_assoc (Qp_plus_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/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index 4c9a3ca3..d2691c55 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -1,4 +1,3 @@
-From Coq.QArith Require Import Qcanon.
From iris.bi Require Import fractional.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import auth csum frac agree.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 03080ae6..7d53c63d 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -1,4 +1,3 @@
-From Coq Require Import Qcanon.
From iris.proofmode Require Import tactics.
From lrust.lang Require Import memcpy.
From lrust.typing Require Export type.
@@ -8,24 +7,24 @@ Set Default Proof Using "Type".
Section own.
Context `{!typeG Σ}.
- Program Definition freeable_sz (n : nat) (sz : nat) (l : loc) : iProp Σ :=
+ Definition freeable_sz (n : nat) (sz : nat) (l : loc) : iProp Σ :=
match sz, n return _ with
| 0%nat, _ => True
| _, 0%nat => False
- | sz, n => †{mk_Qp (sz / n) _}l…sz
+ | sz, n => †{pos_to_Qp (Pos.of_nat sz) / pos_to_Qp (Pos.of_nat n)}l…sz
end%I.
- Next Obligation. intros _ _ _ sz0 ? n ?. by apply Qcmult_pos_pos. Qed.
Arguments freeable_sz : simpl never.
- Global Instance freable_sz_timeless n sz l : Timeless (freeable_sz n sz l).
+
+ Global Instance freeable_sz_timeless n sz l : Timeless (freeable_sz n sz l).
Proof. destruct sz, n; apply _. Qed.
Lemma freeable_sz_full n l :
⎡freeable_sz n n l⎤%I ≡@{vProp _} (⎡†{1}l…n⎤ ∨ ⌜Z.of_nat n = 0⌝)%I.
Proof.
- destruct n.
+ destruct n as [|n].
- iSplit; iIntros "H /="; auto.
- assert (Z.of_nat (S n) = 0 ↔ False) as -> by done. rewrite right_id.
- rewrite /freeable_sz (proj2 (Qp_eq (mk_Qp _ _) 1)) //= /Qcdiv Qcmult_inv_r //.
+ 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,8 +38,8 @@ Section own.
- by rewrite left_id shift_loc_0.
- by rewrite right_id Nat.add_0_r.
- iSplit. by iIntros "[[]?]". by iIntros "[]".
- - rewrite hist_freeable_op_eq. f_equiv. apply Qp_eq.
- rewrite /= -Qcmult_plus_distr_l -Z2Qc_inj_add /Z.add /Qcdiv /=. do 3 f_equal. lia.
+ - rewrite hist_freeable_op_eq. f_equiv.
+ 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_split.v b/theories/typing/product_split.v
index 4463e0d1..a28c8786 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -1,4 +1,3 @@
-From Coq Require Import Qcanon.
From iris.algebra Require Import numbers.
From iris.proofmode Require Import tactics.
From lrust.typing Require Export type.
diff --git a/theories/typing/util.v b/theories/typing/util.v
index 1adf126a..6cbb1e3b 100644
--- a/theories/typing/util.v
+++ b/theories/typing/util.v
@@ -1,4 +1,3 @@
-From Coq Require Import Qcanon.
From lrust.typing Require Export type.
Set Default Proof Using "Type".
--
GitLab