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

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

- 続編: [coqでド・モルガンの法則の証明(一階述語論理版)](https://qiita.com/bellbind/items/76f5f40d2719ca420b57)

## 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で入れられる。

```shell-session
$ brew install coq ledit
$ brew cask install coqide
```

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

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

```el
;; ~/.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を実行させる。

```shell-session
$ ledit coqtop
Welcome to Coq 8.8.1 (August 2018)

Coq <
```

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

```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
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
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
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`は以下のようになる。

```coq
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`部分が実行され、以下のように表示される。

```shell-session
$ 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`経由で使える)。

```shell-sesion
$ 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` の証明

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

```coq
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.
```

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

```coq
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)` の証明

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

```coq
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.
```

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

```coq
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)` の証明

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

```coq
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.
```

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

```coq
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` の証明

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

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

```coq
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`を多段で呼び出すコードとなる:

```coq
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`は一切不要である。

```coq
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`で定理にできる。

```coq
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`を証明すると以下のようになる。

```coq
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)`のように括る必要がある。


結果の定理の実装は、

```coq
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`)の定理:

```coq
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`を証明すると以下のようになる。

```coq
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`でそれぞれ指定する必要がある。
その結果として３つのサブゴールに分かれる。

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

```coq
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 _]
```

となった。