reverse (reverse xs) = xs を証明してみる in Idris2

18 min read読了の目安(約16300字

お久しぶりです

前回色々と記事を書いてみたのですが, 春休みで暇なのと色々知見も溜まってきたなど色々あるので型駆動開発 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の型を調べて実際にうまくいくか見ると良い.
  • サラッと証明できたかのように見えるが, 証明は普通ものすっごく試行錯誤して書くものなので(実際今回もものすっごく試行錯誤した)間違っても自己卑下とかしてはいけない(戒め).

おわりに

依存型プログラミングは場数を踏めば楽しくなってくるはずなので(個人差がありますが), 気楽に楽しんでください. ではでは.