Isabelle ゆるリファレンス（apply-scriptスタイル）

最近は本業の自動テストマンより定理証明支援系に力を入れている Kuniwak です（経緯は過去記事参照）。

orgachem.hatenablog.com

定理証明支援系はいいぞ、ということで本記事では 私がよく使う Isabelle の便利機能の紹介とごく個人的に感じている使い所などを書いています。

そのため全機能を網羅するものではなくかなり漏れがあります。もし「これめっちゃ便利だけど書いてない！」みたいな気づきがありましたらご指摘いただけると嬉しいです！

本記事の対象読者

対象読者は Isabelle の apply-script スタイルを学びたい方で、かつ「Tutorial on Isabelle/HOL 2020 の 1, 2, 3, 5 章を読んでなんとなくわかったけど…」な方です。もし定理証明支援系を使ったことがなく、Tutorial もまだ読んでいない方は 1, 2, 3, 5章を先に読むことをお勧めします（これ以外の章は重要度が低いかあるいはこの記事を読むのに必要なレベルを超えます）：

• 1章: 基礎（The Basics）
• 2章: HOL の関数型プログラミング（Functional Programming in HOL）
• 3章: さらなる関数型プログラミング（More Functional Programming）
• 5章: このゲームのルール（The Rules of the Game）

またかなり前の Tutorial の日本語訳であれば caeruiro さんによる邦訳があります。

ちなみに実のところ私は Tutorial で Isabelle を学んだわけではなく、PRINCIPIA が開催していた Isabelle チュートリアル全4回で上記1-5章+6-7章の内容を学びました（有料なので遠慮なく質問しまくった）。

Isabelle ゆるリファレンス

目次

分類

ここからは コマンド と メソッド の順でよく使う機能を紹介してきます。なお、コマンド とは以下の場所に書くやつです。apply などが代表的です。

(* コマンドはここに書ける *)

datatype A = B | C
 
(* コマンドはここに書ける *)

lemma "hoge = fuga"

apply(...) の括弧の中に書くのは メソッド です。代表的なのは assumption や rule drule erule などです。

よく使うコマンド

apply

命題の宣言である theorem や lemma などに対して メソッド を実行します。めちゃめちゃよく使います。apply(hoge) のようにも書けますし、apply hoge のように括弧が省略されたりします。

thm

thm foo のように指定すると定理 foo の内容を表示します。めちゃめちゃよく使います。theorem や lemma の文脈内でも書けます。

term

term "foo" のようにすると指定した論理式・コードの型を表示します。ただ型をみるために使うより、A ⟶ B ∧ C が A ⟶ (B ∧ C) なのか (A ⟶ B) ∧ C なのかわからないときに、それぞれカッコ付きで term に書いてみて Output にどう表示されるかみて結合を確かめることに使う方が多いですね…

term "A ⟶ (B ∧ C)"
(* 括弧が取れたので正解。
"A ⟶ B ∧ C"
  :: "bool"
*)


term "(A ⟶ B) ∧ C"
(* 括弧が変わらないのでハズレ。
"(A ⟶ B) ∧ C"
  :: "bool"
*)

value

value "list_update [A, B, C] 1 D" や value "1 + 1::nat" のように指定したコードの評価結果を表示します。 なお Enum.enum 型クラスあたりを実装されてないと表示できなかったりするようです（これは後述の quickcheck も同じ）。

sorry

theorem や lemma などの文脈で定理を無理やり証明できたことにして打ち切ります（つまり危険）。 しかし、よく rule_tac とかの挙動を確かめるための雑な定理をつくるときに使えます：

雑な定理の例

definition "A = True"
definition "B = True"

(* 雑な定理 *)
lemma foo: "A = B"
  sorry

(* subst (asm) がどんな動きするかみたい *)
lemma "A ⟹ B"
  apply(subst (asm) foo)
  apply(assumption)
  done

oops

theorem や lemma などの文脈で定理の証明を打ち切ります（sorry とは違って証明したことにはならない）。今は証明できなかったけどあとで証明するぞの気持ちで oops のまま残すことが多いです。

try

theorem や lemma などの文脈で後述する自動証明コマンド（sledgehammer など）と反例探索コマンド（nitpick など）をまとめて実行します。論理式の反例を見つけてくれる反証明コマンドを同時に実行してくれるのがポイントですね。

というのも、困り果てた際に自動証明しても解けないことが多いですが、解けない原因が (1) 本当は真だが難しすぎて解けない、(2) 本当は偽で証明が成り立たない（e.g. 反例がある）のどちらなのかによって対処方法が変わるためです（他のパターンもあるかも？自信がない…）。このとき、(2) が原因の場合は問題設定を見直さないといけないですが、自動証明のどちらも (1)(2) のどちらも外見上は帰ってこない形になってしまうので見分けがつきません。なので裏で反証明コマンドを同時に実行して反例が見つかったら教えて欲しいというわけです。

try が役立つ例

例えば、以下の定理は (2) の例ですが sledgehammer は帰ってこないです：

lemma "∀x y. x = y"
  sledgehammer

このとき try をかけると (2) なら反例が出てくることがあり区別できます：

lemma "∀x y. x = y"
  try
 
(*
   反例が見つかった：
 
   Nitpicking formula...
   Nitpick found a counterexample for card 'a = 3:
    
     Skolem constants:
       x = a1
       y = a2
*)

稀に使うコマンド

by

by(hoge) は apply(hoge) と done の両方を書いたのと同じ意味です。カッコよく見えるから使いたくなりがちですが、定義いじって subgoal 増えた時とかに最後の by を apply に変えて次の subgoal みたいになって保守がめんどいので、最終的には done でいいやになりがちです。なお、sledgehammer はお節介なので by でカッコよく返してきてキレそうになることがあります。

defer/prefer

複数ある subgoal の順番を変えます。defer は今の subgoal を後回しにし、prefer N は指定した subgoal を先頭に持ってきます。最終的にはすべての subgoal を証明する必要がありますが、妙な subgoal だけ先に挑んでみて早い段階で間違いに気づきたいときに使えます。

ただし subgoal の登場順序は使った定理に依存するので、Isabelle のバージョンアップなどで自動証明ロジックや定理が変わると subgoal の順番が変わって今まで通っていた証明が通らなくなることがあります。つまり残しておかない方がいいでしょう。

typ

型レベルの評価結果を表示します。型の評価結果がどうなっているかわからない際に使います。例えば "nat ⇒ nat option list" がどのように結合されてるかわからない場合はとりあえず括弧をつけて typ に投げます：

typ "(nat ⇒ nat) option list"
(* "(nat ⇒ nat) option list" *)
 
typ "nat ⇒ (nat option list)"
(* "nat ⇒ nat option list" *)

下が調べたいものと評価結果が一致しているので下で解釈されているとわかります。

sledgehammer

theorem や lemma などの文脈で後述の auto メソッドより強力な自動証明を実行してくれます。数ある定理証明支援系の中でも Isabelle のキラーコンテンツになっています。

nitpick

theorem や lemma などの文脈で自動で反例を見つけてくれますが、ときに反例になってない反例を見つけてくることがあります。

quickcheck

theorem や lemma などの文脈で自動で反例を見つけます。nitpick のような誤判定はないですが、チェックできる対象が Enum.enum 型クラスを実装している必要があり、自分で定義した代数的データ型が証明で使われると一手間いります。標準ライブラリにおける型クラスの実装例は src/HOL/Enum.thy にあります。なお、これをそのままコピペしても名前空間の問題とかでだいたい動かないので注意が必要です。

自分で実装させた例

datatype 'a diff_elem2 = L2 'a | R2 'a | LR2 'a 'a
 
instantiation diff_elem2 :: (enum) enum
begin
 
definition enum_diff_elem2 where
  "enum_diff_elem2 ≡ (map L2 Enum.enum) @ (map R2 Enum.enum) @ (map (λ(x, y). LR2 x y) (List.product Enum.enum Enum.enum))"
 
definition enum_all_diff_elem2 where
  "enum_all_diff_elem2 P ≡ (Enum.enum_all (λx. P (L2 x))) ∧ (Enum.enum_all (λx. P (R2 x))) ∧ (Enum.enum_all (λx. Enum.enum_all (λy. P (LR2 x y))))"
 
definition enum_ex_diff_elem2 where
  "enum_ex_diff_elem2 P ≡ (Enum.enum_ex (λx. P (L2 x))) ∨ (Enum.enum_ex (λx. P (R2 x))) ∨ (Enum.enum_ex (λx. Enum.enum_ex (λy. P (LR2 x y))))"
 
lemma UNIV_diff_elem2_conv: "UNIV = (range L2) ∪ (range R2) ∪ (⋃ (range (λx. range (λy. LR2 x y))))"
  apply(auto)
  apply(rule_tac y=x in diff_elem2.exhaust)
  apply(auto)
  done
 
instance
  apply(standard)
  apply(simp_all only: enum_diff_elem2_def enum_all_diff_elem2_def enum_ex_diff_elem2_def UNIV_diff_elem2_conv)
  apply(auto simp add: distinct_map enum_UNIV enum_distinct distinct_product inj_def)
  apply(blast)+
done
end

よく使う手動系メソッド

メソッド は apply に指定されるやつです。

以下の説明では 帰結側 とは A ⟹ B の B 側を意味していて、前提側 とは A ⟹ B の A 側を意味しています。前提が複数ある ⟦ A; B ⟧ ⟹ C の場合は、A と B の両方が前提で C が帰結です。なおこの ⟦ A; B ⟧ ⟹ C の別の書き方として A ⟹ B ⟹ C ともできますが前提は A と B、帰結が C に変わりはありません。

rule_tac/drule_tac/frule_tac/erule_tac

subgoal を定理で書き換えていくやつで書き換え方にバリエーションがあります：

apply(rule_tac foo)

定理 A ⟹ B の帰結 B と subgoal の C ⟹ B の帰結 B をマッチして書き換えます。この場合 subgoal は C ⟹ A に変わります。マッチするものがなければエラーになります。

どういう意味かというと「C のもとで B が成り立つ」のを証明したい状況で、あらかじめ「A ならば B が成り立つ」という定理が証明されているとします。このとき「C のもとで A が成り立つ」を証明できれば「C のもとで B が成り立つ」が言えるよね、ということです。

apply(drule_tac foo)

定理 A ⟹ B の前提 A と subgoal の A ⟹ C の前提 A をマッチして書き換えます。この場合 subgoal は B ⟹ C に変わります。マッチするものがなければエラーになります。

どういう意味かというと「A のもとで C が成り立つ」のを証明したい状況で、あらかじめ「A ならば B が成り立つ」という定理が証明されているとします。このとき「A のもと C が成り立つ」の subgoal では「A のもと B は成立しているはず」です。そこで subgoal A ⟹ C の前提 A を B に書き換えて「B が成り立っていれば C が言える」が証明できれば、「A のもと C が成り立つ」と言えるよね、ということです。

apply(frule_tac foo)

定理 A ⟹ B の前提 A と subgoal の A ⟹ C の前提 A をマッチして subgoal の前提に B を追加します。この場合 subgoal は ⟦ A; B ⟧ ⟹ C に変わります。マッチするものがなければエラーになります。

やってることは drule_tac と同じですが、drule_tac は元の前提を消してしまうのに対して frule_tac は消さないという違いがあります（この差によって frule では証明できるが、drule では必要な元の前提が消えてしまって証明できないのように明暗が別れうるので使い分けが大事）。

apply(erule_tac foo)

定理 ⟦ A; B ⟧ ⟹ C の前提 A・帰結 C と、 subgoal の ⟦ A; D ⟧ ⟹ C の前提A・帰結 B をマッチして書き換えます。この場合 subgoal は D ⟹ B に変わります（この規則が最も複雑）。前提と帰結の両方にマッチするものがなければエラーになります。

「A と D のもとで C が成り立つ」のを証明したい状況で、あらかじめ「A と B のもとで C が成り立つ」という定理が証明されているとします。subgoal では「A が成り立っている」とされているので、「定理の前提 B を証明できれば定理と subgoal 双方に共通して帰結 C が言える」状況です。そこで「subgoal 側の余分な前提 D のもとで定理の前提 B が成り立つ」といえれば、「A と D のもとで C が成り立つ」と言えるよね、ということです。

この書き換え規則は場合わけの定理でよく使われます（それ以外にも使われます）。例えば「A がなりたつならば B か C のどちらかの場合しかない。したがって、B と C のいずれのときでも X が成り立てばどんなときでも X が成り立つ」という定理は次のような形になります：

⟦ A; B ⟹ ?X; C ⟹ ?X ⟧ ⟹ ?X

このルールは subgoal の A ⟹ Y を証明したい場合に、erule で定理の前提の A と帰結の ?X（? はなんでもマッチする自由変数の意味）の両方をマッチさせて、2 つの subgoal B ⟹ Y と C ⟹ Y を作ります（狙い通り場合わけされた）。

バリエーション

apply(rule_tac x="y" in foo) （drule_tac/frule_tac/erule_tac も同様）

定理 foo を subgoal にマッチする際に定理内の自由変数に具体的な指定をつけます。x="y" は定理 foo 内の自由変数 ?x を y として書き換える指示になります。例えば定理 foo が P ?x ⟹ Q ?x だったならば P y ⟹ Q y とみなして適用するということです。

もし自由変数が引数をもつ場合（関数や述語など）はラムダ式で引数の数を揃える必要があります（例: 定理 foo が ?f x y の場合は apply(rule_tac f="λx y. x + y" in foo) のようにします）。 複数の自由変数を指定する場合は and で繋ぎます（例: apply(rule_tac x="y" and z="w" in foo)）。

apply(rule foo) （drule/frule/erule も同様）

定理内で自由変数の指定が必要なければ _tac を省略できます（kuniwak注: 内部的には色々違うらしいがよくわからない・・・）。

assumption

今の subgoal で前提から帰結と全く同じものがあらわれた際に subgoal を証明できたことにします。例えば次のような subgoal ⟦ A; B ⟧ ⟹ A や ⟦ A; B ⟧ ⟹ B は assumption で証明できます。意味は「前提より明らか」。

subst

等式 A = B の形で書かれている定理（または定義）を使って subgoal の中の A を B へ書き換えます。置き換え番号の指定・帰結と前提の選択・等式の逆転のオプションは組み合わせて指定できます。

バリエーション

apply(subst foo)

帰結側にあらわれる A を 1つ B へ置き換えます。

apply(subst (1 2) foo)

帰結側の左から 1 と 2 番目の A を両方とも B に書き換えます（数字は 1-based index です）。

apply(subst foo[symmetric])

帰結側にあらわれる B を 1つ A へ置き換えます（foo を逆転させたバージョン）。

apply(subst (asm) foo)

前提側の1つを置き換えます。

apply(subst (asm) (1 2) foo[symmetric])

前提側の左側から 1 と 2 番目の B を両方とも A に書き換えます。

unfold

等式 A = B の形で書かれている定理（または定義）を使って、すべての subgoal ですべての A を B へ置き換えます。帰結と前提のどちらも書き換わります。

例えば definition で定義したものは何もしなければ属性がついておらず auto などで解けないので、unfold などで開いてから auto した方が自動証明は進みやすいです。 他にも簡約を試みる simp と違って余計に簡約することはしないので simp が帰ってこない場合でも安心して使えます。

バリエーション

apply(unfold foo)

すべての subgoal で A をすべて B で置き換えます。

apply(fold foo)

すべての subgoal で B をすべて A で置き換えます（実は apply(unfold foo[symmetric]) で同じことができるがほぼ使わないのでどっちでもいい）。

case_tac

指定した項で場合わけします。

バリエーション

apply(case_tac "foo")

今の subgoal を foo の型で場合わけします。例えば foo が論理式であれば bool 型なので True の場合と False の場合で subgoal が分解されます（前提側に場合わけしたケースが入って subgoal が分裂する）。

apply(case_tac "my_type")

独自定義した代数的データ型でも、それぞれの値コンストラクタで場合わけできます。または apply(rule my_type.exhaust) でも同じことをできます。

subgoal_tac

今の subgoal の前提に指定した補題を追加し、最後の subgoal に指定した補題が加わります。

バリエーション

apply(subgoal_tac "foo")

今の subgoal の前提に論理式 "foo" を追加します。例えば subgoal が ⟦ A; B ⟧ ⟹ C だった場合は ⟦ A; B; foo ⟧ ⟹ C になります。ただし、最後の subgoal に "foo" が追加されます（部分的に解くのを後回しにしているだけ）。

apply(subgoal_tac "x = y")

bool な型を持つものならなんでも補題として追加できるので等式などの論理式も使えます。

intro

今の subgoal で rule foo が失敗するまで1回以上繰り返します。1回も成功しない場合は失敗になります。 よく指定する定理は allI/impI/conjI ですが、だいたい clarify で全部やってくれるので clarify が余計なことをしてくるときのみ出番があります。

なお apply(intro foo) と apply(rule)+ の違いは、前者は「fooを繰り返し適用する」、後者は「そのときどきで可能なruleを繰り返し適用する」です。

違いが分かる例

definition "A ≡ True"
definition "B ≡ True"
definition "C ≡ True"
lemma [intro]: "A"
  sorry
lemma [intro]: "B"
  sorry
lemma [intro]: "C"
  sorry
 
theorem "A ∧ B ∧ C"
  apply(intro conjI)
     apply(rule)+
  done
 
theorem "A ∧ B ∧ C"
  apply(rule)+
  done

elim

今の subgoal で erule foo が失敗するまで1回以上繰り返します。1回も成功しない場合は失敗になります。 よく指定する定理は exE/conjE ですが、だいたい clarify で全部やってくれるので clarify が余計なことをしてくるときが出番です。あとは clarify は subgoal の分割をしないので disjE だけは elim することがありますがごく稀です。

よく使う自動系メソッド

早見表

メソッド	主な使い方	自動で解ける範囲	帰ってこなさ
auto	証明がめんどくさいときにまず試すやつです。帰納法などはやってくれないので、帰納法が必要そうな形式なら先に適用しておいてから auto します。 なお、定理に属性をつけすぎるとどっかで無限ループしてすぐ帰ってこなくなるので慎重につける方がいいです。 また、大きめな証明では過剰に展開しすぎてしまって subgoal の出どころがわからなくなるときがあります。その場合には、forceで小刻みに証明するといいでしょう。	中	大
clarify	auto も force も simp も帰ってこない場合の最後の拠り所で頻繁に使います。	極小（自動で解くためのものではない）	無
clarsimp	simp が帰ってくるマシな状況で手動証明に取り掛かる際の初手です。	小	小
force	auto が帰ってこなかったものの、今の subgoal は自動で解けそうなときに試すやつです（auto は全部の subgoal を解こうとするので後ろの方の subgoal で帰ってこれないと全体として帰ってこなくなる）	中	中
simp	force でも帰ってこないので諦めて手動で解くときの道具。でもたいてい clarsimp の方が便利です。 auto ほどじゃないけど属性をつけすぎるとどっかで無限ループして帰ってこなくなるので困るので属性付与は慎重に。	小	小
simp_all	unfold 代わりに使えるらしいけどあんまり使う機会ないやつです。証明を短くするのには役立つかもしれないかも…？	小	中
sledgehammer	auto では解けなかったものの、なんとなく解けそうな直感があるときに試すやつですが、try の方がお勧めです（理由は try に書きました）。	大	極大（ただし一定時間でタイムアウトになる）

ここに書いていないものに metis や blast fastforce などなどたくさんありますが、私はこれまでいずれも直接書くというより sledgehammer が提示してくる場合に使う程度なので省略しました。

なお自動証明で使われる規則の属性から強さが透けてみえます：

Isabelle/Isar Reference Manual Appendix A.4.

（出典: Isabelle/Isar Reference Manual Appendix A.）

それぞれの属性にどのような定理が含まれるかは print_claset コマンドで確認できます：

safe introduction rules (intro!):
    bdd_below ?A
    bdd_above ?A
    ?A = ?B ⟹ principal ?A = principal ?B
    ?A ⊆ ?B ⟹ principal ?A ≤ principal ?B
    ?x = ?ya ⟹ word.Word ?x = word.Word ?ya
    ...
 
introduction rules (intro):
    bdd_below {?a..}
    bdd_below {?a..?b}
    bdd_below {?a..<?b}
    bdd_below {?a<..}
    ...
 
safe elimination rules (elim!):
    ⟦principal ?A = principal ?B; ?A = ?B ⟹ PROP ?W⟧ ⟹ PROP ?W
    ⟦principal ?A ≤ principal ?B; ?A ⊆ ?B ⟹ PROP ?W⟧ ⟹ PROP ?W
    ⟦word.Word ?x = word.Word ?ya; ?x = ?ya ⟹ PROP ?W⟧ ⟹ PROP ?W
    ...
 
...

auto

すべての subgoal を自動証明で進めます（証明できたところまでで止まる）。

バリエーション

apply(auto)

すべての subgoal に対して自動証明します。いずれかの subgoal で1つでも書き換えが成功すれば全体として成功として扱われ、1つも書き換えられない場合は失敗になります。最後まで証明できなくともある程度までは書き換えてくれます。

なお自動証明で使われる定理は [intro] [dest] [elim] [iff] [simp] などの属性が付与された定理です（標準ライブラリ内ではたくさん付与されている）。使われる定理の一覧は print_claset コマンドで確認できます。

なお、属性を付与すれば自動証明は強くなりますが闇雲につけると無限ループなどで auto が帰ってこなくなって auto が使いものにならなくなるリスクがあります。auto が封じられると非常に痛いので属性は慎重につけましょう。

apply(auto simp add: foo)

すべての subgoal に対して追加で簡約規則として定理 foo を追加して自動証明します。simp add: 以外にも intro: foo のように elim: や dest: も追加できます。

force

今の subgoal を自動証明します。auto とは異なり、subgoal を自動で最後まで証明しきればければ失敗扱いになります（auto は少しでも証明が進めば途中の状態で止まる）。

自動証明で使われる定理は auto と同じく [intro] [dest] [elim] [iff] [simp] などの属性が付与された定理です

clarify

今の subgoal を自動で見通しのいい形へ整理します（subgoal に既に x = y の形の前提がある場合に x を y で置き換えてくれたりします）。

バリエーション

apply(clarify)

今の subgoal を安全な規則のみかつ subgoal の分割が発生しないように自動で整理します（これで証明が通ってしまうこともある）。整理のためのメソッドなので simp より証明の力は弱いですが、無限ループするリスクは simp より少ないです。

apply(clarify intro: foo)

追加で導入規則に定理 foo を追加します。

simp

今の subgoal を自動で簡約します。

バリエーション

apply(simp)

今の subgoal を自動で簡約します。auto とは異なり簡約以外のことはしないため証明の力は弱いです。ただし無限ループするリスクは auto より少ないです。

apply(simp only: foo bar)

簡約規則が無限ループする場合などに特定の簡約規則のみで自動で簡約します。

apply(simp add: foo)

簡約規則に foo を追加して自動で簡約します。

clarsimp

今の subgoal を自動で整理・簡約します（clarify + simp）。

バリエーション

apply(clarsimp)

今の subgoal を見通しのいい形へ自動で整理しつつ簡約も同時にかけます

apply(clarsimp simp add: foo)

simp へのオプションは simp add: や simp only: のように渡せます intro: や dest: や elim: も指定できます。

simp_all

すべての subgoal を自動で簡約します。

バリエーション

apply(simp_all)

すべての subgoal を自動で簡約します。

apply(simp_all only: foo)

すべての subgoal を自動で簡約します。一部のループしない暗黙的な簡約規則は残るらしいので unfold よりわずかに強いようです。

apply(simp_all add: foo)

簡約規則に foo を加えて自動で簡約します。

終わりに

本記事では私がよく使う Isabelle の apply-script スタイルの便利機能の紹介とごく個人的に感じている使い所などを紹介しました。もしここに書いていないものを知りたい場合は「The Isabelle/Isar Reference Manual」を見てみるといいでしょう（もちろんここに書いてあるメソッド・コマンドは全部載っています）。

また、記事冒頭でも書きましたが、もし「これめっちゃ便利だけど書いてない！」みたいな気づきがありましたらご指摘いただけると嬉しいです！

宣伝

また DeNA 公式 Twitter アカウント @DeNAxTech では色々な勉強会での登壇資料も発信してます。ぜひフォローして下さい！