The Coq mailing list

[Ömer Sinan Ağacan <omeragacan AT gmail.com>]

Hi all,

Not having dependent pattern matching in Coq is leading us to verbose
and hard to write/understand programs, using patterns named like
"transport", "convoy" etc. IMHO, programming this way is not fun at
all and this made me lose my interest in Coq a little. (as you can
understand, I'm just a hobbyist :-)

I recently proposed a challenge for dependently typed languages here:
http://osa1.net/posts/2014-09-23-two-challenges-for-dep-typed-langs.html
. Exercises in the link were born from real problems that I tried to
solve but failed. Once I started working on Fin, Vector and similar
dependent type families, things became unbearable.

Few days ago Jason Cockx posted his solution in Agda (see comments
section). One interesting property of his solution is that it doesn't
use Axiom K. Apparently it's possible to have a much more expressive
pattern matching than what we have in Coq right now without relying on
K, as explained by Cockx et al. in "Pattern Matching Without K" paper.

(If you're interested, there's also a Coq solution by jrw linked in
the blog post)

I was wondering if there's a problem with having pattern matching
explained in the paper in Coq, without assuming any axioms.

If there aren't any problems with that, how hard would it be to
incorporate the algorithm in Coq? Do you think it would worth it? Or
do you find efforts like this worthless?

I know we have [Program] and similar libraries to make dependently
typed programming easier using tactics but the goal here is to write
programs directly, without using tactics, because tactics also have
their problems(see my previous blog post in the link above for an
example. I had also sent some emails to here about that).

Thanks.

---
Ömer Sinan Ağacan
http://osa1.net