無限降下法をCoqで示す
Posted on 2021/01/01 in coq
問題
Alectryon を使って記事を書くのにちょうどよい話題があったので書いてみます。
大晦日クイズ
— hatsugai ∈ PRINCIPIA (@hatsugai) December 31, 2020
P は自然数についての述語 pic.twitter.com/YfaI2QyNeS
いわゆる無限降下法というやつですね。
整礎帰納法で示す
無限降下法は整礎帰納法の一種なので、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 -> PropH:forall n : nat, P n -> exists m : nat, m < n /\ P m~ (exists n : nat, P n)
整礎帰納法で示すにはゴールが forall n, ... の形であってほしいので、そのように変換します。
P:nat -> PropH:forall n : nat, P n -> exists m : nat, m < n /\ P m(forall n : nat, ~ P n) -> ~ (exists n : nat, P n)P:nat -> PropH:forall n : nat, P n -> exists m : nat, m < n /\ P mforall n : nat, ~ P n
この変換は一階述語論理の範囲で容易に示せるので、firstorder ですぐに示すことができます。
solve [firstorder].P:nat -> PropH:forall n : nat, P n -> exists m : nat, m < n /\ P m(forall n : nat, ~ P n) -> ~ (exists n : nat, P n)
変換後のゴールを整礎帰納法で示します。 Coq の induction は using で帰納法の定理 (induction scheme) を受け取ることができ、 自然数の整礎帰納法を表す定理は lt_wf_ind という名前で Arith モジュールに存在します。
P:nat -> PropH:forall n : nat, P n -> exists m : nat, m < n /\ P mforall n : nat, ~ P nP:nat -> PropH:forall n : nat, P n -> exists m : nat, m < n /\ P mn:natH0: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 -> PropH: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 -> PropH: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 -> PropH:forall n : nat, P n -> exists m : nat, m < n /\ P mforall n k : nat, k < n -> ~ P k
この変換もやはり firstorder で示せます。
solve [firstorder].P:nat -> PropH: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)
変換されたゴールを帰納法で示します。n = 0 のケースは、 k < 0 という明らかに成り立たない前提を含むので inversion で解決します。
P:nat -> PropH:forall n : nat, P n -> exists m : nat, m < n /\ P mforall n k : nat, k < n -> ~ P kP:nat -> PropH:forall n : nat, P n -> exists m : nat, m < n /\ P mforall k : nat, k < 0 -> ~ P kP:nat -> PropH:forall n : nat, P n -> exists m : nat, m < n /\ P mn:natIHn:forall k : nat, k < n -> ~ P kforall k : nat, k < S n -> ~ P kP:nat -> PropH:forall n : nat, P n -> exists m : nat, m < n /\ P mforall k : nat, k < 0 -> ~ P ksolve [inversion 1].P:nat -> PropH:forall n : nat, P n -> exists m : nat, m < n /\ P mk:natk < 0 -> ~ P k
n <> 0 のケースは、 k < S n に関して場合分けをする必要があります。
P:nat -> PropH:forall n : nat, P n -> exists m : nat, m < n /\ P mn:natIHn:forall k : nat, k < n -> ~ P kforall k : nat, k < S n -> ~ P kP:nat -> PropH:forall n : nat, P n -> exists m : nat, m < n /\ P mn:natIHn:forall k : nat, k < n -> ~ P kk:natHk:k < S n~ P kP:nat -> PropH:forall n : nat, P n -> exists m : nat, m < n /\ P mn:natIHn:forall k : nat, k < n -> ~ P kk:natHk:k < S nH1:k = n~ P nP:nat -> PropH:forall n : nat, P n -> exists m : nat, m < n /\ P mn:natIHn:forall k : nat, k < n -> ~ P kk:natHk:k < S nm:natH1:S k <= nH0:m = n~ P k
k < n のケースは帰納法の仮定から直ちに示せ、k = n のケースは仮定 H によって小さいケースに帰着して、やはり帰納法の仮定を用いることになります。
なんにせよどちらも簡単なので firstorder で示せます。
solve [firstorder].P:nat -> PropH:forall n : nat, P n -> exists m : nat, m < n /\ P mn:natIHn:forall k : nat, k < n -> ~ P kk:natHk:k < S nH1:k = n~ P nsolve [firstorder]. Qed.P:nat -> PropH:forall n : nat, P n -> exists m : nat, m < n /\ P mn:natIHn:forall k : nat, k < n -> ~ P kk:natHk:k < S nm:natH1:S k <= nH0:m = n~ P k
結論
firstorder は強い。
ちなみに命題論理の範囲で示せる場合は tauto を使うとよいでしょう。