From 90d706901746925bee0e69a56dade96d1d32b7cc Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 28 Jul 2021 14:21:45 +0200
Subject: [PATCH] add lookup_take_Some

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

diff --git a/theories/list.v b/theories/list.v
index 9a52d687..29e1b750 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -1195,6 +1195,7 @@ Lemma take_drop_commute l n m : take n (drop m l) = drop m (take (m + n) l).
 Proof.
   revert n m. induction l; intros [|?][|?]; simpl; auto using take_nil with lia.
 Qed.
+
 Lemma lookup_take l n i : i < n → take n l !! i = l !! i.
 Proof. revert n i. induction l; intros [|n] [|i] ?; simpl; auto with lia. Qed.
 Lemma lookup_total_take `{!Inhabited A} l n i : i < n → take n l !!! i = l !!! i.
@@ -1203,6 +1204,15 @@ Lemma lookup_take_ge l n i : n ≤ i → take n l !! i = None.
 Proof. revert n i. induction l; intros [|?] [|?] ?; simpl; auto with lia. Qed.
 Lemma lookup_total_take_ge `{!Inhabited A} l n i : n ≤ i → take n l !!! i = inhabitant.
 Proof. intros. by rewrite list_lookup_total_alt, lookup_take_ge. Qed.
+Lemma lookup_take_Some l n i a : take n l !! i = Some a ↔ l !! i = Some a ∧ i < n.
+Proof.
+  split.
+  - destruct (decide (i < n)).
+    + rewrite lookup_take; naive_solver.
+    + rewrite lookup_take_ge; [done|lia].
+  - intros [??]. by rewrite lookup_take.
+Qed.
+
 Lemma take_alter f l n i : n ≤ i → take n (alter f i l) = take n l.
 Proof.
   intros. apply list_eq. intros j. destruct (le_lt_dec n j).
-- 
GitLab