From 8ed17d99c6be8c1c5c369c3b6d92deba389b6676 Mon Sep 17 00:00:00 2001
From: Olivier Laurent
Date: Sun, 3 May 2020 11:43:18 +0200
Subject: add incl_map incl_filter NoDup_filter

---
 theories/Lists/List.v | 21 ++++++++++++++++++++-
 1 file changed, 20 insertions(+), 1 deletion(-)

(limited to 'theories/Lists')

diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 5d5f74db44..8798ee4fe5 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -2008,6 +2008,9 @@ Section SetIncl.
       now apply incl_cons_inv in Hin.
   Qed.
 
+  Lemma incl_filter f l : incl (filter f l) l.
+  Proof. intros x Hin; now apply filter_In in Hin. Qed.
+
   Lemma remove_incl (eq_dec : forall x y : A, {x = y} + {x <> y}) : forall l1 l2 x,
     incl l1 l2 -> incl (remove eq_dec x l1) (remove eq_dec x l2).
   Proof.
@@ -2018,8 +2021,15 @@ Section SetIncl.
 
 End SetIncl.
 
+Lemma incl_map A B (f : A -> B) l1 l2 : incl l1 l2 -> incl (map f l1) (map f l2).
+Proof.
+  intros Hincl x Hinx.
+  destruct (proj1 (in_map_iff _ _ _) Hinx) as [y [<- Hiny]].
+  apply in_map; intuition.
+Qed.
+
 Hint Resolve incl_refl incl_tl incl_tran incl_appl incl_appr incl_cons
-  incl_app: datatypes.
+  incl_app incl_map: datatypes.
 
 
 (**************************************)
@@ -2412,6 +2422,15 @@ Section ReDun.
     now apply Hnin, in_rev.
   Qed.
 
+  Lemma NoDup_filter f l : NoDup l -> NoDup (filter f l).
+  Proof.
+    induction l; simpl; intros Hnd; auto.
+    apply NoDup_cons_iff in Hnd.
+    destruct (f a); [ | intuition ].
+    apply NoDup_cons_iff; split; intuition.
+    apply filter_In in H; intuition.
+  Qed.
+
   (** Effective computation of a list without duplicates *)
 
   Hypothesis decA: forall x y : A, {x = y} + {x <> y}.
-- 
cgit v1.2.3