整数を使った証明（整数精度のHaar変換）のトライアル - Qiita

目的 Coqのtacticsを改良？したssreflectと定理のライブラリであるmathcompを使って整数精度のHaar変換が可逆であること証明を通じて、整数に関する証明に慣れるのが目的です。 今回のHaar変換の証明のソースはこちらです。 前回Elgamal暗号＆復号の証明をしましたが、それは自然数の処理でした。（今回は整数） 整数の定理はmathcompのalgebraのライブラリのssralg,ssrint,intdivなどに含まれています。(一方、自然数の定理はmathcompのssreflectのライブラリのssrnat,div,primeなどに含まれています。) algebraライブラリの資料はほとんど見当たらずCoq Winter School 2017-2018 (SSReflect & MathComp)のalgebraの資料を参考にしました。 mathcompの整数