From d9cb8f89e83daa7a0385d303171296da5343d8be Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 16 Aug 2024 10:59:43 +0200
Subject: [PATCH] Bump std++ (length_X).
---
coq-reloc.opam | 2 +-
theories/examples/folly_queue/refinement.v | 18 +++++++++---------
theories/examples/symbol.v | 2 +-
theories/logic/spec_ra.v | 2 +-
theories/logic/spec_rules.v | 4 ++--
5 files changed, 14 insertions(+), 14 deletions(-)
diff --git a/coq-reloc.opam b/coq-reloc.opam
index f1cbb1d..303c917 100644
--- a/coq-reloc.opam
+++ b/coq-reloc.opam
@@ -6,7 +6,7 @@ bug-reports: "https://gitlab.mpi-sws.org/dfrumin/reloc/issues"
dev-repo: "git+https://gitlab.mpi-sws.org/dfrumin/reloc.git"
depends: [
- "coq-iris-heap-lang" { (= "dev.2024-02-16.1.06f499e0") | (= "dev") }
+ "coq-iris-heap-lang" { (= "dev.2024-08-16.3.8890e30a") | (= "dev") }
"coq-autosubst" { = "dev" }
]
diff --git a/theories/examples/folly_queue/refinement.v b/theories/examples/folly_queue/refinement.v
index 1f03158..fd8e564 100644
--- a/theories/examples/folly_queue/refinement.v
+++ b/theories/examples/folly_queue/refinement.v
@@ -68,12 +68,12 @@ Section queue_refinement.
list_idx_to_map (xs ++ [x]) = <[length xs := x]>(list_idx_to_map xs).
Proof.
rewrite /list_idx_to_map.
- rewrite app_length /= Nat.add_1_r.
+ rewrite length_app /= Nat.add_1_r.
rewrite seq_S /=.
rewrite zip_with_app /=.
- 2: { by rewrite seq_length. }
+ 2: { by rewrite length_seq. }
rewrite list_to_map_snoc; first done.
- rewrite fst_zip. 2: { rewrite seq_length. done. }
+ rewrite fst_zip. 2: { rewrite length_seq. done. }
intros [i Hl]%elem_of_list_lookup_1.
apply lookup_seq in Hl as Hlm.
simpl in Hlm.
@@ -116,7 +116,7 @@ Section queue_refinement.
rewrite /list_idx_to_map.
rewrite lookup_fmap.
rewrite not_elem_of_list_to_map_1; first done.
- rewrite fst_zip. 2: { rewrite seq_length. done. }
+ rewrite fst_zip. 2: { rewrite length_seq. done. }
rewrite elem_of_list_In.
rewrite in_seq. lia.
Qed.
@@ -139,7 +139,7 @@ Section queue_refinement.
rewrite dom_singleton_L in Hincl.
rewrite dom_make_map in Hincl.
rewrite dom_list_to_map in Hincl.
- rewrite fst_zip in Hincl. 2: { rewrite seq_length. done. }
+ rewrite fst_zip in Hincl. 2: { rewrite length_seq. done. }
rewrite list_to_set_seq in Hincl.
iPureIntro. set_solver.
Qed.
@@ -159,7 +159,7 @@ Section queue_refinement.
rewrite lookup_fmap.
erewrite elem_of_list_to_map_1.
- simpl. reflexivity.
- - rewrite fst_zip. 2: { rewrite seq_length. done. }
+ - rewrite fst_zip. 2: { rewrite length_seq. done. }
apply NoDup_seq.
- apply elem_of_lookup_zip_with.
exists i, i, x.
@@ -729,7 +729,7 @@ Section queue_refinement.
iFrame. simpl.
rewrite big_sepS_empty.
iPureIntro. split; last done. split.
- { rewrite app_length. simpl. lia. }
+ { rewrite length_app. simpl. lia. }
rewrite drop_app_le; last lia.
rewrite Hlisteq. done. }
rel_pures_l.
@@ -782,8 +782,8 @@ Section queue_refinement.
assert (popTicket `max` (pushTicket + 1) = popTicket `max` pushTicket) as -> by lia.
simpl. iFrame.
iPureIntro. split.
- - rewrite app_length. simpl. lia.
- - apply drop_ge. rewrite app_length. simpl. lia. }
+ - rewrite length_app. simpl. lia.
+ - apply drop_ge. rewrite length_app. simpl. lia. }
rel_pures_l.
rel_bind_l (! _)%E.
diff --git a/theories/examples/symbol.v b/theories/examples/symbol.v
index 46b2b06..335ff1c 100644
--- a/theories/examples/symbol.v
+++ b/theories/examples/symbol.v
@@ -273,7 +273,7 @@ Section proof.
rel_store_l_atomic.
iClear "Hls".
iInv sizeN as (m ls) "(Ha & >Hs1 & >Hs2 & >Htbl1 & >Htbl2 & #Hls)" "Hcl".
- iDestruct (gen_heap.pointsto_agree with "Htbl1 Htbl1'") as %->.
+ iDestruct (pointsto_agree with "Htbl1 Htbl1'") as %->.
iCombine "Htbl1 Htbl1'" as "Htbl1".
iModIntro. iExists _. iFrame. iNext. iIntros "[Htbl1 Htbl1']".
repeat rel_pure_l. repeat rel_pure_r. rel_load_r.
diff --git a/theories/logic/spec_ra.v b/theories/logic/spec_ra.v
index 0ead2bd..76f1a81 100644
--- a/theories/logic/spec_ra.v
+++ b/theories/logic/spec_ra.v
@@ -109,7 +109,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.
diff --git a/theories/logic/spec_rules.v b/theories/logic/spec_rules.v
index da703eb..837480f 100644
--- a/theories/logic/spec_rules.v
+++ b/theories/logic/spec_rules.v
@@ -29,7 +29,7 @@ Section rules.
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'.
@@ -359,7 +359,7 @@ Section rules.
by rewrite lookup_ge_None_2. }
iExists (length tp). iFrame "Hj Hfork". iApply "Hclose". iNext.
iExists (<[j:=fill K #()]> 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.
--
GitLab