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 Notherian 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 Notherian 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 `notherian` if it contains a duplicate, or if every extension of `l` by one element is `notherian`. *)
Inductive notherian (A : Type) : list A -> Type :=
| N_duplicates : forall l, has_duplicates l -> notherian A l
| N_step : forall l, (forall a, notherian A (cons a l)) -> notherian A l.
Definition NotherianFinite A := notherian 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)$.
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). $\endgroup$ – Stefan May 4 '20 at 14:22