From e06f7eba8f147eb46572ae935f18bcbf35b9de28 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 20 May 2021 19:31:57 +0200
Subject: [PATCH] Use set_solver+ everywhere instead of set_solver-.
---
theories/lifetime/model/creation.v | 4 ++--
theories/lifetime/model/reborrow.v | 2 +-
theories/typing/lib/arc.v | 14 +++++++-------
theories/typing/lib/rc/rc.v | 6 +++---
theories/typing/lib/rc/weak.v | 2 +-
theories/typing/lib/refcell/ref_code.v | 4 ++--
theories/typing/lib/refcell/refcell.v | 4 ++--
theories/typing/lib/refcell/refcell_code.v | 4 ++--
theories/typing/lib/refcell/refmut_code.v | 4 ++--
theories/typing/lib/rwlock/rwlockreadguard_code.v | 4 ++--
theories/typing/programs.v | 2 +-
11 files changed, 25 insertions(+), 25 deletions(-)
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index df1f6d4c..85bbedc6 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -34,7 +34,7 @@ Proof.
iDestruct (own_cnt_valid_2 with "Hcnt' Hcnt")
as %[?%nat_included _]%auth_both_valid_discrete; lia. }
iMod (box_empty with "Hbox") as "[HP Hbox]"=>//.
- { (* FIXME [solve_ndisj] fails *) set_solver-. }
+ { (* FIXME [solve_ndisj] fails *) set_solver+. }
{ intros i s. by rewrite lookup_fmap fmap_Some=> -[? [/HB -> ->]]. }
rewrite lft_vs_unfold; iDestruct "Hvs" as (n) "[Hcnt Hvs]".
iDestruct (big_sepS_filter_acc (.⊂ κ) _ _ (dom _ I) with "Halive")
@@ -42,7 +42,7 @@ Proof.
{ intros κ'. rewrite elem_of_dom. eauto. }
iApply fupd_trans. iApply fupd_mask_mono; last
iMod ("Hvs" $! I with "[HI Halive] HP Hκ") as "(Hinv & HQ & Hcnt')".
- { set_solver-. }
+ { set_solver+. }
{ rewrite lft_vs_inv_unfold. iFrame. }
rewrite lft_vs_inv_unfold; iDestruct "Hinv" as "(HI&Halive)".
iSpecialize ("Halive'" with "Halive").
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index 27ee3e79..f8502152 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -82,7 +82,7 @@ Proof.
rewrite /to_borUR lookup_fmap. by rewrite HB. }
iMod (slice_fill _ _ false with "Hislice HP Hbox")
as "Hbox".
- { set_solver-. }
+ { set_solver+. }
{ by rewrite lookup_fmap HB. }
iDestruct (@big_sepM_delete with "HB") as "[Hcnt HB]"; first done.
rewrite /=. iDestruct "Hcnt" as "[% H1â—¯]".
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index 238dd508..c85c868c 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -92,7 +92,7 @@ Section arc.
iMod ("Hν†" with "Hν") as "H". iModIntro. iNext. iApply fupd_trans.
iMod "H" as "#Hν".
iMod fupd_mask_subseteq as "Hclose2"; last iMod ("Hvs" with "Hν") as "$".
- { set_solver-. }
+ { set_solver+. }
iIntros "{$Hν} !>".
iMod "Hclose2" as "_". iApply "Hclose". auto.
Qed.
@@ -397,7 +397,7 @@ Section arc.
(* All right, we are done preparing our context. Let's get going. *)
iMod (lft_create with "LFT") as (ν) "[Hν Hν†]"; first done.
wp_bind (_ +ₗ _)%E. iSpecialize ("Hν†" with "Hν").
- iApply wp_mask_mono; last iApply (wp_step_fupd with "Hν†"); [set_solver-..|].
+ iApply wp_mask_mono; last iApply (wp_step_fupd with "Hν†"); [set_solver+..|].
wp_op. iIntros "#H†!>". rewrite shift_loc_0. wp_write. wp_op. wp_write. wp_write.
iApply (type_type _ _ _ [ #lrc â— box (weak ty)]
with "[] LFT HE Hna HL Hk [>-]"); last first.
@@ -771,7 +771,7 @@ Section arc.
iDestruct "Hpersist" as "(? & ? & H†)". wp_bind (_ <- _)%E.
iDestruct "Hdrop" as "[Hν Hdrop]". iSpecialize ("H†" with "Hν").
iApply wp_mask_mono; last iApply (wp_step_fupd with "H†"); first done.
- { set_solver-. (* FIXME [solve_ndisj] fails *) }
+ { set_solver+. (* FIXME [solve_ndisj] fails *) }
iDestruct "Hown" as (???) "(_ & Hlen & _)". wp_write. iIntros "(#Hν & Hown & H†)!>".
wp_seq. wp_op. wp_op. iDestruct "Hown" as (?) "[H↦ Hown]".
iDestruct (ty_size_eq with "Hown") as %?. rewrite Max.max_0_r.
@@ -875,7 +875,7 @@ Section arc.
iDestruct "Hpersist" as "(Ha & _ & H†)". wp_bind (_ <- _)%E.
iSpecialize ("H†" with "Hν").
iApply wp_mask_mono; last iApply (wp_step_fupd with "H†"); first done.
- { (* FIXME [solve_ndisj] fails *) set_solver-. }
+ { (* FIXME [solve_ndisj] fails *) set_solver+. }
wp_write. iIntros "(#Hν & Hown & H†) !>". wp_seq. wp_op. wp_op.
rewrite -(firstn_skipn ty.(ty_size) vl0) heap_mapsto_vec_app.
iDestruct "Hr1" as "[Hr1 Hr2]". iDestruct "Hown" as (vl) "[Hrc' Hown]".
@@ -950,7 +950,7 @@ Section arc.
wp_apply (is_unique_spec with "Hi Htoks"). iIntros ([]) "H"; wp_if.
- iDestruct "H" as "(Hrc & Hrc1 & Hν)". iSpecialize ("Hc" with "Hν"). wp_bind Skip.
iApply wp_mask_mono; last iApply (wp_step_fupd with "Hc"); first done.
- { (* FIXME [solve_ndisj] fails *) set_solver-. }
+ { (* FIXME [solve_ndisj] fails *) set_solver+. }
wp_seq. iIntros "(#Hν & Hown & H†) !>". wp_seq.
iMod ("Hclose2" with "[Hrc Hrc1 H†] Hown") as "[Hb Hα]".
{ iIntros "!> Hown !>". iLeft. iFrame. }
@@ -1036,7 +1036,7 @@ Section arc.
- iIntros "(Hrc0 & Hrc1 & HP1)". wp_case. wp_bind (_ +â‚— _)%E.
iSpecialize ("Hc" with "HP1").
iApply wp_mask_mono; last iApply (wp_step_fupd with "Hc"); first done.
- { (* FIXME [solve_ndisj] fails *) set_solver-. }
+ { (* FIXME [solve_ndisj] fails *) set_solver+. }
wp_op. iIntros "(#Hν & Hrc2 & H†)". iModIntro.
iMod ("Hclose2" with "[Hrc'↦ Hrc0 Hrc1 H†] Hrc2") as "[Hb Hα1]".
{ iIntros "!> Hrc2". iExists [_]. rewrite heap_mapsto_vec_singleton.
@@ -1052,7 +1052,7 @@ Section arc.
iApply type_jump; solve_typing.
- iIntros "[Hν Hweak]". wp_case. iSpecialize ("Hc" with "Hν"). wp_bind (new _).
iApply wp_mask_mono; last iApply (wp_step_fupd with "Hc"); first done.
- { (* FIXME [solve_ndisj] fails *) set_solver-. }
+ { (* FIXME [solve_ndisj] fails *) set_solver+. }
wp_apply wp_new=>//. lia. iIntros (l) "(H†& Hlvl) (#Hν & Hown & H†') !>".
rewrite -!lock Nat2Z.id.
wp_let. wp_op. rewrite !heap_mapsto_vec_cons shift_loc_assoc shift_loc_0.
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 10251242..e2ed4647 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -299,7 +299,7 @@ Section code.
last iMod ("Hνend" with "[$Hν $Hν1]") as "H†"; try done.
iModIntro. iNext. iMod "H†".
iMod fupd_mask_subseteq as "Hclose2"; last iMod ("Hν†" with "H†") as "Hty".
- { set_solver-. }
+ { set_solver+. }
iMod "Hclose2" as "_". iModIntro.
iMod ("Hclose" with "[Hst $Hna]") as "$"; first by iExists _; iFrame.
iModIntro. iNext. iDestruct "Hty" as (vl) "[??]". iExists _. iFrame.
@@ -314,7 +314,7 @@ Section code.
last iMod ("Hνend" with "[$Hν $Hν1]") as "H†"; try done.
iModIntro. iNext. iMod "H†".
iMod fupd_mask_subseteq as "Hclose2"; last iMod ("Hν†" with "H†") as "Hty".
- { set_solver-. }
+ { set_solver+. }
iMod "Hclose2" as "_". iModIntro.
iMod (own_update_2 with "Hst Htok") as "Hst".
{ apply auth_update_dealloc, prod_local_update_1,
@@ -335,7 +335,7 @@ Section code.
last iMod ("Hνend" with "[$Hν $Hν1]") as "H†"; try done.
iModIntro. iNext. iMod "H†".
iMod fupd_mask_subseteq as "Hclose2"; last iMod ("Hν†" with "H†") as "Hty".
- { set_solver-. }
+ { set_solver+. }
iMod "Hclose2" as "_". iModIntro.
iMod ("Hclose" with "[Hst $Hna Hl1 Hl2]") as "$";
first by iExists _; iFrame; iFrame.
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index 5f2f3df2..dfea77e5 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -463,7 +463,7 @@ Section code.
wp_op. rewrite shift_loc_0. wp_write. wp_op. wp_write.
iMod (lft_create with "LFT") as (ν) "[Hν #Hν†]"; first done.
iPoseProof ("Hν†" with "Hν") as "H†". wp_bind (_ <- _)%E.
- iApply wp_mask_mono; last iApply (wp_step_fupd with "H†"); [set_solver-..|].
+ iApply wp_mask_mono; last iApply (wp_step_fupd with "H†"); [set_solver+..|].
wp_write. iIntros "#Hν !>". wp_seq.
iApply (type_type _ _ _ [ #lw â— box (weak ty)]
with "[] LFT HE Hna HL Hk [> -]"); last first.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 9e16fc4f..a77c45b8 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -179,10 +179,10 @@ Section ref_functions.
{ apply auth_update_dealloc.
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.
+ iApply step_fupd_intro; first set_solver+. iExists (q+q'')%Qp. iFrame.
by rewrite assoc (comm _ q0 q). }
wp_bind Endlft. iApply (wp_mask_mono _ (↑lftN ∪ lft_userE)); first done.
- iApply (wp_step_fupd with "INV"); [set_solver-..|]. wp_seq.
+ iApply (wp_step_fupd with "INV"); [set_solver+..|]. wp_seq.
iIntros "INV !>". wp_seq. iMod ("Hcloseβ" with "[$INV] Hna") as "[Hβ Hna]".
iMod ("Hcloseα" with "Hβ") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
iApply (type_type _ _ _ [ #lx â— box (uninit 2)] with "[] LFT HE Hna HL Hk");
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index 3cb95d6b..72219bfa 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -151,11 +151,11 @@ Section refcell.
iExists γ, _. iFrame "Hst Hn Hshr".
iSplitR "Htok2"; last by iExists _; iFrame; rewrite Qp_div_2.
iIntros "!> !> Hν". iMod ("Hhν" with "Hν") as "Hν". iModIntro. iNext. iMod "Hν".
- iApply fupd_mask_mono; last iApply "Hh". set_solver-. rewrite -lft_dead_or. auto.
+ iApply fupd_mask_mono; last iApply "Hh". set_solver+. rewrite -lft_dead_or. auto.
- iMod (own_alloc (◠(refcell_st_to_R $ Some (static, true, (1/2)%Qp, n)))) as (γ) "Hst".
{ by apply auth_auth_valid. }
iFrame "Htok'". iExists γ, _. iFrame. iSplitR.
- { rewrite -step_fupd_intro. auto. set_solver-. }
+ { rewrite -step_fupd_intro. auto. set_solver+. }
iSplitR; [|done]. iExists (1/2)%Qp. rewrite Qp_div_2. iSplitR; [done|].
iApply lft_tok_static.
Qed.
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index f2f279ec..17320a49 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -204,7 +204,7 @@ Section refcell_functions.
+ iIntros "!> Hν". iMod ("Hhν" with "Hν") as "Hν". iModIntro.
iNext. iMod "Hν".
iMod fupd_mask_subseteq as "Hclose"; last iMod ("Hh" with "[Hν]") as "$".
- { set_solver-. }
+ { set_solver+. }
* rewrite -lft_dead_or. auto.
* done.
+ iExists _. iFrame. by rewrite Qp_div_2. }
@@ -284,7 +284,7 @@ Section refcell_functions.
{ iExists _. iFrame. iNext. iSplitL "Hbh".
- iIntros "Hν". iMod ("Hhν" with "Hν") as "Hν". iModIntro. iNext. iMod "Hν".
iMod fupd_mask_subseteq as "Hclose"; last iMod ("Hbh" with "[Hν]") as "$".
- { set_solver-. }
+ { set_solver+. }
* rewrite -lft_dead_or. auto.
* done.
- iSplitL; [|done]. iExists _. iFrame. by rewrite Qp_div_2. }
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index 4b1c9d04..4dc1d3bd 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -149,11 +149,11 @@ Section refmut_functions.
iDestruct "INV" as "(H†& Hq & _)".
rewrite /= (_:Z.neg (1%positive â‹… n') + 1 = Z.neg n');
last (rewrite pos_op_plus; lia). iFrame.
- iApply step_fupd_intro; [set_solver-|]. iSplitL; [|done].
+ iApply step_fupd_intro; [set_solver+|]. iSplitL; [|done].
iDestruct "Hq" as (q' ?) "?". iExists (q+q')%Qp. iFrame.
rewrite assoc (comm _ q'' q) //. }
wp_bind Endlft. iApply (wp_mask_mono _ (↑lftN ∪ lft_userE)); first done.
- iApply (wp_step_fupd with "INV"); [set_solver-|]. wp_seq. iIntros "{Hb} Hb !>".
+ iApply (wp_step_fupd with "INV"); [set_solver+|]. wp_seq. iIntros "{Hb} Hb !>".
iMod ("Hcloseβ" with "Hb Hna") as "[Hβ Hna]".
iMod ("Hcloseα" with "Hβ") as "Hα". iMod ("Hclose" with "Hα HL") as "HL". wp_seq.
iApply (type_type _ _ _ [ #lx â— box (uninit 2)]
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index f1d4d70e..e5ac1c55 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -96,14 +96,14 @@ Section rwlockreadguard_functions.
iCombine "Hν" "Hν'" as "Hν". iDestruct "Hq" as %->.
iApply (step_fupd_mask_mono ((↑lftN ∪ lft_userE) ∪ (⊤ ∖ ↑rwlockN ∖ ↑lftN ∖ lft_userE)));
last iApply (step_fupd_mask_frame_r _ (lft_userE)).
- { set_solver-. }
+ { set_solver+. }
{ solve_ndisj. }
{ rewrite difference_difference. apply: disjoint_difference_r1. done. }
{ (* FIXME [solve_ndisj] fails. *)
apply: disjoint_difference_r1. done. }
iMod ("H†" with "Hν") as "H†". iModIntro. iNext. iMod "H†".
iMod fupd_mask_subseteq as "Hclose"; last iMod ("Hh" with "H†") as "Hb".
- { set_solver-. }
+ { set_solver+. }
iMod "Hclose" as "_". iIntros "!> Hlx". iExists None. iFrame.
iApply (own_update_2 with "Hâ— Hâ—¯"). apply auth_update_dealloc.
rewrite -(right_id None op (Some _)). apply cancel_local_update_unit, _.
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 4eba7c32..d3e564c7 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -220,7 +220,7 @@ Section typing_rules.
iDestruct "Hκ" as (Λ) "(% & Htok & Hend)".
iSpecialize ("Hend" with "Htok"). wp_bind Endlft.
iApply (wp_mask_mono _ (↑lftN ∪ lft_userE)); first done.
- iApply (wp_step_fupd with "Hend"); first set_solver-. wp_seq.
+ iApply (wp_step_fupd with "Hend"); first set_solver+. wp_seq.
iIntros "#Hdead !>". wp_seq. iApply ("He" with "LFT HE Htl HL HC [> -]").
iApply (Hub with "[] HT"). simpl in *. subst κ. rewrite -lft_dead_or. auto.
Qed.
--
GitLab