Coqは証明支援系というらしいですが、普通の意味でのプログラミングできないことにはあまり役にたたないと思います。証明にこだわらないで、せめてソート関数なり、、、いやもっと実用的なものをプログラミングしてみたら良いんじゃないかと思います。ですが…