An awkward inductive definition that resists `destruct`

Using Coq
1

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!

2

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