From 73f69784d9b39ab1857cbddd06a04ebc7c9147c2 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 12 Aug 2022 22:19:23 +0200
Subject: [PATCH] Bump Iris.
---
coq-lambda-rust.opam | 2 +-
theories/lang/lib/arc.v | 12 ++++++------
theories/lifetime/frac_borrow.v | 10 +++++-----
theories/lifetime/model/primitive.v | 2 +-
theories/typing/function.v | 8 ++++----
theories/typing/lft_contexts.v | 18 +++++++++---------
theories/typing/lib/arc.v | 2 +-
theories/typing/lib/rc/rc.v | 10 +++++-----
theories/typing/lib/rc/weak.v | 4 ++--
theories/typing/lib/refcell/ref.v | 2 +-
theories/typing/lib/refcell/ref_code.v | 8 ++++----
theories/typing/lib/refcell/refcell.v | 4 ++--
theories/typing/lib/refcell/refcell_code.v | 8 ++++----
theories/typing/lib/refcell/refmut.v | 2 +-
theories/typing/lib/refcell/refmut_code.v | 6 +++---
theories/typing/lib/rwlock/rwlock.v | 2 +-
theories/typing/lib/rwlock/rwlock_code.v | 6 +++---
theories/typing/lib/rwlock/rwlockreadguard.v | 2 +-
theories/typing/own.v | 4 ++--
theories/typing/product.v | 2 +-
theories/typing/programs.v | 4 ++--
theories/typing/sum.v | 2 +-
theories/typing/type.v | 2 +-
theories/typing/uninit.v | 4 ++--
24 files changed, 63 insertions(+), 63 deletions(-)
diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index d6eb8d55..3a3a6d7b 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -13,7 +13,7 @@ the type system, and safety proof for some Rust libraries.
"""
depends: [
- "coq-iris" { (= "dev.2022-08-11.5.b6b4b694") | (= "dev") }
+ "coq-iris" { (= "dev.2022-08-12.4.9245c4c0") | (= "dev") }
]
build: [make "-j%{jobs}%"]
diff --git a/theories/lang/lib/arc.v b/theories/lang/lib/arc.v
index 63d8295c..264a45ae 100644
--- a/theories/lang/lib/arc.v
+++ b/theories/lang/lib/arc.v
@@ -190,7 +190,7 @@ Section arc.
â—¯ (Some $ Cinl ((1/2)%Qp, xH, None), O))))
as (γ) "[H◠H◯]"; first by apply auth_both_valid_discrete.
iExists _, _. iFrame. iApply inv_alloc. iExists _. iFrame. iExists _. iFrame.
- rewrite Qp_div_2. auto.
+ rewrite Qp.div_2. auto.
Qed.
Lemma create_weak E l :
@@ -213,7 +213,7 @@ Section arc.
destruct st, Hincl as [[=]|(?&?&[= <-]&?&[Hincl|Hincl%csum_included])];
simpl in *; subst.
- setoid_subst. iExists _, _, _, _. by iSplit.
- - destruct Hincl as [->|[(?&[[??]?]&[=<-]&->&[[[??]%frac_included%Qp_lt_sum
+ - destruct Hincl as [->|[(?&[[??]?]&[=<-]&->&[[[??]%frac_included%Qp.lt_sum
?%pos_included]%prod_included _]%prod_included)|(?&?&[=]&?)]]; first done.
iExists _, _, _, _. iSplit=>//. simpl in *. destruct decide; [subst;lia|eauto].
Qed.
@@ -275,11 +275,11 @@ Section arc.
(op_local_update_discrete _ _ (Some (Cinl ((qq/2)%Qp, 1%positive, None))))
=>-[/= Hqa ?]. split;[split|]=>//=; last by rewrite left_id.
apply frac_valid. rewrite -Hq comm_L.
- by apply Qp_add_le_mono_l, Qp_div_le. }
+ by apply Qp.add_le_mono_l, Qp.div_le. }
iMod ("Hclose2" with "Hown") as "HP". iModIntro.
iMod ("Hclose1" with "[Hl Hw Hâ— HP1']") as "_".
{ iExists _. iFrame. iExists _. rewrite /= [xH â‹… _]comm_L. iFrame.
- rewrite [(qq / 2)%Qp â‹… _]comm frac_op -[(_ + _)%Qp]assoc Qp_div_2 left_id_L. auto. }
+ rewrite [(qq / 2)%Qp â‹… _]comm frac_op -[(_ + _)%Qp]assoc Qp.div_2 left_id_L. auto. }
iModIntro. wp_case. iApply "HΦ". iFrame.
- wp_apply (wp_cas_int_fail with "Hl"); [congruence|]. iIntros "Hl".
iMod ("Hclose2" with "Hown") as "HP". iModIntro.
@@ -406,10 +406,10 @@ Section arc.
apply op_local_update_discrete=>Hv. constructor; last done.
split; last by rewrite /= left_id; apply Hv. split=>[|//].
apply frac_valid. rewrite /= -Heq comm_L.
- by apply Qp_add_le_mono_l, Qp_div_le. }
+ by apply Qp.add_le_mono_l, Qp.div_le. }
iFrame. iApply "Hclose1". iExists _. iFrame. iExists _. iFrame.
rewrite /= [xH â‹… _]comm_L frac_op [(_ + q')%Qp]comm -[(_ + _)%Qp]assoc
- Qp_div_2 left_id_L. auto with iFrame.
+ Qp.div_2 left_id_L. auto with iFrame.
+ iIntros "Hl". iFrame. iApply ("Hclose1" with "[-]"). iExists _. iFrame.
iExists q. iCombine "HP1 HP1'" as "$". auto with iFrame.
- iDestruct "H" as "[>$ ?]". iIntros "!>"; iSplit; first by auto with congruence.
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index 761b3053..f73a58ed 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -76,16 +76,16 @@ Section frac_bor.
iIntros "#Hφ (H & Hown & Hφ1)". iNext.
iDestruct "H" as (qφ) "(Hφqφ & Hown' & [%|Hq])".
{ subst. iCombine "Hown'" "Hown" as "Hown".
- by iDestruct (own_valid with "Hown") as %Hval%Qp_not_add_le_l. }
+ by iDestruct (own_valid with "Hown") as %Hval%Qp.not_add_le_l. }
rewrite /frac_bor_inv. iApply bi.sep_exist_r. iExists (q + qφ)%Qp.
iDestruct "Hq" as (q' Hqφq') "Hq'κ". iCombine "Hown'" "Hown" as "Hown".
iDestruct (own_valid with "Hown") as %Hval. rewrite comm_L. iFrame "Hown".
iCombine "Hφ1 Hφqφ" as "Hφq". iDestruct ("Hφ" with "Hφq") as "$".
- assert (q ≤ q')%Qp as [[r ->]%Qp_lt_sum|<-]%Qp_le_lteq.
- { apply (Qp_add_le_mono_l _ _ qφ). by rewrite Hqφq'. }
+ assert (q ≤ q')%Qp as [[r ->]%Qp.lt_sum|<-]%Qp.le_lteq.
+ { apply (Qp.add_le_mono_l _ _ qφ). by rewrite Hqφq'. }
- iDestruct "Hq'κ" as "[$ Hr]".
iRight. iExists _. iIntros "{$Hr} !%".
- by rewrite (comm_L Qp_add q) -assoc_L.
+ by rewrite (comm_L Qp.add q) -assoc_L.
- iFrame "Hq'κ". iLeft. iPureIntro. rewrite comm_L. done.
Qed.
@@ -96,7 +96,7 @@ Section frac_bor.
Proof.
iIntros "#Hφ [H Hκ']". iNext.
iDestruct "H" as (qφ) "(Hφqφ & Hown & Hq)".
- destruct (Qp_lower_bound qκ' qφ) as (qq & qκ'0 & qφ0 & Hqκ' & Hqφ).
+ destruct (Qp.lower_bound qκ' qφ) as (qq & qκ'0 & qφ0 & Hqκ' & Hqφ).
iApply bi.sep_exist_l. iExists qq.
iApply bi.sep_exist_l. iExists qκ'0.
subst qκ' qφ. rewrite /frac_bor_inv.
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 2635c19a..aa235d8d 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -371,7 +371,7 @@ 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 & -> & ->).
+ 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 b374b1ce..71e32514 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -271,9 +271,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]".
@@ -288,7 +288,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.
@@ -296,7 +296,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 3a1f6275..cd7f2a0a 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) : iProp Σ :=
@@ -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 865d1692..2842650f 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -141,7 +141,7 @@ Section arc.
{ iExists _, _, _. iFrame "Hpersist".
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"); first solve_ndisj. by rewrite Qp_mul_1_r. }
+ { iApply (bor_fracture with "LFT"); first solve_ndisj. by rewrite Qp.mul_1_r. }
iApply (bor_share with "Hrc"); solve_ndisj. }
iApply ("Hclose1" with "[]"). by auto.
- iMod ("Hclose1" with "[]") as "_"; first by auto.
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index b9049edc..7806b1cb 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -162,7 +162,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. iExists _.
- iFrame "#∗". rewrite Qp_div_2; auto. }
+ iFrame "#∗". rewrite Qp.div_2; auto. }
iMod (ty_share with "LFT HP Hν1") as "[??]"; first solve_ndisj.
iExists _, _, _. iFrame. iExists ty. iFrame "#". iSplitR; last by auto.
by iApply type_incl_refl. }
@@ -174,7 +174,7 @@ Section rc.
{ iExists _, _, _. iFrame "Hpersist".
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"); first solve_ndisj. by rewrite Qp_mul_1_r. }
+ { iApply (bor_fracture with "LFT"); first solve_ndisj. by rewrite Qp.mul_1_r. }
iApply (bor_na with "Hrc"); solve_ndisj. }
iApply ("Hclose1" with "[]"). by auto.
- iMod ("Hclose1" with "[]") as "_"; first by auto.
@@ -594,12 +594,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 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)]
@@ -1084,7 +1084,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 c40204d5..b2c01660 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -168,12 +168,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 9d707fa6..184daf87 100644
--- a/theories/typing/lib/refcell/ref.v
+++ b/theories/typing/lib/refcell/ref.v
@@ -57,7 +57,7 @@ Section ref.
iMod (bor_persistent with "LFT Hinv Htok") as "[#Hinv $]"; first done.
iMod (bor_sep with "LFT Hb") as "[Hκν Hb]"; first done.
iDestruct (frac_bor_lft_incl with "LFT [> Hκν]") as "#Hκν".
- { iApply bor_fracture; try done. by rewrite Qp_mul_1_r. }
+ { iApply bor_fracture; try done. by rewrite Qp.mul_1_r. }
iMod (bor_na with "Hb") as "#Hb"; first 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 3c1162b3..506c0454 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -74,7 +74,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. }
@@ -83,7 +83,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 _ _ _
@@ -339,7 +339,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.
@@ -351,7 +351,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 f50434c7..e90117a7 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -151,14 +151,14 @@ Section refcell.
iMod (ty_share with "LFT Hvl Htok") as "[Hshr Htok]"; first 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"; first 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; first 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 65c2dfb5..2a6f1f34 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -185,11 +185,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ν]"; first done.
iMod (own_update with "Hownst") as "[Hownst Hreading]"; first by apply
auth_update_alloc, (op_local_update_discrete _ _ (reading_stR (1/2)%Qp ν)).
@@ -207,7 +207,7 @@ Section refcell_functions.
{ set_solver+. }
* rewrite -lft_dead_or. auto.
* 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".
@@ -287,7 +287,7 @@ Section refcell_functions.
{ set_solver+. }
* rewrite -lft_dead_or. auto.
* 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 b67458a4..71d953b1 100644
--- a/theories/typing/lib/refcell/refmut.v
+++ b/theories/typing/lib/refcell/refmut.v
@@ -56,7 +56,7 @@ Section refmut.
iMod (bor_sep with "LFT H") as "[_ H]"; first done.
iMod (bor_sep with "LFT H") as "[H _]"; first done.
iMod (bor_fracture (λ q, (q' * q).[ν])%I with "LFT [H]") as "H"; first done.
- { by rewrite Qp_mul_1_r. }
+ { by rewrite Qp.mul_1_r. }
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 5fd3f1e5..8aba2dc7 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -81,7 +81,7 @@ Section refmut_functions.
iMod (bor_sep with "LFT H") as "[_ H]"; first done.
iMod (bor_sep with "LFT H") as "[H _]"; first done.
iMod (bor_fracture (λ q', (q * q').[ν])%I with "LFT [H]") as "H"; first done.
- { by rewrite Qp_mul_1_r. }
+ { by rewrite Qp.mul_1_r. }
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↦ _]"; first done.
iMod (bor_acc with "LFT H↦ Hα") as "[H↦ Hcloseα]"; first done.
@@ -313,7 +313,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.
@@ -326,7 +326,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 f211296c..f0fc7f51 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -161,7 +161,7 @@ Section rwlock.
iDestruct ("Hclose" with "Htok") as "[$ Htok]".
iExists γ, _. iFrame "Hst Hn". iExists _, _. iIntros "{$Hshr}".
iSplitR; first by auto. iFrame "Htok2". iSplitR; first done.
- rewrite Qp_div_2. iSplitL; last by auto.
+ rewrite Qp.div_2. iSplitL; last by auto.
iIntros "!> !> Hν". iDestruct (lft_tok_dead with "Htok Hν") as "[]".
- iMod (own_alloc (◠writing_st)) as (γ) "Hst". { by apply auth_auth_valid. }
iFrame. iExists _, _. eauto with iFrame.
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index b2f06258..f4aba92a 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -194,11 +194,11 @@ Section rwlock_functions.
split; [split|].
- by rewrite /= Hag 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 _. rewrite Z.add_comm /=. iFrame. iExists _, _.
iFrame "∗#". iSplitR; first by rewrite /= Hag agree_idemp.
- 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 (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]"; first solve_ndisj.
iMod (own_update with "Hownst") as "[Hownst Hreading]"; first by apply
auth_update_alloc, (op_local_update_discrete _ _ (reading_st (1/2)%Qp ν)).
@@ -210,7 +210,7 @@ Section rwlock_functions.
iMod (ty_share with "LFT Hst Htok") as "[#Hshr Htok]"; first solve_ndisj.
iFrame "#". iDestruct ("Hclose" with "Htok") as "[$ Htok2]".
iExists _. iFrame. iExists _, _. iSplitR; first done. iFrame "#∗".
- rewrite Qp_div_2. iSplitL; last done.
+ rewrite Qp.div_2. iSplitL; last done.
iIntros "!> Hν". iApply "Hh". rewrite -lft_dead_or. auto. }
iMod ("Hclose''" with "[$INV]") as "Hβtok1". iModIntro. wp_case.
iMod ("Hclose'" with "[$]") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index 429772c2..063a273b 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 Hinv Htok") as "[#Hinv $]"; first done.
iMod (bor_sep with "LFT Hb") as "[Hκν _]"; first done.
iDestruct (frac_bor_lft_incl with "LFT [> Hκν]") as "#Hκν".
- { iApply bor_fracture; try done. by rewrite Qp_mul_1_r. }
+ { iApply bor_fracture; try done. by rewrite Qp.mul_1_r. }
iExists _. iFrame "#". iApply ty_shr_mono; last done.
iApply lft_intersect_mono; last done. iApply lft_incl_refl.
Qed.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index abf06d11..5f027bee 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -23,7 +23,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 ⊣⊢ †{1}l…(S n).
@@ -40,7 +40,7 @@ Section own.
+ by iIntros "[[]?]".
+ by iIntros "[]".
- rewrite heap_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 55dd12a8..73a1484c 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -117,7 +117,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 abc8515b..ba4af811 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -204,9 +204,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 9038bc5c..7ab3a880 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_op _ 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]".
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 21fa8208..66e82981 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -496,7 +496,7 @@ Section type.
iAssert (â–· ⌜length vl = length vl'âŒ)%I as ">%".
{ iNext. iDestruct (st_size_eq with "Hown") as %->.
iDestruct (st_size_eq with "Hown'") as %->. done. }
- iCombine "Hmt1" "Hmt2" as "Hmt". rewrite heap_mapsto_vec_op // Qp_div_2.
+ iCombine "Hmt1" "Hmt2" as "Hmt". rewrite heap_mapsto_vec_op // Qp.div_2.
iDestruct "Hmt" as "[>% Hmt]". subst. by iApply "Hclose".
Qed.
diff --git a/theories/typing/uninit.v b/theories/typing/uninit.v
index d506d720..c5eb8244 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 :
--
GitLab