induction principle を自分で書く - 論理とか計算機とか数学とか

昨日 (http://lkozima.hatenablog.com/entry/2013/07/19/225156) よくわからないとか言っていたのが冷静に考えたらできた。

なんかこういうのを考えていて，

Inductive mov : nat -> nat -> Prop :=
| mov_1 : forall m, mov (S m) m
| mov_2 : forall m, mov (S (S m)) m
| mov_3 : forall m, mov (S (S (S m))) m.

Inductive losing : nat -> Prop :=
| Losing : forall n,
  (forall m, mov n m -> exists k, mov m k /\ losing k) ->
  losing n.

losing に対する induction principle はどういう形になるべきだろうかという話でした。

結論から書くと

Fixpoint losing_induction P 
  (IH : forall n,
    (forall m, mov n m -> exists k, mov m k /\ losing k /\ P k) -> P n)
  n (H : losing n) : P n :=
  match H with
    | Losing n f =>
      IH n (fun m Hm =>
        match f m Hm with
          | ex_intro k (conj p1 p2) =>
            ex_intro _ k (conj p1 (conj p2 (losing_induction P IH k p2)))
        end)
  end.

でよいと思います。読みにくいですが。Check してみるとこうなってます。

losing_induction
     : forall P : nat -> Prop,
       (forall n : nat,
        (forall m : nat,
         mov n m -> exists k : nat, mov m k /\ losing k /\ P k) -> 
        P n) -> forall n : nat, losing n -> P n

これを使って losing なら 4 の倍数であることも証明できました。証明の中身は lt_wf_ind を使う場合とほとんど同じになりましたが。

でもそれよりも，どうやってこの形を出したかのほうがおもしろいと思うのでその話をします。

帰納法の原理の作り方

以下 $P \subseteq {\mathbb N}$ を述語とみなして $x \in P$ を $P(x)$ と書きます。

$F : \mathcal{P}({\mathbb N}) \to \mathcal{P}({\mathbb N})$ を

$F(P)(n) \Longleftrightarrow (\forall m, \mathtt{mov}(n, m) \Longrightarrow \exists k, \mathtt{mov}(m, k) \wedge P(k))$

で定めます。このとき losing は F の最小不動点です。なのでこの述語に対する帰納法の原理は「F の prefixed-point は losing に含まれる」つまり

$F(P) \subseteq P \Longrightarrow \mathtt{losing} \subseteq P$

になります。これはもうちょっと強めることができて

$F(P \cap \mathtt{losing}) \subseteq P \Longrightarrow \mathtt{losing} \subseteq P$

ともできます。

ここで F の定義を展開すると，上に coq で書いた帰納法の原理が出てきます。長いので帰納法の仮定のところだけ書くと

$n \in F(P \cap \mathtt{losing}) \Longleftrightarrow (\forall m, \mathtt{mov}(n, m) \Longrightarrow \exists k, \mathtt{mov}(m, k) \wedge \mathtt{losing}(k) \wedge P(k))$

となります。forall m : nat, ... の部分に対応していることがわかるでしょう。