定理証明支援系Coqにおける不等式変形記法

IPSJ

Bibliographic Information

Other Title
  • A Tactic Library for Transforming Inequalities in Coq

Search this article

Abstract

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

Formal proofs of inequalities on natural numbers is important for formal proofs of mathematical theorems and properties of programs. However, Coq's notation of formal proofs of inequalities is different from that of informal proofs. For instance, when we write an informal proof of inequality L ≤ R, we usually use a declarative notation like a “chain” such that L = M1 ≤ M2 = M3 ≤ ・・・ ≤ Mn = R. Such notation is common in textbooks, and thus it enables us to understand proofs intuitively. On the other hand, standard Coq does not support such a declarative notation, so that we cannot understand proofs in Coq intuitively. In this paper, we propose a novel approach to enable us to write formal proofs in the “chain” notation. One of main features of our approach is that the chain notation is realized as a tactic library, so that we can use it easily by only loading it as a module, and in conjunction with the conventional notation. We also try writing formal proofs for properties of Ackermann function with our tactic library. The result shows that we can write the formal proofs like informal proofs in a textbook.

Journal

Related Projects

See more

Keywords

Details 詳細情報について

Report a problem

Back to top