From 0ffb8c121e3fcf24b9c83b75c340d09de0fc5799 Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Tue, 26 Jul 2022 20:39:11 +0200
Subject: [PATCH] Add list_lookup_imap_Some
---
theories/list.v | 6 ++++++
1 file changed, 6 insertions(+)
diff --git a/theories/list.v b/theories/list.v
index 0d550335..76a79743 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -3932,6 +3932,9 @@ Section fmap.
Proof. intros; induction l; f_equal/=; auto. Qed.
Lemma list_lookup_fmap l i : (f <$> l) !! i = f <$> (l !! i).
Proof. revert i. induction l; intros [|n]; by try revert n. Qed.
+ Lemma list_lookup_fmap_Some l i x :
+ (f <$> l) !! i = Some x ↔ ∃ y, l !! i = Some y ∧ x = f y.
+ Proof. by rewrite list_lookup_fmap, fmap_Some. Qed.
Lemma list_lookup_total_fmap `{!Inhabited A, !Inhabited B} l i :
i < length l → (f <$> l) !!! i = f (l !!! i).
Proof.
@@ -4290,6 +4293,9 @@ Section imap.
revert f i. induction l as [|x l IH]; intros f [|i]; f_equal/=; auto.
by rewrite IH.
Qed.
+ Lemma list_lookup_imap_Some l i x :
+ imap f l !! i = Some x ↔ ∃ y, l !! i = Some y ∧ x = f i y.
+ Proof. by rewrite list_lookup_imap, fmap_Some. Qed.
Lemma list_lookup_total_imap `{!Inhabited A, !Inhabited B} l i :
i < length l → imap f l !!! i = f i (l !!! i).
Proof.
--
GitLab