From 80bc39658c3f7c5c4c1f0b7980ec03fd0d6428f1 Mon Sep 17 00:00:00 2001
From: Jonas Kastberg Hinrichsen <jihgfee@gmail.com>
Date: Wed, 12 Jan 2022 14:59:24 +0100
Subject: [PATCH] Added some useful lemmas about [list_subseteq]

---
 theories/list.v | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/theories/list.v b/theories/list.v
index 3b056468..13188cc8 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -2743,6 +2743,26 @@ Proof.
   rewrite <-(elem_of_nil x).
   apply Hl, elem_of_cons. by left.
 Qed.
+Lemma list_subseteq_cons x l1 l2 : l1 ⊆ l2 → x :: l1 ⊆ x :: l2 .
+Proof.
+  intros Hin y Hy%elem_of_cons.
+  destruct Hy as [-> | Hy]; [by left|]. right. by apply Hin.
+Qed.
+Lemma list_subseteq_cons_r x l1 l2 : l1 ⊆ l2 → l1 ⊆ x :: l2.
+Proof. intros Hin y Hy. right. by apply Hin. Qed.
+Lemma list_delete_subseteq i l : delete i l ⊆ l.
+Proof.
+  revert i. induction l as [|x l IHl]; intros i; [done|].
+  destruct i as [|i];
+    [by apply list_subseteq_cons_r|by apply list_subseteq_cons].
+Qed.
+Lemma filter_subseteq P `{! ∀ x : A, Decision (P x)} l :
+  filter P l ⊆ l.
+Proof.
+  induction l as [|x l IHl]; [done|]. rewrite filter_cons.
+  destruct (decide (P x));
+    [by apply list_subseteq_cons|by apply list_subseteq_cons_r].
+Qed.
 
 Global Instance list_subseteq_Permutation: Proper ((≡ₚ) ==> (≡ₚ) ==> (↔)) (⊆@{list A}) .
 Proof. intros l1 l2 Hl k1 k2 Hk. apply forall_proper; intros x. by rewrite Hl, Hk. Qed.
-- 
GitLab