#何をどうしていることになるのか、だんだん分からなくなってきた。
#congとかもわかってたつもりなんだけど・・・
#Lists-J.agdaのapp-ass(appendのassociative)の証明なんだけど
#自分でやった時はとりあえずrewrite app-ass xs ys zsしてみてreflにたどり着いた
#notogawaさんの回答みるとcongを使ってる。
#x == yな証明オブジェクトがあれば f x == f yが証明できるよってことなので
#Basicsでも結構使ったんだけど
#app-ass (x :: xs) ys zs = cong (\ as -> x :: as) (app-ass xs ys zs)ってのはどう理解すればいいのでしょう？＋
#app-ass (x :: xs) ys zs = {!!}でholeは
#((x :: xs) ++ ys) ++ zs == (x :: xs) ++ ys ++ zs
#infixr 5 _++_なので
#((x :: xs) ++ ys) ++ zs == (x :: xs) ++ (ys ++ zs)
#って読み換えるとしてここでcongってのはちょっと思いつかない。
#cong (\ as -> x :: as) (app-ass xs ys zs)の最後のapp-ass式は何を返すのだろう？
#(xs ++ ys) ++ zs == xs ++ (ys ++ zs)の証明オブジェクトということになるんだろうけど
#あ、分かった
#自己解決しました。。。
#証明オブジェクトが返ってくるんだろうけど、それは別にcongの第一引数fにとっては関係なくて
#証明されているはずのxs ++ ys ++ zsしたリストが==のlhsとrhsについてるはずで、そいつがasに束縛されて全体にxをconsしてるんだ。
#つまり再帰的に証明されたはずのxs ++ ys ++ zs部分をtailとしてxを後からconsしてるから合同から証明できたということか。
#Basics-Jで出てきたcongって証明したいEqualityのlhsやrhsの部分式だったからそういう使い方しか考えてなかったけど再帰パターンで証明されたものとして全体に何かするということですね。
#いやしかしなんかまた変な気がしてきた。。。
#そもそも合同使っていいのってなんでだろう？
#直後のapp-length : (l1 l2 : natlist) -> length (l1 ++ l2) == length l1 ++ length l2も同じパターンなんだけど
#app-length (x :: xs) ys = cong S (app-length xs ys)
#ap-length xs ysつまり length (l1 ++ l2) == length l1 ++ length l2 の証明があるってことと
#その両辺に+1したらapp-length (x :: xs) ysの証明をしたことになるのってどう関係があるんでしょうか？
#どんなEqualityの証明もそらひとつ前が証明できたとしたら、なんでもcong Sとかcong (cons x)とかすれば良いってのも納得できないんだけど、なぜ？
#app-length (x ∷ xs) ys = { }0 のゴールはlength ((x ∷ xs) ++ ys) ≡ length (x ∷ xs) + length ysで，
#この左辺 length ((x ∷ xs) ++ ys) のC-cC-nが S (length (app xs ys))
#また右辺 length (x ∷ xs) + length ys のC-cC-nが S (plus (length xs) (length ys))
#なので示したいのは， S (length (app xs ys)) ≡ S (plus (length xs) (length ys))
#app-length xs ys のC-cC-dが length (app xs ys) ≡ plus (length xs) (length ys)
#なので cong S でいいですよね？
#なるほど。
#ナットクしました
#app-assも同じかぁ
#いつもありがとうございます > notogawa
#holeが出来たら常にC-cC-tして戦略を練るってことか。今のも命題をそのまま見てたけど、C-cC-tしたら確かにそのままcong使えばいいって分かるな。
#おお、それならrev-lengthも素直に解ける。
#同じくLists-J.agdaのcount-member-nonzeroの証明だけどこれはなぜcongが出てきたんでしょ？
#とりあえず、C-cC-nでみたらble-nat 0 (count 1 xs)になったので
#with count 1 xsして
#... | O = refl
#... | S n = refl
#で解いたのですが、notogawaさんの書いたcong (ble-nat 1) (add-count-commute-count-inc 1 xs)がどこがどうなってcongが出てきたのか知りたいです。
#add-count-commute-count-inc 1 xsの左辺はcount 1 (1 ∷ xs)なのでcong (ble-nat 1)すれば示したいものの左辺になりますよね．
#というよりそもそもこいつ実はrefl一発でカタがつきます．
#てことは、ここはadd-count-commute-count-incが使えるなって直感が働いたからってことですね。
#実はrefl一発でカタがつくって言ってるのはどれのことでしょう？count-member-nonzeroはそのままではダメですよね？
#いやソイツです．
#一発でってのはcount-member-nonzero xs = reflってことですか？
#手元ではそれはダメでした。
#アルェー
#Agda 2.3.2 ですか？
#2.3.2.1です
#2.3.2.1まだ試してないな
#ble-nat の定義が異なるとか…
#ビンゴ > Lost_dog
#ble-nat O _ のパターンを O OとO (S m)とに分かれてました.(私の実装が)
#なるほど
haskell-ja > Archives > 2013/06/13