TypingFlags をちょっと試してみたが、termination check できない再帰関数の定義はとくに問題なく可能。 でも、そういう関数についてなにか証明するのは（手元の Coq 8.9.1 で試した限りでは）難しい感じ。 証明中に tactic が止まらなくなってしまうことがあって、回避できない。
なんとなく、すべての tactic が確実に止まるようにするのは難しいのだと思うけれど、 証明を作れる程度に改善するのはなんとかなるのではないかという気がする。 Coq 本体に入るとすれば、そのような改善が行われることは期待できる、と思いたい。
Coq 開発者との議論のセッションで、今後の Coq 8.10, 8.11 に入る予定の機能が リストアップされていた。
この中で、Coq 8.11 に入る機能に termination check を disable できるようになる、 という話があった。
探してみると、おそらく、TypingFlags のことだと思われる。
Coq Workshop 2019 で、 A Gallina Subset for C Extraction of Non-structural Recursion という発表をした。
PDF にドキュメントタイムスタンプ署名をつけるツールを作ってみた。
<URL:https://github.com/akr/pdftimestamp>
まぁ、作った、というよりは PDFBox の example を組み合わせたという感じで、 自分で書いたコードはかなり少ない。
なお、ドキュメントタイムスタンプ署名というのは、Adobe Acrobat だとタイムスタンプという機能に相当し、 手元のドキュメントを TSA（Time Stamping Authority）に署名してもらうというもの。たぶん。