The Coq mailing list

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

Dear Guillaume,

thanks a lot, your example gives some interesting insight into how match 
works. So if I have nat = bool, I can convince match to accept 1 as a bool:

Definition foo2 (H : nat = bool) : bool :=
  match H in (_ = t) return t with
  | eq_refl => 1
  end.

But I wonder how this really works. I can see that an "in" clause is used to 
bind a variable to a part of the match argument type and this is used in a 
"return" clause. But how does Coq know that it should use the equality to 
relate this to the actual return type? Is there a rule that if the match 
argument is an equality of types, it can be used to unify the declared and 
actual return type?

Coming back to my issues with computations with dependent types: how about 
reducing such matches, in case the types are unifiable, as in the example I 
have shown where the types are "t bool (0+1)" and "t bool 1". This should be 
quite common in computations with concrete values of dependent types, e.g. 
vectors of known length.

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, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928