From ef734bd6b457315a592a9d72cf7e5b2ad0b23657 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 10 Jan 2023 14:35:29 +0100
Subject: [PATCH] more list subseteq lemmas (some of them from Perennial)

---
 stdpp/list.v | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/stdpp/list.v b/stdpp/list.v
index 12db6e64..ac0f3620 100644
--- a/stdpp/list.v
+++ b/stdpp/list.v
@@ -3651,6 +3651,18 @@ Proof.
 Qed.
 Lemma list_subseteq_cons x l1 l2 : l1 ⊆ l2 → l1 ⊆ x :: l2.
 Proof. intros Hin y Hy. right. by apply Hin. Qed.
+Lemma list_subseteq_app_l l1 l2 l : l1 ⊆ l2 → l1 ⊆ l2 ++ l.
+Proof. unfold subseteq, list_subseteq. setoid_rewrite elem_of_app. naive_solver. Qed.
+Lemma list_subseteq_app_r l1 l2 l : l1 ⊆ l2 → l1 ⊆ l ++ l2.
+Proof. unfold subseteq, list_subseteq. setoid_rewrite elem_of_app. naive_solver. Qed.
+
+Lemma list_app_subseteq l1 l2 l :
+  l1 ++ l2 ⊆ l ↔ l1 ⊆ l ∧ l2 ⊆ l.
+Proof. unfold subseteq, list_subseteq. setoid_rewrite elem_of_app. naive_solver. Qed.
+Lemma list_cons_subseteq x l1 l2 :
+  x :: l1 ⊆ l2 ↔ x ∈ l2 ∧ l1 ⊆ l2.
+Proof. unfold subseteq, list_subseteq. setoid_rewrite elem_of_cons. naive_solver. Qed.
+
 Lemma list_delete_subseteq i l : delete i l ⊆ l.
 Proof.
   revert i. induction l as [|x l IHl]; intros i; [done|].
@@ -3664,6 +3676,10 @@ Proof.
   destruct (decide (P x));
     [by apply list_subseteq_skip|by apply list_subseteq_cons].
 Qed.
+Lemma drop_subseteq n l : drop n l ⊆ l.
+Proof. rewrite <-(take_drop n l) at 2. apply list_subseteq_app_r. done. Qed.
+Lemma take_subseteq n l : take n l ⊆ l.
+Proof. rewrite <-(take_drop n l) at 2. apply list_subseteq_app_l. done. Qed.
 
 Global Instance list_subseteq_Permutation:
   Proper ((≡ₚ) ==> (≡ₚ) ==> (↔)) (⊆@{list A}) .
-- 
GitLab