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