著者

村田 康佑 江本 健斗

雑誌

情報処理学会論文誌プログラミング(PRO) (ISSN:18827802)

巻号頁・発行日

vol.11, no.4, pp.1-12, 2018-12-14

---

数学定理やプログラムの性質の形式的証明では,自然数上の不等式についての証明が頻出する.しかし,定理証明支援系Coqでの不等式の形式的証明は,非形式的証明とは異なる記法で記述されるため,数学的な直観がそのまま使えないことも多い.たとえば,非形式的証明では,不等式L ≤ Rを証明するために,しばしばL = M1 ≤ M2 = M3 ≤ ・・・ ≤ Mn = Rのように項を不等号で「鎖状」につなげて示す宣言的な記法が用いられる.こうした記法は数学の教科書等でよく馴染んだ記法であり,直観的に理解・記述することが可能である.一方,Coqにはそうした宣言的な記法は標準では用意されていないため,証明の理解・記述が困難になっている.本論文では,Coq上で,自然数上の不等式変形を,非形式的証明のように「鎖状」に記述する手法を提案する.本手法の特徴は,タクティックライブラリによって「鎖状」記法が実現されることにあり,それゆえ,提案記法はライブラリをモジュールとして読み込むだけで既存記法とあわせて使うことができる.また,このタクティックライブラリを用いて,Ackermann関数の性質についての不等式の証明を試みる.その結果,標準的な数学の教科書と近い記法で形式的証明を記述できることを確認する.