From 4ff965b26be968461cb58f84dfc51d66d9da04c3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 25 Jun 2019 17:25:00 +0200
Subject: [PATCH] `SetUnfold` instances for `reverse` and `fmap` on lists.

This closes issue #36.
---
 theories/sets.v | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/theories/sets.v b/theories/sets.v
index 015b98d6..ff784222 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -286,6 +286,18 @@ Section set_unfold_list.
     constructor; unfold subseteq, list_subseteq.
     apply forall_proper; naive_solver.
   Qed.
+
+  Global Instance set_unfold_reverse x l P :
+    SetUnfoldElemOf x l P → SetUnfoldElemOf x (reverse l) P.
+  Proof. constructor. by rewrite elem_of_reverse, (set_unfold_elem_of x l P). Qed.
+
+  Global Instance set_unfold_list_fmap {B} (f : A → B) l P :
+    (∀ y, SetUnfoldElemOf y l (P y)) →
+    SetUnfoldElemOf x (f <$> l) (∃ y, x = f y ∧ P y).
+  Proof.
+    constructor. rewrite elem_of_list_fmap. f_equiv; intros y.
+    by rewrite (set_unfold_elem_of y l (P y)).
+  Qed.
 End set_unfold_list.
 
 Ltac set_unfold :=
-- 
GitLab