<p>There are many variants of finite sets in constructive mathematics. One that can be defined using just inductive definitions, and is therefore amenable to formalization in type theory, is the <a href="https://dialnet.unirioja.es/descarga/articulo/3217816.pdf" rel="nofollow noreferrer">Noetherian finiteness</a> by Thierry Coquand and Arnaud Spiwack. The idea is to define a set or a type <span class="math-container">$A$</span> to be finite if the following holds: every sequence <span class="math-container">$a : \mathbb{N} \to A$</span> contains a duplicate. The trick is to express an equivalent condition using inductive definitions, so that we get an induction principle for reasoning about such sets.</p>
<p>The definition of Noetherian finiteness from section 2.3 of the linked paper can be translated to Coq like this:</p>
<pre><code>(* [occurs x l] states that x appears in the list l *)
Inductive occurs {A : Type} : A -&gt; list A -&gt; Type :=
  | occurs_head : forall x k, occurs x (cons x k)
  | occurs_tail : forall x y k, occurs x k -&gt; occurs x (cons y k).

(* [has_duplicates l] states that [l] has a duplicate, i.e., that an element appears in it twice. *)
Inductive has_duplicates {A : Type} : list A -&gt; Type :=
  | has_duplicates_head : forall x l, occurs x l -&gt; has_duplicates (cons x l)
  | has_duplicates_tail : forall x l, has_duplicates l -&gt; has_duplicates (cons x l).

(* An auxiliary definition: a list `l` is said to be `noetherian` if it contains a duplicate, or if every extension of `l` by one element is `noetherian`. *)
Inductive noetherian (A : Type) : list A -&gt; Type :=
  | N_duplicates : forall l, has_duplicates l -&gt; noetherian A l
  | N_step : forall l, (forall a, noetherian A (cons a l)) -&gt; noetherian A l.

Definition NoetherianFinite A := noetherian A nil.
</code></pre>
<p>If you're willing to use quotient types or the higher inductive types from homotopy type theory, then you can have a look at the defintion of finite sets <a href="http://hott.github.io/HoTT/coqdoc-html/HoTT.Spaces.Finite.html#Finite" rel="nofollow noreferrer">Finite</a> in the HoTT library. It says that a type <code>X</code> is finite if there is a number <code>n</code> such that <code>X</code> is merely equivalent to the standard finite set <code>{0, 1, ..., n-1}</code>. The word &quot;merely&quot; here means that we <a href="https://www.cs.bham.ac.uk/%7Emhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html#truncation" rel="nofollow noreferrer">truncate</a> the existence, i.e.,
<span class="math-container">$$\textstyle\mathsf{Finite}\, X \mathrel{{:}{=}}
\sum_{n : \mathbb{N}} \left\| X \simeq \mathsf{Fin}\,n\right\|$$</span>
where <span class="math-container">$\mathsf{Fin}\,n$</span> is the standard finite set <span class="math-container">$\sum_{k : \mathbb{N}} (k &lt; n)$</span>.</p>

CC BY-SA 4.0
2020-05-05T13:49:58.690Z
Thanks for the pointers to both the Coq definition and the HoTT based definition. Can you give me some intuition about where my intuition that "(a)sets cannot be equationally reasoned with but (b) inductive definiitions can" breaks? Does (a) break, or (b), or both?
Siddharth Bhat
CC BY-SA 4.0
2020-05-05T18:02:16.827Z
Finite sets can be equationally reasoned *about* because the finite subsets of a type $A$ are the commutative monoid freely generated by $A$. So there will be equations (of the commutative monoid) and an induction principle (the free generation).
Andrej Bauer
CC BY-SA 4.0
2020-05-05T19:55:59.243Z
It is unclear to me why they correspond to the free commutative monoid. Won't the free commutative monoid of a type $S$ with inhabitants $a:S, b:S$ contain terms such as $\epsilon, a, b, ab, a^2, b^2, a^2b^2\dots$, while the subsets of $S$ are only $\epsilon, a, b, ab$?
Siddharth Bhat
CC BY-SA 4.0
2020-05-06T08:54:25.593Z
Oops, its the free *idempotent* commutative monoid, i.e., $x^2 = x$ for all $x$. Without idempotence we get *mutisets*.
Andrej Bauer
CC BY-SA 4.0
2020-05-06T14:43:18.780Z
OK, I agree that idempotent works. However, isn't the problem the same --- how does one impose idempotency within an inductive type? That then circles back to the clever construction you gave above, is my current understanding of the story?
Siddharth Bhat
CC BY-SA 4.0
2020-05-06T18:03:34.797Z
You asked if there are reasoning principles. The answer is "yes, the equations of a semilattice (which is what an idempotent commutative monoid is), and an induction principle". If a given framework can't handle the reasoning, that's the problem for the framework, the reasoning principles still are there.
Andrej Bauer
CC BY-SA 4.0
2020-05-05T09:05:19.987Z
2023-04-25T19:06:15.403Z
2023-04-25T19:06:15.403Z
Andrej Bauer
<p>To represent finite sets within coq, we either use something like <a href="https://www.cs.yale.edu/flint/cs428/coq/library/Coq.Lists.ListSet.html" rel="nofollow noreferrer"><code>ListSet</code></a>, which are just definitions on top of <code>list</code>, or we build something like <a href="http://compcert.inria.fr/doc-1.6/html/Maps.html#MAP" rel="nofollow noreferrer"><code>Compcert.Map</code></a>, and then we define a <code>set A</code> as a <code>map</code> from <code>A</code> to <code>()</code>.</p>

<p>However, neither of these approaches manage to define sets <em>inductively</em>. What I want to know is a way to define a set type in the form of:</p>

<pre><code>Inductive set (A: Type) : Type := 
 nil: set A | add: A -&gt; set A -&gt; &lt;fill in the blanks&gt; -&gt; set A
</code></pre>

<p>Is it possible to have such an "inductive definition" for finite sets? If not, can I be supplied with a proof of why not?</p>

<p>My intuition is that such a thing is not possible, because an inductive type allows for equational reasoning, while sets cannot be equationally reasoned with:</p>

<p><span class="math-container">$$
\texttt{add}~(1, \emptyset) = \texttt{add}(1, \texttt{add}(1, \emptyset)) \quad \text{(union is idempotent.)}
$$</span></p>

<p>however:</p>

<pre><code>add 1 (add 1 nil) &lt;&gt; add 1 nil 
</code></pre>

<p>So we will always have to go through some "extensional interface". Unfortunately, I don't know how to <em>prove</em> such a thing!</p>

CC BY-SA 4.0
2020-05-04T14:22:33.940Z
You might like to look into "quotient types" (and higher-inductive types, which are a kind of generalization of quotients).  Another approach might be to make your `add` constructor take a proof that the new element is not yet in the set (which you might be able to define as an inductive-recursive definition).
Stefan
CC BY-SA 4.0
2020-05-04T15:18:23.453Z
Can you show me how to write the inductive-recursive definition? I'd be glad if you could. Regarding quotient types: Right, I'd forgotten about their existence! I guess I can encode this in cubical agda? (cubical so the quotients are computable)
Siddharth Bhat
<type-theory><dependent-type><coq><formal-methods>
Defining finite sets inductively in a proof assistant?
Siddharth Bhat
# Defining finite sets inductively in a proof assistant?

(Asked by: username_0 on 2020-05-04)

To represent finite sets within coq, we either use something like ListSet, which are just definitions on top of list, or we build something like Compcert.Map, and then we define a set A as a map from A to ().
However, neither of these approaches manage to define sets inductively. What I want to know is a way to define a set type in the form of:
Inductive set (A: Type) : Type := 
 nil: set A | add: A -> set A ->  -> set A

Is it possible to have such an "inductive definition" for finite sets? If not, can I be supplied with a proof of why not?
My intuition is that such a thing is not possible, because an inductive type allows for equational reasoning, while sets cannot be equationally reasoned with:
$$
\texttt{add}~(1, \emptyset) = \texttt{add}(1, \texttt{add}(1, \emptyset)) \quad \text{(union is idempotent.)}
$$
however:
add 1 (add 1 nil) <> add 1 nil 

So we will always have to go through some "extensional interface". Unfortunately, I don't know how to prove such a thing!

**Tags:** type-theory, dependent-type, coq, formal-methods

> **Comments:**
> **username_1**: You might like to look into "quotient types" (and higher-inductive types, which are a kind of generalization of quotients).  Another approach might be to make your `add` constructor take a proof that the new element is not yet in the set (which you might be able to define as an inductive-recursive definition).  
> **username_0**: Can you show me how to write the inductive-recursive definition? I'd be glad if you could. Regarding quotient types: Right, I'd forgotten about their existence! I guess I can encode this in cubical agda? (cubical so the quotients are computable)  

---

## 1 answers

### Answer by username_2 on 2020-05-05. Score: 7 | Accepted answer

There are many variants of finite sets in constructive mathematics. One that can be defined using just inductive definitions, and is therefore amenable to formalization in type theory, is the Noetherian finiteness by Thierry Coquand and Arnaud Spiwack. The idea is to define a set or a type $A$ to be finite if the following holds: every sequence $a : \mathbb{N} \to A$ contains a duplicate. The trick is to express an equivalent condition using inductive definitions, so that we get an induction principle for reasoning about such sets.
The definition of Noetherian finiteness from section 2.3 of the linked paper can be translated to Coq like this:
(* [occurs x l] states that x appears in the list l *)
Inductive occurs {A : Type} : A -> list A -> Type :=
  | occurs_head : forall x k, occurs x (cons x k)
  | occurs_tail : forall x y k, occurs x k -> occurs x (cons y k).

(* [has_duplicates l] states that [l] has a duplicate, i.e., that an element appears in it twice. *)
Inductive has_duplicates {A : Type} : list A -> Type :=
  | has_duplicates_head : forall x l, occurs x l -> has_duplicates (cons x l)
  | has_duplicates_tail : forall x l, has_duplicates l -> has_duplicates (cons x l).

(* An auxiliary definition: a list `l` is said to be `noetherian` if it contains a duplicate, or if every extension of `l` by one element is `noetherian`. *)
Inductive noetherian (A : Type) : list A -> Type :=
  | N_duplicates : forall l, has_duplicates l -> noetherian A l
  | N_step : forall l, (forall a, noetherian A (cons a l)) -> noetherian A l.

Definition NoetherianFinite A := noetherian A nil.

If you're willing to use quotient types or the higher inductive types from homotopy type theory, then you can have a look at the defintion of finite sets Finite in the HoTT library. It says that a type X is finite if there is a number n such that X is merely equivalent to the standard finite set {0, 1, ..., n-1}. The word "merely" here means that we truncate the existence, i.e.,
$$\textstyle\mathsf{Finite}\, X \mathrel{{:}{=}}
\sum_{n : \mathbb{N}} \left\| X \simeq \mathsf{Fin}\,n\right\|$$
where $\mathsf{Fin}\,n$ is the standard finite set $\sum_{k : \mathbb{N}} (k < n)$.

> **Comments:**
> **username_0**: Thanks for the pointers to both the Coq definition and the HoTT based definition. Can you give me some intuition about where my intuition that "(a)sets cannot be equationally reasoned with but (b) inductive definiitions can" breaks? Does (a) break, or (b), or both?  
> **username_2**: Finite sets can be equationally reasoned *about* because the finite subsets of a type $A$ are the commutative monoid freely generated by $A$. So there will be equations (of the commutative monoid) and an induction principle (the free generation).  
> **username_0**: It is unclear to me why they correspond to the free commutative monoid. Won't the free commutative monoid of a type $S$ with inhabitants $a:S, b:S$ contain terms such as $\epsilon, a, b, ab, a^2, b^2, a^2b^2\dots$, while the subsets of $S$ are only $\epsilon, a, b, ab$?  
> **username_2**: Oops, its the free *idempotent* commutative monoid, i.e., $x^2 = x$ for all $x$. Without idempotence we get *mutisets*.  
> **username_0**: OK, I agree that idempotent works. However, isn't the problem the same --- how does one impose idempotency within an inductive type? That then circles back to the clever construction you gave above, is my current understanding of the story?  
> **username_2**: You asked if there are reasoning principles. The answer is "yes, the equations of a semilattice (which is what an idempotent commutative monoid is), and an induction principle". If a given framework can't handle the reasoning, that's the problem for the framework, the reasoning principles still are there.  

---

