coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] How to prove that all vectors of 0 length are equal to Vector.nil

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] How to prove that all vectors of 0 length are equal to Vector.nil
Date: Tue, 10 Feb 2015 16:01:09 +0000
Accept-language: de-DE, en-US

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

[Coq-Club] How to prove that all vectors of 0 length are equal to Vector.nil, Soegtrop, Michael, 02/10/2015
- Re: [Coq-Club] How to prove that all vectors of 0 length are equal to Vector.nil, Pierre Boutillier, 02/10/2015
  - Re: [Coq-Club] How to prove that all vectors of 0 length are equal to Vector.nil, Tom Hirschowitz, 02/10/2015
    - Re: [Coq-Club] How to prove that all vectors of 0 length are equal to Vector.nil, Adam Chlipala, 02/10/2015
  - RE: [Coq-Club] How to prove that all vectors of 0 length are equal to Vector.nil, Soegtrop, Michael, 02/11/2015