The Coq mailing list

[James McKinna <james.mckinna AT cs.ru.nl>]

Michael,

Dmitri is right to alert you to the use of an explicit 'return family' P 
in the match syntax

   match <term> in <type> return P with...

But you can make slightly better use of this syntax to streamline 
Dmitri's idea (I learnt this trick from Hugo Herbelin in Tallinn at 
Christmas last year, but it may well be much older, going back to when 
V8.0 introduced 'return' clauses to match expressions): namely to choose 
a nice family P which:
--- is trivial in the 'bad' cases;
--- does 'what you want' in the good ones.

E.g. here you could try

P = match m with 0 => True | S _ => A

to obtain

Definition get_first (n:nat) (v : vec (S n)) : A :=
 match v in (vec m) return (match m with 0 => True | S _ => A) with
 | Vnil => I
 | Vcons a _ _ =>  a

where I is the trivial proof of True which knocks off the bad Vnil 
branch. In this case you don't even need the equations and 
simplifications and reflexivity proofs which an inversion-derived 
solution gives you.

Of course if you use this trick, then you still (might) need to do by 
hand the equational pre-processing of families P which Epigram would do 
for you in more complex examples such as Vec_tail, where you need to do 
the equational reasoning to push a Vec n to a Vec m ... having 
simplified Sm = Sn to m = n etc.

It is true that a true 'dependent pattern matching' vernacular syntax 
would be very nice to have in Coq, ... so people have begun working on 
this. In the meantime, let the optional 'return' clause in match 
expressions be your friend...

Best wishes,

James McKinna

Dimitri Hendriks wrote:
> for pattern matching over dependent types you
> have to use an explicit elimination predicate
> to predict the type of the righthand side.
> see ch. 15 of the manual.
>
> if you first ...
>
> you can see what the predicate should look like:
>   (vec m) -> (m = S n -> A)
>
> and this may insprire you to write for instance:
>
> ...
> Definition get_first (n:nat) (v : vec (S n)) : A :=
>   match v in (vec m) return (m = S n -> A) with
>   | Vnil => fun H => False_rect A (disc_O_S n H)
>   | Vcons a _ _ => fun _ => a
>   end (refl_equal (S n)).
>
> dimitri