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

---
 .../12237-list-more-filter-incl.rst                 |  4 ++++
 theories/Lists/List.v                               | 21 ++++++++++++++++++++-
 2 files changed, 24 insertions(+), 1 deletion(-)
 create mode 100644 doc/changelog/10-standard-library/12237-list-more-filter-incl.rst

diff --git a/doc/changelog/10-standard-library/12237-list-more-filter-incl.rst b/doc/changelog/10-standard-library/12237-list-more-filter-incl.rst
new file mode 100644
index 0000000000..7b4b0e86d3
--- /dev/null
+++ b/doc/changelog/10-standard-library/12237-list-more-filter-incl.rst
@@ -0,0 +1,4 @@
+- **Added:**
+  new lemmas in ``List``: ``incl_map``, ``incl_filter``, ``NoDup_filter``
+  (`#12237 <https://github.com/coq/coq/pull/12237>`_,
+  by Olivier Laurent).
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


From 14e5b1ac33f268d50ca379a12bfc729f6183161e Mon Sep 17 00:00:00 2001
From: Olivier Laurent
Date: Sun, 3 May 2020 22:01:45 +0200
Subject: strenghten nth_ext

---
 theories/Lists/List.v | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 8798ee4fe5..e4b87507f4 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -517,18 +517,20 @@ Section Elts.
       exists (a::l1); exists l2; simpl; split; now f_equal.
   Qed.
 
-  Lemma nth_ext : forall l l' d, length l = length l' ->
-    (forall n, nth n l d = nth n l' d) -> l = l'.
+  Lemma nth_ext : forall l l' d d', length l = length l' ->
+    (forall n, n < length l -> nth n l d = nth n l' d') -> l = l'.
   Proof.
-    induction l; intros l' d Hlen Hnth; destruct l' as [| b l'].
+    induction l; intros l' d d' Hlen Hnth; destruct l' as [| b l'].
     - reflexivity.
     - inversion Hlen.
     - inversion Hlen.
     - change a with (nth 0 (a :: l) d).
-      change b with (nth 0 (b :: l') d).
+      change b with (nth 0 (b :: l') d').
       rewrite Hnth; f_equal.
-      apply IHl with d; [ now inversion Hlen | ].
-      intros n; apply (Hnth (S n)).
+      + apply IHl with d d'; [ now inversion Hlen | ].
+        intros n Hlen'; apply (Hnth (S n)).
+        now simpl; apply lt_n_S.
+      + simpl; apply Nat.lt_0_succ.
   Qed.
 
   (** Results about [nth_error] *)
-- 
cgit v1.2.3


From 1a11eaddca057bea4e1ea0b3c276fc5228e5b4b2 Mon Sep 17 00:00:00 2001
From: Olivier Laurent
Date: Mon, 4 May 2020 10:48:30 +0200
Subject: add incl_Forall_in_iff

---
 doc/changelog/10-standard-library/12237-list-more-filter-incl.rst | 2 +-
 theories/Lists/List.v                                             | 4 ++++
 2 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/doc/changelog/10-standard-library/12237-list-more-filter-incl.rst b/doc/changelog/10-standard-library/12237-list-more-filter-incl.rst
index 7b4b0e86d3..37aaf697b5 100644
--- a/doc/changelog/10-standard-library/12237-list-more-filter-incl.rst
+++ b/doc/changelog/10-standard-library/12237-list-more-filter-incl.rst
@@ -1,4 +1,4 @@
 - **Added:**
-  new lemmas in ``List``: ``incl_map``, ``incl_filter``, ``NoDup_filter``
+  new lemmas in ``List``: ``incl_map``, ``incl_filter``, ``NoDup_filter``, ``incl_Forall_in_iff``
   (`#12237 <https://github.com/coq/coq/pull/12237>`_,
   by Olivier Laurent).
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index e4b87507f4..bdaaa91828 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -2968,6 +2968,10 @@ Section Exists_Forall.
     now apply neg_Forall_Exists_neg.
   Defined.
 
+  Lemma incl_Forall_in_iff l l' :
+    incl l l' <-> Forall (fun x => In x l') l.
+  Proof. now rewrite Forall_forall; split. Qed.
+
 End Exists_Forall.
 
 Hint Constructors Exists : core.
-- 
cgit v1.2.3