reverse (reverse xs) = xs を証明してみる in Idris2
お久しぶりです
前回色々と記事を書いてみたのですが, 春休みで暇なのと色々知見も溜まってきたなど色々あるので型駆動開発 in Idris2シリーズを更新しようと思います. そのうちIdris2自体への入門記事も書かなきゃだめだよねぇと思いつつ...
今回のお題
今回は, 反転したリストを反転させると元のリストと等価になるという言明,
reverse (reverse xs) = xs
を証明していこうと思います. 実はIdris2のData.List.reverseInvolutiveというterm
が正にその証明をしてくれているので本当は必要ないのですが, 一度は自分の手でやってみると驚くほど理解が深まるというのが私の経験則です. 今回は一切モジュールをロードせずに, reverse関数を定義するところからやっていきます.
reverse関数の定義
Data.List.reverseに習ってreverse関数を定義します. reverseOntoはいつものaccumulatorに結果を蓄える補助関数です.
module revInvolutive
%default total
reverseOnto : (acc : List a) -> (xs : List a) -> List a
reverseOnto acc [] = acc
reverseOnto acc (x :: xs) = reverseOnto (x :: acc) xs
reverse : (xs : List a) -> List a
reverse = reverseOnto []
Idrisで証明に用いることが出来るのは全域な関数のみです. 今回全てのproof termも勿論全域関数として実装されるので, "%default total"というディレクティブによってそれ以降に定義する関数がデフォルトで全域でなければならないことをコンパイラに伝えておきます. これは別にやらなくてもよいのですが, 本来関数毎に行うはずのtotal宣言を省くことができて, かつもしもうっかり部分関数を書いてしまった(正確に言うとIdrisの全域性検査器が全域であると判定出来ない関数を書いてしまった)際にコンパイルエラーが発生します. Idris2では他にも"%default covering", "%default partial"なるディレクティブがそれぞれ関数がデフォルトでcovering(全ての入力パターンを網羅している)もしくはpartial(部分関数)であることを表すことになります.
本題の定理の表明
次に, 今回証明したい定理を表現します. 名前はrevInvolutiveとしましょう.
revInvolutive : (xs : List a) -> reverse (reverse xs) = xs
早速, エディタプラグインを使ってtemplate definitionを作成した後xsをデータ構築子に沿って場合分けしてみます.
revInvolutive : (xs : List a) -> reverse (reverse xs) = xs
revInvolutive [] = ?revInvolutive_rhs_1
revInvolutive (x :: xs) = ?revInvolutive_rhs_2
revInvolutive_rhs_1の型を調べると次のようになります.
0 a : Type
----------
revInvolutive_rhs_1 : [] = []
つまりreflexiveです. 従ってこのholeをReflで置き換えます.
revInvolutive : (xs : List a) -> reverse (reverse xs) = xs
revInvolutive [] = Refl
revInvolutive (x :: xs) = ?revInvolutive_rhs_2
次に, revInvolutive_rhs_2の型はこうなっています.
0 a : Type
x : a
xs : List a
------------------------------
revInvolutive_rhs_2 : reverseOnto [] (reverseOnto [x] xs) = x :: xs
reverse関数はreverseOnto関数によって定義されているのでこれは当然ですが, これ以上は評価のしようが無い以上どうしようもありません. 従って, とりあえず何らかの補題(lemma)を考える必要がありそうです. とりあえず, reverseOnto acc xsはreverse xs ++ accと等しいなぁという観察を証明してみて, reverseOnto [x] xsを書き換えてみましょう. 次の補題を証明します.
補題 revOnto の証明
revOnto : (acc, xs : List a) -> reverseOnto acc xs = reverse xs ++ acc
いつもの如く, template definitionを生成してから主な引数であるxsで場合分けします.
revOnto : (acc, xs : List a) -> reverseOnto acc xs = reverse xs ++ acc
revOnto acc [] = ?revOnto_rhs_1
revOnto acc (x :: xs) = ?revOnto_rhs_2
?revOnto_rhs_1の型は
0 a : Type
acc : List a
------------------------------
revOnto_rhs_1 : acc = acc
であるためこのholeはReflです. 問題は下のrevOnto_rhs_2の型ですが,
0 a : Type
x : a
xs : List a
acc : List a
------------------------------
revOnto_rhs_2 : reverseOnto (x :: acc) xs = reverseOnto [x] xs ++ acc
reverseOnto (x :: acc) xsに注目して, とりあえず再帰的にrevOnto (x :: acc) xsで書き換えを試みます.
revOnto : (acc, xs : List a) -> reverseOnto acc xs = reverse xs ++ acc
revOnto acc [] = Refl
revOnto acc (x :: xs)
= rewrite revOnto (x :: acc) xs in
?revOnto_rhs_2
すると, revOntO_rhs_2の型が下のように書き換わります.
0 a : Type
x : a
xs : List a
acc : List a
------------------------------
revOnto_rhs_2 : reverseOnto [] xs ++ (x :: acc) = reverseOnto [x] xs ++ acc
よく見ると, reverseOnto [] xsはreverse xsそのものであり, x :: accは[x] ++ accと等価です. 従って, appendAssociative
appendAssociative : (l, c, r : List a) -> l ++ (c ++ r) = (l ++ c) ++ r
appendAssociative [] c r = Refl
appendAssociative (x :: xs) c r = rewrite appendAssociative xs c r in Refl
を使ってappendAssociative (reverse xs) [x] accで書き換えを試みるとうまく行きそうです. ひとまず, このtermをletで受けてrevOnto_rhs_2の型を調べます.
revOnto : (acc, xs : List a) -> reverseOnto acc xs = reverse xs ++ acc
revOnto acc [] = Refl
revOnto acc (x :: xs)
= rewrite revOnto (x :: acc) xs in
let prf = appendAssociative (reverse xs) [x] acc in
?revOnto_rhs_2
するとこのようになります.
0 a : Type
x : a
xs : List a
acc : List a
prf : reverseOnto [] xs ++ (x :: acc) = (reverseOnto [] xs ++ [x]) ++ acc
------------------------------
revOnto_rhs_2 : reverseOnto [] xs ++ (x :: acc) = reverseOnto [x] xs ++ acc
良さそうなので書き換えるとholeはこのようになりました.
0 a : Type
x : a
xs : List a
acc : List a
------------------------------
revOnto_rhs_2 : (reverseOnto [] xs ++ [x]) ++ acc = reverseOnto [x] xs ++ acc
あとは右辺のreverseOnto [x] xsをrevOnto [x] xsで書き換えて
revOnto : (acc, xs : List a) -> reverseOnto acc xs = reverse xs ++ acc
revOnto acc [] = Refl
revOnto acc (x :: xs)
= rewrite revOnto (x :: acc) xs in
rewrite appendAssociative (reverse xs) [x] acc in
rewrite revOnto [x] xs in ?revOnto_rhs_2
holeの型は
0 a : Type
x : a
xs : List a
acc : List a
------------------------------
revOnto_rhs_2 : (reverseOnto [] xs ++ [x]) ++ acc
= (reverseOnto [] xs ++ [x]) ++ acc
のように両辺等しくなったため, めでたくReflです. 補題revOntoの証明が完了しました.
revOnto : (acc, xs : List a) -> reverseOnto acc xs = reverse xs ++ acc
revOnto acc [] = Refl
revOnto acc (x :: xs)
= rewrite revOnto (x :: acc) xs in
rewrite appendAssociative (reverse xs) [x] acc in
rewrite revOnto [x] xs in Refl
これで(ようやく)本題の証明に戻りましょう.
revInvolutiveの続き
revInvolutive : (xs : List a) -> reverse (reverse xs) = xs
revInvolutive [] = Refl
revInvolutive (x :: xs) = ?revInvolutive_rhs_2
holeの型はこうなっています.
0 a : Type
x : a
xs : List a
------------------------------
revInvolutive_rhs_2 : reverseOnto [] (reverseOnto [x] xs) = x :: xs
のでrevOnto [x] xsで書き換えてみます.
revInvolutive : (xs : List a) -> reverse (reverse xs) = xs
revInvolutive [] = Refl
revInvolutive (x :: xs)
= rewrite revOnto [x] xs in
?revInvolutive_rhs_2
すると, holeの型は下のようになります.
0 a : Type
x : a
xs : List a
------------------------------
revInvolutive_rhs_2 : reverseOnto [] (reverseOnto [] xs ++ [x]) = x :: xs
先程の観察下通り, reverseOnto [] xs = revrese xsであり, 従って左辺の式は
reverse (reverse xs ++ reverse [x])とみなせます. 例えば一般に
revAppend : reverse ns ++ reverse vs = reverse (vs ++ ns)が成り立つことは直感的に分かると思うので, とりあえずこれを新たな補題として証明して, holeを書き換えてみましょう.
補題 revAppendの証明
revAppend : (vs, ns : List a) -> reverse ns ++ reverse vs = reverse (vs ++ ns)
を証明します.
revAppend : (vs, ns : List a) ->
reverse ns ++ reverse vs = reverse (vs ++ ns)
revAppend [] ns = ?revAppend_rhs_1
revAppend (x :: xs) ns = ?revAppend_rhs_2
と表せますが, revAppend_rhs_1の型は
0 a : Type
ns : List a
------------------------------
revAppend_rhs_1 : reverseOnto [] ns ++ [] = reverseOnto [] ns
と, revOnto [] ns : redverseOnto [] ns = reverse ns ++ []に注目すれば
すぐさま書き換えが出来ます. ただし, Idrisのrewriteはpremiseにあるx = yなる言明を用いてconclusionのxの出現をyで書き換える仕組みになっているため,
sym : (0 _ : x = y) -> y = xを用いて等号の両辺を交換してから書き換えます.
revAppend : (vs, ns : List a) ->
reverse ns ++ reverse vs = reverse (vs ++ ns)
revAppend [] ns = rewrite sym $ revOnto [] ns in Refl
revAppend (x :: xs) ns = ?revAppend_rhs_2
revAppend_rhs_2の型は,
0 a : Type
x : a
xs : List a
ns : List a
------------------------------
revAppend_rhs_2 : reverseOnto [] ns ++ reverseOnto [x] xs
= reverseOnto [x] (xs ++ ns)
となっており, ひとまず reverseOnto [x] xsをrevOnto [x] xsで書き換えてみます.
0 a : Type
x : a
xs : List a
ns : List a
------------------------------
revAppend_rhs_2 : reverseOnto [] ns ++ (reverseOnto [] xs ++ [x])
= reverseOnto [x] (xs ++ ns)
今度は右辺のreverseOnto [x] (xs ++ ns)をrevOnto [x] (xs ++ ns)で書き換えてみます.
0 a : Type
x : a
xs : List a
ns : List a
------------------------------
revAppend_rhs_2 : reverseOnto [] ns ++ (reverseOnto [] xs ++ [x])
= reverseOnto [] (xs ++ ns) ++ [x]
すると, 右辺にreverseOnto [] (xs ++ ns) (= reverse (xs ++ ns))が出現するので,
revAppend ns xsを再帰的に適用してみると, 次のコードを得ます.
revAppend : (vs, ns : List a) ->
reverse ns ++ reverse vs = reverse (vs ++ ns)
revAppend [] ns = rewrite sym $ revOnto [] ns in Refl
revAppend (x :: xs) ns
= rewrite revOnto [x] xs in
rewrite revOnto [x] (xs ++ ns) in
let prf = revAppend xs ns in ?revAppend_rhs_2
この時holeの型は
0 a : Type
x : a
xs : List a
ns : List a
prf : reverseOnto [] ns ++ reverseOnto [] xs = reverseOnto [] (xs ++ ns)
------------------------------
revAppend_rhs_2 : reverseOnto [] ns ++ (reverseOnto [] xs ++ [x])
= reverseOnto [] (xs ++ ns) ++ [x]
であり, 先程と同様にsym prfを使って書き換えを行えそうです. 書き換えると,
revAppend : (vs, ns : List a) ->
reverse ns ++ reverse vs = reverse (vs ++ ns)
revAppend [] ns = rewrite sym $ revOnto [] ns in Refl
revAppend (x :: xs) ns
= rewrite revOnto [x] xs in
rewrite revOnto [x] (xs ++ ns) in
rewrite sym $ revAppend xs ns in
?revAppend_rhs_2
というコードが得られ, holeの型は
0 a : Type
x : a
xs : List a
ns : List a
------------------------------
revAppend_rhs_2 : reverseOnto [] ns ++ (reverseOnto [] xs ++ [x])
= (reverseOnto [] ns ++ reverseOnto [] xs) ++ [x]
となります. こうなると, あとはappendAssociativeを使えばReflに置き換えられることが分かるはずです. これで証明が完了しました.
revAppend : (vs, ns : List a) ->
reverse ns ++ reverse vs = reverse (vs ++ ns)
revAppend [] ns = rewrite sym $ revOnto [] ns in Refl
revAppend (x :: xs) ns
= rewrite revOnto [x] xs in
rewrite revOnto [x] (xs ++ ns) in
rewrite sym $ revAppend xs ns in
rewrite appendAssociative (reverse ns) (reverse xs) [x] in
Refl
ようやくrevInvolutiveの証明へ...
さて, 長い補題の証明が終わったところで, 現在の状況をおさらいします.
RevInvolutive.idrは以下のようになっているのでした.
module RevInvolutive
%default total
reverseOnto : (acc : List a) -> (xs : List a) -> List a
reverseOnto acc [] = acc
reverseOnto acc (x :: xs) = reverseOnto (x :: acc) xs
reverse : (xs : List a) -> List a
reverse = reverseOnto []
appendAssociative : (l, c, r : List a) -> l ++ (c ++ r) = (l ++ c) ++ r
appendAssociative [] c r = Refl
appendAssociative (x :: xs) c r = rewrite appendAssociative xs c r in Refl
revOnto : (acc, xs : List a) -> reverseOnto acc xs = reverse xs ++ acc
revOnto acc [] = Refl
revOnto acc (x :: xs)
= rewrite revOnto (x :: acc) xs in
rewrite appendAssociative (reverse xs) [x] acc in
rewrite revOnto [x] xs in Refl
revAppend : (vs, ns : List a) ->
reverse ns ++ reverse vs = reverse (vs ++ ns)
revAppend [] ns = rewrite sym $ revOnto [] ns in Refl
revAppend (x :: xs) ns
= rewrite revOnto [x] xs in
rewrite revOnto [x] (xs ++ ns) in
rewrite sym $ revAppend xs ns in
rewrite appendAssociative (reverse ns) (reverse xs) [x] in
Refl
revInvolutive : (xs : List a) -> reverse (reverse xs) = xs
revInvolutive [] = Refl
revInvolutive (x :: xs)
= rewrite revOnto [x] xs in
?revInvolutive_rhs_2
残った唯一のholeであるrevInvolutive_rhs_2の型は, 下のようになっています.
0 a : Type
x : a
xs : List a
------------------------------
revInvolutive_rhs_2 : reverseOnto [] (reverseOnto [] xs ++ [x]) = x :: xs
左辺の reverseOnto [] (reverseOnto [] xs ++ [x])が reverse (reverse xs ++ [x])とみなせるので, ここで revAppend (reverse xs) [x]を用いて書き換えができそうです.
revInvolutive : (xs : List a) -> reverse (reverse xs) = xs
revInvolutive [] = Refl
revInvolutive (x :: xs)
= rewrite revOnto [x] xs in
let prf = revAppend (reverse xs) [x] in
?revInvolutive_rhs_2
するとholeの型は
0 a : Type
x : a
xs : List a
prf : x :: reverseOnto [] (reverseOnto [] xs)
= reverseOnto [] (reverseOnto [] xs ++ [x])
------------------------------
revInvolutive_rhs_2 : reverseOnto [] (reverseOnto [] xs ++ [x]) = x :: xs
となります. つまり, sym prfで書き換えが出来るということです. 書き換えるとholeの型は
下のようになります.
0 a : Type
x : a
xs : List a
------------------------------
revInvolutive_rhs_2 : x :: reverseOnto [] (reverseOnto [] xs) = x :: xs
reverseOnto [] (reverseOnto [] xs)は既にreverse (reverse xs)と等価であることを鑑みれば, revInvolutive xs : reverse (reverse xs) = xsで書き換えができそうです.
revInvolutive : (xs : List a) -> reverse (reverse xs) = xs
revInvolutive [] = Refl
revInvolutive (x :: xs)
= rewrite revOnto [x] xs in
rewrite sym $ revAppend (reverse xs) [x] in
rewrite revInvolutive xs in
?revInvolutive_rhs_2
すると, holeは
0 a : Type
x : a
xs : List a
------------------------------
revInvolutive_rhs_2 : x :: xs = x :: xs
となり, めでたくReflとなって証明が完了しました.
revInvolutive : (xs : List a) -> reverse (reverse xs) = xs
revInvolutive [] = Refl
revInvolutive (x :: xs)
= rewrite revOnto [x] xs in
rewrite sym $ revAppend (reverse xs) [x] in
rewrite revInvolutive xs in
Refl
ソースコード全体
ソースコード全体は以下のようになります. 運営さんは早いとこIdrisのsyntax highlightingを入れてもろて.
module RevInvolutive
%default total
reverseOnto : (acc : List a) -> (xs : List a) -> List a
reverseOnto acc [] = acc
reverseOnto acc (x :: xs) = reverseOnto (x :: acc) xs
reverse : (xs : List a) -> List a
reverse = reverseOnto []
appendAssociative : (l, c, r : List a) -> l ++ (c ++ r) = (l ++ c) ++ r
appendAssociative [] c r = Refl
appendAssociative (x :: xs) c r = rewrite appendAssociative xs c r in Refl
revOnto : (acc, xs : List a) -> reverseOnto acc xs = reverse xs ++ acc
revOnto acc [] = Refl
revOnto acc (x :: xs)
= rewrite revOnto (x :: acc) xs in
rewrite appendAssociative (reverse xs) [x] acc in
rewrite revOnto [x] xs in Refl
revAppend : (vs, ns : List a) ->
reverse ns ++ reverse vs = reverse (vs ++ ns)
revAppend [] ns = rewrite sym $ revOnto [] ns in Refl
revAppend (x :: xs) ns
= rewrite revOnto [x] xs in
rewrite revOnto [x] (xs ++ ns) in
rewrite sym $ revAppend xs ns in
rewrite appendAssociative (reverse ns) (reverse xs) [x] in
Refl
revInvolutive : (xs : List a) -> reverse (reverse xs) = xs
revInvolutive [] = Refl
revInvolutive (x :: xs)
= rewrite revOnto [x] xs in
rewrite sym $ revAppend (reverse xs) [x] in
rewrite revInvolutive xs in
Refl
まとめとTips
- 証明をするときは%default totalディレクティブを宣言して全域じゃない関数をうっかり書いてしまわないようにコンパイラに手助けしてもらうと良い.
- 今回のように書き換えが連続する証明では, これいけそうと思った書き換え候補をlet prf = term in ?holeのようにして変数で受け止めた後にholeの型を調べて実際にうまくいくか見ると良い.
- サラッと証明できたかのように見えるが, 証明は普通ものすっごく試行錯誤して書くものなので(実際今回もものすっごく試行錯誤した)間違っても自己卑下とかしてはいけない(戒め).
おわりに
依存型プログラミングは場数を踏めば楽しくなってくるはずなので(個人差がありますが), 気楽に楽しんでください. ではでは.
Discussion