--.--
--
上記の広告は1ヶ月以上更新のないブログに表示されています。
新しい記事を書く事で広告が消せます。

08.08
Fri
Coqの勉強をしていて、練習問題によく(?)取り上げられる、リストを2回反転させるともとのリストに戻るというのを証明してみます.どのように考えたかを残しておこうと思います。

まずリストとappendとreverseの定義をします。これが要するにプログラムとなるわけです.
リストは簡単のため要素に自然数しか取れないものを定義しました。



でこのプログラムがもつ性質をCoqで証明します
今回はどんなリストを渡しても2回reverseするともとに戻るというものです。

以下にコードを貼りますが、証明はトップダウンに書いてあるので(思考の過程としては補題を証明してから定理を証明したわけではない)一番下からから読むとどうしてその補題が必要になるのかわかってわかりやすいと思います.



まずをlistに関する帰納法で真っ向から証明してみようとすると、詰みます。なのでなにか補助定理が必要だろうと思います。

は定義よりとなります。(xsはlistのcdr部、xはcar部)
これにreverseをかけた物がになるのでという事になりす。

ここからがちょっと試行錯誤というかひらめきが必要だったのですが(自分は)、xsとxに適当に値を代入して考えてみます.
例えばl = (1,2,3,4)みたいなリストの時xs = (2,3,4),x = 1となりますが上に代入してみるととなります。
これを少しずつ簡単にしていくと
という風になるわけですが、
ここで別にappendしてからreverseしてしなくても先にreverseしてからappendしても同じようになるなーとか、
そのままreverseを先にやるとreverseを2回適用する形が出てきてしまって堂々巡りになりそうだなーと思いつきます。
ということでを補題として証明してやるとうまくいきました。




スポンサーサイト

comment 0 trackback 0
トラックバックURL
http://telracsmoratori.blog.fc2.com/tb.php/192-927368af
トラックバック
コメント
管理者にだけ表示を許可する
 
上記広告は1ヶ月以上更新のないブログに表示されています。新しい記事を書くことで広告を消せます。