From 997c3ed8176d71c76fd8637331a6e9caaa74b248 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Wed, 14 Dec 2016 18:31:15 +0100 Subject: [PATCH] list: relate nth and lookup --- theories/prelude/list.v | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/theories/prelude/list.v b/theories/prelude/list.v index dbd6e73b..4348af93 100644 --- a/theories/prelude/list.v +++ b/theories/prelude/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