<p>I usually use</p>
<pre><code>Definition finite X : Prop := exists l, forall x : X, In x l.
Definition fin {X} (P : X -&gt; Prop) := exists l, forall x, P x &lt;-&gt; In x l.
</code></pre>
<p>These ones have quite good properties.</p>

CC BY-SA 4.0
2024-09-03T09:33:17.830Z
2024-09-03T09:33:17.830Z
Dominique Larchey-Wendling
<p>I am a beginner and trying to figure out how to work with finite sets and maps in Coq. I want to define an inductive type X with a single constructor that takes as an argument a finite set of elements of type X, for example:</p>
<p>Inductive X : Set :=
| constr : FinSet X -&gt; X.</p>
<p>I am unsure which data structure to use for finite sets here. I looked into the std++ library but do not understand the data structure provided there: Set_ seems to require two types, A and C, and I do not know why the second type C is needed. Ideally I want a finite set constructor that takes one type as an argument (the type of elements), which is countable but not necessarily ordered. I am a beginner so I have a hard time reading Coq library files; can someone maybe post a code snippet? Thank you.</p>

CC BY-SA 4.0
2024-09-02T16:53:33.390Z
In `stdpp` the type you want to use is `gset`, defined in `gmap.v`.
JoJoModding
CC BY-SA 4.0
2024-09-02T17:09:09.470Z
@JoJoModding Thank you, I tried it but it does not work: Unable to satisfy the following constraints:
In environment:
X : Type

?EqDecision0 : "base.RelDecision eq"

?H : "countable.Countable X"

It seems the issue is that by using gset inside an inductive definition, Coq does not automatically derive countability.
anonymous
CC BY-SA 4.0
2024-09-02T17:17:43.413Z
Ah, yes, it does not. That is unfortunate, but I don't think this can be fixed.
JoJoModding
CC BY-SA 4.0
2024-09-04T15:40:56.347Z
This is not a research-level question in theoretical computer science, so it does not belong here. But it does belong on https://proofassistants.stackexchange.com, so perhaps you should ask it there instead.
Andrej Bauer
<coq>
Finite sets in Coq
anonymous
# Finite sets in Coq

(Asked by: username_0 on 2024-09-02)

I am a beginner and trying to figure out how to work with finite sets and maps in Coq. I want to define an inductive type X with a single constructor that takes as an argument a finite set of elements of type X, for example:

Inductive X : Set :=
| constr : FinSet X -> X.

I am unsure which data structure to use for finite sets here. I looked into the std++ library but do not understand the data structure provided there: Set\_ seems to require two types, A and C, and I do not know why the second type C is needed. Ideally I want a finite set constructor that takes one type as an argument (the type of elements), which is countable but not necessarily ordered. I am a beginner so I have a hard time reading Coq library files; can someone maybe post a code snippet? Thank you.

**Tags:** coq

> **Comments:**
> **username_1**: In `stdpp` the type you want to use is `gset`, defined in `gmap.v`.  
> **username_0**: @username_1 Thank you, I tried it but it does not work: Unable to satisfy the following constraints: In environment: X : Type  ?EqDecision0 : "base.RelDecision eq"  ?H : "countable.Countable X"  It seems the issue is that by using gset inside an inductive definition, Coq does not automatically derive countability.  
> **username_1**: Ah, yes, it does not. That is unfortunate, but I don't think this can be fixed.  
> **username_2**: This is not a research-level question in theoretical computer science, so it does not belong here. But it does belong on https://proofassistants.stackexchange.com, so perhaps you should ask it there instead.  

---

## 1 answers

### Answer by username_3 on 2024-09-03. Score: 0

I usually use
Definition finite X : Prop := exists l, forall x : X, In x l.
Definition fin {X} (P : X -> Prop) := exists l, forall x, P x <-> In x l.

These ones have quite good properties.


---

