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

coqで一階述語論理版のド・モルガンの法則の証明を行うために、必要となる知識と情報をまとめた。

この記事は、「[coqでド・モルガンの法則の証明をするまで (命題論理版)](https://qiita.com/bellbind/items/b69d4ce436b4a5bc8a8d) 」の続きとなっている。
coqの導入方法、使い方、命題論理の証明手順、および、命題論理でのド・モルガンの定理とその証明全体については、上記のリンク先に記載している。

## 述語論理について

述語論理の「述語(Predicate」とは、**パラメータを持った命題**のことである。
Coqの構文では、とある`A: Type`(もしくは`A: Set`)をパラメータとした、`P: A->Prop`が述語に当たる。
述語は、`A`に属する値`a: A`を一つ受け取ることで、命題`P a: Prop`となる。
一階述語論理は、変数を述語のパラメータとしてのみ使用することに制限した論理である。

述語としては、より具体的な型を引数にとり、具体的な判定を備えた具体的な関数の場合もありうる。
しかし、命題論理の命題の名前自体に意味がなく、どのような命題であっても成立する論理を扱うように、述語論理もまた**任意の述語に対して、成立する論理**を扱うことが基本である。

述語はそれ単体では命題とならないので、論理式にするにはパラメータを指定する必要がある。
述語論理では、この述語に与えるパラメータを用意する手段として、**∀(forall)と∃(exists)の二種類の束縛**がある。

- ∀a: A, 〜  => 「〜は、任意のAの要素aについて成立する」
- ∃a: A, 〜 => 「〜は、特定のAの要素aについては成立する」

この∀と∃を混ぜ込んだ論理式が、述語論理となる。

「述語＋パラメータ」を命題とみなした場合、パラメータ`a0 a1 a2 ...: A`に対して、各述語`P`ごとにそれぞれ命題`(P a0) (P a1) (P a2) ...: Prop`が存在するものとみなせる。
この視点での変数束縛は、命題への`/\`や`\/`をパラメータ全体に対して適用したものとみなせる。つまり:

- `∀ a: A, P a` => `True /\ (P a0) /\ (P a1) /\ (P a2) /\ ...`
- `∃ a: A, P a` => `False \/ (P a0) \/ (P a1) \/ (P a2) \/ ...`

という解釈が可能である。
むしろ∀や∃は、~以降をandやorの列挙に展開されるイメージ認識するつほうが、そ直感的なの意味を間違わないだろう。(特に、∃の解釈で)

そして、推論規則や証明においても、この**`forall` <=> `/\`および`exists` <=> `\/`に類似性がある**ので、述語論理での証明を考えるときも`/\`や`\/`に置き換えた命題論理での証明を想定すると、整理しやすいかもしれない。

## coqでの述語論理の表現

coqでは、

- ∀: `forall a: A, P a`
- ∃: `exists a: A, P a`

と表現する。`forall`も`exists`も後続の`->`より結合度が低いので、述語論理の式では多くカッコで括ることになるだろう。

- `(forall a: A, P a -> Q a) -> (exists a: A, Q a -> R a) -> (exists a: A, P a -> R a)` => 前２つのカッコは外せない
- `(forall a: A, P a -> (exists a: A, P a))`  => これはカッコをすべて外しても同じ

命題論理では、命題変数`A B: Prop`を導入するために`forall`を使ったが、ここでは述語のみに`forall`をつかうようにするために、**型変数は`Theorem`のパラメータ構文で指定する**ことにする。

- `Theorem ABBA (A B: Prop): A/\B -> B/\A.`

`forall`での宣言と唯一違う点は、パラメータ側に変数を置くと、証明モードでは、**変数ははじめから同名で仮定リストに追加された状態**で始まることである。

## 述語論理のためのtactic一覧

`forall`と`exists`にも、`/\`や`\/`と同様、導入と除去の推論規則がある。

導入規則:

- `|- forall a: A, B a` [`intro a0`] `a0: A |- B a0`
- `a0: A |- exists a: A, B a` [`exists a0`] `a0: A |- B a0` (`a`部分すべてを`a0`に置き換える)

除去規則の類似品:

- `a0: A, FA: (forall a: A, B a) |- C` [`specialize FA with a0 as Ba0`] `a0: A, FA: (forall a: A, B a), Ba0: (B a0) |- C`
- `EA: (exists a: A, B a) |- C` [`destruct EA as [a0 Ba0]`] `a0: A, Ba0: (B a0) |- C`.

また`forall`除去として`apply`も使用できる。これは`specialize`した上で、命題として`apply`することに相当する。

- `a0: A, FA: (forall a: A, B a) |- B a0` [`apply FA`] `a0: A, FA: (forall a: A, B a) |-`
- `a0: A, FA: (forall a: A, B a -> C) |- C` [`apply FA with a0`] `a0: A, FA: (forall a: A, B a -> C) |- B a0`
- `a0: A, Ba0: (B a0), FA: (forall a: A, B a -> C) |- D` [`apply FA with a0 in Ba0`] `a0: A, Ba0: C, FA: (forall a: A, B a -> C) |- D`
- `a0: A, Ba0: (B a0), FA: (forall a: A, B a -> C) |- D` [`apply FA with a0 in Ba0 as C1`] `a0: A, Ba0: (B a0), FA: (forall a: A, B a -> C), C1: C |- D`

ゴールではなく仮定に対して`apply`する場合、`apply ~ in`を使う(`as`を入れないと、指定した仮定を置き換える)。

普通の推論規則でのように、ゴールに対して、除去規則を使う場合は以下で可能なようだ:

- `a0: A |- B a0` [`generalize a0 as a`] `a0: A |- forall a: A, B a`
- `a: A |- B a` [`apply ex_ind with A (fun a0: A => B a0)`] `a: A |- forall x : A, B x -> B a ; a: A |- exists a0: A, B a0`

coqで`exact`マッチさせる場合、ゴール側を一般化させずに、仮定側を具体化するほうが普通は楽だろう。

## 述語論理版のド・モルガンの法則

命題論理でのド・モルガンの法則の4定理は、以下のものであった。

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

前述した変数束縛と命題の対応関係のように`A/\B`を`forall a: A, P a`、`A\/B`を`exists a: A, P a`に置き換えると、そのまま以下のようになる:

- `~(exists a: A, P a) -> (forall a: A, ~(P a))`
- `(forall a: A, ~(P a)) -> ~(exists a: A, P a)`
- `(exists a: A, ~(P a)) -> ~(forall a: A, P a)`
- `~(forall a: A, P a) -> (exists a: A, ~(P a))`

これら4つの定理が、述語飯のド・モルガンの法則となる。

命題論理のときと同様に、4つ目の定理の証明には、`NNPP`が必須となる。

## ド・モルガンの法則1: `~(exists a: A, P a) -> (forall a: A, ~(P a))` の証明

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

```coq
Theorem deMorgan1 (A: Type) (P: A->Prop):
  ~(exists x: A, P x) -> (forall x: A, ~(P x)).
Proof.
  intros NxPx x0 Px0.
  apply NxPx.
  (* NxPx: ~(exists x: A, P x), x0: A, Px0: (P x0) |- exists x: A, P x *)
  exists x0.
  exact Px0.
Qed.

Print deMorgan1.
```

命題論理版では、`split`してそれぞれ`left`/`right`でゴールを選んで`exact`で解決させた。
述語論理ではそれが`x0`の`intro`と`exists`に置き換わることで、場合わけなしで解決される。

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

```coq
deMorgan1 =
fun (A : Type) (P : A -> Prop) (NxPx : ~ (exists x : A, P x))
  (x0 : A) (Px0 : P x0) => NxPx (ex_intro (fun x : A => P x) x0 Px0)
     : forall (A : Type) (P : A -> Prop),
       ~ (exists x : A, P x) -> forall x : A, ~ P x

Argument scopes are [type_scope function_scope _ _]
```

パラメータや型部分が多いが、本体は`NxPx (ex_intro (fun x : A => P x) x0 Px0)`だけである。
`ex_intro`は`ex`型のコンストラクタで、このインスタンスの型になる`ex a (P a)`型の構文糖が`exists a: A, P a`である。

## ド・モルガンの法則2: `(forall a: A, ~(P a)) -> ~(exists a: A, P a)` の証明

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

```coq
Theorem deMorgan2 (A: Type) (P: A->Prop):
  (forall x: A, ~(P x)) -> ~(exists x: A, P x).
Proof.
  intros xNPx xPx.
  destruct xPx as [x0 Px0].
  (* xNPx: (forall x: A, ~P x), x0: A, Px0: (P x0)  |- False *)
  specialize xNPx with x0 as NPx0.
  (* xNPx: (forall x: A, ~P x), x0: A, Px0: (P x0), NPx0: ~(P x0)  |- False *)
  apply NPx0.
  exact Px0.
Qed.

Print deMorgan2.
```

命題論理版では、仮定の`~A/\~B`も`destruct`したが、述語版では全称除去として`specialize`が使える。

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

```coq
deMorgan2 =
fun (A : Type) (P : A -> Prop) (xNPx : forall x : A, ~ P x)
  (xPx : exists x : A, P x) =>
match xPx with
| ex_intro _ x0 Px0 => let NPx0 : ~ P x0 := xNPx x0 in NPx0 Px0
end
     : forall (A : Type) (P : A -> Prop),
       (forall x : A, ~ P x) -> ~ (exists x : A, P x)

Argument scopes are [type_scope function_scope function_scope]
```

となった。(本体は`match ~ end`部分)


## ド・モルガンの法則3: `(exists a: A, ~(P a)) -> ~(forall a: A, P a)` の証明

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

```coq
Theorem deMorgan3 (A: Type) (P: A->Prop):
  (exists x: A, ~(P x)) -> ~(forall x: A, P x).
Proof.
  intros xNPx xPx.
  destruct xNPx as [x0 NPx0].
  (* xPx: (forall x: A, P x),  x0: A, NPx0: ~(P x0) |- False*)
  specialize xPx with x0 as Px0.
  (* xPx: (forall x: A, P x),  x0: A, NPx0: ~(P x0), Px0: (P x0) |- False *)
  apply NPx0.
  exact Px0.
Qed.

Print deMorgan3.
```

命題論理同様、2とほぼ同じ手順となる。

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

```coq
deMorgan3 =
fun (A : Type) (P : A -> Prop) (xNPx : exists x : A, ~ P x)
  (xPx : forall x : A, P x) =>
match xNPx with
| ex_intro _ x0 NPx0 => let Px0 : P x0 := xPx x0 in NPx0 Px0
end
     : forall (A : Type) (P : A -> Prop),
       (exists x : A, ~ P x) -> ~ (forall x : A, P x)

Argument scopes are [type_scope function_scope _]
```

となった。

## ド・モルガンの法則4: `~(forall a: A, P a) -> (exists a: A, ~(P a))` の証明

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

```coq
Theorem deMorgan4 (A: Type) (P: A->Prop):
  ~(forall x: A, P x) -> (exists x: A, ~(P x)).
Proof.
  Require Import Classical.

  intro NxPx.
  apply NNPP.
  intro NxNPx.
  (* NxPx: ~(forall x: A, P x), NxNPx: ~(exists x: A, ~P x) |- False *)
  apply NxPx.
  intro x0.
  apply NNPP.
  intro NPx0.
  (* NxPx: ~(forall x: A, P x), NxNPx: ~(exists x: A, ~P x),
     x0: A, NPx0: ~(P x0) |- False *)
  apply NxNPx.
  exists x0.
  exact NPx0.
Qed.

Print deMorgan4.
```

1と同様、`split`、`left`/`right`のかわりに、`x0`の`intro`と`exists`を使う。
そのうえで、命題論理での場合と同等の位置(ゴールが、`exists`全体、および、`P x0`のとき)で、`apply NNPP`する。


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

```coq
deMorgan4 =
fun (A : Type) (P : A -> Prop) (NxPx : ~ (forall x : A, P x)) =>
NNPP (exists x : A, ~ P x)
  (fun NxNPx : ~ (exists x : A, ~ P x) =>
   NxPx
     (fun x0 : A =>
      NNPP (P x0)
        (fun NPx0 : ~ P x0 => NxNPx (ex_intro (fun x : A => ~ P x) x0 NPx0))))
     : forall (A : Type) (P : A -> Prop),
       ~ (forall x : A, P x) -> exists x : A, ~ P x

Argument scopes are [type_scope function_scope _]
```

となった。

## まとめ

命題論理でのド・モルガンの法則の証明では、その推論規則を網羅しており、この証明によってそれなりの証明スキルが身につけることが期待できる。
一方、一階述語論理版の述語式には`forall`と`exists`の入れ子になった複雑な構造はないので、これだけやって十分というものではないだろう。
むしろ、命題論理から述語論理へ学習を進める場合の、第一ステップに適した題材だと思う。

最後に、述語版`deMorgan4`を使った`NNPP`を証明を載せ、その等価性を示しておく。

```coq
Theorem nnpp (P: Prop): ~~P -> P.
Proof.
  intro NNP.
  (*NOTE: ~~P => ~(P -> False) => ~(forall _: P, False) *)
  apply deMorgan4 in NNP as PNN.
  (* NNP: ~~P, PNN: (exists _: P, ~False) |- P *)
  destruct PNN as [P0 NN].
  exact P0.
Qed.

Print nnpp.
```


## 付録: 要素が空の可能性

(coqの系と、普通の一階述語論理と少し違う部分について)

`exists a: A, B a`が成立するには、`exists a0`での`a0`のように、`A`には少なくとも一つの元がなくてはいけない。
しかし、coqの型は、`False`がそうであるように、要素が一つもない空集合的な型も存在しうる。

たとえば、論理式`(forall a: A, P a) -> (exists a: A, P a)`は、これだけでは証明は成立しない。
この証明には、`exists` tacticに渡す変数が仮定リストに必要だからである。

通常の一階述語論理での存在導入規則`P a => exists x, Px`では、空集合でないとして、適当な変数`a`を与えられるが、これはcoqでは不可能となる。
この結論の`exists a: A, ...`を成立させる場合には、`A`が空でない要素がある前提/仮定が必要になる。

このため、`(exists a: A, True)->...`のように`destruct`で`A`の元の存在を前提に導入したり、もしくは`forall a: A, ...`のように`intro`で`A`の元が1つは存在する前提を作れるように、定理を記述する必要がある。

たとえば先の例に、`(exists a: A, ...)->`をつけることで、

```coq
Theorem ae (A: Type) (P: A->Prop): (exists a: A, True) -> (forall a: A, P a) -> (exists a: A, P a).
Proof.
  intros eA aPa.
  destruct eA as [a0 T].
  exists a0.
  apply aPa.
Qed.
```

と証明できる。

このように、結論の`exists a: A, ...`のためには、`exists a0`ができる可能性を定理中に含まなくてはいけない。