From c033e7dfa2bc96c1642cf7e5289e3e9f09a4a697 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 10 Jan 2023 14:12:49 +0100
Subject: [PATCH] port some list lemmas from Perennial
---
stdpp/list.v | 18 ++++++++++++++++++
stdpp/list_numbers.v | 24 ++++++++++++++++++------
2 files changed, 36 insertions(+), 6 deletions(-)
diff --git a/stdpp/list.v b/stdpp/list.v
index 079a8133..12db6e64 100644
--- a/stdpp/list.v
+++ b/stdpp/list.v
@@ -2135,6 +2135,12 @@ Proof. rewrite <-(take_drop n l) at 2. apply prefix_app_r. done. Qed.
Lemma prefix_lookup l1 l2 i x :
l1 !! i = Some x → l1 `prefix_of` l2 → l2 !! i = Some x.
Proof. intros ? [k ->]. rewrite lookup_app_l; eauto using lookup_lt_Some. Qed.
+Lemma prefix_lookup_lt l1 l2 i :
+ i < length l1 → l1 `prefix_of` l2 → l1 !! i = l2 !! i.
+Proof.
+ intros Hlt Hprefix. apply lookup_lt_is_Some_2 in Hlt as [? Hlookup].
+ rewrite Hlookup. eapply prefix_lookup in Hlookup; eauto.
+Qed.
Lemma prefix_length l1 l2 : l1 `prefix_of` l2 → length l1 ≤ length l2.
Proof. intros [? ->]. rewrite app_length. lia. Qed.
Lemma prefix_snoc_not l x : ¬l ++ [x] `prefix_of` l.
@@ -2181,6 +2187,18 @@ Proof.
apply not_elem_of_app_cons_inv_l in Hle; [|done..]. unfold prefix. naive_solver.
Qed.
+Lemma list_prefix_eq l1 l2 :
+ l1 `prefix_of` l2 → length l2 ≤ length l1 → l1 = l2.
+Proof.
+ intros Hprefix Hlen.
+ assert (length l1 = length l2).
+ { apply prefix_length in Hprefix; lia. }
+ eapply list_eq_same_length; [ done | done | ].
+ intros i x y ? Hlookup1 Hlookup2.
+ eapply prefix_lookup in Hlookup1; eauto.
+ congruence.
+Qed.
+
Section prefix_ops.
Context `{!EqDecision A}.
Lemma max_prefix_fst l1 l2 :
diff --git a/stdpp/list_numbers.v b/stdpp/list_numbers.v
index 4d347802..aea79e12 100644
--- a/stdpp/list_numbers.v
+++ b/stdpp/list_numbers.v
@@ -87,12 +87,6 @@ Section seq.
Qed.
Lemma NoDup_seq j n : NoDup (seq j n).
Proof. apply NoDup_ListNoDup, seq_NoDup. Qed.
- (* FIXME: This lemma is in the stdlib since Coq 8.12 *)
- Lemma seq_S n j : seq j (S n) = seq j n ++ [j + n].
- Proof.
- revert j. induction n as [|n IH]; intros j; f_equal/=; [done |].
- by rewrite IH, Nat.add_succ_r.
- Qed.
Lemma elem_of_seq j n k :
k ∈ seq j n ↔ j ≤ k < j + n.
@@ -101,6 +95,24 @@ Section seq.
Lemma Forall_seq (P : nat → Prop) i n :
Forall P (seq i n) ↔ ∀ j, i ≤ j < i + n → P j.
Proof. rewrite Forall_forall. setoid_rewrite elem_of_seq. auto with lia. Qed.
+
+ Lemma drop_seq j n m :
+ drop m (seq j n) = seq (j + m) (n - m).
+ Proof.
+ revert j m. induction n as [|n IH]; simpl; intros j m.
+ - rewrite drop_nil. done.
+ - destruct m; simpl.
+ + rewrite Nat.add_0_r. done.
+ + rewrite IH. f_equal; lia.
+ Qed.
+ Lemma take_seq j n m :
+ take m (seq j n) = seq j (m `min` n).
+ Proof.
+ revert j m. induction n as [|n IH]; simpl; intros j m.
+ - rewrite take_nil. replace (m `min` 0) with 0 by lia. done.
+ - destruct m; simpl. 1:done.
+ rewrite IH. done.
+ Qed.
End seq.
(** ** Properties of the [seqZ] function *)
--
GitLab