Isabelleの練習 - 命題論理の自然演繹

「PPLサマースクール2017 Isabelle/HOL による証明とプログラミング」 http://ppl.jssst.or.jp/index.php?ss2017 を受講しに行っていた。結果として自分がIsabelleを咀嚼するのはまだかかりそうだという感想だったが、もっと初歩的なことをやって練習していくことにしたい。

題材としては論理学の教科書に出てくるような自然演繹による証明をIsabelleでやってみることにする。

自然演繹というのは、命題論理の証明を「P,Q... |- R」のように前提P,Q,...から帰結Rが出てくるものとするとP,Q,...に対してあらかじめ用意されたルールを適用して変形することで最終的にRが出てくれば証明完了というものだ。

Isabellの証明はtheoryという構造の中に書く。jEditで次のようなファイルを作ってNaturalDeduction.thyというファイル名で保存する。

theory NaturalDeduction
  imports Main
begin
  (* ... *)
end

ファイル名とtheoryの名前は一致しなければならない。また、jEditは特に拡張子を自動でつけてくれないが、拡張子がないと証明ファイルとして認識されないので注意しなければならない。

"imports Main"とは何か、はよくわかっていないが気にしないことにする。#include <stdio.h>のようなものだろう。

コメントはMLスタイルで、「(*」と「*)」で囲む。

1つ目の例題として、"P∩Q, R |- Q∩R"を証明してみよう。なお、この記事で使う例題はすべてHuth and Ryan (2004) "Logic in Computer Science"から採っている。

これを証明するにはまずP∩QからQを取り出し（P∩Qが成立するということはQ単独でも成立する）、QとRからQ∩Rを作る（QとRが成立するということはQ∩Rも成立する）必要がある。

問題はIsabelleでそのようなルールが何という名前で提供されているかだが、既存の定理を探すにはfind_theoremsというコマンド（？）を使う。

find_theorems "_ ∧ _ ⟹ _"
find_theorems "_ ⟹ _ ∧ _"

このように書くと検索結果の最初のほうに出てくるconunct2とconjIが求めているものだとわかる。

  HOL.conjunct2: ?P ∧ ?Q ⟹ ?Q
  HOL.conjI: ?P ⟹ ?Q ⟹ ?P ∧ ?Q

さて、"P∩Q, R |- Q∩R"という定理を表明するにはこのように書けばいいようだ。

theorem Example_1_4:
  (*fixes P Q*)
  assumes 1: "P ∧ Q"
  assumes 2: "R"
  shows "Q ∧ R"

つまり前提をassumes、帰結をshowsのところに書く。前提はassumes 1: "P ∧ Q" and 2: "R"と書いてもいいようだ。

コメントアウトしているfixes P Qは「任意のPとQをとった時に」という意味だがこれは書かなくても暗黙の裡にそうなるそうだ。

「1:」とかいうのは前提などに後で使うための名前を付けている。

これだけだと問題を表現しただけで、証明ではない。証明は続けて書くのだが、こうなる。

proof-
  have 3: "Q" using 1 by (rule conjunct2)
  show 4: "Q ∧ R" using 3 2 by (rule conjI)
qed

proofのあとにハイフンをつけるのは…なんだっけ。セミナーで説明してもらったと思うのだがあまり理解できず、忘れてしまった。ともかくこの例ではハイフンを消すとエラーになる。

前提からこういう事実が導けますというのをhaveとかshowで宣言する。haveとshowの違いは、途中に来るのがhaveで最後に来る（証明したかった）ものがshowだと考えればよいようだ。

1から3はconjunct2で変形できるのでby (rule conunct2)になる。usingがIsabelle的にどういう機能なのかきちんと理解していないのだが、とりあえずこの例ではルールの引数を指定するようなイメージのものだと解釈できる。3と2を使ってconjIを使うと4が出せる。

なお、jEditのOutputパネルでProof stateを表示しておくとproofの先頭にカーソルを置くと

proof (state)
goal (1 subgoal):
 1. Q ∧ R

と表示され、show 4:...の行末では

goal:
No subgoals!

となる。「No subgoals!になったらそこにqedと書く」と思っておけばよいようだ。

次に二重否定の除去（~~PからPを導く）と導入（Pから~~Pを導く）を扱う例を書きたい。

find_theorems "¬¬ _ ⟹ _"
theorem notnotI: "P ⟹ ¬¬P" by auto

検索により二重否定の除去はnotnotDが使えるとわかる。二重否定の導入は見つからなかったので独自に定理として作る。by autoで自動的に証明できてしまうのだが、それがなぜかは気にしないことにする。

これらを使うと"P, ~~(Q∩R) |- ~~P∩R"の証明が書ける。

theorem Example_1_5:
  assumes 1: "P"
  assumes 2: "¬¬(Q∧R)"
  shows "¬¬P∧R"
proof-
  have 3: "¬¬P" using 1 by (rule notnotI)
  have 4: "Q∧R" using 2 by (rule notnotD)
  have 5: "R" using 4 by (rule conjunct2)
  show 6: "¬¬P∧R" using 3 5 by (rule conjI)
qed

次にmodus ponensとmodus tollensを使った証明をしたい。いずれもそのものはIsabelleの中にないようなので定理として作っておく。

theorem  mp: "(P⟹Q) ⟹ P ⟹ Q" by auto
theorem  mt: "(P⟹Q) ⟹ ¬Q ⟹ ¬P" by auto

"P⇒(Q⇒R), P, ~R |- ~Q"はMPとMTを順に適用することで証明できる。

theorem Example_1_7:
  assumes 1: "P⟹(Q⟹R)"
  assumes 2: "P"
  assumes 3: "¬R"
  shows "¬Q"
proof-
  have 4: "Q⟹R" using 1 2 by (rule mp)
  show 5: "¬Q" using 4 3 by (rule mt)
qed

次は==>を導入するような式変形ルールを使う。これはいままでのルールとはちょっと違って「Pを仮定したときにQが導けるならばP==>Qを導いてよい」というものだ。これをIsabelle上で行うには、"P==>Q"の証明の中でassume Pを使って最後にshow Qを行えばよい。

"~Q⇒P |- P⇒~~Q"を証明する例が次のものだ。

theorem Example_1_9:
  assumes 1: "¬Q⟹¬P"
  shows "P⟹¬¬Q"
proof-
  assume 2: "P"
  have 3: "¬¬P" using 2 by (rule notnotI)
  show 4: "¬¬Q" using 1 3 by (rule mt)
qed

==>がいくつもあるような証明を行うときは入れ子構造になる。

theorem Example_1_11:
  shows "(Q⟹R) ⟹ ((¬Q⟹¬P) ⟹(P⟹R))"
proof-
  assume 1: "Q⟹R"
  show "(¬Q⟹¬P) ⟹(P⟹R)"
    proof-
      assume 2: "¬Q⟹¬P"
      show "P⟹R"
        proof-
          assume 3: "P"
          have 4: "¬¬P" using 3 by (rule notnotI)
          have 5: "¬¬Q" using 2 4 by (rule mt)
          have 6: "Q" using 5 by (rule notnotD)
          show 7: "R" using 1 6 by (rule mp)
        qed
    qed
qed

これは前提がないので"|- (Q⟹R) ⟹ ((¬Q⟹¬P) ⟹(P⟹R))"ということである。いままでhaveやshowで宣言した式の証明をするのにbyを使ってきたが、ここではbyの代わりに入れ子のproofを書いている。

ただし上の例はフラットに書いても同じことができる。

theorem Example_1_11':
  shows "(Q⟹R) ⟹ ((¬Q⟹¬P) ⟹(P⟹R))"
proof-
  assume 1: "Q⟹R"
  assume 2: "¬Q⟹¬P"
  assume 3: "P"
  have 4: "¬¬P" using 3 by (rule notnotI)
  have 5: "¬¬Q" using 2 4 by (rule mt)
  have 6: "Q" using 5 by (rule notnotD)
  show 7: "R" using 1 6 by (rule mp)
qed

連言、二重否定、条件とやったので今度は選言を使う。選言には「PがいえるならばP∪Qも言える」というもの（導入）と、「P∪Qが言えて、Pの場合とQの場合でいずれもRが導けるならば、Rを導いてよい」（除去）の2つがある。

前者はIsabelleに既にあり、後者はなかったので独自の定理を作る。

find_theorems "_ ⟹ _ ∨ _"
theorem disjE: "P∨Q ⟹ (P⟹R) ⟹ (Q⟹R) ⟹ R" by auto

これらを両方使うと"Q⇒R |- P∪Q ⟹ P∪R"の証明が書ける。

theorem Example_1_16:
  assumes 1: "Q⟹R"
  shows "P∨Q ⟹ P∨R"
proof-
  assume 2: "P∨Q"
  show "P∨R"
  proof-
    have 34: "P⟹(P∨R)"
    proof-
      assume 3: "P"
      show 4: "P∨R" using 3 by (rule disjI1)
    qed
    have 57: "Q⟹(P∨R)"
    proof-
      assume 5: "Q"
      have 6: "R" using 1 5 by (rule mp)
      show 7: "P∨R" using 6 by (rule disjI2)
    qed
    show "P∨R" using 2 34 57 by (rule disjE)
  qed
qed

次に"P⟹(Q⟹P)"を証明することを考えてみる。この場合Pは前提としているんだからQは関係なくPを前提しているということからそのままPが出てくるはずだ。Huth and Ryan (2004)ではこのルールをcopyと呼んでいる。適当に入力してあたりをつけてみたところ、Isabelleでは「by assupmtion」と書けばいいようだ。

theorem Example_copy:
  shows "P⟹(Q⟹P)"
proof-
  assume 1: "P"
  show "Q⟹P"
  proof-
    assume 2: "Q"
    show 3: "P" using 1 by assumption
  qed
qed

次の証明では「Pと~Pが両方出てきたら矛盾している」と例の「矛盾からは何でも出てくる」を使う。前者はnotE、後者はFalseEとしてIsabelleで用意されている。

theorem Example_1_20:
  assumes 1:"¬P∨Q"
  shows "P⟹Q"
proof-
  have a: "¬P⟹(P⟹Q)"
  proof-
    assume a2: "¬P"
    show "P⟹Q"
    proof-
      assume a3: "P"
      have a4: "False" using a2 a3 by (rule notE)
      show "Q" using a4 by (rule FalseE)
    qed
  qed
  have b: "Q⟹(P⟹Q)"
  proof-
    assume b2: "Q"
    show "P⟹Q"
    proof-
      assume b3: "P"
      show "Q" using b2 by assumption
    qed
  qed
  show "P⟹Q" using 1 a b by (rule disjE)
qed

最後に「Pと仮定して矛盾が導かれるならばPではない（~Pを導ける）」を使う。これはIsabelleではnotIという名前である。

theorem Example_1_21:
  assumes 1: "P⟹Q"
  assumes 2: "P⟹¬Q"
  shows "¬P"
proof-
  have 36: "P⟹False"
  proof-
    assume 3: "P"
    have 4: "Q" using 1 3 by (rule mp)
    have 5: "¬Q" using 2 3 by (rule mp)
    show 6: "False" using 5 4 by (rule notE)
  qed
  show "¬P" using 36 by (rule notI)
qed

以上Isabelleで命題論理の自然演繹の証明をいくつか書いてみた。「～のようだ」が多い記事になったことは申し訳なく思う。