From 97ab0949d9b4ee67f02b095b94d31c6f22c56479 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 7 Jul 2019 21:18:59 +0200
Subject: [PATCH] prove list_find_fmap

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

diff --git a/theories/list.v b/theories/list.v
index abadc41f..23f31c0d 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -907,6 +907,15 @@ Section find.
     induction 1 as [|x y l ? IH]; intros; simplify_option_eq; eauto.
     by destruct IH as [[i x'] ->]; [|exists (S i, x')].
   Qed.
+
+  Lemma list_find_fmap {B : Type} (f : B → A) (l : list B) :
+    list_find P (f <$> l) = prod_map id f <$> list_find (P ∘ f) l.
+  Proof.
+    induction l as [|x y IH]; [done|]. simpl.
+    case_decide; [done|].
+    change (list_fmap B A f y) with (f <$> y). (* FIXME it simplified too much *)
+    rewrite IH. by destruct (list_find (P ∘ f) y).
+  Qed.
 End find.
 
 (** ** Properties of the [reverse] function *)
-- 
GitLab