From cdcfeee83ddef343f5bb92ae1167fa0c123bccfa Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 14 Dec 2016 18:31:15 +0100
Subject: [PATCH] list: relate nth and lookup

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

diff --git a/theories/list.v b/theories/list.v
index b17af16f..020a84ac 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -477,6 +477,26 @@ Lemma list_lookup_middle l1 l2 x n :
   n = length l1 → (l1 ++ x :: l2) !! n = Some x.
 Proof. intros ->. by induction l1. Qed.
 
+Lemma nth_lookup_or_length l i d :
+  {l !! i = Some (nth i l d)} + {(length l ≤ i)%nat}.
+Proof.
+  revert i; induction l; intros i.
+  - right. simpl. omega.
+  - destruct i; simpl.
+    + left. done.
+    + destruct (IHl i) as [->|]; [by left|].
+      right. omega.
+Qed.
+
+Lemma nth_lookup l i d x :
+  l !! i = Some x → nth i l d = x.
+Proof.
+  revert i; induction l; intros i; [done|].
+  destruct i; simpl.
+  - congruence.
+  - apply IHl.
+Qed.
+
 Lemma list_insert_alter l i x : <[i:=x]>l = alter (λ _, x) i l.
 Proof. by revert i; induction l; intros []; intros; f_equal/=. Qed.
 Lemma alter_length f l i : length (alter f i l) = length l.
-- 
GitLab