###手元で散々やって解けなかった理由は単純にfibの実装で fib (suc (suc n)) = fib n + fib (suc n)にしてたため.
#fib-is-FibFuncの証明自体は同じ物を書いてて，エラーになったのですが何でだか意味が分からなくて困ってた状況．
#Q1. そもそも証明がfibの実装に依存するの何で？
#Q2. 依存するんだろうけど，そうするとFib型の定義が提示された時点でfibの実装はこれ一択になるの？だとするとここからfibの実装を最適化しようとした場合証明の扱いはどうなるの？
#A1. fibの実装に依存するのはある意味当然でしょう．もっと速いfibだったりすると証明はガラリと変わるでしょうし，足し算逆にしただけで+の交換則が必要になったりとか．
#A2. 一択にはなりません．fibの実装がfib (suc (suc n)) = fib n + fib (suc n)だったとしてもfibがFibFuncの性質を持つことは証明できます．
#再帰呼び1本の速いfib実装で証明したやつを投稿してみました．足し算逆のケースもコメントとして付けといたので参考までに
#ありがとうございます.
#とても手におえませぬ...
#ウボァー
#+-commとか知らなかったとしたら
#どういう風に考えるんでしょう.
#直截には
#flip : forall {n x y} -> Fib n x -> Fib (suc n) y -> Fib (suc (suc n)) (x + y)
#な関数があれば
#fib-is-FibFunc (suc (suc n)) = flip (fib-is-FibFunc n) (fib-is-FibFunc (suc n)
#)
#となってflipの実装が出きればよさそう.
#たぶんそのflip作るときに+-comm使いますね
#なんか出来そうに思って手を付けはじめたけど,
#そうですよねー
#まぁ，stdlibに+-commあるの知らなくても，自分で+の交換則証明してもいいですし
#なんだか自分が何を証明しようとしているのかが分からなくなってきた.
#substとか+-commを使った部分の読み方というか、正明寺の気分はどんな感じでしょう？
#足し算逆のやつだと普通に逆になったやつができるから，substと+-commで逆になったところを交換してあげてるって感じです
#subst は {a p : Level} {A : Set a} (P : A → Set p) {x y : A} → x ≡ y → P x → P y なので P y を示すのに P x と x ≡ y を示せばよくなって，
#P x がfibの定義から再帰で作る足し算逆になったアレで x ≡ y が+の交換則みたいな
#ふむふむ
#substの第一引数ってFib (suc (suc n))だったか
#data Fibって証明するための公理みたいなもんだと思ってたんですが、Fib0とかFibNみたいなコンストラクタが公理だとすると、SetであるところのFibってなは何だろう？やはり命題でいいのか？公理の命題って…なんか違うくさい…
#普通に命題と証明でいいのかな
#Fib 0 1が0番目のフィボナッチ数は1であるという命題でその証明がFib0
#Fib1も同様
#このFib a bではFibは"aとbが満たすべき性質(=もしくはaとbの間にあるべき関係)"で，それはコンストラクタの定義の仕方によりbがフィボナッチ数のa番目となっている
#suc n番目のフィボナッチ数がxでn番目がyならsuc (suc n)番目はx+yであるの証明はFibN f1 f0みたいな感じで。
#むむ？
#あぁはい
#なるほど関係か
#むしろフィボナッチ数の定義みたいなもんか。
#帰納的にフィボナッチ数がどういうもんかを定義してると見れそう
#fib-is-FibFunc 0とかはFib 0 1型で、それは定義よりGib0で証明というか自明というか。
haskell-ja > Archives > 2013/05/29