The Coq mailing list

[Guillaume Brunerie <guillaume.brunerie AT gmail.com>]

2011/9/15 Adam Chlipala <adamc AT csail.mit.edu>

Guillaume Brunerie wrote:

I also tried defining [T] and [f] as one function:
Fixpoint Tf (n : nat) : {B : Type & A n -> B} :=
 match n with
   | 0 => […]
   | S n' => […]
 end.

This didn’t work either, I think this is because in the first branch of the match Coq want a function of type [A n -> B] but I just have something of type [A 0 -> B] (and there is the same problem in the second branch, is this what is called dependent pattern matching?)

Yes, you need dependent pattern matching here.  If the function body is type-correct, I think you shouldn't need to do any more work, but adding an annotation can be helpful while you're debugging.  Try this instead and you'll probably get more informative error messages:

Fixpoint Tf (n : nat) : {B : Type & A n -> B} :=

 match n return {B : Type & A n -> B} with
  | 0 => […]
  | S n' => […]
 end.

Thanks, adding the explicit type annotation to the match made it work (and I also had to explicitly write [(unit : Type)] in the body because I want [T 0 = unit] and [unit] is of type [Set] by default).

But I do not understand why this is working. I had the impression that Coq does not support dependent pattern matching. Perhaps there is a limited dependent pattern matching support for simple types like integers?

By the way, I’m working on homotopy type theory where fully general dependent pattern matching is inconsistent (because it implies Streicher’s axiom K for instance). Is it ok to use dependent pattern matching on integers anyway?

Guillaume Brunerie