The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Laurent,

your suggestion works like a charm in many cases, but I got across one case I 
don't see how I could solve it:

Require Import Coquelicot.Coquelicot.
Require Import Reals.

Definition Mprepend_row {T : Type} {m n : nat} (V : @Tn n T) (M : @matrix T m 
n) : @matrix T (S m) n := (V, M).

Fixpoint Mprepend_col {T : Type} {m n : nat} : @Tn m T -> @matrix T m n -> 
@matrix T m (S n) :=
  match m return @Tn m T -> @matrix T m n -> @matrix T m (S n) with
  | 0     => (fun V M => tt)
  | S m'  => (fun V M => (fst V, fst M, Mprepend_col (snd V) (snd M)) ) 
  end.

(* The above works, but replacing the pair with a call to Mprepend_row 
doesn't work: *)

Fixpoint Mprepend_col' {T : Type} {m n : nat} : @Tn m T -> @matrix T m n -> 
@matrix T m (S n) :=
  match m return @Tn m T -> @matrix T m n -> @matrix T m (S n) with
  | 0     => (fun V M => tt)
  | S m'  => (fun V M => Mprepend_row (fst V, fst M) (Mprepend_col (snd V) 
(snd M)) ) 
  end.

It fails with 

The term "(fst V, fst M)" has type "(T * Tn n T)%type" while it is expected 
to have type "Tn ?n ?T".

Here Coq doesn't see that ?n is (S n), so that Tn ?n T is T * Tn n T. It is 
understandable that unification can't handle this without knowing that ?n=S 
n, but I wonder if there is a way to fix it. It is not so nice that replacing 
a pair with a function which does the same just with more restricted types 
doesn't work. I find the variant using Mprepend_row more readable and easier 
to write, because it is more restricted in its argument types.

Another interesting point is that I usually need the return annotation to get 
around the first case in case the second case is wrong. But if the second 
case is correct, the return statement is not needed. That is if I remove the 
return in the above example, it fails in the first branch. I think this is a 
bit odd because the return statement I give is the same as the return type of 
the function and thus the type match should return. I am not sure why it 
makes a difference to match - it looks a bit redundant.

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