Isabelle/HOLの基本 その1

HOLはsimply-typedなlanguageにlogicを組み込んだみたいなやつ

• base type: bool, natとか色々

• function type: => でかく。

• type variable: 型変数はシングルクオートを前につけて 'a とか 'b とかかく。MLとかの記法らしい。

例えば cons : 'a => 'a list => 'a list とか。

• term: MLぽい感じでifとかletとかcaseとかある

• formula: formulaはbool型のtermで、TrueとFalseとandとかorとかの命題結合子たちからなる。implicationは -->

• equality: = : 'a => 'a => bool でかく組み込みのrelation symbol。

• quantifier: forall, existが使える

• judgement: |- Fm : Typ みたいな形のjudgementを扱う。型は適当に推論されるので省略できるときはする。

最後に、HOLではなくてIsabelle側の特殊な論理記号としてuniversal quantifier ⋀ (大きい∧)と implication ==> があって、これはHOLのロジックとは別物でIsabelle組み込みのコマンドといい感じに組み合わさって動いたりするやつ。多分使ってたらわかる。

Isabelleのファイルは .thy という拡張子で保存し、1ファイルに1つのtheory(モジュール的なもの)を基本とする。

  theory Test
  imports Main
  begin

  end

theory の後にはファイル名と同じ名前を書く。 imports Main は Main というtheoryを読み込むことを表す。 begin ... end の間に証明を書く。

bool, nat, listは

  datatype bool = True | False
  datatype nat = Zero | Suc nat
  datatype 'a list = nil | cons 'a "'a list"

で定義できる。(組み込みの型はZeroを0とかくなどのnotationの違いはある) ここで、1つの「Isabelleの項」はスペースを含む場合に必ずダブルクオーテーションで囲まないといけないことに注意。

例えばadd関数はパターンマッチを使って

  fun add :: "nat ⇒ nat ⇒ nat" where
    "add 0 n = n"
    | "add (Suc m) n = Suc (add m n)"

とかやって定義できる。 functionでもダブルクオーテーションに注意。

パターンマッチを使うとexhaustive checkが働くのでパターンマッチが網羅的でないと警告が出る。

項の即時評価には value というコマンドが使えて、

  value "add (Suc (Suc 0)) (Suc 0)"
  (* "Suc (Suc (Suc 0))" :: "nat" と表示される *)

とかやる。

pdfに載ってるtheory of listを写経したらこうなる:

  theory MyList
  imports Main
  begin

  datatype 'a list = Nil | Cons 'a "'a list"

  fun app :: "'a list ⇒ 'a list ⇒ 'a list" where
    "app Nil ys = ys"
    | "app (Cons x xs) ys = Cons x (app xs ys)"

  fun rev :: "'a list ⇒ 'a list" where
    "rev Nil = Nil"
    | "rev (Cons x xs) = app (rev xs) (Cons x Nil)"

  value "rev (Cons True (Cons False Nil))"
  (* "Cons False (Cons True Nil)" :: "bool list" と表示される *)

  (* コメント *)

  end

さて定理証明界のfizzbuzzこと³リストが2回reverseすると元に戻るという定理を示そう。 まずはステートメントを述べる。

  theorem rev_rev: "rev (rev xs) = xs"

theoremかlemmaに続けてformulaを書くと定理として認識される。(theorem, lemmaに違いはない) rev_rev: と書いておくと名前がついて示したあとで使えるようになるけど省略しても良い。

さてこれをxsについての帰納法で示したいので次のようにしよう。

  apply (induction xs)

するとアウトプットパネルに2つのゴールが表示されると思う。 まぁよくわからないけど勝手に証明してくれ頼むってしたいときはautoコマンドを使う。

  apply auto

さてゴール1は自動で証明されてゴール2が残った。このゴールはいきなり示すのは難しいので、いくつか補題を置いてがんばることにする。

  lemma rev_app [simp]: "rev (app xs ys) = app (rev ys) (rev xs)"

先程も言ったとおりlemmaはtheoremと同じ。 ちなみに [simp] というのが(attributeという)くっついているけど、これを付けておくとsimpコマンドを使った時に自動的にこの定理も(使用可能ならば)使ってくれるようになるというもの。

さてこの補題を示そう。xsについての帰納法が良さそうなのでそうする。

  apply (induction xs)

またゴールが2つ表示されるけれど、これはautoコマンドでIsabelle頼む〜ってやるとまたしても上手く行かない。 さらに補題が必要そうなので補題をおく。

必要な補題をじゃんじゃんおいて示そう。

  lemma app_Nil [simp]: "app xs Nil = xs"
  apply (induction xs)
  apply auto
  done

  lemma app_assoc [simp]: "app (app xs ys) zs = app xs (app ys zs)"
  apply (induction xs)
  apply auto
  done

ご覧の通りIsabelleのautoコマンドが強力すぎて楽勝だなという気分になってくる。

さて、この2つの補題を使うとさっきの rev_app が示せるようになる。 [simp] アトリビュートをつけた補題が自動的にautoコマンドで使われるのでさっきはダメだった証明が今度は上手く行くようになる。

  lemma rev_app [simp]: "rev (app xs ys) = app (rev ys) (rev xs)"
  apply (induction xs)
  apply auto
  done

さて一番最初の rev_rev も同じようにするだけ。

  lemma "rev (rev xs) = xs"
  apply (induction xs)
  apply auto
  done

型のエイリアスには type_synonym を使う。

  type_synonym string = "char list"

データ型の宣言には datatype を使うことはすでに見た。 datatypeで宣言すると、そのデータに関する構造帰納法が自動生成される。上でも自作のlist型に対してinductionコマンドを使っていたが、そのときには生成された構造帰納法を使って式を変形していた。

定義をするにはdefinitionを使う。 これはrecursiveでないfunctionの定義に使う。

  definition sq :: "nat => nat" where
    "sq n = n * n"

funと違ってこちらはsimpなどを使っても勝手に展開されない。 sq n を n * n に変形したいときは自動生成された定理 sq_def を使う。

  abbreviation sq' :: "nat => nat" where
    "sq' n == n * n"

abbreviationはdefinitionみたいなものだけど中が勝手に展開される。 sq'_def は自動生成されない(必要ないので)。 abbreviationはdefinitionと違って = ではなく == (または \<equiv>) を使うことに注意。

また、 [simp] はつけていないけれどsimpコマンドを行う時に使う定理を追加することができる。

  apply (simp add: thm1 thm2 .. thmn)

  (* あるいはautoでも使える *)

  apply (auto simp add: thm1 thm2)

後でも述べるが、autoコマンドはゴールが複数ある時に全てのゴールに対して変形を行う。 simpを全てのゴールに対して行う simp_all コマンドもある。

次のように、caseによる場合分けをする必要がある定理を示したいとする。

  lemma "P (case e of 0 => a | Suc n => b n) = ((e = 0 --> P a) /\ (∀n. e = Suc n --> P (b n)))"

この時は split をつけて

  apply (simp split: nat.split)

のようにできる。