The Coq mailing list

[Laurent Thery <Laurent.Thery AT inria.fr>]

> Fixpoint first_col {T : Type} {m n : nat} (M : @matrix T m (S n)) :
> @matrix T m 1 :=
> 
>   match m return @matrix T m 1 with
> 
>   | 0    => ()
> 
>   | S m' => ( (fst (fst M), ()), first_col (snd M))
> 
>   end.
> 

as M depends on m you need to internalise it :


Fixpoint first_col {T : Type} {m n : nat} : @matrix T m (S n) -> matrix
m 1 :=

  match m return matrix m (S n) -> matrix m 1 with

  | 0    => fun M => ()

  | S m' => fun M => ( (fst (fst M), ()), first_col (snd M))

  end.








>  
> 
>  
> 
> Coq does not see that since m=S m', M has at least one row in “fst M”. I
> guess I need a more fancy in/as/return annotation for the match or some
> explicit type annotations here and there, but I can’t figure it out.
> Btw.: the return as given is required – without it Coq doesn’t accept
> the 0 case term.
> 
>  
> 
> I guess this would be much easier with the Equations plugin. I guess it
> is due time to look into it, but I also find it worthwhile to understand
> how it would work in basic Coq.
> 
> Best regards,
> 
>  
> 
> Michael
> 
> Intel Deutschland GmbH
> Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
> Tel: +49 89 99 8853-0, www.intel.de
> Managing Directors: Christin Eisenschmid, Gary Kershaw
> Chairperson of the Supervisory Board: Nicole Lau
> Registered Office: Munich
> Commercial Register: Amtsgericht Muenchen HRB 186928
>