From 1f024e5290defd1ac0d902c711e9c3c8b8f79341 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 28 Oct 2020 18:09:37 +0100
Subject: [PATCH] add a way to obtain a set with all elements of a finite type

---
 theories/sets.v | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

diff --git a/theories/sets.v b/theories/sets.v
index 251f9898..3a81880c 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -2,7 +2,7 @@
 importantly, it implements some tactics to automatically solve goals involving
 sets. *)
 From stdpp Require Export orders list list_numbers.
-From stdpp Require Import options.
+From stdpp Require Import options finite.
 
 (* FIXME: This file needs a 'Proof Using' hint, but they need to be set
 locally (or things moved out of sections) as no default works well enough. *)
@@ -873,6 +873,18 @@ Section option_and_list_to_set.
   Proof. induction 1; set_solver. Qed.
 End option_and_list_to_set.
 
+(** * Finite types to sets. *)
+Definition fin_to_set (A : Type) `{SemiSet A C, Finite A} : C :=
+  list_to_set (enum A).
+
+Section fin_to_set.
+  Context `{SemiSet A C, Finite A}.
+  Implicit Types a : A.
+
+  Lemma elem_of_fin_to_set a : a ∈ fin_to_set A.
+  Proof. apply elem_of_list_to_set, elem_of_enum. Qed.
+End fin_to_set.
+
 
 (** * Guard *)
 Global Instance set_guard `{MonadSet M} : MGuard M :=
-- 
GitLab