Coq命題論理の証明

Coq命題論理の証明

命題論理の例題をtautoに頼らずに証明するためのTips

大まかなtacticを使う順序

大体、下記の原則で考える。

• まずgoalをintroを使って分解して、goalを簡単にし、仮定を増やす事を考える。
  • goalが -> の式の場合（演算子順序を考えると A -> B の形の式と考えられる場合）は、intro, intros などを使えばOK、
  • goalが ~ の式（演算子順序を考えると ~X の形）の場合、goalがFalseになるまでintroして、「goal=Falseの場合」へ。
• goalを導ける仮定がある場合（goalがAで、H: X->A のような仮定がある場合）、apply H してgoalをXに変更する。
• goal, 仮定の /¥, ¥/ は基本的には仮定の方から先に処理するのが楽だと思う。
  • 仮定が H: A /¥ B の形なら destruct H as [HA HB]、仮定が H: A ¥/ B の形なら destruct H as [HA | HB] の様に仮定Hをより簡単な式に分解する。（destructの使い方はガリグ先生の講義資料に詳しい）
    • H: A ¥/ B の形をdestructすると、HがHAに変わった場合と、HがHBに変わった場合の２つに証明が分岐してしまう。なので二度手間を避ける意味では他のところから手を付けた方が手間は減るのだが、場合分けしてしまった方が式が簡単になるというメリットもある。
  • goalが A ¥/ B の形の場合、今の手持ちの仮定を眺めて A と B とどちらなら仮定から証明出来るか考える。もし判らないならば、まだleftとかrightとかを入力すべきタイミングでは無いのかもしれない。（もしかして仮定の¥/をdestructすべきで無かった場合もあり得る？）
  • goalが A /¥ B の形の場合、split すると goal=A, subgoal=B となる。ここで証明が分岐してしまうので、goalをsplitする前に仮定のdestructを先にやった方が二度手間にならずに済む。
  • つまり、仮定の /¥ の destructは優先、goalのsplitは安全だが二度手間は増える、goalのleft/rightは行けると思えば早めに実施だが判らない時は後回し、仮定の¥/のdestructは優先順位低い。
• elim Hは今ひとつ使い方が明確でないので、使用の優先順位を下げた。他にやれる事が無い場合はelimするしか無い。
  • goal=Falseの場合で、仮定の中でH:~Xの形をしているものがあれば、比較的優先してelim Hする。するとgoal=Xになる。その様なHが複数ある場合は迷うが、同じ仮定を何回もelimするメリットはあまり無いことが多い様にも思う。

その他

• apply False_ind. を行うとゴールが何であれ、goal=Falseになってしまう。通常は使える情報が減るだけなので使わないが、二重否定除去を使う様な問題でたまに使う。
• 仮定に二重否定除去規則を含んだ古典論理の問題は、Hypothesis NNPP : forall P : Prop, ~~P -> P. ならば、初手は apply NNPPする。（Pが古典論理で証明出来るならば、~~Pは直観論理で証明出来る。従って初手は~~をgoalに付ける。）
• 二重否定除去規則から排中律を出す証明は「そもそも頭が良い」か「証明の型を知っている」のどちらかが必要なんじゃないかしらん。素直に証明を検索するのがいいかも。なお、tautoで証明してPrintすれば証明の型を知る事ができるので、そこから証明を考えるのも勉強になります。
• 逆に排中律から二重否定除去規則を出すのは簡単です。というのは、排中律を仮定しちゃうと簡単に場合分け出来ちゃうから。

知ってると便利なTips

• 今、仮定 H : xxx があれば便利なのに、と思った場合、cut H : xxx と入力すると仮定 H : xxx が増える。但し、subgoalにxxxが追加され、後から証明する必要がある。証明順序を入れ替えるのに使えるので、人間が考える際に便利な事が多い。
  • 例えば EM : forall P : Prop, P ¥/ ~P. とかが仮定にある場合、cut HA : A ¥/ ~A. cut HB : B ¥/ ~B. みたいに全部の命題変数について仮定を増やしてdestruct HA as ... みたいに場合分けすれば簡単に証明可能。
• tautoで自動証明（古典論理でしか証明出来ない場合は ~~ つけて tauto）して、Print して証明を与える式を調べる、というのは手で証明するののヒントになる。