Equality on inductive types

Question

How do I prove the following trivial lemma:

Require Import Vector.

Lemma t0_nil : forall A (x : t A 0), x = nil A.
forall (A : Type) (x : t A 0), x = nil A
Proof.
forall (A : Type) (x : t A 0), x = nil A
Abort.

FAQ recommends decide equality and discriminate tactics but I could not find a way to apply either of them. For the reference, here is inductive definition:

Inductive t (A : Type) : nat -> Type :=
    nil : t A 0
  | cons : A -> forall n : nat, t A n -> t A (S n)

Arguments t _%type_scope _%nat_scope
Arguments nil _%type_scope
Arguments cons _%type_scope _ _%nat_scope _

Answer

What you want to do is to invert on x. Unfortunately, it turns out that general inversion of dependently typed hypotheses is undecidable, see Adam Chlipala's CPDT. You can pattern match on the structure manually though, e.g. with:

Lemma t0_nil : forall A (x : t A 0), x = nil A.
forall (A : Type) (x : t A 0), x = nil A
Proof.
forall (A : Type) (x : t A 0), x = nil A
  intros.
A: Type
x: t A 0
x = nil A
  refine (match x with
          | nil _ => _
          | cons _ _ _ _ => _
          end).
A: Type
x: t A 0
nil A = nil A
A: Type
x: Vector.t A 0
a: A
n: nat
t: Vector.t A n
IDProp
  -
A: Type
x: t A 0
nil A = nil A reflexivity.
  -
A: Type
x: Vector.t A 0
a: A
n: nat
t: Vector.t A n
IDProp exact @id.
Qed.

In many cases you can also use the tactic dep_destruct provided by CPDT. In that case your proof simply becomes:

Require Import CpdtTactics.

Lemma t0_nil : forall A (x : t A 0), x = nil A.
  intros. dep_destruct x. reflexivity.
Qed.

A: An elegant solution by Pierre Boutillier, taken from this Coq-club post:

Definition t0_nil A (x : t A 0) : x = nil A := match x with nil _ => eq_refl end.