 # An awkward inductive definition that resists `destruct`

I’m a fairly new user of Coq. I came up with an inductive definition `FiniteSet : nat -> Set`, for which `FiniteSet n` is intended to have exactly `n` elements:

``````Inductive FiniteSet : nat -> Set :=
(* Taking the successor means we introduce a new element. *)
| Fin_n (n : nat)                   : FiniteSet (S n)
(* We may lift the elements from the previous set into the next. *)
| Fin_s {n : nat} (F : FiniteSet n) : FiniteSet (S n).
``````

I wanted to try and prove that `Fin_n 0` is the unique element of `FiniteSet 1` as so:

``````Remark finite_one_unique : forall a : FiniteSet 1, a = Fin_n 0.
Proof. intro a. destruct a. (* I thought I could continue from here... *)
``````

But this doesn’t work; Coq complains [some lines omitted]:

``````Abstracting over the terms "n" and "a" leads to a term
fun (n0 : nat) (a0 : FiniteSet n0) => a0 = Fin_n 0
which is ill-typed.
Reason is: Illegal application:
The term "@eq" of type "forall A : Type, A -> A -> Prop"
``````

I don’t know how to perform case analysis on this object. I’ve also tried using `inversion` but to no avail.

There’s clearly some issue with how I parameterize this type via `n`, but I simply don’t know how I can fix it so that I can perform this analysis. Any help would be appreciated!

Your definition is exactly the same as `Coq.Vectors.Fin.t`; I expect you’ll find reading through that file informative: coq/Fin.v at master · coq/coq · GitHub

In your case, a direct proof looks like this:

``````Inductive FiniteSet : nat -> Set :=
| Fin_n (n : nat)                   : FiniteSet (S n)
| Fin_s {n : nat} (F : FiniteSet n) : FiniteSet (S n).

Definition finiteset_nonzero {n: nat} (f: FiniteSet n)
: match n return FiniteSet n -> Prop with
| 0 => fun p => False
| S _ => fun _ => True
end f.
Proof. destruct f; reflexivity. Qed.

Definition finiteset_1 {n: nat} (f: FiniteSet n)
: match n return FiniteSet n -> Prop with
| 1 => fun p => p = Fin_n 0
| _ => fun _ => True
end f.
Proof.
destruct f, n; try reflexivity.
exfalso; apply (finiteset_nonzero f).
Qed.

Remark finite_one_unique : forall a : FiniteSet 1, a = Fin_n 0.
intros; apply (finiteset_1 a).
Qed.
``````

(You can surely make it more succinct, but I find it readable this way)

1 Like