From 05bf88b79cdd537529d0e5c02b0e129f4882d285 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 7 Jul 2019 21:25:23 +0200
Subject: [PATCH] prove list_find_proper

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

diff --git a/theories/list.v b/theories/list.v
index 23f31c0d..33d15d59 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -916,6 +916,14 @@ Section find.
     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.
+
+  Lemma list_find_proper (Q : A → Prop) `{∀ x, Decision (Q x)} l :
+    (∀ x, P x ↔ Q x) →
+    list_find P l = list_find Q l.
+  Proof.
+    intros HPQ. induction l as [|x y IH]; [done|]. simpl.
+    erewrite decide_iff by done. by rewrite IH.
+  Qed.
 End find.
 
 (** ** Properties of the [reverse] function *)
-- 
GitLab