Isabelle/HOLの基本 その2

さてsimpとautoの2つのproof methodはすでに見た。 このセクションではより強力な自動証明や証明ツールをみていく。

この2つの特徴として

• 上手く行かなかったら(ゴールの解消を途中で諦めた場合は)、ゴールを変形したところで止める

• 証明可能な命題だからといって必ずこれらで証明できるわけではない。むしろ出来ないものもたくさんある。

autoより強力なproof methodにfastforceがある:

  lemma "⟦ ∀ xs ∈ A. ∃ys. xs = ys @ ys; us ∈ A ⟧ ⟹ ∃ n. length us = n + n"
  by fastforce

これはquantifierが複雑なのでautoでは証明できない。 fastforceは失敗することもあり、また最初のゴールに対してしか作用しない。fastforceは複雑なlogicに弱いがequality reasoningに強い。

さらに複雑なゴールを示せるproof methodにblastがある。

  lemma "⟦ ∀x y. T x y ∨ T y x; ∀x y. A x y ∧ A y x ⟶ x = y; ∀x y. T x y ⟶ A x y ⟧ ⟹ ∀x y. A x y ⟶ T x y"
  by blast

blastも失敗することもあり、logic,setに強いがequality reasoningに弱い。

sledgehammerはproof searchを行うコマンドである。 これは現在証明可能な定理とblast,auto,simpなどのproof methodを組み合わせて現在のゴールを解消するような証明を自動生成するツールである。

  lemma "⟦ xs @ ys = ys @ xs; length xs = length ys ⟧ ⟹ xs = ys"

ここでsledgehammerと入力するか、またはjEditのsledgehammerパネルでApplyのボタンを押す。 するといくつかの候補が表示されるので、好きな証明をクリックするとそれが実際に挿入される。

    using append_eq_append_conv by blast

ここで、使われている append_eq_append_conv という補題が自動的に採用されていることに注意。

sledgehammerはいくつかのsolverをそれぞれ回して証明を探索するので、いくつかの証明が得られることもあれば難しい命題の場合には全て諦めてしまうこともある。 sledgehammerが metis を含む証明を提案した場合、metisは与えられた補題だけからゴールを解消するためのコマンドであり、現実的な時間で応答が返らないこともあることに注意。

arithmetic formula (変数、数値、 +,-,=,<)の解消には arith を使う。

  lemma "⟦ (a::nat) ≤ x + b; 2*x < c ⟧ ⟹ 2*a + 1 ≤ 2*b + c"
  by arith

簡単なarithmetic formulaならautoやsimpでも解ける可能性はある。 また、arithは整数や実数が対象でもよい。

全てのproof methodを試すなら try コマンドを使う。あるいは try0 というより簡単なものを使っても良い。

導入規則を適用するruleというコマンドがある。 ruleは定理を1つ受け取ってそれをintroルールとして現在のゴールに適用する。いくつかのintro ruleはすでに知っているので省略できることもある。

定理が A ==> B の形の時(ここでのimplicationは ==> であって --> ではないことに注意。後者は単なるHOLのlogical connectiveだが前者はIsabelleで特別な意味を持つ)、 A に何かを適用したいときはOFを使う: 例えば r: A ==> B かつ s: A のとき、 r [OF s] は B という定理を表す。

さらに、定理が自由変数(?hoge のような形の変数)を含んでいる時、これをofで束縛できる: 例えば、 r: ?P ?x のとき、 r [of "λx. x = 10" 20] は 20 = 10 という命題を表す。

OF/ofは複数適用する場合はスペース区切りで横に並べる。1つの項がスペースを含む場合は例によってダブルクオーテーションで囲むこと。

例：

  thm conjI
  (* conjIが ?P ==> ?Q ==> ?P /\ ?Q であるとき *)

  thm refl
  (* reflが ?P = ?P であるとき *)

  thm conjI[OF refl[of a] refl[of b]]
  (* は、 a=a /\ b=b という定理になる *)

fastforce,blast,autoに対して、modifier intro, dest が用意されている。

• intro: blast intro: [thm] などとすることで、 A ==> B の定理を用いて結論のBをAに書き換えて証明を行う

• dest: blast dest: [thm] などとすることで、 A ==> B の定理を用いて仮定のA(あるいはAを含む定理)をBに書き換えて証明を行う

inductive predicateをinductiveキーワードを使って定義できる。

  inductive even :: "nat => bool" where
    ev0: "ev 0"
  | evS: "ev n ==> ev (n + 2)"

は、 ev n = True とnが偶数であることが同値であるような述語を表す。

inductiveで定義した述語に対する場合分けや構造帰納法などが自動で生成される。 上のようにevenを定めた場合、例えばjEditのQueryパネルに name:even と入力することで even.cases や even.induct などの定理が自動で生成されていることがわかるだろう。

この帰納法を用いて証明を行う場合、次のように書ける:

  lemma "even m ==> P m"
  apply (induction m rule: even.induct)