From 221197c43d43ce34b211068b84eff0ec4a9ee57a Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Sun, 20 Feb 2022 17:23:34 +0100
Subject: [PATCH] Add set_unfold_list_bind (+ test)

`set_unfold_bind` for sets already exists; this brings the list variant on par.
---
 tests/sets.v    | 5 +++++
 theories/sets.v | 4 ++++
 2 files changed, 9 insertions(+)

diff --git a/tests/sets.v b/tests/sets.v
index 9aea1a62..9939a187 100644
--- a/tests/sets.v
+++ b/tests/sets.v
@@ -2,3 +2,8 @@ From stdpp Require Import sets.
 
 Lemma foo `{Set_ A C} (x : A) (X Y : C) : x ∈ X ∩ Y → x ∈ X.
 Proof. intros Hx. set_unfold in Hx. tauto. Qed.
+
+(** Test [set_unfold_list_bind]. *)
+Lemma elem_of_list_bind_again {A B} (x : B) (l : list A) f :
+  x ∈ l ≫= f ↔ ∃ y, x ∈ f y ∧ y ∈ l.
+Proof. set_solver. Qed.
diff --git a/theories/sets.v b/theories/sets.v
index 6152085c..ec22d0c2 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -308,6 +308,10 @@ Section set_unfold_list.
     SetUnfoldElemOf x l P → SetUnfoldElemOf x (rotate n l) P.
   Proof. constructor. by rewrite elem_of_rotate, (set_unfold_elem_of x l P). Qed.
 
+  Global Instance set_unfold_list_bind {B} (f : A → list B) l P Q y :
+    (∀ x, SetUnfoldElemOf x l (P x)) → (∀ x, SetUnfoldElemOf y (f x) (Q x)) →
+    SetUnfoldElemOf y (l ≫= f) (∃ x, Q x ∧ P x).
+  Proof. constructor. rewrite elem_of_list_bind. naive_solver. Qed.
 End set_unfold_list.
 
 Tactic Notation "set_unfold" :=
-- 
GitLab