Idrisの有界な自然数で遊んでみる(1) — 証明をつける

前回はIdrisで「有界な自然数の冪乗を計算する」finPower2 : Fin n -> Fin (power 2 n) という関数を実装したが、いくつか後回しにした証明があった。今回はIdrisの証明支援機能を使ってこれを埋める。

まずはターミナルを開いて idris FinPower2.idr を実行しよう。（この記事はIdrisのインストールが終わっていることが前提になっている）

$ idris FinPower2.idr⏎
     ____    __     _                                          
    /  _/___/ /____(_)____                                     
    / // __  / ___/ / ___/     Version 0.9.16
  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/      
 /___/\__,_/_/  /_/____/       Type :? for help               

Idris is free software with ABSOLUTELY NO WARRANTY.            
For details type :warranty.
Metavariables: Main.proof3, Main.proof2, Main.proof1
*FinPower2>

最後から2番目の行に出てきた Metavariables: というのが、前回やり残した証明だ。:type コマンドで型を確認しておこう。

*FinPower2> :type proof1⏎
  m : Nat
  inductiveHypothesis : S (power2m1 m) = power (fromInteger 2) m
--------------------------------------
proof1 : S (S (plus (power2m1 m) (plus (power2m1 m) 0))) =
         plus (power 2 m) (plus (power 2 m) 0)
Metavariables: Main.proof3, Main.proof2, Main.proof1
*FinPower2>

元々証明したい等式は S (power2m1 (S m)) = power 2 (S m) だったはずだが、コンパイラによってある程度簡約されている。他の proof2 と proof3 も確認しておこう。

*FinPower2> :type proof2⏎
  m : Nat
--------------------------------------
proof2 : S (S (plus (power2m1 m) (plus (power2m1 m) 0))) =
         plus (power 2 m) (plus (power 2 m) 0)
Metavariables: Main.proof3, Main.proof2, Main.proof1
*FinPower2> :type proof3⏎
  m : Nat
  k : Fin m
--------------------------------------
proof3 : plus (power 2 m) (power 2 m) =
         plus (power 2 m) (plus (power 2 m) 0)
Metavariables: Main.proof3, Main.proof2, Main.proof1
*FinPower2>

証明・一個目

では早速 proof1 の証明を埋めよう。:prove コマンドを使うとインタラクティブな証明モードに入る。

*FinPower2> :prove proof1⏎


----------                 Goal:                  ----------
{hole0} : (m : Nat) ->
          (S (power2m1 m) = power (fromInteger 2) m) ->
          S (S (plus (power2m1 m) (plus (power2m1 m) 0))) =
          plus (power 2 m) (plus (power 2 m) 0)
-Main.proof1>

Goal: 以下にあるのが示すべき命題だ。この状態では (m : Nat) と S (power2m1 m) = power (fromInteger 2) m という引数を取る関数の型になっている。論理で言うと含意（「ならば」）を使った形になっている。intro というtacticを使うと、「仮定」を導入して関数の引数を減らすことができる。

-Main.proof1> intro⏎
----------              Other goals:              ----------
{hole0}
----------              Assumptions:              ----------
 m : Nat
----------                 Goal:                  ----------
{hole1} : (S (power2m1 m) = power (fromInteger 2) m) ->
          S (S (plus (power2m1 m) (plus (power2m1 m) 0))) =
          plus (power 2 m) (plus (power 2 m) 0)
-Main.proof1>

Assumptions: という項目に m : Nat が増えて、Goal: にあった関数の引数 (m : Nat) がなくなった。もう一回 intro を使うと、帰納法の仮定 (S (power2m1 m) = power (fromInteger 2) m) も Assumptions: に移動する。

-Main.proof1> intro⏎
----------              Other goals:              ----------
{hole1},{hole0}
----------              Assumptions:              ----------
 m : Nat
 inductiveHypothesis : S (power2m1 m) = power (fromInteger 2) m
----------                 Goal:                  ----------
{hole2} : S (S (plus (power2m1 m) (plus (power2m1 m) 0))) =
          plus (power 2 m) (plus (power 2 m) 0)
-Main.proof1>

ちなみに、intros というtacticを使うと、複数回の intro を一括でやってくれる。

Goal の左辺の plus (power2m1 m) (plus (power2m1 m) 0) は 2 * power2m1 m を簡約したもの、右辺の plus (power 2 m) (plus (power 2 m) 0) は 2 * power 2 m を簡約したものだと思われる。つまり、実質的に示すべき命題は

S (S (2 * power2m1 m)) = 2 * power 2 m

である。この右辺は帰納法の仮定 S (power2m1 m) = power 2 m を使うと 2 * (S (power2m1 m)) に置き換えられる。

この「置き換え」をやってくれるのが rewrite taticである。rewrite tacticに x=y という型の値（証明）を与えると、goal中の y を x で置き換えてくれる。

-Main.proof1> rewrite inductiveHypothesis⏎
----------              Other goals:              ----------
{hole2},{hole1},{hole0}
----------              Assumptions:              ----------
 m : Nat
 inductiveHypothesis : S (power2m1 m) = power (fromInteger 2) m
----------                 Goal:                  ----------
{hole3} : S (S (plus (power2m1 m) (plus (power2m1 m) 0))) =
          plus (S (power2m1 m)) (plus (S (power2m1 m)) 0)
-Main.proof1>

ごちゃごちゃして見にくいが、y = power2m1 m と置き換えてみると

S (S (y + (y + 0))) = S y + ((S y) + 0)

を証明しろということである。やっぱりごちゃごちゃしているが、compute tacticを使うと、goalを正規化してくれる（らしい）。

-Main.proof1> compute⏎
----------              Other goals:              ----------
{hole2},{hole1},{hole0}
----------              Assumptions:              ----------
 m : Nat
 inductiveHypothesis : S (power2m1 m) = power (fromInteger 2) m
----------                 Goal:                  ----------
{hole3} : S (S (plus (power2m1 m) (plus (power2m1 m) 0))) =
          S (plus (power2m1 m) (S (plus (power2m1 m) 0)))
-Main.proof1>

これでも少し見にくいが、y = power2m1 m, z = (power2m1 m) + 0 と置き換えてみると、証明すべき命題は

S (S (y + z)) = S (y + (S z))

となっている。ペアノの公理に \(\mathrm{S }(y + z) = y + (\mathrm{S }z)\) みたいなのがあった気がするし、これは加法の割と基本的な性質である。この証明は標準ライブラリに用意されていて、

plusSuccRightSucc : (left : Nat) -> (right : Nat) -> S (left + right) = left + (S right)

という名前と型がついている。今の状況だと、

plusSuccRightSucc (power2m1 m) ((power2m1 m) + 0) : S (power2m1 m + (power2m1 m + 0)) = power2m1 m + S (power2m1 m + 0)

とやれば欲しい命題になる。これを使って rewrite してやればよい。

-Main.proof1> rewrite plusSuccRightSucc (power2m1 m) ((power2m1 m) + 0)⏎
----------              Other goals:              ----------
{hole3},{hole2},{hole1},{hole0}
----------              Assumptions:              ----------
 m : Nat
 inductiveHypothesis : S (power2m1 m) = power (fromInteger 2) m
----------                 Goal:                  ----------
{hole7} : S (S (plus (power2m1 m) (plus (power2m1 m) 0))) =
          S (S (plus (power2m1 m) (plus (power2m1 m) 0)))
-Main.proof1>

示すべき命題が自明になった。trivial と打ち込む。

-Main.proof1> trivial⏎
proof1: No more goals.
-Main.proof1>

証明が終わった。qed と打ち込むと証明モードが終わる。

-Main.proof1> qed⏎
Proof completed!
Main.proof1 = proof
  intros
  rewrite inductiveHypothesis
  compute
  rewrite plusSuccRightSucc (power2m1 m) ((power2m1 m) + 0)
  trivial


Metavariables: Main.proof3, Main.proof2
*FinPower2>

:addproof コマンドを実行すると、もとのソースコードに今作った証明が書き込まれる。

*FinPower2> :addproof⏎
Added proof Main.proof1
Metavariables: Main.proof3, Main.proof2
*FinPower2>

FinPower2.idr を確認すると、次のようなものが書き込まれている。

(略)

---------- Proofs ----------

Main.proof1 = proof
  intros
  rewrite inductiveHypothesis
  compute
  rewrite plusSuccRightSucc (power2m1 m) ((power2m1 m) + 0)
  trivial

証明・二個目

*FinPower2> :prove proof2⏎


----------                 Goal:                  ----------
{hole0} : (m : Nat) ->
          S (S (plus (power2m1 m) (plus (power2m1 m) 0))) =
          plus (power 2 m) (plus (power 2 m) 0)
-Main.proof2> intros⏎
----------              Other goals:              ----------
{hole0}
----------              Assumptions:              ----------
 m : Nat
----------                 Goal:                  ----------
{hole1} : S (S (plus (power2m1 m) (plus (power2m1 m) 0))) =
          plus (power 2 m) (plus (power 2 m) 0)

ここで、前回用意して、さっき証明を完成させた

succPower2m1Power2 : (k : Nat) -> S (power2m1 k) = power 2 k

が活きる。

-Main.proof2> rewrite succPower2m1Power2 m⏎
----------              Other goals:              ----------
{hole1},{hole0}
----------              Assumptions:              ----------
 m : Nat
----------                 Goal:                  ----------
{hole2} : S (S (plus (power2m1 m) (plus (power2m1 m) 0))) =
          plus (S (power2m1 m)) (plus (S (power2m1 m)) 0)
-Main.proof2> compute⏎
----------              Other goals:              ----------
{hole1},{hole0}
----------              Assumptions:              ----------
 m : Nat
----------                 Goal:                  ----------
{hole2} : S (S (plus (power2m1 m) (plus (power2m1 m) 0))) =
          S (plus (power2m1 m) (S (plus (power2m1 m) 0)))

あとはさっきと同じパターンである。

-Main.proof2> rewrite plusSuccRightSucc (power2m1 m) (power2m1 m + 0)⏎
----------              Other goals:              ----------
{hole2},{hole1},{hole0}
----------              Assumptions:              ----------
 m : Nat
----------                 Goal:                  ----------
{hole7} : S (S (plus (power2m1 m) (plus (power2m1 m) 0))) =
          S (S (plus (power2m1 m) (plus (power2m1 m) 0)))
-Main.proof2> trivial⏎
proof2: No more goals.
-Main.proof2> qed⏎
Proof completed!
Main.proof2 = proof
  intros
  rewrite succPower2m1Power2 m
  compute
  rewrite plusSuccRightSucc (power2m1 m) (power2m1 m + 0)
  trivial


Metavariables: Main.proof3
*FinPower2> :addproof⏎
Added proof Main.proof2
*FinPower2>

証明・三個目

*FinPower2> :prove proof3⏎


----------                 Goal:                  ----------
{hole0} : (m : Nat) ->
          Fin m ->
          plus (power 2 m) (power 2 m) =
          plus (power 2 m) (plus (power 2 m) 0)
-Main.proof3> intros⏎
----------              Other goals:              ----------
{hole1},{hole0}
----------              Assumptions:              ----------
 m : Nat
 k : Fin m
----------                 Goal:                  ----------
{hole2} : plus (power 2 m) (power 2 m) =
          plus (power 2 m) (plus (power 2 m) 0)

示すべき命題の何が自明じゃないかと言ったら、power 2 m = power 2 m + 0 である。つまり、右から 0 を足しても値は変わらないということである。これは

plusZeroRightNeutral : (left : Nat) -> left + 0 = left

を使えば良い。

-Main.proof3> rewrite plusZeroRightNeutral (power 2 m)⏎
----------              Other goals:              ----------
{hole2},{hole1},{hole0}
----------              Assumptions:              ----------
 m : Nat
 k : Fin m
----------                 Goal:                  ----------
{hole3} : plus (plus (power 2 m) 0) (plus (power 2 m) 0) =
          plus (plus (power 2 m) 0) (plus (power 2 m) 0)
-Main.proof3> trivial⏎
proof3: No more goals.
-Main.proof3> qed⏎
Proof completed!
Main.proof3 = proof
  intros
  rewrite plusZeroRightNeutral (power 2 m)
  trivial


*FinPower2> :addproof⏎
Added proof Main.proof3
*FinPower2>

最終的な FinPower2.idr の内容

import Data.Fin

power2m1 : Nat -> Nat
power2m1 Z = Z
power2m1 (S k) = S (2 * power2m1 k)

succPower2m1Power2 : (k : Nat) -> S (power2m1 k) = power 2 k
succPower2m1Power2 Z = Refl
succPower2m1Power2 (S m) =
  let inductiveHypothesis = succPower2m1Power2 m
  in ?proof1

finPower2 : {n : Nat} -> Fin n -> Fin (power 2 n)
finPower2 {n = S m} FZ = f (FS FZ)
  where
    p : S (S (2 * power2m1 m)) = power 2 (S m)
    p = ?proof2
    f : Fin (S (S (2 * power2m1 m))) -> Fin (power 2 (S m))
    f = replace {P=Fin} p
finPower2 {n = S m} (FS k) = let x = finPower2 k
                             in replace p (x + x)
  where
    p : (power 2 m) + (power 2 m) = power 2 (S m)
    p = ?proof3

---------- Proofs ----------

Main.proof3 = proof
  intros
  rewrite plusZeroRightNeutral (power 2 m)
  trivial


Main.proof2 = proof
  intros
  rewrite succPower2m1Power2 m
  compute
  rewrite plusSuccRightSucc (power2m1 m) (power2m1 m + 0)
  trivial


Main.proof1 = proof
  intros
  rewrite inductiveHypothesis
  compute
  rewrite plusSuccRightSucc (power2m1 m) ((power2m1 m) + 0)
  trivial

参考資料

Tutorial
Wikiのマニュアル
Theorem Proving (注意書きにあるように、古い)

Spread the love