The Coq mailing list

[Michael Day <mikeday AT yeslogic.com>]

Hi,

I have defined a simple vector type and a function to get the first 
element of non-empty vectors as follows:

Inductive vec (A:Type) : nat -> Type :=
    | Vnil : vec A 0
    | Vcons : forall (a:A) (n:nat), vec A n -> vec A (S n).

Definition get_first (A:Type) (n:nat) (v:vec A (S n)) (default:A) : A :=
    match v with
    | Vnil => default    (* I want to delete this line *)
    | Vcons a _ _ => a
    end.

Coq prevents me from calling get_first with an empty vector, so the Vnil 
case will never be matched and the default value will never be used. 
However, Coq does not permit me to omit this case:

Error: Non exhaustive pattern-matching: no clause found for pattern Vnil

This is incredibly frustrating. Why does Coq think that "Vnil" is an 
inhabitant of "vec (S n)"? After reading Conor McBride's papers on 
Epigram I expect the system to understand that 0 <> S n :)

The Vhead function in the Bvector module in the standard library uses 
the inversion tactic instead, but that seems to generate a very large 
and complicated definition for something that should be quite simple.

Best regards,

Michael

--
Print XML with Prince!
http://www.princexml.com