The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>]

Require Vector.
Definition Vector_0_is_nil (T : Type) (v : Vector.t T 0) : v = Vector.nil T :=
match v with Vector.nil => eq_refl end.

:-) Yes, destruct is less smart than it should as the term inference is able 
to solve this case … Life’s too short to do all we would like to do!

Pierre B.

> On 10 Feb 2015, at 17:01, Soegtrop, Michael 
> <michael.soegtrop AT intel.com>
>  wrote:
> 
> Dear Coq users,
> 
> I have difficulties to show the following:
> 
>       Require Import Vector.
>       Lemma Vector_0_is_nil: forall (T : Type) (v : Vector.t T 0), v = 
> Vector.nil T.
> 
> Since Vector.nil is the only constructor for vectors of length 0, this 
> should be the case, but I can't find a way to prove it. Inversion on v 
> yields nothing and tactics like destruct and induction lead to type checker 
> errors. Also generalizing over arbitrary length with hypothesis n=0 leads 
> to type checker errors.
> 
> Best regards,
> 
> Michael