From f15b04fd3d1809e2b1dac3b90409c557ee80f163 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 13 Aug 2019 21:52:44 +0200
Subject: [PATCH] bump GPFSL
---
theories/lang/arc.v | 12 +++---
theories/lang/arc_cmra.v | 50 +++++++++++-----------
theories/lifetime/model/primitive.v | 8 ++--
theories/typing/lib/rc/rc.v | 4 +-
theories/typing/lib/rc/weak.v | 2 +-
theories/typing/lib/refcell/ref_code.v | 6 +--
theories/typing/lib/refcell/refcell_code.v | 2 +-
theories/typing/lib/refcell/refmut_code.v | 4 +-
theories/typing/lib/rwlock/rwlock.v | 4 +-
9 files changed, 46 insertions(+), 46 deletions(-)
diff --git a/theories/lang/arc.v b/theories/lang/arc.v
index 2c3042fc..fbb6da04 100644
--- a/theories/lang/arc.v
+++ b/theories/lang/arc.v
@@ -602,11 +602,11 @@ Section arc.
⎡ own γ ((ε, ◯ ((Some 1%Qp, ε)), ε) : arcUR) ⎤)%I as ">Own".
{ do 9 setoid_rewrite <- embed_sep. do 9 setoid_rewrite <- own_op.
iMod (own_alloc (A:=arcUR)) as (γ) "Own"; last by iExists γ.
- rewrite 5!(@pair_op (prodUR (authUR strong_stUR) (authUR weak_stUR))
+ rewrite -5!(@pair_op (prodUR (authUR strong_stUR) (authUR weak_stUR))
(prodUR (prodUR move_selfUR move_otherUR) move_otherUR)).
- rewrite /= 2!pair_op /= !left_id /=. split.
+ rewrite /= -2!pair_op /= !left_id /=. split.
{ by split; apply auth_both_valid. }
- do 2 setoid_rewrite pair_op. rewrite /= !left_id !right_id.
+ do 2 setoid_rewrite <-pair_op. rewrite /= !left_id !right_id.
split; split; [..|by apply auth_both_valid|by apply auth_auth_valid];
(split; [by apply auth_both_valid|rewrite /= right_id]);
[|rewrite left_id]; by apply auth_auth_valid. }
@@ -659,11 +659,11 @@ Section arc.
WeakUpAuth γ ∅ ∗ WkUps γ 1%Qp ∅)%I as ">Own".
{ do 8 setoid_rewrite <- embed_sep. do 8 setoid_rewrite <- own_op.
iMod (own_alloc (A:=arcUR)) as (γ) "?"; last by iExists γ.
- rewrite 4!(@pair_op (prodUR (authUR strong_stUR) (authUR weak_stUR))
+ rewrite -4!(@pair_op (prodUR (authUR strong_stUR) (authUR weak_stUR))
(prodUR (prodUR move_selfUR move_otherUR) move_otherUR)).
- rewrite /= 2!pair_op /= !left_id /=. split.
+ rewrite /= -2!pair_op /= !left_id /=. split.
{ by split; apply auth_both_valid. }
- do 2 setoid_rewrite pair_op. rewrite /= !left_id !right_id.
+ do 2 setoid_rewrite <-pair_op. rewrite /= !left_id !right_id.
split; split; [..|by apply auth_both_valid|by apply auth_auth_valid];
(split; [by apply auth_both_valid|rewrite /= right_id]);
[|rewrite left_id]; by apply auth_auth_valid. }
diff --git a/theories/lang/arc_cmra.v b/theories/lang/arc_cmra.v
index 71210a3a..09bfa2b4 100644
--- a/theories/lang/arc_cmra.v
+++ b/theories/lang/arc_cmra.v
@@ -154,7 +154,7 @@ Section ArcGhost.
rewrite /Fractional => p q. rewrite -embed_sep -own_op.
apply embed_proper, own.own_proper.
apply pair_proper; [done|]. do 3 (apply pair_proper; [|done]). simpl.
- by rewrite -auth_frag_op -Some_op pair_op frac_op' agree_idemp.
+ by rewrite -auth_frag_op -Some_op -pair_op frac_op' agree_idemp.
Qed.
Global Instance StrMoves_asfractional γ q Mt :
AsFractional (StrMoves γ q Mt) (λ q, StrMoves γ q Mt) q.
@@ -164,9 +164,9 @@ Section ArcGhost.
rewrite /Fractional => p q. rewrite -embed_sep -own_op.
apply embed_proper, own.own_proper.
apply pair_proper; [done|]. apply pair_proper; [|done].
- rewrite /=. setoid_rewrite pair_op. apply pair_proper; [done|].
- rewrite pair_op. apply pair_proper; [|done].
- by rewrite -auth_frag_op -Some_op pair_op frac_op' lat_op_join' lat_join_idem_L.
+ rewrite /=. setoid_rewrite <-pair_op. apply pair_proper; [done|].
+ rewrite -pair_op. apply pair_proper; [|done].
+ by rewrite -auth_frag_op -Some_op -pair_op frac_op' lat_op_join' lat_join_idem_L.
Qed.
Global Instance StrDowns_asfractional γ q Dt :
AsFractional (StrDowns γ q Dt) (λ q, StrDowns γ q Dt) q.
@@ -176,8 +176,8 @@ Section ArcGhost.
rewrite /Fractional => p q. rewrite -embed_sep -own_op.
apply embed_proper, own.own_proper.
do 2 (apply pair_proper; [done|]).
- rewrite /=. setoid_rewrite pair_op. apply pair_proper; [|done].
- by rewrite -auth_frag_op -Some_op pair_op frac_op' lat_op_join' lat_join_idem_L.
+ rewrite /=. setoid_rewrite <-pair_op. apply pair_proper; [|done].
+ by rewrite -auth_frag_op -Some_op -pair_op frac_op' lat_op_join' lat_join_idem_L.
Qed.
Global Instance WkUps_asfractional γ q Ut :
AsFractional (WkUps γ q Ut) (λ q, WkUps γ q Ut) q.
@@ -194,7 +194,7 @@ Section ArcGhost.
Lemma arc_ghost_move_self_main_valid Mt1 Mt2 q:
✓ (moveSAuth Mt1 ⋅ moveSMain q Mt2) → Mt2 = Mt1.
Proof.
- rewrite pair_op right_id.
+ rewrite -pair_op right_id.
move => [/= /auth_both_valid [/Some_included
[[_ /= /to_agree_inj /to_latT_inj /leibniz_equiv_iff //]|
/prod_included[_ /to_agree_included /to_latT_inj /leibniz_equiv_iff //]]_]_].
@@ -202,14 +202,14 @@ Section ArcGhost.
Lemma arc_ghost_move_self_cert_valid Mt1 Mt2:
✓ (moveSAuth Mt1 ⋅ certS Mt2) → Mt2 ⊆ Mt1.
- Proof. rewrite pair_op => [[_ /auth_both_valid [/latT_included // _]]]. Qed.
+ Proof. rewrite -pair_op => [[_ /auth_both_valid [/latT_included // _]]]. Qed.
Lemma StrongMoveAuth_agree γ Mt q Mt':
StrongMoveAuth γ Mt ∗ StrMoves γ q Mt' -∗ ⌜Mt = Mt'âŒ.
Proof.
rewrite -embed_sep -own_op.
iIntros "own". iDestruct (own_valid with "own") as %VALID. iPureIntro.
- move : VALID => [/=_ [/= ]]. rewrite pair_op.
+ move : VALID => [/=_ [/= ]]. rewrite -pair_op.
move => [/= /arc_ghost_move_self_main_valid //].
Qed.
@@ -219,7 +219,7 @@ Section ArcGhost.
rewrite -embed_sep -own_op.
iIntros "own". iDestruct (own_valid with "own") as %VAL. iPureIntro.
move : VAL => [/=_ [/= [[VAL _]_]_]]. move :VAL.
- rewrite /= -auth_frag_op -Some_op pair_op auth_valid_discrete /= Some_valid.
+ rewrite /= -auth_frag_op -Some_op -pair_op auth_valid_discrete /= Some_valid.
move => [_ /agree_op_inv' /to_latT_inj /leibniz_equiv_iff // ].
Qed.
@@ -228,7 +228,7 @@ Section ArcGhost.
Proof.
rewrite -embed_sep -own_op.
iIntros "own". iDestruct (own_valid with "own") as %VALID. iPureIntro.
- move :VALID => [/= _ [/= ]]. rewrite pair_op.
+ move :VALID => [/= _ [/= ]]. rewrite -pair_op.
move => [/= /arc_ghost_move_self_cert_valid //].
Qed.
@@ -240,9 +240,9 @@ Section ArcGhost.
iMod (own_update with "own") as "$"; [|done].
apply prod_update; [done|].
apply prod_update; [|rewrite /= left_id right_id //].
- setoid_rewrite pair_op. rewrite /=.
+ setoid_rewrite <-pair_op. rewrite /=.
apply prod_update; [|rewrite /= left_id right_id //].
- rewrite /= 2!pair_op /= 2!right_id left_id.
+ rewrite /= -2!pair_op /= 2!right_id left_id.
apply prod_update; simpl.
- by apply auth_update, option_local_update, exclusive_local_update.
- apply auth_update_alloc.
@@ -258,7 +258,7 @@ Section ArcGhost.
Lemma arc_ghost_move_other_main_valid Mt1 Mt2:
✓ (moveOAuth Mt1 ⋅ moveOMain 1%Qp Mt2) → Mt2 = Mt1.
Proof.
- rewrite pair_op.
+ rewrite -pair_op.
move => [/= /auth_both_valid [/Some_included
[[/= _ /to_latT_inj /leibniz_equiv_iff //]|
/prod_included [/= /frac_included /= // _]]]].
@@ -267,7 +267,7 @@ Section ArcGhost.
Lemma arc_ghost_move_other_cert_valid Mt1 Mt2:
✓ (moveOAuth Mt1 ⋅ certO Mt2) → Mt2 ⊆ Mt1.
Proof.
- rewrite pair_op right_id.
+ rewrite -pair_op right_id.
move => [/= _ /auth_both_valid [/latT_included // ]].
Qed.
@@ -293,7 +293,7 @@ Section ArcGhost.
Proof.
rewrite -embed_sep -own_op. apply embed_proper, own.own_proper.
do 2 (apply pair_proper; [done|]; apply pair_proper; [|done]).
- simpl. rewrite -auth_frag_op -Some_op pair_op -frac_op' lat_op_join'.
+ simpl. rewrite -auth_frag_op -Some_op -pair_op -frac_op' lat_op_join'.
rewrite (lat_le_join_l_L (Dt ∪ Dt') Dt'); [done|solve_lat].
Qed.
@@ -319,7 +319,7 @@ Section ArcGhost.
Proof.
rewrite -embed_sep -own_op. apply embed_proper, own.own_proper.
do 2 (apply pair_proper; [done|]). apply pair_proper; [|done]. simpl.
- rewrite -auth_frag_op -Some_op pair_op -frac_op' lat_op_join'.
+ rewrite -auth_frag_op -Some_op -pair_op -frac_op' lat_op_join'.
rewrite (lat_le_join_l_L (Ut ∪ Ut') Ut'); [done|solve_lat].
Qed.
@@ -329,7 +329,7 @@ Section ArcGhost.
Proof.
rewrite -embed_sep -own_op. apply embed_proper, own.own_proper.
do 2 (apply pair_proper; [done|]; apply pair_proper; [|done]).
- simpl. by rewrite -auth_frag_op -Some_op pair_op -frac_op' lat_op_join'.
+ simpl. by rewrite -auth_frag_op -Some_op -pair_op -frac_op' lat_op_join'.
Qed.
Lemma StrDowns_update γ Dt1 Dt2 Dt' q :
@@ -340,9 +340,9 @@ Section ArcGhost.
iMod (own_update with "own") as "$"; [|done].
apply prod_update; [done|]. simpl.
apply prod_update; [|rewrite /= !right_id //].
- setoid_rewrite pair_op. rewrite /=.
+ setoid_rewrite <-pair_op. rewrite /=.
apply prod_update; [rewrite /= !right_id //|].
- rewrite /= 2!pair_op /= 2!right_id left_id. rewrite -2!lat_op_join'.
+ rewrite /= -2!pair_op /= 2!right_id left_id. rewrite -2!lat_op_join'.
apply prod_update; simpl.
- apply auth_update, option_local_update, prod_local_update_2.
rewrite (cmra_comm_L (to_latT Dt1)) (cmra_comm_L (to_latT Dt2)).
@@ -448,7 +448,7 @@ 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_plus_comm -pos_op_plus /= -frac_op' -pair_op Some_op.
+ rewrite Pos.add_comm Qp_plus_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').
@@ -479,7 +479,7 @@ Section ArcGhost.
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 /=
- -frac_op' -pair_op -Cinl_op Some_op.
+ -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').
@@ -507,7 +507,7 @@ Section ArcGhost.
iMod (@own_update _ arcUR with "own") as "$"; [|done].
apply prod_update; [|simpl; by rewrite right_id]. apply prod_update; [|done].
apply auth_update_dealloc.
- rewrite -frac_op' -pos_op_plus /= (cmra_comm_L q) -pair_op Some_op.
+ rewrite -frac_op' -pos_op_plus /= (cmra_comm_L q) pair_op Some_op.
by apply (cancel_local_update_unit (Some _)), _.
Qed.
@@ -531,7 +531,7 @@ Section ArcGhost.
iMod (@own_update _ arcUR with "own") as "$"; [|done].
apply prod_update; [|simpl; by rewrite right_id]. apply prod_update; [done|].
apply auth_update_dealloc. apply prod_local_update; [done|].
- rewrite -frac_op' -pos_op_plus /= (cmra_comm_L q) -pair_op -Cinl_op Some_op.
+ rewrite -frac_op' -pos_op_plus /= (cmra_comm_L q) pair_op Cinl_op Some_op.
by apply (cancel_local_update_unit (Some _)), _.
Qed.
@@ -570,7 +570,7 @@ Section ArcGhost.
Proof.
rewrite -embed_sep -own_op. iIntros "own".
iDestruct (@own_valid _ arcUR with "own") as %[[_ VAL] _]. simpl in VAL.
- iPureIntro. move : VAL. rewrite -auth_frag_op pair_op -Some_op frac_op'.
+ iPureIntro. move : VAL. rewrite -auth_frag_op -pair_op -Some_op frac_op'.
move => /auth_valid_discrete /= [/= ? _].
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|].
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 843edb0d..697b4ec5 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -241,7 +241,7 @@ Proof.
destruct (A !! Λ) as [[? V]|] eqn:EQΛ; intros [= ->].
assert (({[Λ := Cinr (to_agree $ to_latT V)]} ⋅ to_alftUR A) ≡ to_alftUR A) as HAinsert.
{ move=>Λ'. destruct (decide (Λ = Λ')) as [<-|Hne].
- + rewrite lookup_op lookup_fmap EQΛ lookup_singleton -Some_op Cinr_op agree_idemp //.
+ + rewrite lookup_op lookup_fmap EQΛ lookup_singleton -Some_op -Cinr_op agree_idemp //.
+ rewrite lookup_op lookup_fmap !lookup_insert_ne // lookup_empty left_id -lookup_fmap //. }
iMod (own_update _ ((â— to_alftUR A)) with "HA") as "HA".
{ eapply (auth_update_alloc _ _ ({[Λ := Cinr (to_agree $ to_latT V)]}⋅∅)),
@@ -306,11 +306,11 @@ Proof.
- iIntros "H". iDestruct "H" as (V') "[#? H] ".
(* FIXME : the Proper instance for singleton cannot be found automatically here. *)
rewrite (fin_maps.singleton_proper Λ _ (Cinl (_, to_latT V' ⋅ to_latT V'))); last first.
- { rewrite lat_op_join /= lat_join_idem //. } rewrite -pair_op -Cinl_op -op_singleton.
+ { rewrite lat_op_join /= lat_join_idem //. } rewrite pair_op Cinl_op -op_singleton.
iDestruct "H" as "[Hp Hq]". iSplitL "Hp"; auto.
- iIntros "[Hp Hq]". iDestruct "Hp" as (Vp') "[#HVp' p]".
iDestruct "Hq" as (Vq') "[#HVq' Hq]". iExists (_ ⊔ _).
- rewrite -lat_op_join' -pair_op -Cinl_op -op_singleton auth_frag_op own_op.
+ rewrite -lat_op_join' pair_op Cinl_op -op_singleton auth_frag_op own_op.
iFrame. iCombine "HVp' HVq'" as "HVpq'".
iDestruct (monPred_in_intro with "HVpq'") as (V) "[HV [%%]]".
rewrite (_:Vp' ⊔ Vq' ⊑ V) //. solve_lat.
@@ -324,7 +324,7 @@ Proof.
rewrite /lft_tok. rewrite -monPred_objectively_big_sepMS_entails -big_sepMS_sep.
apply big_sepMS_mono=>// Λ ?. iStartProof (iProp _). iDestruct 1 as (V) "[#? H]".
rewrite (fin_maps.singleton_proper Λ _ (Cinl (_, to_latT V ⋅ to_latT bot))); last first.
- { rewrite lat_op_join' right_id //. } rewrite -pair_op -Cinl_op -op_singleton.
+ { rewrite lat_op_join' right_id //. } rewrite pair_op Cinl_op -op_singleton.
iDestruct "H" as "[Hp Hq]". iSplitL "Hp"; [by auto|]. iIntros (?). iExists bot. auto.
Qed.
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index a64d605a..306d82a0 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -376,7 +376,7 @@ Section code.
iFrame. iExists _. iFrame. auto with iFrame.
* iMod (own_update_2 with "Hst Htok") as "Hst".
{ apply auth_update_dealloc.
- rewrite -pair_op -Cinl_op Some_op -{1}(left_id 0%nat _ weak) -pair_op.
+ rewrite pair_op Cinl_op Some_op -{1}(left_id 0%nat _ weak) pair_op.
apply (cancel_local_update_unit _ (_, _)). }
iApply "Hclose". iFrame. iExists _. iFrame. iExists (q+q'')%Qp. iFrame.
iSplitL; first last.
@@ -596,7 +596,7 @@ Section code.
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. }
- rewrite right_id -Some_op Cinl_op pair_op. iDestruct "Hνtok" as "[Hνtok1 Hνtok2]".
+ 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.
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index 051166ae..e5ef1983 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -178,7 +178,7 @@ Section code.
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 right_id -Some_op Cinl_op pair_op.
+ 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.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index d89fc965..a257f41e 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -82,7 +82,7 @@ Section ref_functions.
wp_let. wp_apply (wp_memcpy with "[$Hlr $H↦]"); [done..|].
iIntros "[Hlr H↦]". wp_seq. iMod ("Hcloseα2" with "[$H◯] Hna") as "[Hα1 Hna]".
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.
+ { 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. }
iMod ("Hcloseβ" with "Hδ") as "Hβ". iMod ("Hcloseα1" with "[$H↦]") as "Hα2".
@@ -177,7 +177,7 @@ Section ref_functions.
by rewrite Pos.add_1_l Pos.pred_succ. }
iMod (own_update with "Hâ—â—¯") as "$".
{ apply auth_update_dealloc.
- rewrite -(agree_idemp (to_agree _)) -!pair_op Some_op.
+ rewrite -(agree_idemp (to_agree _)) !pair_op Some_op.
apply (cancel_local_update_unit (reading_stR q ν)), _. }
iApply step_fupd_intro; first set_solver. iExists (q+q'')%Qp. iFrame.
by rewrite assoc (comm _ q0 q). }
@@ -348,7 +348,7 @@ Section ref_functions.
iDestruct "Hrefs" as "(Hrefs1 & Hrefs2 & Hrefs3 & Hrefs4)".
rewrite !shift_loc_assoc. wp_write. do 3 (wp_op; wp_write).
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.
+ { 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. }
iMod ("Hβclose" with "Hβ") as "Hα". iMod ("Hclose1" with "Hα HL") as "HL".
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index d0a55fec..81d8b73a 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -189,7 +189,7 @@ Section refcell_functions.
apply Qcplus_le_mono_r, Qp_ge_0.
- done. }
iFrame "∗#". iExists (Some (ν, false, _, _)). iFrame "∗#".
- rewrite [_ â‹… _]comm -Some_op !pair_op agree_idemp. iFrame.
+ rewrite [_ â‹… _]comm -Some_op -!pair_op agree_idemp. iFrame.
iExists _. iFrame. rewrite -(assoc Qp_plus) Qp_div_2 //.
- iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". done.
iMod (own_update with "Hownst") as "[Hownst Hreading]"; first by apply
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index 4b34ab08..bd2587ea 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -142,7 +142,7 @@ Section refmut_functions.
iDestruct "Hq" as (q) "(<- & ?)". iFrame.
- simpl in *. setoid_subst. iExists (Some (_, _, _, _)).
iMod (own_update_2 with "Hâ— Hâ—¯") as "$".
- { apply auth_update_dealloc. rewrite -(agree_idemp (to_agree _)) -!pair_op Some_op.
+ { apply auth_update_dealloc. rewrite -(agree_idemp (to_agree _)) !pair_op Some_op.
apply (cancel_local_update_unit (writing_stR q _)), _. }
iDestruct "INV" as "(H†& Hq & _)".
rewrite /= (_:Z.neg (1%positive â‹… n') + 1 = Z.neg n');
@@ -321,7 +321,7 @@ Section refmut_functions.
rewrite !shift_loc_assoc. wp_write. do 3 (wp_op; wp_write).
iMod ("Hclosena" with "[Hlrc H◠Hν1 H†] Hna") as "[Hβ Hna]".
{ iExists (Some (_, true, _, _)).
- rewrite -Some_op !pair_op agree_idemp /= (comm _ xH _).
+ 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. }
iMod ("Hβclose" with "Hβ") as "Hα". iMod ("Hclose1" with "Hα HL") as "HL".
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 4305c315..06fc0cbb 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -73,7 +73,7 @@ Section rwlock_inv.
iMod (own_update with "g") as "$"; [|done]. apply auth_update_alloc.
rewrite Pos.add_comm Qp_plus_comm -pos_op_plus /=
-{2}(agree_idemp (to_agree _)) -frac_op'
- -2!pair_op -Cinr_op Some_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.
@@ -146,7 +146,7 @@ Section rwlock_inv.
iMod (own_update with "mr") as "$"; [|done].
apply auth_update_dealloc.
rewrite -frac_op' -pos_op_plus /= (cmra_comm_L q)
- -{1}(agree_idemp (to_agree _)) -2!pair_op -Cinr_op Some_op.
+ -{1}(agree_idemp (to_agree _)) 2!pair_op Cinr_op Some_op.
by apply (cancel_local_update_unit (Some _)), _.
Qed.
--
GitLab