From 3cbd41e4720e20ae2ecdcf95dc8f1242a979173b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 2 Jun 2015 20:56:31 +0200
Subject: [PATCH] Conversion list -> collection.

---
 theories/collections.v | 25 +++++++++++++++++++------
 1 file changed, 19 insertions(+), 6 deletions(-)

diff --git a/theories/collections.v b/theories/collections.v
index 71695303..45282d1a 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -93,14 +93,27 @@ Section simple_collection.
   End dec.
 End simple_collection.
 
-Definition of_option `{Singleton A C} `{Empty C} (x : option A) : C :=
+Definition of_option `{Singleton A C, Empty C} (x : option A) : C :=
   match x with None => ∅ | Some a => {[ a ]} end.
+Fixpoint of_list `{Singleton A C, Empty C, Union C} (l : list A) : C :=
+  match l with [] => ∅ | x :: l => {[ x ]} ∪ of_list l end.
 
-Lemma elem_of_of_option `{SimpleCollection A C} (x : A) o :
-  x ∈ of_option o ↔ o = Some x.
-Proof.
-  destruct o; simpl; rewrite ?elem_of_empty, ?elem_of_singleton; naive_solver.
-Qed.
+Section of_option_list.
+  Context `{SimpleCollection A C}.
+  Lemma elem_of_of_option (x : A) o : x ∈ of_option o ↔ o = Some x.
+  Proof.
+    destruct o; simpl;
+      rewrite ?elem_of_empty, ?elem_of_singleton; naive_solver.
+  Qed.
+  Lemma elem_of_of_list (x : A) l : x ∈ of_list l ↔ x ∈ l.
+  Proof.
+    split.
+    * induction l; simpl; [by rewrite elem_of_empty|].
+      rewrite elem_of_union, elem_of_singleton;
+        intros [->|?]; constructor (auto).
+    * induction 1; simpl; rewrite elem_of_union, elem_of_singleton; auto.
+  Qed.
+End of_option_list.
 
 Global Instance collection_guard `{CollectionMonad M} : MGuard M :=
   λ P dec A x, match dec with left H => x H | _ => ∅ end.
-- 
GitLab