The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Pierre,

très élégant! I guess going through an Agda tutorial also helps for Coq from 
time to time. 

Best regards,

Michael

-----Original Message-----
From: 
coq-club-request AT inria.fr
 
[mailto:coq-club-request AT inria.fr]
 On Behalf Of Pierre Boutillier
Sent: Tuesday, February 10, 2015 5:13 PM
To: 
coq-club AT inria.fr
Subject: Re: [Coq-Club] How to prove that all vectors of 0 length are equal 
to Vector.nil

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