The Coq mailing list

[Eric Finster <ericfinster AT gmail.com>]

Based on Adam's response (thanks Adam!) I came up with the following:

   Fixpoint zero_len_eq (A : Type) n (v : Vect A n) :=
     match v in (Vect _ n) return (match n with O => identity _ _ | S
_ => unit end) with
       | VNil => identity_refl (VNil A)
       | VCons _ _ _ => tt
     end.

Which looks like some good progress.

   Check zero_len_eq.

   *******

   zero_len_eq
        : forall A : Type,
          forall n : nat,
          Vect A n
          → match n with
            | 0 => identity (VNil A) (VNil A)
            | S _ => unit
            end

But I still cannot seem to use this to prove the lemma as stated.

   Lemma zero_len_is_nil_prf (A : Type) (v : Vect A 0) : v = VNil A.
   Proof.
     apply (zero_len_eq A O v).

   ********
   Error: Impossible to unify "identity (VNil A) (VNil A)" with "v = VNil A".

Am I asking for too much here?

Eric

On Sat, Nov 26, 2011 at 3:48 PM, Adam Chlipala 
<adamc AT csail.mit.edu>
 wrote:
> Eric Finster wrote:
>>
>> I'm trying to do a case analysis over an inductive type where the
>> allowed constructors are restricted by the type of a term.  It
>> essentially equivalent to the following setup with indexed lists:
>>
>> Inductive Vect (A : Type) : nat → Type :=
>> | VNil : Vect A 0
>> | VCons : forall n : nat, A → Vect A n → Vect A (S n).
>>
>> Lemma zero_len_is_nil (A : Type) (v : Vect A 0) : v = VNil A.
>>
>
> This precise type family, and some functions and theorems closely related to
> your question, are considered in detail in Chapters 8 and 9 of CPDT:
>    http://adam.chlipala.net/cpdt/
>