From b6462587acf6823920f5be3e9f09f167a921435a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 16 Aug 2024 11:00:35 +0200
Subject: [PATCH] Bump std++ (length_X).
---
coq-gpfsl.opam | 2 +-
coq-orc11.opam | 2 +-
gpfsl-examples/algebra/mono_list_list.v | 2 +-
.../exchanger/proof_graph_piggyback.v | 10 +-
.../exchanger/proof_graph_resource.v | 2 +-
gpfsl-examples/exchanger/proof_mp_client.v | 4 +-
.../exchanger/proof_sequential_client.v | 2 +-
gpfsl-examples/graph/graph_extend.v | 16 ++--
gpfsl-examples/history/history.v | 8 +-
gpfsl-examples/list_helper.v | 22 ++---
gpfsl-examples/map_seq.v | 2 +-
gpfsl-examples/queue/proof_hw_graph.v | 50 +++++-----
gpfsl-examples/queue/proof_mp2_graph.v | 2 +-
gpfsl-examples/queue/proof_ms_abs_graph.v | 72 +++++++-------
.../queue/proof_producer_consumer.v | 12 +--
gpfsl-examples/queue/proof_spsc_graph.v | 8 +-
gpfsl-examples/set_helper.v | 4 +-
gpfsl-examples/stack/proof_elim_graph.v | 22 ++---
gpfsl-examples/stack/proof_history_abs.v | 16 ++--
gpfsl-examples/stack/proof_treiber_at.v | 22 ++---
gpfsl-examples/stack/proof_treiber_graph.v | 24 ++---
gpfsl-examples/stack/proof_treiber_history.v | 94 +++++++++----------
gpfsl-examples/stack/spec_history.v | 6 +-
gpfsl/base_logic/na.v | 6 +-
gpfsl/logic/lifting.v | 2 +-
orc11/memory.v | 2 +-
orc11/progress.v | 6 +-
27 files changed, 210 insertions(+), 210 deletions(-)
diff --git a/coq-gpfsl.opam b/coq-gpfsl.opam
index 6ac076f9..6e301ca8 100644
--- a/coq-gpfsl.opam
+++ b/coq-gpfsl.opam
@@ -10,7 +10,7 @@ version: "dev"
synopsis: "A combination of GPS and FSL in the promising semantics WITHOUT promises"
depends: [
- "coq-iris" { (= "dev.2024-07-19.0.426f2d2e") | (= "dev") }
+ "coq-iris" { (= "dev.2024-08-16.3.8890e30a") | (= "dev") }
"coq-orc11" {= version}
]
diff --git a/coq-orc11.opam b/coq-orc11.opam
index 6d9be623..01d20939 100644
--- a/coq-orc11.opam
+++ b/coq-orc11.opam
@@ -10,7 +10,7 @@ version: "dev"
synopsis: "A Coq formalization of the ORC11 semantics for weak memory"
depends: [
- "coq-stdpp" { (= "dev.2024-06-17.2.2bcaf3c5") | (= "dev") }
+ "coq-stdpp" { (= "dev.2024-08-16.0.6190d85d") | (= "dev") }
]
build: ["./make-package" "orc11" "-j%{jobs}%"]
diff --git a/gpfsl-examples/algebra/mono_list_list.v b/gpfsl-examples/algebra/mono_list_list.v
index 9dd054f2..90a2dd4a 100644
--- a/gpfsl-examples/algebra/mono_list_list.v
+++ b/gpfsl-examples/algebra/mono_list_list.v
@@ -113,7 +113,7 @@ Section max_prefix_list_list.
rewrite /to_max_prefix_list_list !fmap_map_seq.
rewrite option_includedN_total=> -[|].
- move=>/lookup_map_seq_None=> -[|]; [lia|].
- rewrite fmap_length /=. move=>/lookup_ge_None_2 => -> /=. by case_match.
+ rewrite length_fmap /=. move=>/lookup_ge_None_2 => -> /=. by case_match.
- move=> [?][?]. rewrite !lookup_map_seq_0.
intros ((? & -> & ->)%list_lookup_fmap_inv & (? & -> & ->)%list_lookup_fmap_inv & ?).
simpl. by apply max_prefix_list.to_max_prefix_list_includedN_aux.
diff --git a/gpfsl-examples/exchanger/proof_graph_piggyback.v b/gpfsl-examples/exchanger/proof_graph_piggyback.v
index d70532fd..b2e57936 100644
--- a/gpfsl-examples/exchanger/proof_graph_piggyback.v
+++ b/gpfsl-examples/exchanger/proof_graph_piggyback.v
@@ -318,7 +318,7 @@ Qed.
Lemma toXChgHist_lookup_None {t0 LVs t} :
toXChgHist t0 LVs !! t = None ↔
(t < t0)%positive ∨ (t0 +p (length LVs) ≤ t)%positive.
-Proof. by rewrite lookup_map_seqP_None fmap_length. Qed.
+Proof. by rewrite lookup_map_seqP_None length_fmap. Qed.
Lemma toXChgHist_lookup_Some_None {t0 LVs t p} :
toXChgHist t0 LVs !! t = Some p →
@@ -331,7 +331,7 @@ Proof.
apply toXChgHist_lookup_Some in EqS as [Letx0 [on [Eqv Eqt]]].
have EqL1 : (1 ≤ length LVs)%nat.
{ clear -Eqt Letx0. apply lookup_lt_Some in Eqt. lia. }
- move : EqL. rewrite fmap_length /pos_add_nat; lia.
+ move : EqL. rewrite length_fmap /pos_add_nat; lia.
Qed.
Lemma toXChgHist_comparable_nullable_loc {LVs t0 t v} (on : option loc) :
@@ -372,7 +372,7 @@ Proof.
exists on'. split; [done|]. by apply (lookup_app_l_Some _ _ _ _ Eq1).
+ apply toXChgHist_lookup_None.
apply toXChgHist_lookup_None in Eqi as [?|Eqi]; [by left|right].
- rewrite app_length /=. move : Eqi.
+ rewrite length_app /=. move : Eqi.
rewrite Nat.add_1_r pos_add_succ_r_2.
rewrite (_: t0 +p length LVs = t); [lia|]. rewrite -Eq /pos_add_nat; lia.
Qed.
@@ -534,7 +534,7 @@ Proof.
have NIne21 : (emx, emi) ∉ G.(com). { move => /gcons_com_included [/=]. lia. }
have Eqe12 : (emi = S emx ∨ emx = S emi) by lia.
have EqEs' : G'.(Es) = (G.(Es) ++ [Emi]) ++ [Emx] by apply (app_assoc _ [_] [_]).
- have Eqemx : emx = length (Es G ++ [Emi]). { rewrite app_length /=. lia. }
+ have Eqemx : emx = length (Es G ++ [Emi]). { rewrite length_app /=. lia. }
constructor; [|split| |split|..].
- (* DView *) rewrite /= (app_assoc _ [_]). clear -LeV11 LeV22 CONDv.
apply graph_insert_event_is_releasing;
@@ -1288,7 +1288,7 @@ Proof.
have EqE'' : E'' = E' ++ [Evmax].
{ by rewrite /E'' /E' /= (app_assoc _ [_] [_]). }
have EqE' : E' = E4 ++ [Evmin]. { done. }
- have Eqxmx : xchgmax = length E'. { rewrite /= app_length /=. clear; lia. }
+ have Eqxmx : xchgmax = length E'. { rewrite /= length_app /=. clear; lia. }
have FRGmx4 : (length E4 ≤ xchgmax)%nat. { clear -LtX12. subst E4. simpl. lia. }
have LeL14 : (length E1 <= length E4)%nat by apply prefix_length, SubG1.
have LeL024 : (length E02 <= length E4)%nat by apply prefix_length, SubG02.
diff --git a/gpfsl-examples/exchanger/proof_graph_resource.v b/gpfsl-examples/exchanger/proof_graph_resource.v
index 67fad133..89b08dd5 100644
--- a/gpfsl-examples/exchanger/proof_graph_resource.v
+++ b/gpfsl-examples/exchanger/proof_graph_resource.v
@@ -159,7 +159,7 @@ Proof.
{ rewrite Eqe1. clear. intros ?%elem_of_set_seq. lia. }
(* update our ghost state *)
iMod (GsetDisjAuth_insert _ _ e1 with "GA") as "[GA Tok1]"; [done|].
- have EqL : length G'.(Es) = S (length G.(Es)). { rewrite EqG' app_length /=. lia. }
+ have EqL : length G'.(Es) = S (length G.(Es)). { rewrite EqG' length_app /=. lia. }
iIntros "!>". iRight.
iExists V', G', e1, e2. iExists v2, Ve1, Ve2, M'. iFrame "I sV'".
(* case distinction *)
diff --git a/gpfsl-examples/exchanger/proof_mp_client.v b/gpfsl-examples/exchanger/proof_mp_client.v
index 726ee011..504f12e2 100644
--- a/gpfsl-examples/exchanger/proof_mp_client.v
+++ b/gpfsl-examples/exchanger/proof_mp_client.v
@@ -101,7 +101,7 @@ Section ex.
iIntros (V1 G1 xchg1 xchg2 v2 Vx1 Vx2 M1) "(EI & #sV1 & %F & CASE)".
destruct F as (SubG' & _ & _ & _ & EqX1 & EqEs & _).
have EqL : length G1.(Es) = S (length G'.(Es)).
- { rewrite EqEs app_length /=. lia. }
+ { rewrite EqEs length_app /=. lia. }
have EqLX1 : G1.(Es) !! xchg1 = Some (mkGraphEvent (Exchange 1 v2) Vx1 M1).
{ by rewrite EqEs EqX1 lookup_app_1_eq. }
@@ -150,7 +150,7 @@ Section ex.
{ apply (excl_auth_update _ _ true). }
have EqL : length G1.(Es) = S (length G'.(Es)).
- { rewrite EqEs app_length /=. lia. }
+ { rewrite EqEs length_app /=. lia. }
(* Close the client invariant *)
iMod ("Close" with "[EI Tokγ21 Hown1 Hown2 ]") as "_".
diff --git a/gpfsl-examples/exchanger/proof_sequential_client.v b/gpfsl-examples/exchanger/proof_sequential_client.v
index 2742fbe3..f9d8b0d1 100644
--- a/gpfsl-examples/exchanger/proof_sequential_client.v
+++ b/gpfsl-examples/exchanger/proof_sequential_client.v
@@ -103,7 +103,7 @@ Proof.
have LtL1 : (xchg2 < length G1.(Es))%nat.
{ apply (gcons_com_included G1 (xchg1, xchg2)), LeG2. rewrite EqCo2. set_solver-. }
have EqL: length G1.(Es) = S (length G.(Es)).
- { rewrite EqEs1 app_length /=. lia. }
+ { rewrite EqEs1 length_app /=. lia. }
clear -Eqxchg1 NEq2 LtL1 EqL MAX2. lia.
Qed.
End sequential_1.
diff --git a/gpfsl-examples/graph/graph_extend.v b/gpfsl-examples/graph/graph_extend.v
index fbc70291..03959adf 100644
--- a/gpfsl-examples/graph/graph_extend.v
+++ b/gpfsl-examples/graph/graph_extend.v
@@ -44,7 +44,7 @@ Lemma graph_insert_xo_eco E eV :
Proof.
intros EC IN e1 e2 eV2 [Eqe|[-> <-]]%lookup_app_1.
- apply (EC _ _ _ Eqe).
- - intros Lt%IN%lookup_lt_is_Some. rewrite app_length /= in Lt. lia.
+ - intros Lt%IN%lookup_lt_is_Some. rewrite length_app /= in Lt. lia.
Qed.
End graph_insert_props.
@@ -60,10 +60,10 @@ Program Definition graph_insert_event eV G : graph :=
mkGraph (G.(Es) ++ [eV]) G.(com) G.(so) _ _.
Next Obligation.
intros; eapply bool_decide_pack; intros ? []%gcons_com_included;
- rewrite app_length /=; lia. Qed.
+ rewrite length_app /=; lia. Qed.
Next Obligation.
intros; eapply bool_decide_pack; intros ? []%gcons_so_included;
- rewrite app_length /=; lia. Qed.
+ rewrite length_app /=; lia. Qed.
Lemma graph_insert_event_eq eV G :
let G' := graph_insert_event eV G in
@@ -119,12 +119,12 @@ Next Obligation.
intros e1 eV2 G Le1. apply bool_decide_unpack in Le1.
eapply bool_decide_pack;
intros ? [->%elem_of_singleton|[]%gcons_com_included]%elem_of_union;
- rewrite app_length /=; lia. Qed.
+ rewrite length_app /=; lia. Qed.
Next Obligation.
intros e1 eV2 G Le1. apply bool_decide_unpack in Le1.
eapply bool_decide_pack;
intros ? [->%elem_of_singleton|[]%gcons_so_included]%elem_of_union;
- rewrite app_length /=; lia. Qed.
+ rewrite length_app /=; lia. Qed.
Lemma graph_insert_edge_eq (e1 : event_id) eV2 G
(Le1 : bool_decide (e1 < length G.(Es))%nat) :
@@ -206,11 +206,11 @@ Program Definition graph_insert2
_ _.
Next Obligation.
intros; eapply bool_decide_pack => ?;
- rewrite !elem_of_union !elem_of_singleton app_length;
+ rewrite !elem_of_union !elem_of_singleton length_app;
intros [[->| ->]|[]%gcons_com_included]; simpl; lia. Qed.
Next Obligation.
intros; eapply bool_decide_pack => ?;
- rewrite !elem_of_union !elem_of_singleton app_length;
+ rewrite !elem_of_union !elem_of_singleton length_app;
intros [[->| ->]|[]%gcons_so_included]; simpl; lia. Qed.
Lemma graph_insert2_eq eV1 eV2 G :
@@ -255,7 +255,7 @@ Proof.
set eV1' := mkGraphEvent eV1 V1 M'.
set eV2' := mkGraphEvent eV2 V2 M'.
set G' := graph_insert2 eV1' eV2' G.
- have Eqe2 : e2 = length (G.(Es) ++ [eV1']). { rewrite app_length /=; lia. }
+ have Eqe2 : e2 = length (G.(Es) ++ [eV1']). { rewrite length_app /=; lia. }
have SubM' : set_in_bound M' G'.(Es).
{ intros ?. rewrite !elem_of_union !elem_of_singleton /=.
intros [[[-> | ->]|[]%SubM1]|[]%SubM2].
diff --git a/gpfsl-examples/history/history.v b/gpfsl-examples/history/history.v
index c4cb9d24..1295a1f1 100644
--- a/gpfsl-examples/history/history.v
+++ b/gpfsl-examples/history/history.v
@@ -89,17 +89,17 @@ Lemma hb_xo_add E eV
(HB_XO : hb_ord E (seq 0 (length E))) :
hb_ord (E ++ [eV]) (seq 0 (length (E ++ [eV]))).
Proof.
- unfold hb_ord. rewrite app_length seq_app /=.
+ unfold hb_ord. rewrite length_app seq_app /=.
intros i1 i2 e1 e2 eV2 ORD_i1 ORD_i2 EV2 IN_LVIEW.
case (decide (i1 = length (seq 0 (length E)))) as [->|NE1];
[apply lookup_last_Some_2 in ORD_i1 as ->
|rewrite lookup_app_1_ne in ORD_i1; [|done]; apply lookup_lt_Some in ORD_i1 as LT1;
- rewrite seq_length in LT1; rewrite lookup_xo in ORD_i1; [|done]; injection ORD_i1 as ->];
+ rewrite length_seq in LT1; rewrite lookup_xo in ORD_i1; [|done]; injection ORD_i1 as ->];
(case (decide (i2 = length (seq 0 (length E)))) as [->|NE2];
[apply lookup_last_Some_2 in ORD_i2 as ->
|rewrite lookup_app_1_ne in ORD_i2; [|done]; apply lookup_lt_Some in ORD_i2 as LT2;
- rewrite seq_length in LT2; rewrite lookup_xo in ORD_i2; [|done]; injection ORD_i2 as ->]);
- rewrite ->seq_length in * |- *.
+ rewrite length_seq in LT2; rewrite lookup_xo in ORD_i2; [|done]; injection ORD_i2 as ->]);
+ rewrite ->length_seq in * |- *.
- done.
- exfalso. rewrite lookup_app_1_ne in EV2; [|done].
move: (hwf_logview_closed _ WF _ _ EV2 _ IN_LVIEW) => [?].
diff --git a/gpfsl-examples/list_helper.v b/gpfsl-examples/list_helper.v
index 2f5e09ca..531280a3 100644
--- a/gpfsl-examples/list_helper.v
+++ b/gpfsl-examples/list_helper.v
@@ -16,7 +16,7 @@ Proof. intros [ly Eql] Inl. subst l'. apply elem_of_app. by left. Qed.
Lemma prefix_length_eq l l' :
l `prefix_of` l' → length l' ≤ length l → l' = l.
Proof.
- intros [ly ->] LeL. rewrite app_length in LeL. destruct ly.
+ intros [ly ->] LeL. rewrite length_app in LeL. destruct ly.
- by rewrite app_nil_r.
- exfalso. simpl in LeL. lia.
Qed.
@@ -86,7 +86,7 @@ Proof.
intros Eq.
apply elem_of_list_split_length in Eq as (l1 & l2 & Eql & EqL).
subst l.
- move : EqL. rewrite app_length /= -Nat.add_sub_assoc; last lia.
+ move : EqL. rewrite length_app /= -Nat.add_sub_assoc; last lia.
rewrite /= Nat.sub_0_r.
destruct l2; simpl.
- intros _. by exists l1.
@@ -97,7 +97,7 @@ Lemma lookup_last_Some_2 l x y :
(l ++ [y]) !! length l = Some x → x = y.
Proof.
rewrite (_: length l = length (l ++ [y]) - 1); last first.
- { rewrite app_length /=. lia. }
+ { rewrite length_app /=. lia. }
intros [??]%lookup_last_Some. by simplify_list_eq.
Qed.
@@ -127,7 +127,7 @@ Lemma lookup_app_1_ne l e i :
Proof.
case (decide (length l < i)) => [?|NLt] ?.
- rewrite (lookup_ge_None_2 l); [|lia]. apply lookup_ge_None_2.
- rewrite app_length /=. lia.
+ rewrite length_app /=. lia.
- intros. apply lookup_app_l. lia.
Qed.
@@ -148,7 +148,7 @@ Proof.
intros [[]%lookup_app_1|[-> ?]]%lookup_app_1.
- by left.
- by right; left.
- - right; right. rewrite app_length /=. split; [lia|done].
+ - right; right. rewrite length_app /=. split; [lia|done].
Qed.
Lemma lookup_app_2' l y1 y2 i x :
@@ -161,7 +161,7 @@ Proof.
- by apply list_lookup_middle.
- rewrite (app_assoc _ [_] [_]) (_ : S (length l) = length (l ++ [y1])).
+ apply lookup_app_1_eq.
- + rewrite app_length /=. lia.
+ + rewrite length_app /=. lia.
Qed.
Lemma list_equal_tail l1 x l2 y :
@@ -366,7 +366,7 @@ Proof.
rewrite lookup_app_r in Hx; last first. {
simpl.
assert (length (filter P [x]) <= 1); last lia.
- trans (length [x]); auto. apply filter_length.
+ trans (length [x]); auto. apply length_filter.
}
apply elem_of_list_lookup_2, elem_of_list_filter in Hx as [_ Hx].
apply elem_of_seq in Hx; lia.
@@ -524,11 +524,11 @@ Proof.
apply lookup_app_Some in Eqj.
destruct Eqj as [Eqj|[]]; [|done].
apply lookup_lt_Some in Eqj.
- rewrite app_length /= in Eqj. lia.
+ rewrite length_app /= in Eqj. lia.
- exists x', (length l1 + 1)%nat. split.
+ exists l1, l2. by simplify_list_eq.
+ rewrite Eq1. rewrite (app_assoc _ [x]). split.
- * apply list_lookup_middle. by rewrite app_length /=.
+ * apply list_lookup_middle. by rewrite length_app /=.
* subst i. clear -Ltj. lia.
Qed.
@@ -600,7 +600,7 @@ Proof.
exists (length l1). split.
- rewrite (lookup_app_r l1) // Nat.sub_diag //.
- rewrite (_ : l1 ++ [x; x'] ++ l2 = (l1 ++ [x]) ++ ([x'] ++ l2)).
- + have EqL1 : length (l1 ++ [x]) = length l1 + 1 by rewrite app_length /=.
+ + have EqL1 : length (l1 ++ [x]) = length l1 + 1 by rewrite length_app /=.
rewrite lookup_app_r.
* by rewrite EqL1 Nat.sub_diag //.
* by rewrite EqL1.
@@ -633,7 +633,7 @@ Lemma xo_events l : Forall (λ e, is_Some (l !! e)) (seq 0 (length l)).
Proof.
rewrite Forall_lookup => i e H. have H' := H. apply lookup_lt_is_Some_2.
rewrite lookup_xo in H; simplify_eq;
- apply lookup_lt_Some in H'; by rewrite seq_length in H'.
+ apply lookup_lt_Some in H'; by rewrite length_seq in H'.
Qed.
Lemma ord_nodup N ord (PERM : ord ≡ₚ seq 0 N) : NoDup ord.
diff --git a/gpfsl-examples/map_seq.v b/gpfsl-examples/map_seq.v
index e20d7c6e..83bb405d 100644
--- a/gpfsl-examples/map_seq.v
+++ b/gpfsl-examples/map_seq.v
@@ -40,7 +40,7 @@ Proof.
+ apply lookup_map_seq_Some.
apply lookup_map_seq_Some in Eqi' as [Lei' Eqi'].
split; [done|]. rewrite list_lookup_insert_ne; [done|lia].
- + apply lookup_map_seq_None. rewrite insert_length.
+ + apply lookup_map_seq_None. rewrite length_insert.
by apply lookup_map_seq_None in Eqi'.
Qed.
diff --git a/gpfsl-examples/queue/proof_hw_graph.v b/gpfsl-examples/queue/proof_hw_graph.v
index 1781c51b..befe3af5 100644
--- a/gpfsl-examples/queue/proof_hw_graph.v
+++ b/gpfsl-examples/queue/proof_hw_graph.v
@@ -309,7 +309,7 @@ Qed.
Lemma toSlotHist0_lookup_None {t0 LVs t} :
(toSlotHist0 t0 LVs) !! t = None ↔
(t < t0)%positive ∨ (t0 +p (length LVs) ≤ t)%positive.
-Proof. by rewrite lookup_map_seqP_None zip_with_length_r_eq // repeat_length. Qed.
+Proof. by rewrite lookup_map_seqP_None length_zip_with_r_eq // repeat_length. Qed.
Lemma toSlotHist0_lookup_Some_None {t0 LVs t p} :
toSlotHist0 t0 LVs !! t = Some p →
@@ -323,7 +323,7 @@ Proof.
apply toSlotHist0_lookup_Some in EqS as [Letx0 [on [Eqv Eqt]]].
have EqL1 : (1 ≤ length LVs)%nat.
{ clear -Eqt Letx0. apply lookup_lt_Some in Eqt. lia. }
- move : EqL. rewrite zip_with_length_r_eq; [|by rewrite repeat_length].
+ move : EqL. rewrite length_zip_with_r_eq; [|by rewrite repeat_length].
rewrite /pos_add_nat; lia.
Qed.
@@ -337,15 +337,15 @@ Proof.
intros i. case (decide (i = t)) => [->|?].
- rewrite lookup_insert. symmetry.
apply toSlotHist0_lookup_Some. rewrite Eq.
- repeat split; [lia|rewrite app_length /=; lia|apply lookup_app_1_eq].
+ repeat split; [lia|rewrite length_app /=; lia|apply lookup_app_1_eq].
- rewrite lookup_insert_ne; [|done].
destruct (toSlotHist0 t0 LVs !! i) as [[vi Vi]|] eqn:Eqi; rewrite Eqi; symmetry.
+ apply toSlotHist0_lookup_Some in Eqi as (Letn & LtL & -> & Eq1).
apply toSlotHist0_lookup_Some.
- rewrite (lookup_app_l_Some _ _ _ _ Eq1) app_length /=. naive_solver lia.
+ rewrite (lookup_app_l_Some _ _ _ _ Eq1) length_app /=. naive_solver lia.
+ apply toSlotHist0_lookup_None.
apply toSlotHist0_lookup_None in Eqi as [?|Eqi]; [by left|right].
- rewrite app_length /=. move : Eqi.
+ rewrite length_app /=. move : Eqi.
rewrite Nat.add_1_r pos_add_succ_r_2.
rewrite (_: t0 +p length LVs = t); [lia|]. rewrite -Eq /pos_add_nat; lia.
Qed.
@@ -429,17 +429,17 @@ Lemma toSlotHist_insert_0 {s t0 LVs0 t1 LVs1 t V} Vn :
Proof.
destruct s as [| |[[v M] [Ve e]]|[[v M] [Ve e]] Vd]; simpl; intros EqS EqN Let0 NE0.
- exists (LVs0 ++ [Vn]), LVs1, (t1 + 1)%positive. split; [naive_solver|].
- split. { rewrite app_length /= Nat.add_1_r pos_add_succ_r_2. lia. }
+ split. { rewrite length_app /= Nat.add_1_r pos_add_succ_r_2. lia. }
by apply (toSlotHist0_lookup_Some_None_insert_0 _ EqS EqN).
- exists (LVs0 ++ [Vn]), LVs1, (t1 + 1)%positive. split; [naive_solver|].
- split. { rewrite app_length /= Nat.add_1_r pos_add_succ_r_2. lia. }
+ split. { rewrite length_app /= Nat.add_1_r pos_add_succ_r_2. lia. }
by apply (toSlotHist0_lookup_Some_None_insert_0 _ EqS EqN).
- assert (t ≠t1).
{ intros ->. rewrite lookup_insert in EqS. inversion EqS. subst v; lia. }
rewrite lookup_insert_ne in EqS; [|done].
apply lookup_insert_None in EqN as [EqN ?].
exists (LVs0 ++ [Vn]), LVs1, t1. split; [naive_solver|]. split.
- + rewrite app_length /= Nat.add_1_r pos_add_succ_r_2.
+ + rewrite length_app /= Nat.add_1_r pos_add_succ_r_2.
destruct (toSlotHist0_lookup_Some_None EqS EqN) as [Le1 Le2].
assert ((t0 +p length LVs0) = t + 1)%positive as Eq1.
{ rewrite /pos_add_nat. lia. }
@@ -458,7 +458,7 @@ Proof.
{ intros ->. rewrite lookup_insert in EqS2. inversion EqS2. subst v; lia. }
rewrite lookup_insert_ne in EqS2; [|done].
exists (LVs0 ++ [Vn]), LVs1, t1. split; [naive_solver|]. split.
- + rewrite app_length /= Nat.add_1_r pos_add_succ_r_2.
+ + rewrite length_app /= Nat.add_1_r pos_add_succ_r_2.
destruct (toSlotHist0_lookup_Some_None EqS2 EqN2) as [Le1 Le2].
assert ((t0 +p length LVs0) = t + 1)%positive as Eq1.
{ rewrite /pos_add_nat. lia. }
@@ -501,8 +501,8 @@ Lemma toBackHist_lookup_None {n t0 LVs t} :
toBackHist n t0 LVs !! t = None ↔
(t < t0)%positive ∨ (t0 +p (length LVs) ≤ t)%positive.
Proof.
- intros EqL. rewrite lookup_map_seqP_None zip_with_length_r_eq; [done|].
- by rewrite fmap_length seq_length.
+ intros EqL. rewrite lookup_map_seqP_None length_zip_with_r_eq; [done|].
+ by rewrite length_fmap length_seq.
Qed.
Lemma toBackHist_lookup_Some_None {n t0 LVs t p} :
@@ -513,7 +513,7 @@ Lemma toBackHist_lookup_Some_None {n t0 LVs t p} :
Proof.
intros EqLn EqS EqN.
assert (EqL := lookup_map_seqP_last_idx _ _ _ _ EqS EqN). move : EqL.
- rewrite zip_with_length_r_eq; last by rewrite fmap_length seq_length.
+ rewrite length_zip_with_r_eq; last by rewrite length_fmap length_seq.
by rewrite EqLn /pos_add_nat; lia.
Qed.
@@ -541,9 +541,9 @@ Proof.
+ apply toBackHist_lookup_Some in Eqi as (Letn & -> & ? & Eq3).
apply toBackHist_lookup_Some. do 2 (split; [done|]).
split; [lia|]. by apply (lookup_app_l_Some _ _ _ _ Eq3).
- + apply toBackHist_lookup_None. { rewrite app_length /= Eq2. lia. }
+ + apply toBackHist_lookup_None. { rewrite length_app /= Eq2. lia. }
apply toBackHist_lookup_None in Eqi as [?|Eqi]; [by left|right|done].
- rewrite app_length /=. move : Eqi.
+ rewrite length_app /=. move : Eqi.
rewrite Nat.add_1_r pos_add_succ_r_2 Eq2.
rewrite (_: t0 +p S n = t); [lia|]. rewrite -Eq1 /pos_add_nat. lia.
Qed.
@@ -1612,10 +1612,10 @@ Proof.
iMod ("IH" with "HL") as (γs EqLs) "Hs {IH}".
iMod (AtomicPtsTo_CON_from_na with "Hi") as (γ t0 V0) "(sV & sζ & AT)".
iIntros "!>". iExists (γs ++ [γ]).
- iSplit. { iPureIntro. rewrite app_length /=. lia. }
+ iSplit. { iPureIntro. rewrite length_app /=. lia. }
rewrite fmap_app /= map_seq_snoc big_sepM_insert; last first.
{ apply lookup_map_seq_None. by right. }
- iFrame "Hs". iExists t0, V0. rewrite /= fmap_length EqLs shift_lblock_assoc.
+ iFrame "Hs". iExists t0, V0. rewrite /= length_fmap EqLs shift_lblock_assoc.
by iFrame. }
iDestruct "Hslots" as (γs EqLs) "Hslots".
@@ -1632,7 +1632,7 @@ Proof.
assert (QP: QueueProps (Pos.to_nat sz) 0 L ∅ ∅).
{ split.
- - by rewrite /L fmap_length.
+ - by rewrite /L length_fmap.
- intros i.
rewrite /L -list_lookup_fmap -list_fmap_compose
list_lookup_fmap fmap_Some /= -EqLs -lookup_lt_is_Some.
@@ -1763,7 +1763,7 @@ Proof.
have Eqtb10 : (Pos.to_nat tb1 - Pos.to_nat tb0)%nat = n' by lia.
split; [by f_equal|].
have EqLn : length LVb1 = n'.
- { move : EqLVb1. clear. rewrite app_length /=. lia. }
+ { move : EqLVb1. clear. rewrite length_app /=. lia. }
move : EqVr2. rewrite Eqtb10 -EqLn lookup_app_r // Nat.sub_diag /=.
by inversion 1. }
@@ -1784,9 +1784,9 @@ Proof.
with "[Close1 GM SLM OLs Ob SLb bv]" as ">Tok".
{ rewrite Eqζb2.
have EqLVb1' : length LVb1 = n'.
- { move : EqLVb1. clear. rewrite app_length /= Nat.add_1_r. lia. }
+ { move : EqLVb1. clear. rewrite length_app /= Nat.add_1_r. lia. }
have EqLVb' : length ((LVb1 ++ [Vt1]) ++ [Vw2]) = S (S n').
- { rewrite app_length EqLVb1 /=; clear; lia. }
+ { rewrite length_app EqLVb1 /=; clear; lia. }
have FALVb' : Forall (λ x : view, x ⊑ Vw2) (LVb1 ++ [Vt1]).
{ move : FALVb1. clear -LeVr2. rewrite !Forall_forall.
move => FA V /elem_of_app [/FA|/elem_of_list_singleton -> //].
@@ -1835,7 +1835,7 @@ Proof.
{ rewrite (view_at_objective_iff (SeenPreEnqueued _ _ _ _ _ _)).
rewrite {2}/SeenPreEnqueued big_sepL_app big_sepL_singleton.
iDestruct "SLb" as "#SLb". iFrame "SLb".
- rewrite Nat.add_0_r app_length /= Nat.add_1_r EqLVb1' (Nat.min_l (S n')); [|lia].
+ rewrite Nat.add_0_r length_app /= Nat.add_1_r EqLVb1' (Nat.min_l (S n')); [|lia].
iIntros (i' [Lti'| ->]%(Nat.lt_succ_r i')%Nat.le_lteq).
- rewrite /SeenPreEnqueued big_sepL_app big_sepL_singleton EqLVb1'.
iDestruct "SLb" as "[_ SLb]".
@@ -1858,7 +1858,7 @@ Proof.
iSplitL;[by iFrame "SLb'"|by iPureIntro]. }
(* QueueProps *)
- iPureIntro. split; [by rewrite insert_length|..|done|done].
+ iPureIntro. split; [by rewrite length_insert|..|done|done].
- clear -HUN Ltn' EqL. apply Nat.le_succ_l in Ltn'.
rewrite -EqL Nat.min_l; [|done]. intros i. rewrite /L'.
case (decide (i = n')) => [->|?].
@@ -2004,7 +2004,7 @@ Proof.
apply (lookup_weaken _ _ _ _ Eqt), lookup_map_seqP_Some in Subζn'.
destruct Subζn' as [Letn0 _].
specialize (MAXt3 t (ltac:(by eexists))). lia.
- + move : LP. by rewrite zip_with_length_r_eq // repeat_length.
+ + move : LP. by rewrite length_zip_with_r_eq // repeat_length.
- iSplit; [|by iPureIntro]. rewrite view_at_view_at. by iFrame "SEs". }
assert (NI: ∀ e1 e2, (e1, e2) ∈ G'.(com) → e1 ≠enqId ∧ e2 ≠enqId).
@@ -2067,7 +2067,7 @@ Proof.
have QP' : QueueProps (Pos.to_nat sz) n2 L' T' G'.
{ split.
- - by rewrite insert_length.
+ - by rewrite length_insert.
- clear -Len2 HUN2 Eqn' BEq. intros i.
case (decide (i = n')) => [->|?].
+ rewrite list_lookup_insert //. split; [lia|done].
@@ -2605,7 +2605,7 @@ Proof.
have QP' : QueueProps (Pos.to_nat sz) n2 L' T2 G'.
{ rewrite -EqL2 in Ltidx.
split.
- - by rewrite insert_length.
+ - by rewrite length_insert.
- intros i. case (decide (i = idx)) => [->|?].
+ rewrite list_lookup_insert // /= HUN2 Eqγi /=. clear; naive_solver.
+ by rewrite list_lookup_insert_ne.
diff --git a/gpfsl-examples/queue/proof_mp2_graph.v b/gpfsl-examples/queue/proof_mp2_graph.v
index cabb223a..c407f619 100644
--- a/gpfsl-examples/queue/proof_mp2_graph.v
+++ b/gpfsl-examples/queue/proof_mp2_graph.v
@@ -167,7 +167,7 @@ Proof using All.
iPureIntro. split_and!; [| |done|done|done| |done].
- subst enqId1 enqId2.
have ? : (length (Es G1) < length (Es G1')).
- { rewrite EsG1' app_length /=. lia. }
+ { rewrite EsG1' length_app /=. lia. }
suff ? : (length (Es G1') ≤ length (Es G2))%nat by lia.
apply prefix_length. by destruct SubG1'2.
- eapply prefix_lookup_Some; [done|].
diff --git a/gpfsl-examples/queue/proof_ms_abs_graph.v b/gpfsl-examples/queue/proof_ms_abs_graph.v
index 46ae2bed..03a716c3 100644
--- a/gpfsl-examples/queue/proof_ms_abs_graph.v
+++ b/gpfsl-examples/queue/proof_ms_abs_graph.v
@@ -169,7 +169,7 @@ Qed.
Lemma dequeue_mask_length (lenD lenL : nat) :
length (dequeue_mask lenD lenL) = (lenD + lenL)%nat.
-Proof. by rewrite app_length 2!repeat_length. Qed.
+Proof. by rewrite length_app 2!repeat_length. Qed.
Lemma dequeue_mask_append (lenD lenL : nat) :
dequeue_mask lenD (S lenL) = dequeue_mask lenD lenL ++ [false].
@@ -230,7 +230,7 @@ Proof.
destruct (L !! i); [simpl; naive_solver|done].
- apply Nat.nlt_ge in EqL.
rewrite lookup_app_r; [|done].
- rewrite (lookup_ge_None_2 L); [|by rewrite fmap_length in EqL].
+ rewrite (lookup_ge_None_2 L); [|by rewrite length_fmap in EqL].
split; [|done].
by intros ?%elem_of_list_lookup_2%elem_of_list_singleton.
Qed.
@@ -241,11 +241,11 @@ Proof.
rewrite /next_nodes. destruct L as [|i' L]; [done|].
rewrite /= Nat.sub_0_r. intros Eqi. split; [lia|].
move : (lookup_lt_Some _ _ _ Eqi).
- rewrite app_length /= fmap_length Nat.add_1_r => /Nat.lt_succ_r Lti.
+ rewrite length_app /= length_fmap Nat.add_1_r => /Nat.lt_succ_r Lti.
case (decide (length L ≤ i)%nat) => [Le|/Nat.nle_gt Lt].
- by apply : anti_symm.
- exfalso.
- rewrite lookup_app_l in Eqi; [|by rewrite fmap_length].
+ rewrite lookup_app_l in Eqi; [|by rewrite length_fmap].
move : Eqi. rewrite list_lookup_fmap.
by apply lookup_lt_is_Some_2 in Lt as [? ->].
Qed.
@@ -259,7 +259,7 @@ Proof.
rewrite /next_nodes. destruct L as [|z L]; simpl.
- exists []. by simplify_list_eq.
- exists (Some <$> L ++ [x]). simplify_list_eq.
- by rewrite app_length /= fmap_length Nat.add_1_r.
+ by rewrite length_app /= length_fmap Nat.add_1_r.
Qed.
Lemma infos_next_lookup L (dms : list bool) d i ηs :
@@ -291,15 +291,15 @@ Lemma infos_dequeue ηs s D L η n :
Proof.
intros CL lenD lenL lenD' lenL' infos infos' EqL.
have EqLD' : (lenD' + lenL' = lenD + lenL)%nat.
- { rewrite /lenD' /lenL' /lenD /lenL app_length /=. clear.
+ { rewrite /lenD' /lenL' /lenD /lenL length_app /=. clear.
by rewrite Nat.add_1_r Nat.add_succ_comm. }
have EqLI: length infos = length infos'.
- { rewrite 2!zip_with_length. f_equal. by rewrite 2!dequeue_mask_length. }
+ { rewrite 2!length_zip_with. f_equal. by rewrite 2!dequeue_mask_length. }
have EqL' : length CL = length infos' by rewrite EqL.
have Eqη : CL !! length ((ηs, s) :: D) = Some (η,n).
{ rewrite /CL (lookup_app_r (_::_)); [|done]. by rewrite Nat.sub_diag. }
have LtLCL: (lenD < length CL)%nat.
- { rewrite (app_length (_::_)) /= -Nat.add_succ_r.
+ { rewrite (length_app (_::_)) /= -Nat.add_succ_r.
apply Nat.lt_add_pos_r. lia. }
destruct (lookup_lt_is_Some_2 _ _ LtLCL) as [[η' n'] Eq'].
split. { by eauto. }
@@ -308,14 +308,14 @@ Proof.
destruct (infos_next_lookup _ _ _ _ _ Eq) as (EqNN & DQM & Eqηn').
destruct ηn' as [ηn'|]; last first.
{ apply next_nodes_lookup_None in EqNN as [? EqN].
- exfalso. move : EqN. rewrite /CL (app_length (_::_)) /=. lia. }
+ exfalso. move : EqN. rewrite /CL (length_app (_::_)) /=. lia. }
have ?: ηn' = (η,n).
- { rewrite /lenD cons_length in Eqη. rewrite Nat.add_1_r Eqη in Eqηn'.
+ { rewrite /lenD length_cons in Eqη. rewrite Nat.add_1_r Eqη in Eqηn'.
by inversion Eqηn'. } subst ηn'.
have ?: d = false.
{ by apply (dequeue_mask_lookup_Some_r _ _ _ _ DQM). } subst d.
split; [done|].
- have LtD: (lenD < lenD')%nat. { rewrite /lenD /lenD' app_length /=. lia. }
+ have LtD: (lenD < lenD')%nat. { rewrite /lenD /lenD' length_app /=. lia. }
have DQM' : dequeue_mask lenD' lenL' !! lenD = Some true.
{ destruct (lookup_lt_is_Some_2 (dequeue_mask lenD' lenL') lenD) as [d' Eqd'].
- rewrite dequeue_mask_length. lia.
@@ -333,9 +333,9 @@ Proof.
exists ηs', d'. split; [done|]. split ;[done|].
apply dequeue_mask_lookup_Some'.
apply dequeue_mask_lookup_Some in EqD as [[Lti ?]|[[Lei Lti] ?]].
- - left. split; [|done]. rewrite /lenD' app_length /=. lia.
+ - left. split; [|done]. rewrite /lenD' length_app /=. lia.
- right. split; [|done]. split; [|by rewrite EqLD'].
- rewrite /lenD' app_length /=. lia.
+ rewrite /lenD' length_app /=. lia.
Qed.
@@ -362,7 +362,7 @@ Lemma toHeadHist_lookup_None DL Vs t0 t :
(t < t0)%positive ∨ (t0 +p (length DL) ≤ t)%positive.
Proof.
intros EqL.
- by rewrite lookup_map_seqP_None fmap_length zip_with_length_l_eq fmap_length.
+ by rewrite lookup_map_seqP_None length_fmap length_zip_with_l_eq length_fmap.
Qed.
Lemma toHeadHist_lookup_Some_is_comparable_loc t0 DL Vs t v l1 :
@@ -393,11 +393,11 @@ Proof.
rewrite (lookup_app_l_Some _ _ _ _ Eq1) (lookup_app_l_Some _ _ _ _ Eq2) /=.
naive_solver.
+ have ?: length (L ++ [(η, n)]) = length (Vs ++ [V])
- by rewrite !app_length /= EqL.
+ by rewrite !length_app /= EqL.
apply toHeadHist_lookup_None; [done|].
apply toHeadHist_lookup_None in Eqi; [|done].
destruct Eqi as [?|Eqi]; [by left|right].
- rewrite app_length /=. move : Eqi.
+ rewrite length_app /=. move : Eqi.
rewrite Nat.add_1_r pos_add_succ_r_2.
rewrite (_: t0 +p length L = t); [lia|]. rewrite -Eq /pos_add_nat; lia.
Qed.
@@ -962,22 +962,22 @@ Proof.
destruct (next_nodes_app_2 L' (η, n) (η', n')) as (LS' & Eq1' & Eq2' & EqLLS').
rewrite Eq1' Eq2'.
assert (EqLCL: length CL = (lenD + lenL)%nat).
- { by rewrite /CL (app_length (_::_)) /= /lenD /lenL Nat.add_succ_r. }
+ { by rewrite /CL (length_app (_::_)) /= /lenD /lenL Nat.add_succ_r. }
assert (Eqi' : i = (lenD + lenL - 1)%nat).
{ by rewrite Eqi EqLCL. }
assert (∃ Ld, (dequeue_mask lenD lenL) = Ld ++ [d]) as [Ld EqLd].
{ apply lookup_last_Some. rewrite dequeue_mask_length -Eqi'.
clear -Eq. apply lookup_zip_with_Some in Eq as (?&?&?&_&?).
by simplify_eq. }
- rewrite app_length Nat.add_1_r dequeue_mask_append EqLd.
+ rewrite length_app Nat.add_1_r dequeue_mask_append EqLd.
have EqLSd: length LS' = length Ld.
{ have EqL1 : S (length Ld) = (lenD + lenL)%nat.
- { by rewrite -dequeue_mask_length EqLd app_length /= Nat.add_1_r. }
+ { by rewrite -dequeue_mask_length EqLd length_app /= Nat.add_1_r. }
have EqL2 : S (length LS') = length CL.
- { by rewrite EqCL app_length /= Nat.add_1_r EqLLS'. }
+ { by rewrite EqCL length_app /= Nat.add_1_r EqLLS'. }
clear -EqL1 EqL2 EqLCL. move : EqL2. rewrite EqLCL -EqL1. lia. }
rewrite zip_with_app // /= zip_with_app; last first.
- { clear -EqLSd. rewrite 2!app_length /=. lia. }
+ { clear -EqLSd. rewrite 2!length_app /=. lia. }
rewrite zip_with_app // /=.
rewrite big_sepL2_app_same_length; last by right.
rewrite big_sepL2_app_same_length; last by right.
@@ -987,7 +987,7 @@ Proof.
iIntros (j [η1 n1] [η2 n2] Eq1 Eq2) "Link".
iSpecialize ("Link" with "[%]").
{ clear -EqCL Eqi Eq1. intros ?. subst j.
- move : Eqi. rewrite EqCL app_length /= Nat.add_sub => ?. subst i.
+ move : Eqi. rewrite EqCL length_app /= Nat.add_sub => ?. subst i.
apply lookup_lt_Some in Eq1. lia. }
by iApply (Link_map_mono with "Link").
+ simpl. by iFrame "Lη".
@@ -2180,14 +2180,14 @@ Proof.
+ rewrite list_lookup_fmap -(lookup_app_l _ [(η,n)]); [by rewrite Eqi|].
have LTi : (i ≤ length (D2 ++ L2))%nat.
{ apply Nat.lt_succ_r. apply lookup_lt_Some in Eqi.
- rewrite app_length /= in Eqi. by rewrite Nat.add_1_r in Eqi. }
+ rewrite length_app /= in Eqi. by rewrite Nat.add_1_r in Eqi. }
apply Nat.lt_eq_cases in LTi as [|LTi]; [done|]. exfalso.
subst i. rewrite lookup_app_r in Eqi; [|done].
rewrite /= Nat.sub_diag /= in Eqi. by inversion Eqi.
+ rewrite list_lookup_fmap -(lookup_app_l _ [(η,n)]); [by rewrite Eqj|].
have LTj : (j ≤ length (D2 ++ L2))%nat.
{ apply Nat.lt_succ_r. apply lookup_lt_Some in Eqj.
- rewrite app_length /= in Eqj. by rewrite Nat.add_1_r in Eqj. }
+ rewrite length_app /= in Eqj. by rewrite Nat.add_1_r in Eqj. }
apply Nat.lt_eq_cases in LTj as [|LTj]; [done|]. exfalso.
subst j. rewrite lookup_app_r in Eqj; [|done].
rewrite /= Nat.sub_diag /= in Eqj. by inversion Eqj. }
@@ -2226,7 +2226,7 @@ Proof.
([η2' n2] & ? & Eqj)%list_lookup_fmap_inv & Leij).
simplify_eq.
have LTi := lookup_lt_Some _ _ _ Eqi.
- rewrite app_length Nat.add_1_r in LTi.
+ rewrite length_app Nat.add_1_r in LTi.
apply (Nat.lt_succ_r i), Nat.lt_eq_cases in LTi as [LTi|Eqij].
- rewrite lookup_app_l in Eqi; [|done].
have Le1 : (1 ≤ length (D2 ++ L2))%nat.
@@ -2265,14 +2265,14 @@ Proof.
+ rewrite list_lookup_fmap -(lookup_app_l _ [(η,n)]); [by rewrite Eqi|].
have LTi : (i ≤ length (D2 ++ L2))%nat.
{ apply Nat.lt_succ_r. apply lookup_lt_Some in Eqi.
- by rewrite app_length /= Nat.add_1_r in Eqi. }
+ by rewrite length_app /= Nat.add_1_r in Eqi. }
apply Nat.lt_eq_cases in LTi as [|LTi]; [done|]. exfalso.
subst i. rewrite lookup_app_r in Eqi; [|done].
rewrite /= Nat.sub_diag /= in Eqi. by inversion Eqi.
+ rewrite list_lookup_fmap -(lookup_app_l _ [(η,n)]); [by rewrite Eqj|].
have LTj : (j ≤ length (D2 ++ L2))%nat.
{ apply Nat.lt_succ_r. apply lookup_lt_Some in Eqj.
- by rewrite app_length /= Nat.add_1_r in Eqj. }
+ by rewrite length_app /= Nat.add_1_r in Eqj. }
apply Nat.lt_eq_cases in LTj as [|LTj]; [done|]. exfalso.
subst j. rewrite lookup_app_r in Eqj; [|done].
rewrite /= Nat.sub_diag /= in Eqj. by inversion Eqj.
@@ -2313,7 +2313,7 @@ Proof.
intros e1 e2 eV2 [Eq1|[-> <-]]%lookup_app_1.
+ by apply CON7a.
+ move => /= /Sub'. clear. intros Lt%lookup_lt_is_Some.
- rewrite app_length /= in Lt. lia. }
+ rewrite length_app /= in Lt. lia. }
constructor; [..|done|].
- (* 1 *)
intros ??? [Eq1|[-> <-]]%lookup_app_1; [by apply (CON0 _ _ _ Eq1)|].
@@ -2800,7 +2800,7 @@ Proof.
(prefix_lookup_Some _ _ _ _ Eqη2e LeDe). }
have Eqie': (De ++ [(η2, n2)]).*1 !! ie = Some ηe.
{ apply (prefix_lookup_inv _ _ _ _ (prefix_lookup_Some _ _ _ _ Eqie LeDL13)).
- - apply lookup_lt_is_Some. rewrite fmap_app /= app_length fmap_length /=.
+ - apply lookup_lt_is_Some. rewrite fmap_app /= length_app length_fmap /=.
clear -NIN Eqi. lia.
- destruct LeDe as [De' EqDe'].
rewrite EqDe' (fmap_app _ _ L3) (fmap_app _ _ De') -app_assoc. by eexists. }
@@ -2827,7 +2827,7 @@ Proof.
destruct LeCL1 as [L2' EqL2'].
rewrite /CL2 EqL2' /CL1 app_comm_cons lookup_app_l in EqDL2; [done|].
clear -EqieDL1 LtLen. apply lookup_lt_Some in EqieDL1.
- rewrite fmap_length in EqieDL1. etrans; [apply LtLen|exact EqieDL1]. }
+ rewrite length_fmap in EqieDL1. etrans; [apply LtLen|exact EqieDL1]. }
have EqjsDL1' : CL1.*1 !! i = Some η2 by rewrite list_lookup_fmap EqjsDL1.
destruct (lookup_strict_subseq _ _ _ _ _ EqjsDL1' EqieDL1 LtLen)
as (η' & jη' & SSη' & Eqjη' & Lejη').
@@ -3118,7 +3118,7 @@ Proof.
have Eqth34:
(Pos.to_nat th4 - Pos.to_nat th3)%nat = (length ((ηs, s) :: D4) - 1)%nat.
{ set Eq2 := lookup_map_seqP_last_idx' _ _ _ _ EqTH Eqth4'.
- move : Eq2. by rewrite fmap_length zip_with_length_l_eq fmap_length. }
+ move : Eq2. by rewrite length_fmap length_zip_with_l_eq length_fmap. }
have Eqn2 : ((ηs, s) :: D4) !! (length ((ηs, s) :: D4) - 1)%nat = Some (η2, n2).
{ apply toHeadHist_lookup_Some in EqTH as (_ & _ & η'' & l'' & Eq & Eq').
inversion Eq. clear Eq. subst l''.
@@ -3252,10 +3252,10 @@ Proof.
exists (length D2), ((length D2) + i1)%nat. rewrite fmap_app.
have ? : (length D2 <= length D2 + i1)%nat by lia.
split; last split; [..|done].
- - rewrite EqL4 lookup_app_r; [|clear; by rewrite fmap_length].
- by rewrite fmap_length Nat.sub_diag /=.
- - rewrite lookup_app_r; [|by rewrite fmap_length].
- by rewrite fmap_length Nat.add_comm Nat.add_sub. }
+ - rewrite EqL4 lookup_app_r; [|clear; by rewrite length_fmap].
+ by rewrite length_fmap Nat.sub_diag /=.
+ - rewrite lookup_app_r; [|by rewrite length_fmap].
+ by rewrite length_fmap Nat.add_comm Nat.add_sub. }
(* TODO: ORD is implied by MONO *)
assert (LE2 := MONO _ _ _ _ LB Eqη24 Eqη1).
have Eq2 : e1 = enqId. { clear -LE1 LE2. by apply : anti_symm. }
@@ -3435,7 +3435,7 @@ Proof.
have EqL2 := take_app_length D20 ([(η2, n2)] ++ D22).
rewrite EqD2' (_: length D2' = length D20) in EqL1.
- by rewrite EqL1 in EqL2.
- - by rewrite -(fmap_length fst D2') -(fmap_length fst D20) Eq1. }
+ - by rewrite -(length_fmap fst D2') -(length_fmap fst D20) Eq1. }
rewrite -EqD2. iFrame. }
iAssert (@{V'} SeenDequeueds γg γ (D2 ++ [(η2', n2')]))%I with "[GMA LT]" as "#SD'".
diff --git a/gpfsl-examples/queue/proof_producer_consumer.v b/gpfsl-examples/queue/proof_producer_consumer.v
index dee9ddf2..6795330e 100644
--- a/gpfsl-examples/queue/proof_producer_consumer.v
+++ b/gpfsl-examples/queue/proof_producer_consumer.v
@@ -70,9 +70,9 @@ Proof.
rewrite -{1}(take_drop_middle _ _ _ VAL).
rewrite /to_arr fmap_app fmap_cons /=.
rewrite ->own_loc_na_vec_app, own_loc_na_vec_cons.
- rewrite fmap_take take_length.
+ rewrite fmap_take length_take.
apply lookup_lt_Some in VAL as LT.
- have {}LT : (i < length (to_arr vl))%nat by rewrite fmap_length.
+ have {}LT : (i < length (to_arr vl))%nat by rewrite length_fmap.
rewrite (_ : i `min` (length (to_arr vl)) = i)%nat; [done|lia].
Qed.
@@ -133,7 +133,7 @@ Proof using All.
case (decide (i + 1 = n)) as [->|NE].
{ wp_rec. wp_op. rewrite bool_decide_true; [|done]. wp_pures. by iApply "Post". }
iApply ("IH" $! _ _ _ (i + 1) with "[%] [%] P' PA Post").
- { subst es' i. rewrite app_length //=. }
+ { subst es' i. rewrite length_app //=. }
{ lia. }
Qed.
@@ -193,8 +193,8 @@ Proof using All.
iIntros "_". wp_let. wp_op. rewrite bool_decide_true; [|done]. wp_if.
(* write to the array *)
- have LENi : length (take i vl) = i by rewrite take_length; lia.
- have LENi' : length (take (i + 1) vl) = i + 1 by rewrite take_length; lia.
+ have LENi : length (take i vl) = i by rewrite length_take; lia.
+ have LENi' : length (take (i + 1) vl) = i + 1 by rewrite length_take; lia.
have VAL0 : (take i vl ++ replicate (m - i) 0%Z) !! i = Some 0%Z.
{ rewrite lookup_app_r; [|lia]. apply lookup_replicate. lia. }
rewrite ->(array_access ca _ _ _ VAL0).
@@ -218,7 +218,7 @@ Proof using All.
{ wp_rec. wp_op. rewrite bool_decide_true; [|done]. wp_pures.
iApply "Post". rewrite Nat.sub_diag /= app_nil_r. by iFrame "CA". }
iApply ("IH" $! _ _ ds' (i + 1) with "[%] [%] C' CA Post").
- { subst ds' i. rewrite app_length //=. }
+ { subst ds' i. rewrite length_app //=. }
{ lia. }
Qed.
diff --git a/gpfsl-examples/queue/proof_spsc_graph.v b/gpfsl-examples/queue/proof_spsc_graph.v
index bc2de328..829d01d5 100644
--- a/gpfsl-examples/queue/proof_spsc_graph.v
+++ b/gpfsl-examples/queue/proof_spsc_graph.v
@@ -223,7 +223,7 @@ Proof.
iSplitR "â—¯e"; last iSplit; last iSplit; [|done| |done].
{ (* SPSCInv *)
iNext. iExists _. iFrame. iPureIntro. split_and!; [|done|done| |done].
- - subst enqId. rewrite EsG' app_length /= seq_app /=.
+ - subst enqId. rewrite EsG' length_app /= seq_app /=.
rewrite -(assoc app es) (comm app _ (ds ++ xs)).
rewrite (assoc app es). by f_equiv.
- intros i' d'. specialize (MATCH' i' d'). split.
@@ -282,7 +282,7 @@ Proof.
{ (* SPSCInv *)
iNext. iExists (xs ++ [deqId]). iFrame.
iPureIntro. split_and!; [|done|done| | ].
- - subst deqId. rewrite EsG' app_length /= seq_app /=.
+ - subst deqId. rewrite EsG' length_app /= seq_app /=.
rewrite (assoc app ds) (assoc app es). by f_equiv.
- apply (matches_stable _ G' _ _ SubGG' ComG' MATCH).
- constructor. intros ?? [Xi0|[-> <-]]%lookup_app_1.
@@ -347,7 +347,7 @@ Proof.
{ rewrite PERM. apply elem_of_app. left. by eapply elem_of_list_lookup_2. }
rewrite ->Forall_forall in LTall. trans (length (Es G)).
- by apply LTall.
- - rewrite EsG' app_length /=. lia. }
+ - rewrite EsG' length_app /=. lia. }
have [v_e_i ENQ_e_i] : ∃ v_e_i, e_iV.(ge_event) = Enq v_e_i.
{ destruct PROD' as [ENQS]. specialize (ENQS _ _ Ei) as (?&?& He_iV' &?).
rewrite He_iV in He_iV'. injection He_iV' as <-. by eexists. }
@@ -420,7 +420,7 @@ Proof.
iSplitR "â—¯d"; last iSplit; last iSplit; [|done| |].
{ (* SPSCInv *)
iNext. iExists _. iFrame. iPureIntro. split_and!; [|done|done| |done].
- - subst deqId. rewrite EsG' app_length /= seq_app /=.
+ - subst deqId. rewrite EsG' length_app /= seq_app /=.
rewrite -(assoc app ds) -(comm app xs).
rewrite (assoc app ds) (assoc app es). by f_equiv.
- intros i' d'. specialize (MATCH i' d'). split.
diff --git a/gpfsl-examples/set_helper.v b/gpfsl-examples/set_helper.v
index 62b105ba..a6c69ec2 100644
--- a/gpfsl-examples/set_helper.v
+++ b/gpfsl-examples/set_helper.v
@@ -16,7 +16,7 @@ Section set_seq.
unfold to_set. split.
- destruct E as [|e' E].
+ simpl; set_solver.
- + rewrite cons_length, set_seq_S_end_union_L. destruct E as [|? E]; simpl.
+ + rewrite length_cons, set_seq_S_end_union_L. destruct E as [|? E]; simpl.
* rewrite (right_id_L _ _). set_solver.
* intros Eqe.
assert (Eq1 : S (length E) ∈ ({[e]} : gset _)).
@@ -29,6 +29,6 @@ Section set_seq.
Lemma to_set_append E e : to_set (E ++ [e]) = {[ length E ]} ∪ to_set E.
Proof.
- unfold to_set. by rewrite app_length, Nat.add_1_r, set_seq_S_end_union_L.
+ unfold to_set. by rewrite length_app, Nat.add_1_r, set_seq_S_end_union_L.
Qed.
End set_seq.
diff --git a/gpfsl-examples/stack/proof_elim_graph.v b/gpfsl-examples/stack/proof_elim_graph.v
index 5c0c3ec4..4733f2c9 100644
--- a/gpfsl-examples/stack/proof_elim_graph.v
+++ b/gpfsl-examples/stack/proof_elim_graph.v
@@ -318,7 +318,7 @@ Lemma StackProps_dom_l_insert Eb T eV :
stk_props_dom_l Eb T → stk_props_dom_l (Eb ++ [eV]) T'.
Proof.
intros e' T' DL. intros e.
- rewrite elem_of_app elem_of_list_singleton app_length /= DL.
+ rewrite elem_of_app elem_of_list_singleton length_app /= DL.
rewrite Nat.add_1_r Nat.lt_succ_r Nat.lt_eq_cases. naive_solver.
Qed.
Lemma StackProps_dom_l_insert_r Eb T e :
@@ -1111,7 +1111,7 @@ Proof.
set egVx := mkGraphEvent (Exchange vp v) Vppx Mx'.
assert (egVx = xe) as <-.
- { rewrite /psx EqEx app_length /= Nat.add_sub in Eqppx.
+ { rewrite /psx EqEx length_app /= Nat.add_sub in Eqppx.
apply (lookup_last_Some_2 Ex). rewrite -EqEx -Eqppx. exact EqGx. }
rewrite /= bool_decide_false in Eqxe; last first.
{ clear -Posv. by intros [_ ->]. }
@@ -1173,7 +1173,7 @@ Proof.
assert (SP': StackProps G' Gb Gx' T' false).
{ constructor.
- - by rewrite /= !app_length /= (stk_dom_length SP).
+ - by rewrite /= !length_app /= (stk_dom_length SP).
- by apply (StackProps_inj_insert _ _ FRT), (stk_event_id_map_inj SP).
- by apply StackProps_dom_l_insert_r, (stk_event_id_map_dom_l SP).
- rewrite EqGx'. apply StackProps_dom_r_insert; [done|].
@@ -1331,7 +1331,7 @@ Proof.
iExists true, V', G', psIde, (Push v), Vps', M'.
have EqLGb' : length Gb'.(Es) = S (length Gb.(Es)).
- { (* TODO: add to spec to avoid repeat *) rewrite EqGb' app_length /=. lia. }
+ { (* TODO: add to spec to avoid repeat *) rewrite EqGb' length_app /=. lia. }
have EqTps' : T' !! psIde = Some (inl psId).
{ by rewrite /psIde -(stk_dom_length SP) lookup_app_1_eq. }
have EqGbps : Gb'.(Es) !! psId = Some (mkGraphEvent ps Vps Mb').
@@ -1344,7 +1344,7 @@ Proof.
have SP' : StackProps G' Gb' Gx T' true.
{ constructor.
- - by rewrite 2!app_length (stk_dom_length SP) /=.
+ - by rewrite 2!length_app (stk_dom_length SP) /=.
- by apply (StackProps_inj_insert _ _ FRT), (stk_event_id_map_inj SP).
- rewrite EqGb'. apply StackProps_dom_l_insert, (stk_event_id_map_dom_l SP).
- apply StackProps_dom_r_insert_l, (stk_event_id_map_dom_r SP).
@@ -1705,7 +1705,7 @@ Proof.
{ destruct (xchg_cons_matches _ ECx' psx ppx) as [EqS _]; [done|].
clear -Lt EqS. subst ppx. destruct EqS as [-> | ->]; lia. }
have EqL' : length Ex' = psx.
- { by rewrite Eqpsx EqEx' app_length /= Nat.add_sub. }
+ { by rewrite Eqpsx EqEx' length_app /= Nat.add_sub. }
assert (xe = eVpsx) as ->.
{ rewrite Eqpsx in EqLps. apply lookup_last_Some in EqLps as [Exx' Eqx'].
@@ -1717,7 +1717,7 @@ Proof.
assert (EqLTr : psId = length Tr).
{ clear -EqlT SP.
- by rewrite /psId -(stk_dom_length SP) EqlT app_length /= Nat.add_sub. }
+ by rewrite /psId -(stk_dom_length SP) EqlT length_app /= Nat.add_sub. }
rewrite -EqLTr in UPp.
have EqlT' : T !! psId = Some (inr psx).
{ rewrite EqlT EqLTr -EqL'. by apply list_lookup_middle. }
@@ -1791,7 +1791,7 @@ Proof.
have SP' : StackProps G' Gb Gx' T' true.
{ constructor.
- - by rewrite /= !app_length /= (stk_dom_length SP).
+ - by rewrite /= !length_app /= (stk_dom_length SP).
- by apply (StackProps_inj_insert _ _ FRT), (stk_event_id_map_inj SP).
- apply StackProps_dom_l_insert_r, (stk_event_id_map_dom_l SP).
- rewrite EqGx'. apply StackProps_dom_r_insert; [done|].
@@ -1996,7 +1996,7 @@ Proof.
inl ppId ∉ T) as (Eqpp & EqLGb' & FRT).
{ clear -CASE SP. destruct CASE as [(_&_&->&->&_)|(_&_&_&->&_&->&_)];
(split; [by apply list_lookup_middle|]);
- (split; [rewrite app_length /=; lia|]);
+ (split; [rewrite length_app /=; lia|]);
by intros ?%(StackProps_is_Some_l_1_2 SP)%lookup_length_not_is_Some. }
destruct CASE as [CASE|CASE].
@@ -2049,7 +2049,7 @@ Proof.
have SP' : StackProps G' Gb' Gx T' true.
{ constructor.
- - by rewrite 2!app_length /= (stk_dom_length SP).
+ - by rewrite 2!length_app /= (stk_dom_length SP).
- by apply (StackProps_inj_insert _ _ FRT), (stk_event_id_map_inj SP).
- rewrite EqGb'. apply StackProps_dom_l_insert, (stk_event_id_map_dom_l SP).
- by apply StackProps_dom_r_insert_l, (stk_event_id_map_dom_r SP).
@@ -2262,7 +2262,7 @@ Proof.
(* TODO: dup with push case also *)
have SP' : StackProps G' Gb' Gx T' true.
{ constructor.
- - by rewrite 2!app_length /= (stk_dom_length SP).
+ - by rewrite 2!length_app /= (stk_dom_length SP).
- by apply (StackProps_inj_insert _ _ FRT), (stk_event_id_map_inj SP).
- rewrite EqGb'. apply StackProps_dom_l_insert, (stk_event_id_map_dom_l SP).
- by apply StackProps_dom_r_insert_l, (stk_event_id_map_dom_r SP).
diff --git a/gpfsl-examples/stack/proof_history_abs.v b/gpfsl-examples/stack/proof_history_abs.v
index dedc31a7..ab414568 100644
--- a/gpfsl-examples/stack/proof_history_abs.v
+++ b/gpfsl-examples/stack/proof_history_abs.v
@@ -57,7 +57,7 @@ Proof.
iAssert (Stack γs s S') with "[SI]" as "S".
{ destruct SC as [xo' lin' stk' XO LIN_PERM ??? INTERP_XO]. subst E' xo'.
iExists _, stk'. iFrame "SI". iPureIntro.
- rewrite app_length /= seq_app /= in INTERP_XO *.
+ rewrite length_app /= seq_app /= in INTERP_XO *.
rewrite filter_app filter_cons_True in INTERP_XO *; last first.
{ intros ? EV. rewrite HpushE in EV. by injection EV as <-. }
rewrite filter_nil in INTERP_XO *.
@@ -93,7 +93,7 @@ Proof.
iExists v, V, S. iFrame "⊒V".
iSplitL; [|by auto]. iSplitL; [|by iLeft].
iNext. iExists _,_. iFrame. iPureIntro. split; [|done].
- subst E'. rewrite app_length /= seq_app /=.
+ subst E'. rewrite length_app /= seq_app /=.
rewrite filter_app filter_cons_False; last first.
{ intros NE. by specialize (NE _ HpopE). }
rewrite filter_nil app_nil_r.
@@ -102,7 +102,7 @@ Proof.
- destruct CASE as (? & -> & -> & ? & -> & ? & pushE & HpushE & ? & ?).
(* reconstruct the state before the pop *)
destruct SC as [xo' lin' stk' XO LIN_PERM ??? INTERP_XO]. subst E' xo'.
- rewrite app_length /= seq_app /= in INTERP_XO *.
+ rewrite length_app /= seq_app /= in INTERP_XO *.
rewrite filter_app filter_cons_True in INTERP_XO *; last first.
{ intros ? EV. rewrite HpopE in EV. by injection EV as <-. }
rewrite filter_nil in INTERP_XO *.
@@ -119,7 +119,7 @@ Proof.
iDestruct (monPred_in_mono _ _ SYNC with "⊒V'") as "$".
iSplitL; [|by auto]. iSplitL; [|by iRight].
iNext. iExists _,_. iFrame. iPureIntro. split; [|done].
- rewrite app_length /= seq_app /= in INTERP_XO *.
+ rewrite length_app /= seq_app /= in INTERP_XO *.
rewrite filter_app filter_cons_True in INTERP_XO *; last first.
{ intros ? EV. rewrite HpopE in EV. by injection EV as <-. }
done.
@@ -149,7 +149,7 @@ Proof.
iAssert (Stack γs s S') with "[SI]" as "S".
{ destruct SC as [xo' lin' stk' XO LIN_PERM ??? INTERP_XO]. subst E' xo'.
iExists _, stk'. iFrame "SI". iPureIntro.
- rewrite app_length /= seq_app /= in INTERP_XO *.
+ rewrite length_app /= seq_app /= in INTERP_XO *.
rewrite filter_app filter_cons_True in INTERP_XO *; last first.
{ intros ? EV. rewrite HpushE in EV. by injection EV as <-. }
rewrite filter_nil in INTERP_XO *.
@@ -188,7 +188,7 @@ Proof.
iExists v, V, S. iFrame "⊒V".
iSplitL; [|by auto]. iSplitL; [|by iRight; iLeft].
iNext. iExists _,_. iFrame. iPureIntro. split; [|done].
- subst E'. rewrite app_length /= seq_app /=.
+ subst E'. rewrite length_app /= seq_app /=.
rewrite filter_app filter_cons_False; last first.
{ intros NE. by specialize (NE _ HpopE). }
rewrite filter_nil app_nil_r.
@@ -197,7 +197,7 @@ Proof.
- destruct CASE as (? & -> & -> & ? & -> & ? & pushE & HpushE & ? & ?).
(* reconstruct the state before the pop *)
destruct SC as [xo' lin' stk' XO LIN_PERM ??? INTERP_XO]. subst E' xo'.
- rewrite app_length /= seq_app /= in INTERP_XO *.
+ rewrite length_app /= seq_app /= in INTERP_XO *.
rewrite filter_app filter_cons_True in INTERP_XO *; last first.
{ intros ? EV. rewrite HpopE in EV. by injection EV as <-. }
rewrite filter_nil in INTERP_XO *.
@@ -214,7 +214,7 @@ Proof.
iDestruct (monPred_in_mono _ _ SYNC with "⊒V'") as "$".
iSplitL; [|by auto]. iSplitL; [|by iRight; iRight].
iNext. iExists _,_. iFrame. iPureIntro. split; [|done].
- rewrite app_length /= seq_app /= in INTERP_XO *.
+ rewrite length_app /= seq_app /= in INTERP_XO *.
rewrite filter_app filter_cons_True in INTERP_XO *; last first.
{ intros ? EV. rewrite HpopE in EV. by injection EV as <-. }
done.
diff --git a/gpfsl-examples/stack/proof_treiber_at.v b/gpfsl-examples/stack/proof_treiber_at.v
index 8ce8dede..0fbaeae9 100644
--- a/gpfsl-examples/stack/proof_treiber_at.v
+++ b/gpfsl-examples/stack/proof_treiber_at.v
@@ -46,7 +46,7 @@ Qed.
Lemma toHeadHist_lookup_None t0 LVs t :
(toHeadHist t0 LVs) !! t = None ↔
(t < t0)%positive ∨ (t0 +p (length LVs) ≤ t)%positive.
-Proof. by rewrite lookup_map_seqP_None fmap_length. Qed.
+Proof. by rewrite lookup_map_seqP_None length_fmap. Qed.
Lemma toHeadHist_lookup_Some_is_comparable_nullable_loc LVs t0 t v V (on : option loc) :
toHeadHist t0 LVs !! t = Some (v, V) →
@@ -75,7 +75,7 @@ Proof.
exists on'. split; [done|]. by apply (lookup_app_l_Some _ _ _ _ Eq1).
+ apply toHeadHist_lookup_None.
apply toHeadHist_lookup_None in Eqi as [?|Eqi]; [by left|right].
- rewrite app_length /=. move : Eqi.
+ rewrite length_app /=. move : Eqi.
rewrite Nat.add_1_r pos_add_succ_r_2.
rewrite (_: t0 +p length LVs = t); [lia|]. rewrite -Eq /pos_add_nat; lia.
Qed.
@@ -87,7 +87,7 @@ Definition next_nodes S : list (option loc) :=
end.
Lemma next_nodes_length S : length (next_nodes S) = length S.
-Proof. destruct S; [done|]. rewrite /= app_length fmap_length /=. lia. Qed.
+Proof. destruct S; [done|]. rewrite /= length_app length_fmap /=. lia. Qed.
Lemma next_nodes_cons n S :
next_nodes (n :: S) = hd_error S :: next_nodes S.
@@ -350,8 +350,8 @@ Proof.
clear -FRt Let02 LtL.
apply toHeadHist_lookup_None in FRt as [?|Let']; first (exfalso; lia).
apply : (anti_symm (le)).
- - clear -LtL. rewrite app_length /= in LtL. lia.
- - clear LtL. rewrite app_length /= /pos_add_nat in Let'; lia. }
+ - clear -LtL. rewrite length_app /= in LtL. lia.
+ - clear LtL. rewrite length_app /= /pos_add_nat in Let'; lia. }
rewrite EqL in Eqn2.
assert (Vh2 = Vr ∧ on' = hd_error S2) as [-> ->].
{ clear -Eqn2. apply lookup_last_Some_2 in Eqn2. by inversion Eqn2. }
@@ -376,8 +376,8 @@ Proof.
<[(t' + 1)%positive:=(#n, Vw)]> (toHeadHist t02 (LVs2 ++ [(hd_error S2, Vr)])));
first done.
symmetry. apply (toHeadHist_insert _ _ _ (Some n)).
- - clear -Let02 EqL. rewrite app_length /=. lia.
- - clear. rewrite app_length /=. lia. }
+ - clear -Let02 EqL. rewrite length_app /=. lia.
+ - clear. rewrite length_app /=. lia. }
iIntros "!>". wp_if. by iApply "Post".
Qed.
@@ -502,9 +502,9 @@ Proof.
clear -FRt Let02 LtL.
apply toHeadHist_lookup_None in FRt as [?|Let']; first (exfalso; lia).
apply : (anti_symm (le)).
- - clear -LtL. rewrite app_length /= in LtL. lia.
+ - clear -LtL. rewrite length_app /= in LtL. lia.
- clear LtL.
- rewrite app_length /= /pos_add_nat in Let'; lia. }
+ rewrite length_app /= /pos_add_nat in Let'; lia. }
rewrite EqL in Eqn2.
assert (Vh2 = V2 ∧ ∃ S2', S2 = n :: S2') as (-> & S2' & ->).
{ clear -Eqn2. apply lookup_last_Some_2 in Eqn2. inversion Eqn2 as [Eq1].
@@ -535,8 +535,8 @@ Proof.
rewrite (_ : toHeadHist t02 (LVs' ++ [(hd_error S2', Vw)]) = ζh2);
first done.
rewrite Eqζh2 toHeadHist_insert; [done|..].
- - clear -EqL Let02. rewrite app_length /= -EqL. lia.
- - clear. rewrite app_length /=. lia. }
+ - clear -EqL Let02. rewrite length_app /= -EqL. lia.
+ - clear. rewrite length_app /=. lia. }
iDestruct (view_at_elim with "sV2 Hnd") as "(Hd & P & Hn†)".
iIntros "!>". wp_if. wp_op.
diff --git a/gpfsl-examples/stack/proof_treiber_graph.v b/gpfsl-examples/stack/proof_treiber_graph.v
index 97a6c290..e58e6812 100644
--- a/gpfsl-examples/stack/proof_treiber_graph.v
+++ b/gpfsl-examples/stack/proof_treiber_graph.v
@@ -125,7 +125,7 @@ Definition next_nodes S : list (option loc) :=
end.
Lemma next_nodes_length S : length (next_nodes S) = length S.
-Proof. destruct S; [done|]. rewrite /= app_length fmap_length /=. lia. Qed.
+Proof. destruct S; [done|]. rewrite /= length_app length_fmap /=. lia. Qed.
Lemma next_nodes_cons n S :
next_nodes (n :: S) = hd_error S :: next_nodes S.
@@ -146,7 +146,7 @@ Qed.
Lemma toHeadHist_lookup_None t0 LVs t :
(toHeadHist t0 LVs) !! t = None ↔
(t < t0)%positive ∨ (t0 +p (length LVs) ≤ t)%positive.
-Proof. by rewrite lookup_map_seqP_None fmap_length. Qed.
+Proof. by rewrite lookup_map_seqP_None length_fmap. Qed.
Lemma toHeadHist_lookup_Some_is_comparable_nullable_loc LVs t0 t v V (on : option loc) :
toHeadHist t0 LVs !! t = Some (v, V) →
@@ -175,7 +175,7 @@ Proof.
exists on'. split; [done|]. by apply (lookup_app_l_Some _ _ _ _ Eq1).
+ apply toHeadHist_lookup_None.
apply toHeadHist_lookup_None in Eqi as [?|Eqi]; [by left|right].
- rewrite app_length /=. move : Eqi.
+ rewrite length_app /=. move : Eqi.
rewrite Nat.add_1_r pos_add_succ_r_2.
rewrite (_: t0 +p length LVs = t); [lia|]. rewrite -Eq /pos_add_nat; lia.
Qed.
@@ -1099,8 +1099,8 @@ Proof.
clear -FRt Let02 LtL.
apply toHeadHist_lookup_None in FRt as [?|Let']; first (exfalso; lia).
apply : (anti_symm (le)).
- - clear -LtL. rewrite app_length /= in LtL. lia.
- - clear LtL. rewrite app_length /= /pos_add_nat in Let'; lia. }
+ - clear -LtL. rewrite length_app /= in LtL. lia.
+ - clear LtL. rewrite length_app /= /pos_add_nat in Let'; lia. }
rewrite EqL in Eqn2.
assert (Vh2 = Vr ∧ on' = hd_error S2) as [-> ->].
{ clear -Eqn2. apply lookup_last_Some_2 in Eqn2. by inversion Eqn2. }
@@ -1301,8 +1301,8 @@ Proof.
assert (Eqζh2' : toHeadHist t02 LVs' =
<[(t' + 1)%positive:=(#n, Vw)]> (toHeadHist t02 (LVs2 ++ [(hd_error S2, Vr)]))).
{ symmetry. apply (toHeadHist_insert _ _ _ (Some n)).
- - clear -Let02 EqL. rewrite app_length /=. lia.
- - clear. rewrite app_length /=. lia. }
+ - clear -Let02 EqL. rewrite length_app /=. lia.
+ - clear. rewrite length_app /=. lia. }
rewrite Eqζn -Eqζh2'. iExists t02, _, Vw. iSplitL "H". { iFrame "H". }
iSplitR; last first. { iSplitL "As"; [by iFrame "As"|by iFrame "Is"]. }
(* show that n is the latest write *)
@@ -1319,7 +1319,7 @@ Proof.
rewrite lookup_fmap_Some' => [[[n1 Vn1] [Eq Eqt1]]].
simpl in Eq. subst n1.
apply toHeadHist_lookup_Some in Eqt1 as (Let1' & on & Eq & Eqt1%lookup_lt_Some).
- rewrite app_length /= -EqL in Eqt1. clear - Eqt1 Ltt1 Let1' Let02. lia.
+ rewrite length_app /= -EqL in Eqt1. clear - Eqt1 Ltt1 Let1' Let02. lia.
* rewrite lookup_insert_ne; [|done]. intros Int0.
intros t1 Let1. case (decide (t1 = (t' + 1))%positive) => [->|?].
{ rewrite lookup_insert /=. by inversion 1. }
@@ -1746,9 +1746,9 @@ Proof.
clear -FRt Let02 LtL.
apply toHeadHist_lookup_None in FRt as [?|Let']; first (exfalso; lia).
apply : (anti_symm (le)).
- - clear -LtL. rewrite app_length /= in LtL. lia.
+ - clear -LtL. rewrite length_app /= in LtL. lia.
- clear LtL.
- rewrite app_length /= /pos_add_nat in Let'; lia. }
+ rewrite length_app /= /pos_add_nat in Let'; lia. }
rewrite EqL in Eqn2.
assert (Vh2 = V2 ∧ ∃ S2', S2 = n :: S2') as (-> & S2' & ->).
{ clear -Eqn2. apply lookup_last_Some_2 in Eqn2. inversion Eqn2 as [Eq1].
@@ -1965,8 +1965,8 @@ Proof.
have EQH : toHeadHist t02 (LVs' ++ [(hd_error S2', Vw)]) =
<[(t' + 1)%positive:=(#(oloc_to_lit (hd_error S2')), Vw)]> (toHeadHist t02 LVs').
{ rewrite toHeadHist_insert; [done|..].
- - clear -EqL Let02. rewrite app_length /= -EqL. lia.
- - clear. rewrite app_length /=. lia. }
+ - clear -EqL Let02. rewrite length_app /= -EqL. lia.
+ - clear. rewrite length_app /=. lia. }
iExists (Vb ⊔ V2'), t02, LVs', Vw. iSplitL "H".
{ rewrite Eqζh2 -EQH. by iFrame "H". }
iFrame "As". iSplit; last first.
diff --git a/gpfsl-examples/stack/proof_treiber_history.v b/gpfsl-examples/stack/proof_treiber_history.v
index a473366f..b45dc994 100644
--- a/gpfsl-examples/stack/proof_treiber_history.v
+++ b/gpfsl-examples/stack/proof_treiber_history.v
@@ -212,10 +212,10 @@ Lemma length_concat_fmap_take_plus_S (f : _ → list event_id) gen1' emo x N
Proof.
apply lookup_lt_Some in GEN1 as LEgen1'.
rewrite -{1}(take_drop gen1' emo).
- rewrite take_app_add'; last first. { rewrite take_length. lia. }
- rewrite fmap_app concat_app app_length.
+ rewrite take_app_add'; last first. { rewrite length_take. lia. }
+ rewrite fmap_app concat_app length_app.
rewrite (drop_S _ _ _ GEN1). rewrite firstn_cons fmap_cons /=.
- rewrite app_length. done.
+ rewrite length_app. done.
Qed.
Lemma emo_idx_to_lin_idx_inj esi emo eidx1 eidx2 e
@@ -333,11 +333,11 @@ Proof.
- done.
- subst. apply lookup_emo_inv_e in EMO_LOOKUP as (? & GEN & ?). des. simplify_list_eq.
have LT : gen' < length emo.
- { apply lookup_lt_Some in GEN. by rewrite !fmap_length in GEN. }
+ { apply lookup_lt_Some in GEN. by rewrite !length_fmap in GEN. }
rewrite take_app_le; [done|lia].
- subst. apply lookup_emo_inv_ne in EMO_LOOKUP as GEN. des.
have LT : gen' < length emo.
- { apply lookup_lt_Some in GEN. by rewrite !fmap_length in GEN. }
+ { apply lookup_lt_Some in GEN. by rewrite !length_fmap in GEN. }
rewrite take_app_le; [done|lia].
Qed.
@@ -363,16 +363,16 @@ Proof.
+ by eapply lookup_emo_app.
- rewrite list_lookup_middle in LIN_I; [|done]. simplify_eq.
exists (emo_ne (length emo)). list_simplifier. split; red.
- + subst len. by rewrite /lin_of_emo app_length.
- + by rewrite -!(fmap_length fst) lookup_app_1_eq.
+ + subst len. by rewrite /lin_of_emo length_app.
+ + by rewrite -!(length_fmap fst) lookup_app_1_eq.
- rewrite ->lookup_app_r,lookup_cons in LIN_I; [|lia].
case Esub: (i - len) => [|i']; [lia|]. rewrite -/len Esub in LIN_I.
have {Esub}Hi : i = len + S i' by lia. subst.
- subst len. unfold lin_of_emo in *. rewrite app_length.
+ subst len. unfold lin_of_emo in *. rewrite length_app.
exists (emo_e (S (length emo)) i'). split; red.
+ rewrite /emo_idx_to_lin_idx. list_simplifier. done.
+ unfold lookup_emo. list_simplifier.
- by rewrite -(fmap_length fst) -(fmap_length snd) lookup_app_1_eq.
+ by rewrite -(length_fmap fst) -(length_fmap snd) lookup_app_1_eq.
Qed.
Lemma lookup_emo_lin_of_emo_lookup esi emo eidx e
@@ -462,7 +462,7 @@ Proof.
{ rewrite list_lookup_fmap. rewrite EG.
by list_simplifier. }
apply take_S_r in H. rewrite H.
- rewrite concat_app /= app_nil_r app_length cons_length. lia.
+ rewrite concat_app /= app_nil_r length_app length_cons. lia.
Qed.
Lemma lin_idx_ne_e_gen_mono esi emo gen1' gen2 i2' (LEgen : S gen1' ≤ gen2) :
@@ -551,7 +551,7 @@ Lemma lookup_emo_old_esi esi emo eidx e e0
Proof.
destruct eidx as [[|gen'] i'|gen']; simplify_list_eq; [|done|done].
have LEi' : (i' < length esi)%nat.
- { apply lookup_lt_Some in EMO_LOOKUP. rewrite app_length /= in EMO_LOOKUP.
+ { apply lookup_lt_Some in EMO_LOOKUP. rewrite length_app /= in EMO_LOOKUP.
have ? : i' ≠length esi by intros ->. lia. }
by rewrite lookup_app_l in EMO_LOOKUP.
Qed.
@@ -624,13 +624,13 @@ Lemma lookup_emo_old_emo_ne esi emo eidx e0 e msg0
(NEedix : eidx ≠emo_ne (length emo)) :
lookup_emo esi emo eidx = Some e.
Proof.
- rewrite -(fmap_length fst) -(fmap_length snd) in NEedix.
+ rewrite -(length_fmap fst) -(length_fmap snd) in NEedix.
destruct eidx as [[|gen'] i'|gen']; simplify_list_eq; [done|..];
case (decide (gen' = (length emo.*1.*2))) as [->|NE].
- rewrite lookup_app_1_eq /= in EMO_LOOKUP. done.
- rewrite lookup_app_1_ne in EMO_LOOKUP; done.
- - rewrite fmap_length -(fmap_length fst) in EMO_LOOKUP. simplify_eq.
- - rewrite fmap_length -(fmap_length fst) in NE.
+ - rewrite length_fmap -(length_fmap fst) in EMO_LOOKUP. simplify_eq.
+ - rewrite length_fmap -(length_fmap fst) in NE.
rewrite lookup_app_1_ne in EMO_LOOKUP; done.
Qed.
@@ -699,7 +699,7 @@ Proof.
apply Permutation_inj in LIN_PERM as [_ (f & INJ_f & LIN_PERM)].
rewrite ->LIN_PERM in LIN1,LIN2.
apply lookup_lt_Some in LIN1 as LT1, LIN2 as LT2.
- rewrite seq_length in LT1,LT2.
+ rewrite length_seq in LT1,LT2.
rewrite ->lookup_xo in LIN1,LIN2; [|done..].
rewrite -LIN1 in LIN2. injection LIN2 as EQ%(inj f).
by eapply emo_idx_to_lin_idx_inj in EQ.
@@ -753,10 +753,10 @@ Proof.
intros eidx1 eidx2 e.
case (decide (eidx1 = emo_ne (length emo.*1.*1))) => [->|NE1]; simpl;
[rewrite !fmap_app /= lookup_app_1_eq; intros [= <-]
- |rewrite !fmap_length in NE1; intros HL1%lookup_emo_old_emo_ne; [|done]];
+ |rewrite !length_fmap in NE1; intros HL1%lookup_emo_old_emo_ne; [|done]];
(case (decide (eidx2 = emo_ne (length emo.*1.*1))) => [->|NE2]; simpl;
[rewrite !fmap_app /= lookup_app_1_eq; (intros [= <-] || intros _)
- |rewrite !fmap_length in NE2; intros HL2%lookup_emo_old_emo_ne; [|done]]).
+ |rewrite !length_fmap in NE2; intros HL2%lookup_emo_old_emo_ne; [|done]]).
- done.
- exfalso. eapply (emo_ids_le_new E) in HL2; [lia|done].
- exfalso. eapply (emo_ids_le_new E) in HL1; [lia|done].
@@ -778,7 +778,7 @@ Proof.
- rewrite Forall_lookup => i' e ES_i'.
specialize (EMPPOPS _ _ ES_i') as [eV [EV' ?]].
exists eV. split; [|done]. by eapply prefix_lookup_Some.
- - destruct SubE as [E ->]. rewrite app_length /= seq_app.
+ - destruct SubE as [E ->]. rewrite length_app /= seq_app.
apply sublist_inserts_r, EMPPOP_XO_SUB.
Qed.
@@ -810,7 +810,7 @@ Proof.
apply lookup_seq in In. lia. }
apply (prefix_lookup_inv E1 E2); [done| |done].
apply lookup_lt_is_Some_2. lia.
- - destruct SubE as [E ->]. rewrite app_length seq_app.
+ - destruct SubE as [E ->]. rewrite length_app seq_app.
apply sublist_inserts_r, EMPPOP_XO_SUB.
Qed.
@@ -904,7 +904,7 @@ Proof.
rewrite /= !fmap_app /= in EMO_eidx1.
apply lookup_last_Some_2 in EMO_eidx1 as ->.
eapply lookup_emo_old_emo_ne in EMO_eidx2;
- [|subst eidx gen'; rewrite !fmap_length in NE2; done].
+ [|subst eidx gen'; rewrite !length_fmap in NE2; done].
exploit (emo_ids_le_new E esi emo eidx2 e2); [done..|]. intro.
rewrite lookup_app_l in EV2; [|done].
move: (hwf_logview_closed _ EWF _ _ EV2 _ IN_LVIEW) => /lookup_lt_is_Some.
@@ -914,15 +914,15 @@ Proof.
apply lookup_last_Some_2 in EMO_eidx2 as ->.
apply lookup_last_Some_2 in EV2 as ->.
eapply lookup_emo_old_emo_ne in EMO_eidx1;
- [|subst eidx gen'; rewrite !fmap_length in NE1; done].
+ [|subst eidx gen'; rewrite !length_fmap in NE1; done].
have MAXgen : (gen_of eidx1 ≤ gen')%nat.
- { subst gen'. rewrite !fmap_length. by eapply max_gen. }
+ { subst gen'. rewrite !length_fmap. by eapply max_gen. }
destruct eidx1 as [gen1 i1'|gen1']; intros; simpl in *.
++ apply emo_idx_le_e_ne_1. lia.
++ apply emo_idx_le_ne_ne. lia.
-- (* old ∈ old.lview *)
eapply lookup_emo_old_emo_ne in EMO_eidx1,EMO_eidx2;
- [|subst eidx gen'; rewrite !fmap_length in NE1,NE2; done..].
+ [|subst eidx gen'; rewrite !length_fmap in NE1,NE2; done..].
exploit (emo_ids_le_new E esi emo eidx2 e2); [done..|]. intros.
rewrite lookup_app_l in EV2; [|done].
by eapply (HB_EMO eidx1 eidx2).
@@ -1288,7 +1288,7 @@ Qed.
Lemma toHeadHist_lookup_None ti mo t :
(toHeadHist ti mo) !! t = None ↔
(t < ti)%positive ∨ (ti +p (length mo) ≤ t)%positive.
-Proof. by rewrite lookup_map_seqP_None fmap_length. Qed.
+Proof. by rewrite lookup_map_seqP_None length_fmap. Qed.
Lemma toHeadHist_lookup_Some_is_comparable_nullable_loc mo ti t v V (on : option loc) :
toHeadHist ti mo !! t = Some (v, V) →
@@ -1391,7 +1391,7 @@ Proof.
exists on'. split; [done|]. by apply (lookup_app_l_Some _ _ _ _ Eq1).
+ apply toHeadHist_lookup_None.
apply toHeadHist_lookup_None in Eqi as [?|Eqi]; [by left|right].
- rewrite app_length /=. move : Eqi.
+ rewrite length_app /=. move : Eqi.
rewrite Nat.add_1_r pos_add_succ_r_2.
rewrite (_: ti +p length mo = t); [lia|]. rewrite -Eq /pos_add_nat; lia.
Qed.
@@ -1637,8 +1637,8 @@ Proof.
clear -FRt Letitr2 LtL.
apply toHeadHist_lookup_None in FRt as [?|Let']; first (exfalso; lia).
apply : (anti_symm (le)).
- - clear -LtL. rewrite cons_length /= in LtL. lia.
- - clear LtL. rewrite cons_length /= /pos_add_nat in Let'; lia. }
+ - clear -LtL. rewrite length_cons /= in LtL. lia.
+ - clear LtL. rewrite length_cons /= /pos_add_nat in Let'; lia. }
rewrite EqL in Eqn2.
assert (ont2 = on1 ∧ Vt2 = Vr2) as [-> ->].
@@ -1696,10 +1696,10 @@ Proof.
case (decide (eidx = (emo_ne (length emo2.*1.*1)))) as [->|NEeidx].
- subst emo2'. simpl in *. rewrite !fmap_app /= in EMO_LOOKUP.
apply lookup_last_Some_2 in EMO_LOOKUP as ->.
- rewrite !fmap_length -(fmap_length snd). rewrite -EqL.
+ rewrite !length_fmap -(length_fmap snd). rewrite -EqL.
rewrite (_ : Pos.of_nat (Pos.to_nat ti + S (Pos.to_nat tr2 - Pos.to_nat ti)) = tr2 + 1)%positive; [done|lia].
- case (decide (e = psId)) as [->|NEe].
- { exfalso. rewrite !fmap_length in NEeidx.
+ { exfalso. rewrite !length_fmap in NEeidx.
apply lookup_emo_old_emo_ne in EMO_LOOKUP; [|done].
eapply emo_ids_le_new in EMO_LOOKUP; [|done]. subst psId. lia. }
apply (seen_msgs_mono _ esi2 _ emo2' _ ζh2) in SM0; [|done| |done..|by etrans].
@@ -1707,7 +1707,7 @@ Proof.
+ intros ? ?. eapply event_in_esi_emo; [done|]. by apply SubME0. }
have LIN_PERM2' : lin_of_emo esi2 emo2' ≡ₚ seq 0 (length E2').
- { rewrite app_length. apply lin_perm_add_emo_ne.
+ { rewrite length_app. apply lin_perm_add_emo_ne.
destruct Props2 as (LAST_MSG&?&?&?&ESI_EMO_GOOD&?). des. by destruct ESI_EMO_GOOD. }
iMod (history_master_update _ _ E2' with "Eâ—2") as "[Eâ—2' #Eâ—¯2']";
@@ -1722,8 +1722,8 @@ Proof.
iFrame "∗". iNext. iSplitL; last iSplitL.
{ (* at↦ *) subst ζn2. rewrite (toHeadHist_insert _ _ _ (Some n)).
- subst emo2'. rewrite !fmap_app /=. eauto with iFrame.
- - clear -Letitr2 EqL. rewrite cons_length /=. lia.
- - clear. rewrite cons_length /=. lia. }
+ - clear -Letitr2 EqL. rewrite length_cons /=. lia.
+ - clear. rewrite length_cons /=. lia. }
{ (* SeenMsgsAll γh s E2' esi2 emo2' ti *) iIntros (e eidx eV EV EMO_LOOKUP).
(* TODO: Suspicious repetition of the same case analysis in SM2' proof. *)
case (decide (eidx = emo_ne (length emo2.*1.*1))) as [->|NEeidx].
@@ -1731,7 +1731,7 @@ Proof.
apply lookup_last_Some_2 in EMO_LOOKUP as ->.
apply lookup_last_Some_2 in EV as ->. subst egV'. simpl.
iExists ζh2. iFrame (SM2') "sn⊒2".
- - rewrite !fmap_length in NEeidx.
+ - rewrite !length_fmap in NEeidx.
apply lookup_emo_old_emo_ne in EMO_LOOKUP; [|done].
apply (emo_ids_le_new E2) in EMO_LOOKUP as OLD; [|done].
rewrite lookup_app_l in EV; [|done].
@@ -1989,7 +1989,7 @@ Proof.
+ exploit (SM0 e eidx); [|done..]. set_solver +SEEN NEe.
+ by trans esi1. }
have LIN_PERM1' : lin_of_emo esi1' emo1 ≡ₚ seq 0 (length E1').
- { rewrite app_length. by apply lin_perm_add_esi. }
+ { rewrite length_app. by apply lin_perm_add_esi. }
iMod (emo_auth_own_update_esi ppId with "Mâ—1") as "[Mâ—1' #Mâ—¯1']".
@@ -2030,7 +2030,7 @@ Proof.
destruct ESI_GOOD,ESI_GOOD'. constructor.
++ apply Forall_app. split; [done|]. simpl. apply Forall_singleton.
eexists. split; [apply lookup_app_1_eq|done].
- ++ rewrite app_length seq_app /=. by apply sublist_app.
+ ++ rewrite length_app seq_app /=. by apply sublist_app.
-- apply (Forall_impl _ _ _ GEN_GOOD). intros [[? ?] [? ?]] GOOD.
by apply (emo_gen_good_mono _ _ _ _ _ _ GOOD).
-- (* XO_AGREE *) by rewrite write_xo_snoc_e.
@@ -2098,7 +2098,7 @@ Proof.
apply (seen_msgs_mono _ esi1 _ emo1' _ ζh1) in SM0; [|done|done|done|by etrans..].
exploit (SM0 e eidx); [|done..]. set_solver +SEEN NEe. }
have LIN_PERM1' : lin_of_emo esi1 emo1' ≡ₚ seq 0 (length E1').
- { rewrite app_length. by eapply lin_perm_add_emo_e. }
+ { rewrite length_app. by eapply lin_perm_add_emo_e. }
iMod (emo_auth_own_update_emo_e gen' ppId with "Mâ—1") as "[Mâ—1' #Mâ—¯1']".
@@ -2152,7 +2152,7 @@ Proof.
rewrite -(write_xo_stable E1); [|lia|done].
by apply (stack_interp_mono_prefix E1).
** done.
- ** rewrite app_length seq_app /=. by apply sublist_app.
+ ** rewrite length_app seq_app /=. by apply sublist_app.
++ rewrite /emo_insert_e list_lookup_alter_ne in GEN0'; [|done].
specialize (GEN_GOOD _ _ GEN0'). simpl in GEN_GOOD.
by apply (emo_gen_good_mono E1).
@@ -2302,8 +2302,8 @@ Proof.
clear -FRt Letitr2 LtL.
apply toHeadHist_lookup_None in FRt as [?|Let']; first (exfalso; lia).
apply : (anti_symm (le)).
- - clear -LtL. rewrite cons_length /= in LtL. lia.
- - clear LtL. rewrite cons_length /= /pos_add_nat in Let'; lia. }
+ - clear -LtL. rewrite length_cons /= in LtL. lia.
+ - clear LtL. rewrite length_cons /= /pos_add_nat in Let'; lia. }
rewrite EqL in Eqn2.
assert (ont2 = Some n1 ∧ Vt2 = Vr2) as [-> ->].
@@ -2321,16 +2321,16 @@ Proof.
have {}LAST_MSG : last emo2.*2 = Some (Some n1, Vr2).
{ rewrite last_cons in LAST_MSG. by case_match. }
have LAST : length emo2 = length (write_xo E2).
- { apply (f_equal length) in XO_AGREE. by rewrite !fmap_length in XO_AGREE. }
+ { apply (f_equal length) in XO_AGREE. by rewrite !length_fmap in XO_AGREE. }
have [es GEN] : ∃ es, emo2 !! (Nat.pred (length emo2)) = Some (e, es, (Some n1, Vr2)).
{ clear -LAST_MSG LAST XO_AGREE ORD EVENT.
- rewrite last_lookup fmap_length in LAST_MSG.
+ rewrite last_lookup length_fmap in LAST_MSG.
apply list_lookup_fmap_inv in LAST_MSG as ([[? es] [? ?]] & [= <- <-] & LAST_MSG).
rewrite ORD in XO_AGREE.
apply (f_equal ((!!) (Nat.pred (length emo2)))) in XO_AGREE.
rewrite !list_lookup_fmap LAST_MSG /= in XO_AGREE.
apply (f_equal length) in ORD. rewrite -LAST in ORD. rewrite ORD in XO_AGREE.
- rewrite app_length /= -Nat.add_pred_r /= in XO_AGREE; [|lia].
+ rewrite length_app /= -Nat.add_pred_r /= in XO_AGREE; [|lia].
rewrite Nat.add_0_r lookup_app_1_eq in XO_AGREE. injection XO_AGREE as ->.
by exists es. }
rewrite ->Forall_lookup in GEN_GOOD.
@@ -2459,7 +2459,7 @@ Proof.
exploit (lookup_emo_new_ne E2 esi2 emo2); [done|done|].
intros ->. simpl.
assert (Pos.of_nat (Pos.to_nat ti + S (length emo2)) = tr2 + 1)%positive as ->.
- { rewrite fmap_length in EqL. lia. }
+ { rewrite length_fmap in EqL. lia. }
apply lookup_union_is_Some. by left. }
iAssert (@{V2} s sn⊒{γh} (ζh2 ∪ ζhps))%I as "sn⊒2'".
@@ -2471,7 +2471,7 @@ Proof.
{ iExists (ζh2 ∪ ζhps). iFrame (SM2') "sn⊒2'". }
have LIN_PERM2' : lin_of_emo esi2 emo2' ≡ₚ seq 0 (length E2').
- { rewrite app_length. apply lin_perm_add_emo_ne.
+ { rewrite length_app. apply lin_perm_add_emo_ne.
destruct Props2 as (LAST_MSG&TOP_SEEN_PUSH&?&HB_XO&ESI_EMO_GOOD&XO_INTERP).
des. by destruct ESI_EMO_GOOD. }
@@ -2492,8 +2492,8 @@ Proof.
iFrame "∗". iSplitL; last iSplitL.
{ (* at↦ *) subst ζn2. rewrite (toHeadHist_insert _ _ _ onn).
- subst emo2'. rewrite !fmap_app /=. eauto with iFrame.
- - clear -Letitr2 EqL. rewrite cons_length /=. lia.
- - clear. rewrite cons_length /=. lia. }
+ - clear -Letitr2 EqL. rewrite length_cons /=. lia.
+ - clear. rewrite length_cons /=. lia. }
{ (* SeenMsgsAll γh s E2' esi2 emo2' ti *) iNext.
iIntros (e eidx eV EV EMO_LOOKUP).
case (decide (eidx = emo_ne (length emo2.*1.*1))) as [->|NEeidx].
@@ -2501,7 +2501,7 @@ Proof.
apply lookup_last_Some_2 in EMO_LOOKUP as ->.
apply lookup_last_Some_2 in EV as ->. subst pp. simpl.
iFrame "SM2'".
- - rewrite !fmap_length in NEeidx.
+ - rewrite !length_fmap in NEeidx.
apply lookup_emo_old_emo_ne in EMO_LOOKUP; [|done].
apply (emo_ids_le_new E2) in EMO_LOOKUP as OLD; [|done].
rewrite lookup_app_l in EV; [|done].
diff --git a/gpfsl-examples/stack/spec_history.v b/gpfsl-examples/stack/spec_history.v
index a8424099..4e6070da 100644
--- a/gpfsl-examples/stack/spec_history.v
+++ b/gpfsl-examples/stack/spec_history.v
@@ -238,7 +238,7 @@ Lemma write_xo_stable E1 E2 e (LEN : (e ≤ length E1)%nat) (SubE : E1 ⊑ E2) :
Proof.
destruct SubE as [E ->]. apply list_filter_iff'.
rewrite Forall_lookup => i e' H.
- apply lookup_lt_Some in H as LT. rewrite seq_length in LT.
+ apply lookup_lt_Some in H as LT. rewrite length_seq in LT.
rewrite lookup_xo in H; [|done]. injection H as ->.
unfold not_empty_pop. split; intros NE eV' EV'.
- rewrite lookup_app_l in EV'; [|lia]. apply (NE _ EV').
@@ -451,7 +451,7 @@ Lemma write_xo_snoc_e E eV
(HE: eV.(ge_event) = EmpPop) :
write_xo (E ++ [eV]) = write_xo E.
Proof.
- unfold write_xo. rewrite app_length seq_app filter_app.
+ unfold write_xo. rewrite length_app seq_app filter_app.
rewrite filter_cons_False; last first. {
unfold not, not_empty_pop; intros H.
specialize (H eV). rewrite lookup_app_1_eq in H.
@@ -466,7 +466,7 @@ Lemma write_xo_snoc_ne E eV
(HNE: eV.(ge_event) ≠EmpPop) :
write_xo (E ++ [eV]) = write_xo E ++ [length E].
Proof.
- unfold write_xo. rewrite app_length seq_app filter_app.
+ unfold write_xo. rewrite length_app seq_app filter_app.
rewrite filter_cons_True; last first. {
unfold not_empty_pop; intros ? EV.
rewrite lookup_app_1_eq in EV. by inv EV.
diff --git a/gpfsl/base_logic/na.v b/gpfsl/base_logic/na.v
index 74c7ab9d..ae844147 100644
--- a/gpfsl/base_logic/na.v
+++ b/gpfsl/base_logic/na.v
@@ -10,7 +10,7 @@ Lemma big_sepL_seq {PROP : bi} {A} (P : nat → PROP) (l : list A) :
([∗ list] i↦_ ∈ l, P i) ⊣⊢ ([∗ list] i ∈ seq 0 (length l), P i).
Proof.
induction l as [|?? IHl] using rev_ind; first done.
- rewrite app_length /= Nat.add_1_r seq_S !big_sepL_app /=.
+ rewrite length_app /= Nat.add_1_r seq_S !big_sepL_app /=.
by rewrite IHl Nat.add_0_r.
Qed.
@@ -405,9 +405,9 @@ Section na_props.
-big_sepL_app.
f_equiv. apply reflexive_eq, list_eq=>i.
destruct (decide (i < n1)%nat).
- - rewrite lookup_app_l ?fmap_length ?seq_length // !list_lookup_fmap
+ - rewrite lookup_app_l ?length_fmap ?length_seq // !list_lookup_fmap
!lookup_seq_lt //. lia.
- - rewrite lookup_app_r ?fmap_length ?seq_length ?Nat.le_ngt // !list_lookup_fmap.
+ - rewrite lookup_app_r ?length_fmap ?length_seq ?Nat.le_ngt // !list_lookup_fmap.
destruct (decide (i < n1 + n2)%nat).
+ rewrite !lookup_seq_lt /= ?shift_nat_assoc; repeat f_equal; lia.
+ rewrite !lookup_seq_ge //; lia.
diff --git a/gpfsl/logic/lifting.v b/gpfsl/logic/lifting.v
index b62215c9..f5983fb4 100644
--- a/gpfsl/logic/lifting.v
+++ b/gpfsl/logic/lifting.v
@@ -594,7 +594,7 @@ Proof.
iIntros (Hlen Hf) "Hel HΦ". rewrite -(vec_to_list_to_vec Ql).
generalize (list_to_vec Ql). rewrite Hlen. clear Hlen Ql=>Ql.
iApply (wp_app_vec with "Hel"); [done|]. iIntros (vl) "Hvl".
- iApply ("HΦ" with "[%] Hvl"). by rewrite vec_to_list_length.
+ iApply ("HΦ" with "[%] Hvl"). by rewrite length_vec_to_list.
Qed.
(* NOTES: for other lemmas, look for the iProp version (iwp_) in base_lifting. *)
diff --git a/orc11/memory.v b/orc11/memory.v
index 332b90ae..e7e75d51 100644
--- a/orc11/memory.v
+++ b/orc11/memory.v
@@ -1539,7 +1539,7 @@ Section Memory.
destruct (cell_list'_tail l n M Cl) as [Cl' Eq'].
rewrite Eq'.
assert (HL:= cell_list'_length_exact l n M Cl).
- rewrite Eq' app_length in HL.
+ rewrite Eq' length_app in HL.
assert (HL': length Cl' = n) by lia.
rewrite -HL'. apply lookup_app_r. by rewrite HL'.
Qed.
diff --git a/orc11/progress.v b/orc11/progress.v
index 963b61fa..6f4e5e6d 100644
--- a/orc11/progress.v
+++ b/orc11/progress.v
@@ -638,7 +638,7 @@ Section AllocSteps.
Proof.
move => ð‘šs.
constructor; last done.
- - by rewrite map_length seq_length.
+ - by rewrite map_length length_seq.
- move => n' ð‘š Eq.
rewrite /ð‘šs /alloc_messages in Eq.
apply list_lookup_fmap_inv in Eq as [i [Eq1 [Eq2 Lt]%lookup_seq]].
@@ -755,7 +755,7 @@ Section AllocSteps.
Lemma dealloc_messages_length M n l:
length (dealloc_messages M n l) = n.
- Proof. by rewrite fmap_length seq_length. Qed.
+ Proof. by rewrite length_fmap length_seq. Qed.
Lemma dealloc_messages_eq_loc M n l :
∀ (n': nat) ð‘š, (dealloc_messages M n l) !! n' = Some 𑚠→ ð‘š.(mloc) = l >> n'.
@@ -801,7 +801,7 @@ Section AllocSteps.
move => ð‘šs.
have REMOVE:= dealloc_remove _ _ _ DEALLOC.
constructor; last done.
- - by rewrite map_length seq_length.
+ - by rewrite map_length length_seq.
- move => n' ð‘š Eq. rewrite /ð‘šs /dealloc_messages in Eq.
apply list_lookup_fmap_inv in Eq as [i [Eq1 [Eq2 Lt]%lookup_seq]].
simpl in Eq2. subst i.
--
GitLab