The Coq mailing list

[Adam Koprowski <adam.koprowski AT gmail.com>]

In short, this works: [...]

  Thanks! I'll try to see whether I can make it work on my real problem...

 

For the generation of equalities for the toplevel dependent pattern-matching,
you should get them for free! The automatic inference of the return predicate
was not getting the dependency of the return type in [x], but this can be fixed.
As a result, you get to prove the [correct] tcc in each branch instead of having
to destruct the whole term again and get into these dependency problems.

  Indeed in my previous (simpler) version of this function, when [x] was not dependently typed, that was the case: I got one tcc per branch, with equality constraints and everything worked beautifully.
  By 'this can be fixed' you mean the treatment of such cases by Program? Or is there anything I can do to avoid providing the return clause and benefiting from the Program's extra treatment of pattern matching?

  Cheers,
   Adam
-- 
=====================================================
Adam.Koprowski AT gmail.com, http://www.cs.ru.nl/~Adam.Koprowski

The difference between impossible and possible
lies in determination (Tommy Lasorda)
=====================================================