coqでド・モルガンの法則の証明をするまで (命題論理版)

証明支援システムのcoqを用いて、命題論理の推論規則による証明ができるようにする。
その到達地点として、ド・モルガンの法則の4定理をすべてcoqで証明するまで行う。
そのなかで、証明した「定理」を「プログラムでの関数」としての本体実装のコードを確認することで、その論理式や証明手順がもつ意味を確認していく。

• 続編: coqでド・モルガンの法則の証明(一階述語論理版)

coq公式リンク集

• サイト: https://coq.inria.fr/
• ソース: https://github.com/coq/coq/
• wiki: https://github.com/coq/coq/wiki
• マニュアル: https://coq.inria.fr/distrib/current/refman/
• 標準ライブラリ: https://coq.inria.fr/distrib/current/stdlib/

coqのインストール

coqで命題論理をするために以下のプログラムをインストールする:

• coq: コマンドラインプログラムcoqtop, coqc等
• ledit, rlwrap: coqtopで矢印キーを使えるようにするためのヘルパーのコマンドラインプログラム
• proof-general, company-coq (emacs package): emacsエディタのcoq mode他
• coqide: 対話GUI (オプション: ターミナルでcoqtopが嫌な場合)

coqはmacosではhomebrewで入れられる。

$ brew install coq ledit
$ brew cask install coqide

Windowsではchocolateyにcoqパッケージがある(coqideも含む)。
しかし、Windows 10ならWSLのUbuntuをつかってcoqパッケージを入れて、WSLのコンソール上でmac等と同様にcoqtopを使うほうが無難かもしれない。

emacsでのproof-generalはMELPAにあるものをインストールする。

;; ~/.emacs
(require 'package)
(add-to-list 'package-archives '("melpha" . "https://melpa.org/packages/"))
(package-initialize)

このMELPAの設定をしたうえでemacs上で、Mx package-list-packagesやM-x package-install からproof-generalとcompany-coqを入れておく。

対話型環境coqtopの使い方

(まずはじめに、coqの対話型環境であるcoqtopの使い方の流れをまとめておく。)

普通は、ヒストリやカーソル移動で矢印キーを使うために、rlwrapやledit経由でcoqtopを実行させる。

$ ledit coqtop
Welcome to Coq 8.8.1 (August 2018)

Coq <

ここでは、対話的にコマンドを打ち込んでいく。

Coq < Check Prop.
Prop
     : Type

Coq < Print True.
Inductive True : Prop :=  I : True

Coq <

**コマンド文の終わりの.(ピリオド)**を忘れないこと。

• Checkコマンド: 「式の型情報」を表示する
• Printコマンド: 「関数や型の定義」を表示する

この例は、coqのビルトインのPropやTrueを表示させてみた。

また、Checkで指定する式では、プレースホルダーとして_を複数個おける。
たとえば、演算子の型情報の表示は、Check _ -> _.のようにプレースホルダーを使うとよい。

coqtop上で定理証明

実際に、coqで「証明」を行うときは、まず、最終ゴールの論理式を記述し、ゴールからtacticコマンドを適用して証明を構築していく。
以下は、簡単な定理について、その証明を完成させるまでのcoqtop上の入出力をそのまま載せたものである:

Coq < Theorem taut1: forall A B: Prop, A->B->A.
1 subgoal

  ============================
  forall A B : Prop, A -> B -> A

taut1 < intros A B HA HB.
1 subgoal

  A, B : Prop
  HA : A
  HB : B
  ============================
  A

taut1 < exact HA.
No more subgoals.

taut1 < Qed.
taut1 is defined

Coq <

Theoremコマンドで「定理」の名前とゴールの論理式を与えて、tacticコマンドを入力できる「証明モード」に入る。
この例では、プロンプトが定理名からtaut1 <になっていることで判断できる。

そこで、tacticコマンドを駆使して、サブゴールをすべて解決していったあと、Qedコマンドによって完了させる。
途中のintrosやexactは、coq組み込みのtacticコマンドの一つである。

この証明モード中では、tacticコマンド以外にも以下のような編集系のコマンドが使える:

• Abortコマンド: 証明モードを中止する(定理もなかったことになる)
• Undoコマンド: tacticコマンド1つの適用前の状態に戻る
• Showコマンド: 現在状態を再表示させる

証明した定理(=関数の実装)を表示させる

証明完了した定理(Theorem)をPrintをすれば、実際に生成された関数本体のコードを表示できる。

Coq < Print taut1.
taut1 =
fun (A B : Prop) (HA : A) (_ : B) => HA
     : forall A B : Prop, A -> B -> A

Argument scopes are [type_scope type_scope _ _]

Coq <

これを見れば、Theoremに渡した名前や論理、introsやexactといった**tacticに渡した識別子が、結果の関数のコードに入っているものと対応している**ことがわかるだろう。

実際にはこの「証明」というのは、ゴールの**論理式そのものを「型」とした関数の「型チェックをパスする実装コード」**のことである。

よって、coqでの「証明の構築」というのは、型チェックが失敗しないように、「関数の本体を実装していく」行為である。
すなわち、tacticコマンドというのは、本体の実装コードを生成するプリプロセッサマクロのようなものといえるだろう。
(この例では、introsでfunと引数リストを作り、exactでその1引数を埋め込んでいる。)

作った定理の利用

また定理をtactic経由で証明で使っていく(= 関数呼び出しコードを埋める)こともできる。
このためのtacticとしては、applyを使うことができる。

逆に、プログラミングしてダイレクトに実装した関数も、証明モードで使える定理として扱える。

Coq < Definition taut2 (A B: Prop) (HA: A) (_: B) : A := HA .
taut2 is defined

Coq < Theorem taut3: forall A B C: Prop, A/\B -> C -> A/\B.
1 subgoal

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

taut3 < intros A B C.
1 subgoal

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

taut3 < apply taut2.
No more subgoals.

taut3 < Qed.
taut3 is defined

Coq < Print taut3.
taut3 =
fun A B C : Prop => taut2 (A /\ B) C
     : forall A B C : Prop, A /\ B -> C -> A /\ B

Argument scopes are [type_scope type_scope type_scope _ _]

Coq <

これは、taut1と同じものをtaut2として、証明モードではなく、関数として直接実装した例である。

これを定理として、taut3の証明でapply taut2して利用している。
そして、その結果の実装コードから、taut2を関数として呼び出していることが確認できる。

coqのビルトイン型の構造について

(実際にcoqで定理を表現するには、その要素となる、coqのもつ基本型(タイプ)の関係構造のを把握しておく必要があるだろう。)

定理に使う**Propという型は、命題(Proposition)のための型**で、coqのビルトインの型の一つである。
まず、coqでの型の大本になる型としてTypeが存在しており、PropはTypeの要素の一つである。

このPropの要素として、True、Falseがある。
AやBといった定理内で使う命題もPropの要素として扱う。

さらに、Propの要素の型として、Propをパラメータを持った型and A Bとor A Bがある。 and A Bは**A/\B、or A BはA\/B**とも記述でき、coqでは主にこの表現の方を使用する。

また、Typeのもう一つの要素が、**データの型のためのSet**である。
Setの要素には、boolや自然数の型のnatなどの型がある。

このboolの要素のデータであるtrueやfalseと、Propの要素の型であるTrueとFalseは全く別物である。
Propの**Falseは「矛盾」**を意味し、データとして存在してはいけない扱いをする。
(ここでは、述語論理までは扱わないので、Set側の話ついては、この程度にとどめておく。)

さらに、Type、Set、Propに属する型2つをパラメータに用いる関数の型A->Bがある。
パラメータがPropな型である関数型は、記号論理での->(含意、「ならば」)としても扱う。
ちなみに、->は右結合である。つまり、A->B->CというはA->(B->C)のことである。

最後に、命題の否定~Aというのは、右がFalseな関数型A->Falseの型の構文糖となっている。

まとめると、ビルトイン型は、以下のような階層関係になっている:

• Type
  • Set
    • bool: true, false
    • nat : 0, 1, ...
    • nat->bool, ...
  • Prop
    • True: I
    • False
    • A/\B = and A B
    • A\/B = or A B
    • A, B. C, ...
    • A->B, A->B->C, (A->B)->C, ...
    • ~A = A->False

証明ステップ(仮説リストとサブゴール)の1行表記について

(ここでは、証明の文章説明のための、証明の各段階を1行で表す表記法を独自に規定する。)

これはcoqの文法の話ではなく、説明のための記法の話である。
証明での各ステップの状態を、以下のように|-で区切って1行記述することにする。

• 仮定1, 仮定2, ... |- サブゴール

これは、「仮定リストの論理のいくつかが成立することで、サブゴールの論理は成立する」という意味である。

この1行表現方法では、coqtopでの、

HA: A
HB: B
=======
A

の場合は、HA: A, HB: B |- Aと1行で書くことができる。

そして、特定の状況パターンに対して、以下のような意味がある:

• 証明対象の**定理(Theorem)**は、仮定リストが空の状態になっている
• サブゴール側が空の状態は、証明が完成した状態である

サブゴール分割時の1行表記

ところで、A/\Bのような論理式は、A側とB側双方成立した結果成立する。
この場合、証明の構築を進めると、サブゴールが分割されることになり、そのすべてのサブゴールの証明の構築をしなくてはいけない。

この1行表現では、分割されたサブゴールのリストを、以下のように;で区切って記述することにする。

• 仮定1, 仮定2, ... |- サブゴール1 ; 仮定1, 仮定2, ... |- サブゴール2 ; ...

ここでは、分割サブゴールの仮定リストはそれぞれ全部列挙する。

参考: 以下のように、含意によってサブゴール側に個別の仮定を移すことで、仮定リストを共通にでき、サブゴールごとの仮定リストを個別に書かない表記もできる。

• 仮定0, 仮定1 |- サブゴール1 ; 仮定0, 仮定2 |- サブゴール2
• 仮定0 |- 仮定1 -> サブゴール1 ; 仮定0 |- 仮定2 -> サブゴール2
• 仮定0 |- 仮定1 -> サブゴール1 ; 仮定2 -> サブゴール2

この仮定1, 仮定2 |- サブゴール1 ; サブゴール2の表記は、「それぞれで、仮定リストの論理をいくつかが成立することで、すべてのサブゴールの論理が成立する」というような意味になる。

1行表記の列挙による「証明」

記号論理での伝統的な「証明図」(proof tree)というのは、ゴールを一番下において、上側へ分解していく表記となっている。

• 参考(昔からあるlatexのprooftree.styのドキュメント): http://mirrors.ctan.org/macros/generic/proofs/taylor/prooftree-doc.pdf

この1行表記での証明ステップでは逆に、上から下にステップ順に並べていく。

たとえば、前述のcoqtopでの例を使うと:

• |- A->B->A
• HA: A, HB: B |- A
• HA: A, HB: B |-

ここに、上下推移で適用したtacticコマンドを明記すると、以下のようにcoqtopでのコマンド列になる:

• [Theorem taut1] |- A->B->A
• [intros HA HB] HA: A, HB: B |- A
• [exact HA] HA: A, HB: B |-
• [Qed]

(個々での下から上、つまり証明図での上から下に読めば、introsは「仮説から->を「導入(introduce)」するルール」となっている)

ここで、forall A B: Prop部分へのintros A B部分は省略した。
このforall A B: Propは、定理として、AやBの部分が、C/\Dのような様々な命題式であっても成立しうる、変数扱いできるようにするものである。

また、サブゴール分割後のステップについては、以下のようにそれぞれを分けて入れ子で並べる

• [Theorem and_intro] |- A -> B -> A/\B
• [intros HA HB] HA: A, HB: B |- A/\B
• [split] HA: A, HB: B |- A ; HA: A, HB: B |- B
• (HA: A, HB: B |- A)
  • [exact HA] HA: A, HB: B |-
• (HA: A, HB: B |- B)
  • [exact HB] HA: A, HB: B |-
• [Qed]

命題論理のためのcoqのビルトインtacticコマンド一覧

(先に、命題論理証明のために使うtacticを一覧しておく。)

無から論理式を導出して定理を作る場合では、(証明図を上から下へ進むように、)素材から論理関係を構築するルールである**「推論規則」を用いて、論理式を組み立てることで、単一のゴールの論理式へと導いていく。
しかし、定理に対してその証明を作る場合は逆に、ゴールの定理の論理式から、この推論規則を逆適用させることで論理式を分解**していき、矛盾が無いように証明図を積み上げていくことになる。

coqで行う「証明」とは、基本、後者の行為である。(前者の行為はプログラミングそのもので、構成要素を使って直接実装を組み立てた関数をそのまま法則として提示することに相当する。)

そして、coqのtacticは、この推論規則の逆適用のように使うことができる。
ただし、ビルトインtacticは、命題論理の推論規則そのものを備えているわけではない。

推論規則には、**記号の「導入」と「除去」**の２タイプのルールがある(この導入除去は、前者の論理式構築の方の意味である)。
導入規則に対応するtacticは、それぞれそれらしいものが存在している。

しかし、除去規則のほうは違っている。
通常の命題論理でのandやorの除去規則は、その逆適用によって、サブゴールの論理式を大きくすることになる。
(このため、間違って使うと、式が膨らみ続け、証明構築失敗のもとになる)

coqのビルトインtacticでの、各除去規則の類似品は、サブゴール側の式の拡大をしないようになっている。
このため、命題論理での除去規則よりも、証明構築で扱いやすくなっている。
(これは、帰納型とパターンマッチの言語機能のもと、それが使える型として定義していることによる。)

もちろん、命題論理での各記号の除去規則そのものを「定理として」作ることもできる。
(付録でのせておいた)

導入規則のtactic一覧

• |- A -> B [intro A1] A1: A |- B
  • |- A -> B -> C [intros A1 B1] A1: A, B1: B |- C
• |- A\/B [left] |- A
• |- A\/B [right] |- B
• |- A/\B [split] |- A ; |- B
• |- False [absurd A] |- A ; |- ~A

ちなみに、left、right、splitは、andやor専用ではなく、ユーザー定義データ型にも使える。
型andやorのコンストラクタ定義は、

• A\/B := or_introl: A->A\/B | or_intror: B->A\/B
• A/\B := conj: A -> B -> A/\B

となっており、left、right、splitは、それぞれのゴールの型に応じたコンストラクタ関数or_introl、or_introrやconjをapplyしていることに相当する。

除去規則(の類似品)のtactic一覧

• AB: A->B |- B [apply AB] AB: A->B |- A
• AB: A/\B |- C [destruct AB as [A1 B1]] A1: A, B1: B |- C
• AB: A\/B |- C [destruct AB as [A1 | B1]] A1: A |- C ; B1: B |- C
• NA: ~A |- False [apply NA] NA: ~A |- A

ちなみに、destructは、andやor専用ではなく、ユーザー定義データ型にも使える。
これは、ABへのコンストラクタのパターンマッチ式(match T with ...)で埋めるもので、A1: AやB1: Bを展開していることに相当する。

古典論理のための拡張推論規則NNPP

coqのビルトインtacticがやることは、プログラミング構文の型として、普通に対応がつけられる範囲だけである。

この範囲は、いわゆる**「背理法」が通用する「古典論理」の範囲よりも狭い**。
たとえば、「ド・モルガンの法則」の4定理のうち、~(A/\B) -> ~A\/~Bだけは、この古典論理の範囲に広げなければ証明できない定理である。

coqで古典論理の範囲で証明をするには、標準ライブラリClassicalをインポートする必要がある。

Coq < Require Import Classical.

これによって、**「二重否定の除去」のルールNNPP: forall A: Prop, ~~A -> A**とその等価の規則が追加され、apply経由で利用できるようになる。これは、次のような変換を行う。

• |- A [apply NNPP] |- ~~A

この結果の~~Aとは、~A->Falseのことである。
ここからすぐinntro NAすることによって、NA: ~A |- Falseとなる。

• |- A [apply NNPP] [intro NA] NA: ~A |- False

NNPPを使う基本的な意義は、この**Falseを導く**使い方(矛盾、つまり、背理法)のためである。

そこで、このFalseに対して、他の~がついた仮定をapplyすることで、ゴールに~を外した論理式を置くための手段になる。

• NB: ~B |- A [apply NNPP] [intro NA] [apply NB] NB: ~B, NA: ~A |- B

coqソースファイルについて

(ここでは、coqtopではなく、coqcコンパイルさせるcoqのソースファイルについて、概要を載せておく。)

coqのソースファイルの名前は、**拡張子.v**のmodname.vのように付ける。

コマンドcoqcによって、ソースファイルをコンパイル(coqc modname.v)が成功すると、modname.voファイルが生成される。
コンパイルしたこの**.voファイル**があれば、coqtop上でRequire Import modname.によって、その内容を読み込むことができるようになる。
このように、ファイル名は識別子として使われるため、-や空白等の識別子に入れられない文字はファイル名に入れることはできない。

coqソースファイルでは、coqtopでの入力と同じコマンドを記述できる。
そして、ソース中のPrintやCheckはcoqc実行時に出力される。

ただし、ソースファイルの内容は、coqtopでのコマンド列そのままではなく、「可読性のため」に少し飾り建てさせた表記をする。

例として、記号論理での\/除去のルールを、Theorem or_elimとしてdestructを使った証明のソースor_elim.vは以下のようになる。

Theorem or_elim: forall A B C: Prop, (A->C) -> (B->C) -> (A\/B) -> C.
Proof.
  intros A B C AC BC AB.
  destruct AB as [HA | HB].

  (* AC: A->C, BC: B->C, HA: A |- C *)
  - apply AC.
    exact HA.

  (* AC: A->C, BC: B->C, HB: B |- C *)
  - apply BC.
    exact HB.
Qed.

Print or_elim.

ここには、coqtop上ではめったに使わない、以下の構文が使われている。

• Proofコマンド: あってもなくても結果は同じだが、ProofからQedまでが、証明モードのブロックにあることを示すために用いられている。
• コメント(* ... *): ここでは、サブゴール分割後のそれぞれの状態を載せた。
• ビュレット-: 並列されたサブゴール内の証明に入っていることをビュレットを用いて示している。
  • ビュレットマークには-、+、*とその繰り返しの--等を用いる。違うマークは、入れ子のサブゴール分割を表している。

このファイルをcoqcでコンパイルさせると、Print部分が実行され、以下のように表示される。

$ coqc or_elim.v
or_elim =
fun (A B C : Prop) (AC : A -> C) (BC : B -> C) (AB : A \/ B) =>
match AB with
| or_introl HA => AC HA
| or_intror HB => BC HB
end
     : forall A B C : Prop, (A -> C) -> (B -> C) -> A \/ B -> C

Argument scopes are [type_scope type_scope type_scope function_scope
  function_scope _]

(余談だが、destruct AB as [HA | HB]がmath AB with | or_introl HA => ... | or_intror HB => ...を生み出していることが確認できるだろう)

コンパイルした.voファイルをcoqtopで利用する

こうしてコンパイルしたソース内の定理は、以下のようにインポートして利用させることができる(apply経由で使える)。

$ ls
or_elim.glob   or_elim.v   or_elim.vo
$ ledit coqtop
Welcome to Coq 8.8.1 (August 2018)

Coq < Require Import or_elim.

Coq < Check or_elim.
or_elim
     : forall A B C : Prop, (A -> C) -> (B -> C) -> A \/ B -> C

Coq <

注: 証明のソースでは、名前を自動生成させずに、自分でつける

introsやdestructでは、割り当てる名前を与えなければ、HやH0のような名前を自動で生成するようになっている。

この自動生成名も同様に使えはするが、名前の生成数や命名ルールを正確に把握していないと、その名前がどの命題に相当するかわからなくなってしまう。
coqtopのような対話環境で毎回状態が表示される限りにおいては、それでも良いかもしれないが、コード上ではその時々の状態は表示されない。

そこで、ソースコード上の証明モード内の記述では、名前はその意味がわかりやすいものを選びきちんと列挙するべきだと思っている。
この名前は、証明の結果生成される実装コード中でも変数名として使われるものであり、この観点からもきちんと指定することは理にかなっている。

同様の理由で、仮定リストから一致するゴールを見つけて解決するassumption tacticも使用しないで、exactで名前を指定することにしている。

「ド・モルガンの法則」とは

ド・モルガンの法則(de Morgan laws)は、以下のような、and-orと否定の間での同値関係を表したものである。

• ~(A \/ B) = ~A /\ ~B
• ~(A /\ B) = ~A \/ ~B

同値関係A = Bというのは、A -> Bかつ、B -> Aのことを言い換えたものである。
coqでの定理はapplyさせて使う対象でもあり、このことを視野にいれると、同値関係としてまとめずに->の単位でそれぞれ分けて定理にしたほうがよい。

よって、ド・モルガンの法則は、以下の4つの定理をまとめたものになっている:

• ~(A\/B) -> ~A/\~B
• ~A/\~B -> ~(A\/B)
• ~A\/~B -> ~(A/\B)
• ~(A/\B) -> ~A\/~B

これは、証明の難易度順に並べてある。
そして、1番目と4番目の論理式は一見似ているが、その構成は全く違うのである。

1番目から3番目までの定理は、coqの組み込みtacticだけで自然に導出できる。

一方、4番目の~(A/\B) -> ~A\/~Bだけは、古典論理拡張の規則である**「二重否定の除去」が必須**になっている。
証明も他3つとは比べ物にならないほど複雑であり、この差は証明後Printして関数本体の実装コードを見ることで確認できるだろう。
(ついでに言えば、前3つは、auto tactic一回で、自動的に証明を完成できる。)

ド・モルガンの法則1: ~(A\/B) -> ~A/\~B の証明

定理と証明のコード全体:

Theorem deMorgan1: forall A B:Prop, ~(A\/B) -> ~A/\~B.
Proof.
  intros A B NAB.
  split.

  (* NAB: ~(A\/B) |- ~A *)
  - intro A1.
    apply NAB.
    left.
    exact A1.

  (* NAB ~(A\/B) |- ~B *)
  - intro B1.
    apply NAB.
    right.
    exact B1.
Qed.

Print deMorgan1.

この結果の定理=関数の実装コードは、

deMorgan1 =
fun (A B : Prop) (NAB : ~ (A \/ B)) =>
conj (fun A1 : A => NAB (or_introl A1)) (fun B1 : B => NAB (or_intror B1))
     : forall A B : Prop, ~ (A \/ B) -> ~ A /\ ~ B

Argument scopes are [type_scope type_scope _]

本体は、関数２つを引数に与えた、conjである。
JavaScript風に単純化して書けば、deMorgan1 = NAB => conj(A1 => NAB(or_introl(A1)), B1 => NAB(or_intror(A1))) となっている。

NAB: ~(A\/B)はNAB: (A\/B) -> Falseの関数として認識するとわかりやすい。
よって引数の関数の型は、それぞれ、A->False、B->Falseであり、すなわち~Aと~Bになっている。

ド・モルガンの法則2: ~A/\~B -> ~(A\/B) の証明

定理と証明のコード全体:

Theorem deMorgan2: forall A B:Prop, ~A/\~B -> ~(A\/B).
Proof.
  intros A B NANB AB.
  destruct NANB as [NA NB].
  destruct AB as [A1 | B1].

  (* NA:~A, NB:~B A1:A |- False *)
  - apply NA.
    exact A1.

  (* NA:~A, NB:~B B1:B |- False *)
  - apply NB.
    exact B1.
Qed.

Print deMorgan2.

この結果の定理=関数の実装コードは、

deMorgan2 =
fun (A B : Prop) (NANB : ~ A /\ ~ B) (AB : A \/ B) =>
match NANB with
| conj NA NB =>
    match AB with
    | or_introl A1 => NA A1
    | or_intror B1 => NB B1
    end
end
     : forall A B : Prop, ~ A /\ ~ B -> ~ (A \/ B)

Argument scopes are [type_scope type_scope _]

こちらは1とは逆にconjデータ型をパターンマッチで解体していくコードとなっている。

~(A\/B)は(A\/B) -> Falseのことであり、引数を与えた結果Falseになる。
~AがA->Falseであることから、1でのconjの引数をNA: A->False、NB: B->Falseとすると、最終的にFalseなっていることがわかる。

1の本体コードのconjの両引数の関数を、このNA、NBに割り当てて考えてみるのも面白いかもしれない。

ド・モルガンの法則3: ~A\/~B -> ~(A/\B) の証明

定理と証明のコード全体:

Theorem deMorgan3: forall A B: Prop, ~A\/~B -> ~(A/\B).
Proof.
  intros A B NANB AB.
  destruct AB as [A1 B1].
  destruct NANB as [NA | NB].

  (* A1: A, B1: B, NA:~A |- False *)
  - apply NA.
    exact A1.

  (* A1: A, B1: B, NB:~B |- False *)
  - apply NB.
    exact B1.
Qed.

Print deMorgan3.

この結果の定理=関数の実装コードは、

deMorgan3 =
fun (A B : Prop) (NANB : ~ A \/ ~ B) (AB : A /\ B) =>
match AB with
| conj A1 B1 =>
    match NANB with
    | or_introl NA => NA A1
    | or_intror NB => NB B1
    end
end
     : forall A B : Prop, ~ A \/ ~ B -> ~ (A /\ B)

Argument scopes are [type_scope type_scope _]

2と3は、引数の型だけが違うコードとなった。
これはdestructした順序が同じだからである。

命題論理での証明図のように、2と3で/\導入と\/導入の適用順序が逆転する場合、このパターンマッチの入れ子関係が逆転したコードになる。

ド・モルガンの法則4: ~(A/\B) -> ~A\/~B の証明

問題の最難関の証明である。

定理と証明のコード全体:

Theorem deMorgan4: forall A B: Prop, ~(A/\B) -> ~A\/~B.
Proof.
  Require Import Classical.

  intros A B NAB.
  apply NNPP.
  intro NNANB.
  apply NAB.
  split.

  (* NNANB: ~(~A\/~B) |- A *)
  - apply NNPP.
    intro NA.
    apply NNANB.
    left.
    exact NA.

  (* NNANB: ~(~A\/~B) |- B *)
  - apply NNPP.
    intro NB.
    apply NNANB.
    right.
    exact NB.
Qed.

Print deMorgan4.

古典論理の公理が必須で、「二重否定の除去」NNPP: ~~A -> Aを使う証明となっている。
NNPPを含む標準ライブラリClassicalを読み込むRequire Import Classicalの位置は、NNPPを使う前であれば、証明モードの外でも中でも良い。

最初のNNPPのapplyは、NAB: ~(A/\B)の否定を外すために使う。
サブゴールの\/を分解せずに、最初にNABの否定を外すのが、この証明のポイントとなっている。

その結果のサブゴールA/\Bをsplitしたあとで、A、BそれぞれにNNPPを使って~A、~Bを仮定に置くことで、最初のNNPPによって出来たNNANB: ~(~A\/~B)の否定を外して、その中の~Aや~Bを解決させることで完成させる。

この結果の定理=関数の実装コードは、以下のようにNNPPを多段で呼び出すコードとなる:

deMorgan4 =
fun (A B : Prop) (NAB : ~ (A /\ B)) =>
NNPP (~ A \/ ~ B)
  (fun NNANB : ~ (~ A \/ ~ B) =>
   NAB
     (conj (NNPP A (fun NA : ~ A => NNANB (or_introl NA)))
        (NNPP B (fun NB : ~ B => NNANB (or_intror NB)))))
     : forall A B : Prop, ~ (A /\ B) -> ~ A \/ ~ B

Argument scopes are [type_scope type_scope _]

NNPP: forall A: Prop, ~~A->Aを関数型にするとNNPP: forall A: Prop, (~A->False)->Aである。
最初の引数は型であり、二番目の引数がその否定の型を引数に取る関数となる。
そして、その関数の引数の否定の型自体が、その型を引数に取る関数である(NNANB、NA、NBは否定を外した型を引数に取る関数)。

まとめ

ここで使ったtacticをリストアップすればわかるが、ド・モルガンの法則の4つの定理を証明をすると、前述した命題論理の記号の導入と除去の規則をほとんど使うことになる。

また、1と4の違いを見ると、4でNNPPを使うのは、導く~A\/~Bを単一の命題として扱うために、まとめて背理法を適用する必要があるからである。
1でのように単否定の~A(= A->False)を導く状況では、否定形の仮定のためにNNPPを使う必要はない。

否定形の仮定に対する結論側の構造が、NNPPを必要とすることになる。
たとえば、三重否定から単否定にもっていくことにはNNPPは一切不要である。

Theorem NNNPNP: forall A: Prop, ~~~A -> ~A.
Proof.
  intros A NNNA A1.
  apply NNNA.
  intro NA.
  apply NA.
  exact A1.
Qed.

付録A: and除去規則の定理化とその利用

命題論理の公理のand除去の左右２つ(A/\B -> A、A/\B -> B)は、以下のようにdestructで定理にできる。

Theorem l_and_elim: forall A B: Prop, A/\B->A.
Proof.
  intros A B AB.
  destruct AB as [A1 B1].
  exact A1.
Qed.

Theorem r_and_elim: forall A B: Prop, A/\B->B.
Proof.
  intros A B AB.
  destruct AB as [A1 B1].
  exact B1.
Qed.

これらを用いて、destructは使わずにA/\B -> B/\Aを証明すると以下のようになる。

Theorem ABBA: forall A B: Prop, A/\B -> B/\A.
Proof.
  intros A B AB.
  split.

  (* AB: A/\B |- B *)
  - apply r_and_elin with A.
    exact AB.

  (* AB: A/\B |- A *)
  - apply l_and_elin with B.
    exact AB.
Qed.

Print ABBA.

ゴールにはない型情報を必要とするため、applyするときにwithで足りないほうの型を補う必要がある。
withのパラメータは型であるが、型構文は空白を含みうるので、その場合は、apply e_and_elim with (A/\B)のように括る必要がある。

結果の定理の実装は、

ABBA =
fun (A B : Prop) (AB : A /\ B) =>
conj (r_and_elim A B AB) (l_and_elim A B AB)
     : forall A B : Prop, A /\ B -> B /\ A

Argument scopes are [type_scope type_scope _]

となっている。

付録B: and除去規則の定理化とその利用

先のcoqのコードファイルの内容例として用いたor除去((A->C) -> (B->C) -> (A\/B) -> C)の定理:

Theorem or_elim: forall A B C: Prop, (A->C)->(B->C)->(A\/B)->C.
Proof.
  intros A B C AC BC AB.
  destruct AB as [HA | HB].

  (* AC: A->C, BC: B-C, HA: A |- C *)
  - apply AC.
    exact HA.

  (* AC: A->C, BC: B-C, HB: B |- C *)
  - apply BC.
    exact HB.
Qed.

を用いて、destructを使わずにB\/A -> A\/Bを証明すると以下のようになる。

Theorem BAAB: forall A B: Prop, B\/A -> A\/B.
Proof.
  intros A B BA.
  apply or_elim with B A.

  (* BA: B/\A |- B->A\/B *)
  - intro B1.
    right.
    exact B1.

  (* BA: B/\A |- A->A\/B *)
  - intro A1.
    left.
    exact A1.

  (* BA: B\/A |- B\/A *)
  - exact BA.
Qed.

Print BAAB.

このor_elimのapplyでは、ゴールであるC以外の\/の左右の２つの型をwithでそれぞれ指定する必要がある。
その結果として３つのサブゴールに分かれる。

そして、結果の定理の実装は、

BAAB =
fun (A B : Prop) (BA : B \/ A) =>
or_elim B A (A \/ B) (fun B1 : B => or_intror B1)
  (fun A1 : A => or_introl A1) BA
     : forall A B : Prop, B \/ A -> A \/ B

Argument scopes are [type_scope type_scope _]

となった。