無限降下法をCoqで示す

Posted on 2021/01/01 in coq

このページの作成にはAlectryonを用いています。
Coqのソースコード上で、ボタン()が表示されている文にマウスカーソルををホバーすると、Coqの応答が表示されます。
文をクリックすると、応答の表示が固定されます。
このバナーの下にある Display all goals and responses をクリックすると、全ての応答が固定表示になります。

問題

Alectryon を使って記事を書くのにちょうどよい話題があったので書いてみます。

いわゆる無限降下法というやつですね。

整礎帰納法で示す

無限降下法は整礎帰納法の一種なので、Coq で示すなら整礎帰納法を直接使うのが最も素直でしょう。

 Require Import Arith.

 

forall P : nat -> Prop, (forall n : nat, P n -> exists m : nat, m < n /\ P m) -> ~ (exists n : nat, P n)

forall P : nat -> Prop, (forall n : nat, P n -> exists m : nat, m < n /\ P m) -> ~ (exists n : nat, P n)
P:nat -> Prop
H:forall n : nat, P n -> exists m : nat, m < n /\ P m

~ (exists n : nat, P n)

整礎帰納法で示すにはゴールが forall n, ... の形であってほしいので、そのように変換します。

   
P:nat -> Prop
H:forall n : nat, P n -> exists m : nat, m < n /\ P m

(forall n : nat, ~ P n) -> ~ (exists n : nat, P n)
P:nat -> Prop
H:forall n : nat, P n -> exists m : nat, m < n /\ P m
forall n : nat, ~ P n

この変換は一階述語論理の範囲で容易に示せるので、firstorder ですぐに示すことができます。

   
P:nat -> Prop
H:forall n : nat, P n -> exists m : nat, m < n /\ P m

(forall n : nat, ~ P n) -> ~ (exists n : nat, P n)
solve [firstorder].

変換後のゴールを整礎帰納法で示します。 Coq の induction は using で帰納法の定理 (induction scheme) を受け取ることができ、 自然数の整礎帰納法を表す定理は lt_wf_ind という名前で Arith モジュールに存在します。

   
P:nat -> Prop
H:forall n : nat, P n -> exists m : nat, m < n /\ P m

forall n : nat, ~ P n
P:nat -> Prop
H:forall n : nat, P n -> exists m : nat, m < n /\ P m
n:nat
H0:forall m : nat, m < n -> ~ P m

~ P n

このゴールも一階述語論理の範囲で容易に示せるので、 firstorder が使えます。

     solve [firstorder].
 Qed.

整礎帰納法を明示的に使わない場合

 

forall P : nat -> Prop, (forall n : nat, P n -> exists m : nat, m < n /\ P m) -> ~ (exists n : nat, P n)

forall P : nat -> Prop, (forall n : nat, P n -> exists m : nat, m < n /\ P m) -> ~ (exists n : nat, P n)
P:nat -> Prop
H:forall n : nat, P n -> exists m : nat, m < n /\ P m

~ (exists n : nat, P n)

先程同様 forall の形への変換をしますが、ここで変換先を少し工夫します。 Q n の形のゴールに対して整礎帰納法を用いることは forall k, k < n -> Q k に対して通常の帰納法用いることと同じなでの、以下のようにします。

   
P:nat -> Prop
H:forall n : nat, P n -> exists m : nat, m < n /\ P m

(forall n k : nat, k < n -> ~ P k) -> ~ (exists n : nat, P n)
P:nat -> Prop
H:forall n : nat, P n -> exists m : nat, m < n /\ P m
forall n k : nat, k < n -> ~ P k

この変換もやはり firstorder で示せます。

   
P:nat -> Prop
H:forall n : nat, P n -> exists m : nat, m < n /\ P m

(forall n k : nat, k < n -> ~ P k) -> ~ (exists n : nat, P n)
solve [firstorder].

変換されたゴールを帰納法で示します。n = 0 のケースは、 k < 0 という明らかに成り立たない前提を含むので inversion で解決します。

   
P:nat -> Prop
H:forall n : nat, P n -> exists m : nat, m < n /\ P m

forall n k : nat, k < n -> ~ P k
P:nat -> Prop
H:forall n : nat, P n -> exists m : nat, m < n /\ P m

forall k : nat, k < 0 -> ~ P k
P:nat -> Prop
H:forall n : nat, P n -> exists m : nat, m < n /\ P m
n:nat
IHn:forall k : nat, k < n -> ~ P k
forall k : nat, k < S n -> ~ P k
P:nat -> Prop
H:forall n : nat, P n -> exists m : nat, m < n /\ P m

forall k : nat, k < 0 -> ~ P k
P:nat -> Prop
H:forall n : nat, P n -> exists m : nat, m < n /\ P m
k:nat

k < 0 -> ~ P k
solve [inversion 1].

n <> 0 のケースは、 k < S n に関して場合分けをする必要があります。

     
P:nat -> Prop
H:forall n : nat, P n -> exists m : nat, m < n /\ P m
n:nat
IHn:forall k : nat, k < n -> ~ P k

forall k : nat, k < S n -> ~ P k
P:nat -> Prop
H:forall n : nat, P n -> exists m : nat, m < n /\ P m
n:nat
IHn:forall k : nat, k < n -> ~ P k
k:nat
Hk:k < S n

~ P k
P:nat -> Prop
H:forall n : nat, P n -> exists m : nat, m < n /\ P m
n:nat
IHn:forall k : nat, k < n -> ~ P k
k:nat
Hk:k < S n
H1:k = n

~ P n
P:nat -> Prop
H:forall n : nat, P n -> exists m : nat, m < n /\ P m
n:nat
IHn:forall k : nat, k < n -> ~ P k
k:nat
Hk:k < S n
m:nat
H1:S k <= n
H0:m = n
~ P k

k < n のケースは帰納法の仮定から直ちに示せ、k = n のケースは仮定 H によって小さいケースに帰着して、やはり帰納法の仮定を用いることになります。

なんにせよどちらも簡単なので firstorder で示せます。

       
P:nat -> Prop
H:forall n : nat, P n -> exists m : nat, m < n /\ P m
n:nat
IHn:forall k : nat, k < n -> ~ P k
k:nat
Hk:k < S n
H1:k = n

~ P n
solve [firstorder].
P:nat -> Prop
H:forall n : nat, P n -> exists m : nat, m < n /\ P m
n:nat
IHn:forall k : nat, k < n -> ~ P k
k:nat
Hk:k < S n
m:nat
H1:S k <= n
H0:m = n

~ P k
solve [firstorder]. Qed.

結論

firstorder は強い。

ちなみに命題論理の範囲で示せる場合は tauto を使うとよいでしょう。