概要
古典命題論理をCoq上で展開し、完全性定理・カット除去定理などを証明する coq-contrib/propcalc をコードリーディングした際のメモです。同好の士のために共有します。
propcalc は 6個のファイルから構成されますが、アルファベット順に読めばよいという親切設計です。概要を以下に記します:
- a_base.v: 命題変数とユーティリティ関数を定義します
- b_soundness.v: 健全性を証明します
- c_completeness.v: 完全性の証明をします
- d_hilbert_calculus.v: ヒルベルト流と自然演繹の同等性を示します
- e_sequent_calculus.v: シーケント計算と自然演繹の同等性を示します
- f_cut_elimination.v: カット除去定理を証明します
■ a_base.v
命題変数の型 PropVar を定義して、その決定性を仮定/公理 とします。命題変数の型を nat や string などにすることもできたでしょうが、必要な前提が明確となるという点でこの符号化は優れていると思います。
なお、 propcalc が前提とする仮定は この命題変数の決定性のみです。
■ b_soundness.v
構文論: 論理式型PropFをInductiveに定めます。その構成子から分かるように 論理記号として ⊥,⋀,⋁,→ を採用し、¬や↔はそれらを使って定義します。
意味論: 真理値の割り当ては PropVars->bool な関数を使ってPropF->boolという関数を構成することですが TrueQ というFixpointで素直に実装できます。これを使うと 充足関係Satisfiesや帰結関係Modelsや恒真性Validを定義できます。
証明論: 正しい推論であるNc型をInductiveに定義し Γ ⊢ A というNotationを導入します。推論規則を定義しているということです。前件Γの型はlist PropFで符号化します。論理的定理、すなわち前件が空リストで導出できる論理式に対してProvableという性質を定義します。
健全性と完全性: 以上より forall A, Provable A-> Valid A が命題論理の健全性を符号化した言明であり、その逆が完全性を符号化した言明であることが分かります。それぞれ Prop_Soundness, Prop_Completenessという名前を付けています。より一般にはΓが空でない時を証明する必要がありますが、それは Soundness_general で表します。実際はこちらを先に証明してから Prop_Soundnessを証明します。
健全性証明: 独自のLtacを使って、PropFの決定性・排中律・weakening・演繹定理を随時証明していくことで、証明します。
(Ltac)in_solve: 正しい推論を証明する際に出てくる頻出パターンは、context や Goal に In a Γ という形式を持つものです。ここでΓは何らかの形で分解可能である、すなわち x::Γ' や Γ1++Γ2 などの形式である場合です。そのような場合我々がやるべきことは明確で、Γをdestructして各分岐において少しシンプルになった問題をそれぞれ解けばよいのです。（discriminate等で簡単に証明しえないような）還元しきった問題はすでにNcの構成子で直接証明可能になっているはずです（これは証明できたはず。論理学の教科書を参考にしてください）。それを自動で行うのがこのtacticです。
(Ltac)case_bool: 真理値で場合分けするときのtacticです。真に割り当てられた場合と、偽に割り当てられた場合の二通りに分岐します。TrueQ版のリフレクションです。
■ c_completeness.v
ファイル冒頭に証明の全体像が書かれています。任意の論理式には対応する NNF, CNFがあるので、それらに関する性質を経由して証明します。
NNF関連: InductiveにNNF型を定義します。任意のPropFのオブジェクトをNNFに変形する手続きMakeNNFは、教科書通りにFixpointて実装できます。その逆、つまりNNF型をPropF型に変換するNNFtoPropFというFixpointも自然に実装できます。
CNF関連: Inductiveに定めたLiteral型に対し、その否定操作 Bar を Fixpointとして実装します。また list Literal として Clause を定義し、さらに list Clause で CNF を定義します。リストの各要素を or で結んだ disjunct が論理学での節になるわけです（実装上の都合で Clause の最右には⊥をくっつけます）。CNF を PropF に変換する手続き は CNFtoPropF です。NNFをCNFに変換する手続きMakeCNFも教科書どおりですが、リストでの実装なので一見不明瞭なので手を動かして確かめてみるとよいです。さて、Clauseに対して Valid_Clause という性質を定義できます。これは自明に真であるという構文的な性質で a)節に⊤が含まれる b)節にリテラルmとbar mが共に含まれている のどちらかが成立するものです。
完全性証明のアウトライン: 冒頭のコメントを引用します。証明で使っているtactic自体は、それほど難しいことをしているわけではないので、追えば理解できます:
- If a formula is valid, then so is its NNF;
- If a (formula in) NNF is valid, then so is its CNF;
- If a (formula in) CNF is valid then it's syntactically valid;
- If a CNF is syntactically valid, then its provable;
- If the CNF of a NNF formula is provable, then so is the NNF formula itself.
- If the NNF of a formula is provable, then so is the formula itself.
■ d_hilbert_calculus.v
証明系: Inductiveに論理的公理型 AxiomH を定義します。9つの公理図式を定義したことに相当します。やけに多いのは、論理記号として→,⋀,⋁を採用しているからです。またヒルベルト流の証明型 Hc をInductiveに定め Γ ⊢H A などのNotationを導入します。Hc の構成子が3つあるのは、正しい証明というのが a)非論理的公理そのものである b)AxiomHの例化となる公理である c) φ, φ→Ψ から Ψ を導出した の3パターンしかないことに相当します。なお、空列から導出される性質として ProvH を定義します。
ヒルベルト流と自然演繹の同等性: これまでのNotationを使うと、両者の証明能力が同等であることは forall Γ A, Γ ⊢ A <-> Γ ⊢H A とかけます。inductionを使って帰納的にやれば非常に簡単に証明できます。途中でヒルベルト流での演繹定理をレンマとして使うので証明しています。
■ e_sequent_calculus.v
計算規則: Γ ⊃ Δ というNotationを使って、カットありのシーケント計算の規則をInductive に符号化します。Γは list PropVar で In などを規則に使うので構造規則はつぶれてしまうので含みません。また、Nc型に合わせるために Γ ⊢⊢ Δ というNotationを導入します（Δのどれかの要素δについてΓ⊢δが成立することと定義します)
シーケント→自然演繹: forall Γ Δ, Γ ⊃ Δ -> Γ ⊢ ⋁Δ. が同等性の証明の片側です。これは結構簡単にできて ⊢ に関する性質が ⊢⊢ においても大体同じように成立するという幾つかのLemmaを証明して構成していきます。
自然演繹→シーケント: シーケント計算におけるweakeningの証明が難しいですが、それさえわかればinductionとカットを駆使して証明ができます。
■ f_cut_elimination.v
計算規則: Γ ⊃c Δ というNotationを使って、カットなしのシーケント計算の規則をInductive に符号化します。モデルを経由するので Γ =⊃ Δ というNotationも利用します（⊨との違いは帰結が list PropFであることです）。
証明方針: ⊃cの健全性と完全性を証明できれば、⊃c と ⊃ の同等性はほぼ自明です。健全性は簡単に証明できます(G_to_Gcf, G_sound を参照)。一方、完全性は少し厄介で構造的でない帰納/nonstructural inductionを用います。構造ではないなら何に対する帰納で証明するかというと、自然数であるシーケントの複雑性 sizes です。複雑性の定義は直観的なので読めば分かると思いますが、この方針での証明を追うのは少し難しいです。証明対象を inversion するとsizeが一つ以上減るので、帰納法の仮定が使える形になる、という感じです。