ホワット・ア・ワンダフル・ワールド The Coq Proof Assistant A Tutorial (5) 自然演繹法 II

The Coq Proof Assistant A Tutorial (5) 自然演繹法 II

前回は自然演繹法についてちょっと書いただけで終ってしまったのですが，今回はちゃんと Coq を使います (笑)

とりあえず，Coq のコマンドと，自然演繹法の推論規則の対応を押さえておきましょう．

→ 導入: intro H.
→ 除去: generalize (H1 H2); intro H3.
∧ 導入: split
∧ 除去: elim H; intros H1 H2.
∨ 導入の左側: left.
∨ 導入の右側: right.
∨ 除去: elim H; [intro H1 | intro H2].
￢導入: intro H.
￢除去: absurd A; try assumption. とか contradiction. らしい．まだよくわかりません．
後ろ向き推論: apply

とりあえず，対応表にそって，テキトーに証明を行ってみましょう．

例題は，チュートリアルの通りに，A ∧ B → B ∧ A という，もう証明するまでもなくいかにも成り立ちそうなやつでやってみましょう．


$ coqtop
Welcome to Coq 8.0pl3 (Jan 2006)

Coq < Section Minimal_Logic.

Coq < Variable A B C : Prop.
A is assumed
B is assumed
C is assumed

(* Coq では，∧ は /\\， ∨ は \\/ と書きます *)
(* しかし，HTML では，\\ がそのままでは出ないので，
\\\\ とかに一々書き換えるのが面倒くさい… *)

Coq < Lemma and_commutative : A /\\ B -> B /\\ A.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  ============================
   A /\\ B -> B /\\ A

(* とりあえず，P → Q  の形があったら，P を仮定してみようじゃないか *)

and_commutative < intro.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  H : A /\\ B
  ============================
   B /\\ A

(* とりあえず，∧ 除去規則にしたがって，∧ を分解してみよう *)

and_commutative < elim H ; intros H1 H2.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  H : A /\\ B
  H1 : A
  H2 : B
  ============================
   B /\\ A

(* B ∧ A を成り立たせるためには，A と B を両方仮定から成り立たせれば良い *)

and_commutative < split.
2 subgoals

  A : Prop
  B : Prop
  C : Prop
  H : A /\\ B
  H1 : A
  H2 : B
  ============================
   B

subgoal 2 is:
 A

(* B を成り立たせないといけないのか…
ん ? しめた，B は既に H2 で仮定されてるぞ ! *)

and_commutative < exact H2.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  H : A /\\ B
  H1 : A
  H2 : B
  ============================
   A

(* 同様に，A も．このために，先に A ∧\ B を分解しておいたのだ *)

and_commutative < exact H1.
Proof completed.

返す刀で，A ∨ B → B ∨ A も証明して見ましょう．


Welcome to Coq 8.0pl3 (Jan 2006)

Coq < Section Minimal_Logic.

Coq < Variable A B C : Prop.
A is assumed
B is assumed
C is assumed

Coq < Goal A \\/ B -> B \\/ A.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  ============================
   A \\/ B -> B \\/ A

(* もうすっかりおなじみ DA･YO･NE *)

Unnamed_thm < intro H ; elim H.
2 subgoals

  A : Prop
  B : Prop
  C : Prop
  H : A \\/ B
  ============================
   A -> B \\/ A

subgoal 2 is:
 B -> B \\/ A

(* A \\/ B -> A \\/ B を成り立たせるためには，
A か B のどちらかが成り立てば，必ず
A \\/ B が成り立つことを示せばよい…
って，これってただ，論理式を丁寧に読み替えただけですな．
要するに，両経路を成り立たせる *)

(* とりあえず， A -> A \\/ B が成り立つことを示そう *)
Unnamed_thm < intro.
2 subgoals

  A : Prop
  B : Prop
  C : Prop
  H : A \/ B
  H0 : A
  ============================
   B \\/ A

subgoal 2 is:
 B -> B \/ A

(* B \\/ A は，A か B のどちらかが仮定から導き出せれば成り立つ *)

(* とりあえず，右の A を成り立たせよう *)
Unnamed_thm < right.
2 subgoals

  A : Prop
  B : Prop
  C : Prop
  H : A \\/ B
  H0 : A
  ============================
   A

subgoal 2 is:
 B -> B \\/ A
(* 当然これは，トリビアルに (1 ステップで) 成り立たせることができる *)

Unnamed_thm < trivial.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  H : A \\/ B
  ============================
   B -> B \\/ A

(* 残りも同様に *)
Unnamed_thm < intro.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  H : A \\/ B
  H0 : B
  ============================
   B \\/ A

Unnamed_thm < left.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  H : A \\/ B
  H0 : B
  ============================
   B

Unnamed_thm < trivial.
Proof completed.

練習のため，本当に丁寧に証明過程を記述しましたが，実際は auto コマンドなどを用いて，もっと簡単にできます．


Unnamed_thm < Restart.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  ============================
   A \\/ B -> B \\/ A

Unnamed_thm < intro H ; elim H ; intros.
2 subgoals

  A : Prop
  B : Prop
  C : Prop
  H : A \\/ B
  H0 : A
  ============================
   B \\/ A

subgoal 2 is:
 B \/ A

Unnamed_thm < auto.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  H : A \\/ B
  H0 : B
  ============================
   B \\/ A

Unnamed_thm < auto.
Proof completed.

また，お気づきのように，当然のことながら仮定 H (A \\/ B) は，A または B が仮定された瞬間，全く不要になります．

このような重複した仮定がそのままになっていると，(トリビアルな証明ならそれほど問題にはなりませんが) 仮定が多くなりすぎて，とても見通しが悪くなってしまいますし，たとえ証明できたとしても「美しく」ありません．

clear コマンドを使用すると，不要な仮定を消去できます．


Unnamed_thm < Restart.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  ============================
   A \\/ B -> B \\/ A

Unnamed_thm < intro H ; elim H.
2 subgoals

  A : Prop
  B : Prop
  C : Prop
  H : A \\/ B
  ============================
   A -> B \\/ A

subgoal 2 is:
 B -> B \\/ A

Unnamed_thm < intro.
2 subgoals

  A : Prop
  B : Prop
  C : Prop
  H : A \\/ B
  H0 : A
  ============================
   B \\/ A

subgoal 2 is:
 B -> B \\/ A

Unnamed_thm < clear H.
2 subgoals

  A : Prop
  B : Prop
  C : Prop
  H0 : A
  ============================
   B \/ A

subgoal 2 is:
 B -> B \\/ A

Unnamed_thm < right.
2 subgoals

  A : Prop
  B : Prop
  C : Prop
  H0 : A
  ============================
   A

subgoal 2 is:
 B -> B \\/ A

Unnamed_thm < auto.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  H : A \\/ B
  ============================
   B -> B \\/ A

Unnamed_thm < auto.
Proof completed.

このように，trivial は，auto コマンドに似てますが，より効率を重視 (1 ステップで成り立つことを前提とした推論) した自動検証になっています．

auto コマンドも，一見凄そうに見えますが，実はそんなに強力ではありません．auto は，一切除去を行わないので，上記のような本当にトリビアルなトートロジー (恒真式) すら証明できません．


Unnamed_thm < Restart.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  ============================
   A \\/ B -> B \\/ A

Unnamed_thm < auto.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  ============================
   A \\/ B -> B \\/ A

これは，効率のためだそうです．どんな論理式でも，いつかかならず証明でき，かならず停止するようなアルゴリズムは，チューリングの停止性問題との兼ね合いで，絶対に存在しません．

全てを機械的にやるのはどのみち無理なので，人間の洞察が要るようなステップは人間にまかせて，本当に単純なマッチングのみを効率的に行う，という Coq の思想は，理にかなっていると思います．

けっこう長くなってきたので，今日のところはこの辺で～．

Pagetop

The Coq Proof Assistant A Tutorial (6) トートロジーの自動証明 « ホーム » The Coq Proof Assistant A Tutorial (4) 自然演繹法

トラックバック

この記事にトラックバックする(FC2ブログユーザー)

Pagetop

> これは，効率のためだそうです．どんな論理式でも，いつかかならず証明でき，かならず停止するようなアルゴリズムは，チューリングの停止性問題との兼ね合いで，絶対に存在しません．

まだ単純な命題論理しか扱ってない時点でそれを言われてもあまり説得力がないような…　たしか命題論理ってdecidableじゃありませんでしたっけ?

2006-04-30 09:36 :
さかい URL :
編集

> さかいさん

>> 命題論理ってdecidable

あぁ，そうかもしれません (^^;

弱い体系の話をしているときなのに，私の頭の中には，最終目標 (高階論理) のイメージがあって，ごっちゃになっていました (汗)

しかし，たとえ決定可能 (decidable) であっても，現実的なオーダ (が保証されるアルゴリズム) にはならなかったような気がしますね… よくわかりませんが (すみません)．

命題論理の短い証明ならば，タブロー法か何かで，簡単に自動証明できるのかもしれませんね．

自然演繹の方は… なんとなく，elim が絡んでくると，下手すると，途中で無限ループとかになりそうな気がします (印象論ですが…)．

そんなこんなで，たぶん Coq は，汎用の定理証明器を意識していると思うので，もろもろを考えたトレードオフでこうなっているのではないかと思います．

# 書けば書く程，どんどんボロが出てくるなぁ… さかいさんのつっこみ，非常にありがたいです．大感謝！ (^o^)

2006-04-30 11:13 :
あろは URL :
編集

Pagetop

« 前のページホーム次のページ »

Pagetop

ホワット・ア・ワンダフル・ワールド

The Coq Proof Assistant A Tutorial (5) 自然演繹法 II

> さかい さん

> さかいさん