From fef9016bd3ca6544f0110bdbf8dbe6ca24120450 Mon Sep 17 00:00:00 2001
From: Oliver Nash
Date: Tue, 3 Sep 2019 20:38:16 +0100
Subject: Remove redundant parameter in List.concat_filter_map

---
 theories/Lists/List.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index f45317ba50..88c47b9744 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -1234,11 +1234,11 @@ End Fold_Right_Recursor.
       destruct (f x); simpl; now rewrite IH.
     Qed.
 
-    Lemma concat_filter_map : forall (l : list (list A)) (f : A -> bool),
+    Lemma concat_filter_map : forall (l : list (list A)),
       concat (map filter l) = filter (concat l).
     Proof.
       induction l as [| v l IHl]; [auto|].
-      simpl. rewrite (IHl f). rewrite filter_app. reflexivity.
+      simpl. rewrite IHl. rewrite filter_app. reflexivity.
     Qed.
 
   (** [find] *)
-- 
cgit v1.2.3


From 3d5eec61f7d150f3ac2d6e7785a6e6d31fe0c690 Mon Sep 17 00:00:00 2001
From: Oliver Nash
Date: Tue, 3 Sep 2019 20:38:52 +0100
Subject: Add lemmas directly relating List.nth and List.nth_error

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

diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 88c47b9744..38723e291f 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -536,6 +536,26 @@ Section Elts.
     simpl in *. apply IHn. auto with arith.
   Qed.
 
+  (** Results directly relating [nth] and [nth_error] *)
+
+  Lemma nth_error_nth : forall (l : list A) (n : nat) (x d : A),
+    nth_error l n = Some x -> nth n l d = x.
+  Proof.
+    intros l n x d H.
+    apply nth_error_split in H. destruct H as [l1 [l2 [H H']]].
+    subst. rewrite app_nth2; [|auto].
+    rewrite Nat.sub_diag. reflexivity.
+  Qed.
+
+  Lemma nth_error_nth' : forall (l : list A) (n : nat) (d : A),
+    n < length l -> nth_error l n = Some (nth n l d).
+  Proof.
+    intros l n d H.
+    apply nth_split with (d:=d) in H. destruct H as [l1 [l2 [H H']]].
+    subst. rewrite H. rewrite nth_error_app2; [|auto].
+    rewrite app_nth2; [| auto]. repeat (rewrite Nat.sub_diag). reflexivity.
+  Qed.
+
   (*****************)
   (** ** Remove    *)
   (*****************)
-- 
cgit v1.2.3


From 4297c81eaa43ae43bc4fc31ca19c695539b26b42 Mon Sep 17 00:00:00 2001
From: Oliver Nash
Date: Tue, 3 Sep 2019 20:50:35 +0100
Subject: Add changelog entry for 10731

---
 doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst b/doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst
index f68b2aaaa2..864c4e6a7e 100644
--- a/doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst
+++ b/doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst
@@ -1,4 +1,6 @@
-- New lemmas on :g:`combine`, :g:`filter`, and :g:`nodup` functions on lists. The lemma
-  :g:`filter_app` was moved to the :g:`List` module.
+- New lemmas on :g:`combine`, :g:`filter`, :g:`nodup`, :g:`nth`, and
+  :g:`nth_error` functions on lists. The lemma :g:`filter_app` was moved to the
+  :g:`List` module.
 
-  See `#10651 <https://github.com/coq/coq/pull/10651>`_, by Oliver Nash.
+  See `#10651 <https://github.com/coq/coq/pull/10651>`_, and
+  `#10731 <https://github.com/coq/coq/pull/10731>`_, by Oliver Nash.
-- 
cgit v1.2.3