add a function to obtain a set with all elements of a finite type

This lets us use the existing nice gmap/gset infrastructure even for total functions when the domain type is finite.

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,22 @@ 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.
+
+  Global Instance set_unfold_fin_to_set a :
+    SetUnfoldElemOf a (fin_to_set A) True.
+  Proof. constructor. split; auto using elem_of_fin_to_set. Qed.
+End fin_to_set.
+
 
 (** * Guard *)
 Global Instance set_guard `{MonadSet M} : MGuard M :=