From e5c1de86f633eae2c742ad2809c358a9fa4fec30 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 16 Aug 2024 10:58:39 +0200
Subject: [PATCH] Bump std++ (length_X).
---
coq-iris-examples.opam | 2 +-
theories/lecture_notes/lists.v | 4 ++--
theories/locks/array_based_queuing_lock/abql.v | 16 ++++++++--------
theories/logatom/herlihy_wing_queue/hwq.v | 2 +-
.../F_mu_ref_conc/binary/context_refinement.v | 4 ++--
theories/logrel/F_mu_ref_conc/binary/logrel.v | 2 +-
theories/logrel/F_mu_ref_conc/binary/rules.v | 6 +++---
theories/logrel/F_mu_ref_conc/typing.v | 4 ++--
theories/logrel/F_mu_ref_conc/unary/logrel.v | 2 +-
9 files changed, 21 insertions(+), 21 deletions(-)
diff --git a/coq-iris-examples.opam b/coq-iris-examples.opam
index 867b3cca..a214a10e 100644
--- a/coq-iris-examples.opam
+++ b/coq-iris-examples.opam
@@ -8,7 +8,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/examples.git"
synopsis: "A collection of case studies for Iris -- not meant to be used as a dependency of anything"
depends: [
- "coq-iris-heap-lang" { (= "dev.2024-06-19.1.3818b339") | (= "dev") }
+ "coq-iris-heap-lang" { (= "dev.2024-08-16.3.8890e30a") | (= "dev") }
"coq-autosubst" { = "dev" }
]
diff --git a/theories/lecture_notes/lists.v b/theories/lecture_notes/lists.v
index 6e12ae8b..d9342667 100644
--- a/theories/lecture_notes/lists.v
+++ b/theories/lecture_notes/lists.v
@@ -479,12 +479,12 @@ Proof.
iAssert (⌜ys = (List.map (λ n : Z, #n) (List.map Z.succ xs))âŒ)%I with "[-H_isList]" as %->.
{ iInduction ys as [| y ys'] "IH" forall (xs); iDestruct "H_length" as %H.
- simpl. destruct xs; first by simpl. inversion H.
- - rewrite fmap_length in H. symmetry in H. simpl in H.
+ - rewrite length_fmap in H. symmetry in H. simpl in H.
destruct (about_length _ _ H) as (x & xs' & ->). simpl.
iDestruct "H_post" as "(H_head & H_tail)".
iDestruct "H_head" as (n') "(% & %)". iSimplifyEq.
iDestruct ("IH" with "H_tail []") as %->.
- { by rewrite fmap_length. }
+ { by rewrite length_fmap. }
done.
}
iFrame.
diff --git a/theories/locks/array_based_queuing_lock/abql.v b/theories/locks/array_based_queuing_lock/abql.v
index 95ddb4be..c679444a 100644
--- a/theories/locks/array_based_queuing_lock/abql.v
+++ b/theories/locks/array_based_queuing_lock/abql.v
@@ -196,7 +196,7 @@ Section array_model.
iIntros (Ï•) "[% isArr] Post".
unfold is_array.
iApply (wp_store_offset with "isArr").
- { apply lookup_lt_is_Some_2. by rewrite fmap_length. }
+ { apply lookup_lt_is_Some_2. by rewrite length_fmap. }
rewrite (list_fmap_insert ((λ b : bool, #b) : bool → val) xs i v).
iAssumption.
Qed.
@@ -367,7 +367,7 @@ Section proof.
wp_apply array_repeat; first done.
iIntros (arr) "isArr".
wp_pures.
- wp_apply (array_store with "[$isArr]"); first by rewrite replicate_length.
+ wp_apply (array_store with "[$isArr]"); first by rewrite length_replicate.
iIntros "isArr".
(* We allocate the ghost states for the tickets and value of o. *)
iMod (own_alloc (◠(Excl' 0, GSet ∅) ⋅ ◯ (Excl' 0, GSet ∅))) as (γ) "[Hγ Hγ']".
@@ -381,7 +381,7 @@ Section proof.
iMod (inv_alloc _ _ (lock_inv γ ι κ arr cap p R) with "[-Post Hinvites]").
{ iNext. rewrite /lock_inv. iExists 0, 0, (<[0:=true]> (replicate cap false)).
iFrame. iSplitR.
- - by rewrite insert_length replicate_length.
+ - by rewrite length_insert length_replicate.
- iLeft. iFrame. rewrite Nat.Div0.mod_0_l //. }
wp_pures.
iApply "Post".
@@ -443,7 +443,7 @@ Section proof.
iInv N as (o i xs) "(>%lenEq & >nextPts & isArr & >Inv & Auth & Part)" "Close".
rewrite /is_array rem_mod_eq //.
pose proof (lookup_lt_is_Some_2 ((λ b : bool, #b) <$> xs) ((t `mod` cap))) as [x1 Hsome].
- { subst. rewrite fmap_length. apply Nat.mod_upper_bound. lia. }
+ { subst. rewrite length_fmap. apply Nat.mod_upper_bound. lia. }
wp_apply (wp_load_offset with "isArr"); first apply Hsome.
iIntros "isArr".
apply list_lookup_fmap_inv in Hsome as (x & -> & xsLookup).
@@ -462,7 +462,7 @@ Section proof.
{ iNext. iExists o, i, (list_with_one cap (o `mod` cap)).
rewrite /is_array xsEq. iFrame.
iSplit.
- - by rewrite /list_with_one insert_length replicate_length.
+ - by rewrite /list_with_one length_insert length_replicate.
- iRight. iRight. iFrame. done. }
iModIntro. wp_pures. iApply "Post". by iFrame.
* (* The case where the lock is in the clopen state. In this state all the
@@ -552,7 +552,7 @@ Section proof.
{ iDestruct (right_right_false with "Right Right'") as %[]. }
iMod ("Close" with "[nextPts Invs Auth psPts Issued Right]") as "_".
{ iNext. iExists o, i, (<[(o `mod` cap) := false]> xs).
- rewrite insert_length.
+ rewrite length_insert.
iFrame. iSplit; first done.
iRight. iLeft. iFrame. iPureIntro. subst.
rewrite -> xsEq at 2.
@@ -572,7 +572,7 @@ Section proof.
%[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_both_valid_discrete.
rewrite rem_mod_eq //.
iApply (wp_store_offset with "arrPts").
- { apply lookup_lt_is_Some_2. rewrite fmap_length Hlen. apply Nat.mod_upper_bound. lia. }
+ { apply lookup_lt_is_Some_2. rewrite length_fmap Hlen. apply Nat.mod_upper_bound. lia. }
iModIntro. iIntros "isArr".
(* Combine the left and right we have into a both. *)
iDestruct (left_right_to_both with "Left Right") as "Both".
@@ -586,7 +586,7 @@ Section proof.
{ iNext. iExists (o + 1), (i - 1), (list_with_one cap ((o + 1) `mod` cap)).
assert (o + 1 + (i - 1) = o + i) as -> by lia.
iFrame.
- iSplit. { by rewrite /list_with_one insert_length replicate_length. }
+ iSplit. { by rewrite /list_with_one length_insert length_replicate. }
iSplitL "isArr". { by rewrite /list_with_one /is_array list_fmap_insert xsEq. }
iLeft. iFrame. done. }
iModIntro. iApply "Post". done.
diff --git a/theories/logatom/herlihy_wing_queue/hwq.v b/theories/logatom/herlihy_wing_queue/hwq.v
index 901a7f54..42c2b2f8 100644
--- a/theories/logatom/herlihy_wing_queue/hwq.v
+++ b/theories/logatom/herlihy_wing_queue/hwq.v
@@ -1017,7 +1017,7 @@ Lemma length_array_content sz slots deqs :
length (array_content sz slots deqs) = sz.
Proof.
induction sz as [|sz IH]; first done.
- by rewrite /= app_length Nat.add_comm /= IH.
+ by rewrite /= length_app Nat.add_comm /= IH.
Qed.
Lemma array_content_lookup sz slots deqs i :
diff --git a/theories/logrel/F_mu_ref_conc/binary/context_refinement.v b/theories/logrel/F_mu_ref_conc/binary/context_refinement.v
index d1d67255..b1105143 100644
--- a/theories/logrel/F_mu_ref_conc/binary/context_refinement.v
+++ b/theories/logrel/F_mu_ref_conc/binary/context_refinement.v
@@ -240,14 +240,14 @@ Proof.
intros H1 H2; induction H2; simpl; auto.
rename select (typed_ctx_item _ _ _ _ _) into Hty.
induction Hty => f; asimpl; simpl in *;
- repeat match goal with H : _ |- _ => rewrite fmap_length in H end;
+ repeat match goal with H : _ |- _ => rewrite length_fmap in H end;
try f_equal;
eauto using typed_n_closed;
try match goal with
| H : _ |- _ => by eapply (typed_n_closed _ _ _ H)
| H : _ |- _ => by let H' := fresh in
pose proof (typed_n_closed _ _ _ H) as H';
- rewrite /= fmap_length in H'; eauto
+ rewrite /= length_fmap in H'; eauto
end.
Qed.
diff --git a/theories/logrel/F_mu_ref_conc/binary/logrel.v b/theories/logrel/F_mu_ref_conc/binary/logrel.v
index b17a873f..557e7c19 100644
--- a/theories/logrel/F_mu_ref_conc/binary/logrel.v
+++ b/theories/logrel/F_mu_ref_conc/binary/logrel.v
@@ -225,7 +225,7 @@ Section logrel.
Lemma interp_env_ren Δ (Γ : list type) vvs τi :
⟦ subst (ren (+1)) <$> Γ ⟧* (τi :: Δ) vvs ⊣⊢ ⟦ Γ ⟧* Δ vvs.
Proof.
- apply sep_proper; [apply pure_proper; by rewrite fmap_length|].
+ apply sep_proper; [apply pure_proper; by rewrite length_fmap|].
revert Δ vvs τi; induction Γ=> Δ [|v vs] τi; csimpl; auto.
apply sep_proper; auto. apply (interp_weaken [] [τi] Δ).
Qed.
diff --git a/theories/logrel/F_mu_ref_conc/binary/rules.v b/theories/logrel/F_mu_ref_conc/binary/rules.v
index 6393e76f..0a69f42d 100644
--- a/theories/logrel/F_mu_ref_conc/binary/rules.v
+++ b/theories/logrel/F_mu_ref_conc/binary/rules.v
@@ -112,7 +112,7 @@ Section conversions.
- rewrite lookup_insert_ne; last lia. by rewrite !tpool_lookup lookup_app_l.
- by rewrite lookup_insert tpool_lookup lookup_app_r // Nat.sub_diag.
- rewrite lookup_insert_ne; last lia.
- rewrite !tpool_lookup ?lookup_ge_None_2 ?app_length //=;
+ rewrite !tpool_lookup ?lookup_ge_None_2 ?length_app //=;
change (ofe_car exprO) with expr; lia.
Qed.
@@ -202,7 +202,7 @@ Section cfg.
erased_step (tp, σ) (<[j:=fill K e']> tp ++ efs, σ').
Proof.
intros. rewrite -(take_drop_middle tp j (fill K e)) //.
- rewrite insert_app_r_alt take_length_le ?Nat.sub_diag /=;
+ rewrite insert_app_r_alt length_take_le ?Nat.sub_diag /=;
eauto using lookup_lt_Some, Nat.lt_le_incl.
rewrite -(assoc_L (++)) /=. eexists.
eapply step_atomic; eauto. by apply: Ectx_step'.
@@ -530,7 +530,7 @@ Section cfg.
by rewrite lookup_ge_None_2. }
iExists (length tp). iFrame "Hj Hfork". iApply "Hclose". iNext.
iExists (<[j:=fill K Unit]> tp ++ [e]), σ.
- rewrite to_tpool_snoc insert_length to_tpool_insert //. iFrame. iPureIntro.
+ rewrite to_tpool_snoc length_insert to_tpool_insert //. iFrame. iPureIntro.
eapply rtc_r, step_insert; eauto. econstructor; eauto.
Qed.
End cfg.
diff --git a/theories/logrel/F_mu_ref_conc/typing.v b/theories/logrel/F_mu_ref_conc/typing.v
index abe7e7f5..79914865 100644
--- a/theories/logrel/F_mu_ref_conc/typing.v
+++ b/theories/logrel/F_mu_ref_conc/typing.v
@@ -113,8 +113,8 @@ Proof.
- rename select (_ !! _ = Some _) into H.
apply lookup_lt_Some in H. rewrite iter_up. destruct lt_dec; auto with lia.
- f_equal. eauto.
- - f_equal. rewrite ->fmap_length in *. done.
- - rewrite ->fmap_length in *; by f_equal.
+ - f_equal. rewrite ->length_fmap in *. done.
+ - rewrite ->length_fmap in *; by f_equal.
Qed.
(** Weakening *)
diff --git a/theories/logrel/F_mu_ref_conc/unary/logrel.v b/theories/logrel/F_mu_ref_conc/unary/logrel.v
index 95ab074f..4d8d63d8 100644
--- a/theories/logrel/F_mu_ref_conc/unary/logrel.v
+++ b/theories/logrel/F_mu_ref_conc/unary/logrel.v
@@ -187,7 +187,7 @@ Section logrel.
Lemma interp_env_ren Δ (Γ : list type) (vs : list val) τi :
⟦ subst (ren (+1)) <$> Γ ⟧* (τi :: Δ) vs ⊣⊢ ⟦ Γ ⟧* Δ vs.
Proof.
- apply sep_proper; [apply pure_proper; by rewrite fmap_length|].
+ apply sep_proper; [apply pure_proper; by rewrite length_fmap|].
revert Δ vs τi; induction Γ=> Δ [|v vs] τi; csimpl; auto.
apply sep_proper; auto. apply (interp_weaken [] [τi] Δ).
Qed.
--
GitLab