Coq Workshop 2019 で、 A Gallina Subset for C Extraction of Non-structural Recursion という発表をした。
Coq 開発者との議論のセッションで、今後の Coq 8.10, 8.11 に入る予定の機能が リストアップされていた。
この中で、Coq 8.11 に入る機能に termination check を disable できるようになる、 という話があった。
探してみると、おそらく、TypingFlags のことだと思われる。
TypingFlags をちょっと試してみたが、termination check できない再帰関数の定義はとくに問題なく可能。 でも、そういう関数についてなにか証明するのは（手元の Coq 8.9.1 で試した限りでは）難しい感じ。 証明中に tactic が止まらなくなってしまうことがあって、回避できない。
なんとなく、すべての tactic が確実に止まるようにするのは難しいのだと思うけれど、 証明を作れる程度に改善するのはなんとかなるのではないかという気がする。 Coq 本体に入るとすれば、そのような改善が行われることは期待できる、と思いたい。
[latest]