イントロダクション

Rocqで数学をやりましょう。

当サイトの目的について

1. 私自身がRocqに慣れるため。あとはいくつかのトピックについてより深い理解を得るために、きちんとした証明を書きたい。

2. Rocqに関する日本語の情報が少なすぎると感じているため。Rocq（Coq）は歴史のあるソフトウェアであるため総量としては多少あるかもしれないが、古い情報は今と状況が変わっていたりもするので、「近年の文献」という観点では少ないだろう。

3. Rocqや証明支援系一般の証明テクニックの紹介にもなり得るだろう。

4. 証明支援系で証明されたものは、ただコードだけを見せられることがしばしばある。わざわざ「自分でRocqなどの環境を用意し、バージョンを合わせ、依存ライブラリを導入し、証明をチェックさせる」などということはしないだろう。したがって、このサイトのようにインタラクティブに証明の流れを読者に見せることが重要である。これはAlectryonというツールによって実現されている。

5. 形式的証明は散文によって説明が織り交ぜられているべきである。100行以上ある形式的証明なんて普通は読む気にならない。そのコードは何を目的としているのか、その定理の証明はどのような方針なのか、なぜそれをそのように定義したのか、その初めて見る文法は何の機能を持つのか、それらを自然言語によって説明することが大事である。

指標

「機械が証明の正当性を保証してくれるから、どのように証明を書いてもいい」というものではない。それだと「既知の結果が機械によって正しいと判定されたから何？」となってしまう。もちろん「紙とペンで証明を書くと間違えてしまいやすい定理や分野」であればこの問に対する返答ができるであろうが、それ以外が問題である。我々の、あるいは私の目的は、証明の正当性を機械に保証してもらうことではなく、体系的かつ整合的に、間違いもなく、定理や分野を提示・説明することにある。

形式的な証明は人間が読めるべきである。

1. 1つ1つのステップが明瞭であること。たとえ機械の力で数ステップを省略できたとしても、それによる効果が人間によって理解しにくければその証明は読むことが難しくなる。

2. 適切な抽象度を持つこと。たとえ1つ1つのステップが理解できるものであったとしても、長々とした証明を書かれると「今自分はどこにいるのか」「何を意図してそのステップを踏んだのか」が理解し難くなる。たとえば、3ステップで書けるような証明についても、それが基本的なことであれば補題として分けるべきだろう。

適切な表現かは分からないが、形式的証明のレフェリーは機械であり、読者は人間である。