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

[Soegtrop, Michael]

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,

Mich

[Pierre Boutillier]

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.

Post by Soegtrop, Michael
Dear Coq users,
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

[Tom Hirschowitz]

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

Post by Pierre Boutillier
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.

Post by Soegtrop, Michael
Dear Coq users,
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

[Adam Chlipala]

I think this subtle topic is better understood by reading an
introduction to dependent types in Coq, say Part II of CPDT
<http://adam.chlipala.net/cpdt/>. The original question is quite close
to an example there.

P.S.: If you're going to write out the proof without using the
newfangled [match] desugaring support of recent Coq versions, then I
prefer this one:
Lemma Vector_0_is_nil' : forall T n (v : Vector.t T n),
match n return Vector.t T n -> Prop with
| O => fun v => v = Vector.nil T
| _ => fun _ => True
end v.
Proof.
destruct v; auto.
Qed.

Theorem Vector_0_is_nil : forall T (v : Vector.t T 0), v = Vector.nil T.
Proof.
intros; apply (Vector_0_is_nil' _ _ v).
Qed.

Post by Tom Hirschowitz
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
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

Post by Pierre Boutillier
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.

Post by Soegtrop, Michael
Dear Coq users,
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

[Soegtrop, Michael]

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-***@inria.fr [mailto:coq-club-***@inria.fr] On Behalf Of Pierre Boutillier
Sent: Tuesday, February 10, 2015 5:13 PM
To: coq-***@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.

Post by Soegtrop, Michael
Dear Coq users,
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 che