The Coq mailing list

[Tom Hirschowitz <tom.hirschowitz AT univ-savoie.fr>]

Also stumbled on this a few weeks back.

Nicolas Tabareau showed me this

(** A vector of length [0] is [nil] *)
Definition case0 {A} (P:t A 0 -> Type) (H:P (nil A)) v:P v :=
match v with
  |[] => H
  |_ => fun devil => False_ind (@IDProp) devil (* subterm !!! *)
end.

from VectorDef.v in theories/Vectors, which easily entails the result.

But which i can't type check, although obviously Coq can!

Would you please be able to explain this trick and why it is (was?)
needed?

Tom



Pierre Boutillier 
<pierre.boutillier AT pps.univ-paris-diderot.fr>
 writes:

> 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