論理式の部分式への分解とサブゴール

【 サブゴールはどこから生まれるか 】

前回は、簡単な論理式からより複雑な論理式が構成できるという話をしました。今回のセッションは、その逆、複雑な論理式はより簡単な論理式に分解できるという話から始まります。

でも、この論理式の構成と分解というのは、別々のプロセスではなく、構成のルールが与えられれば、それを反対方向から見れば、分解のルールが与えられることに気づくと思います。

BAR（横棒）の上下に与えられた論理式の集まりを、上から下方向に読むか、逆に、下から上方向に読むかの違いがあるだけです。BAR（横棒）で、論理式の構成と分解を定義するというのは、実はとてもスマートな表現なのです。

今回のセッションでは、論理式の分解にフォーカスします。分解された論理式の一つ一つを「部分式」Sub-formula と呼ぶことにしましょう。

Coqでの証明は、複雑な問題を簡単な部分問題（Coqでは、それを「サブゴール」Sub-goalと呼んでいます）に分割して、そのサブゴールをすべて解くことで、元の問題を解くことを目指します。それは、「大きな問題を小さな問題に分割して解く」という考え方です。

証明のサブゴール(Sub Goal)と命題の部分式（Sub Formula）とは、名前は似ていますが、違うものです。ただ、複雑なものを簡単なものにするという点では、証明のサブゴール(Sub Goal)と命題の部分式(Sub Formula) は似ています。

Coqは、論理式の証明の場合には、証明のサブゴールへの分割と命題の部分式への分解の二つを、同時に行います。この場合には、サブゴールは、命題の部分式の分解の結果として生まれることになります。

もっとも、すべてのサブゴールが部分式への分解の結果として生まれるわけではありません。「数学的帰納法」を利用する場合のサブゴールは、それとは違う形をしています。数学の証明で、数学的帰納法はとても重要です。ただ、それについては章をあらためて、詳しく取り上げたいと思いますので、当面は忘れてもらっても結構です。

-------------------------------------

ショートムービー「 論理式の部分式への分解とサブゴール 」を公開しました。
https://youtu.be/wivcn0E0jvA?list=PLQIrJ0f9gMcPrNFRG1sEmtCRDnemxc1Pc

資料 pdf「論理式の部分式への分解とサブゴール 」
https://drive.google.com/file/d/1kmX2WvkAG_6tOdaER8fJTQdlD-TPwPfz/view?usp=sharing

blog：「 サブゴールはどこから生まれるか 」　

https://maruyama097.blogspot.com/2023/06/blog-post_16.html

「 はじめてのCoq 」まとめページ

https://www.marulabo.net/docs/hellocoq1/