coqの質問はここでいいでしょうか？

よくある論理パズル（正直者と嘘つきがいて、ある人が〜と言った。とかいうやつ）を
coqで解きたいと思ったのですが
要するに命題論理の式をCNF(乗法標準形？）に変形できればいいのですが
coqでうまくやる方法をご存知の方いますか？