#Basics-J.agdaやってるんですが
#plus-id-exampleで出てきたrewriteがよくわからないのですが，これは何をするもの？
#とりあえず plus-id-example n m eq = ?から
#eq C-cC-cしてやると
#plus-id-example .m m relf = {}0
#あとはC-cC-aでreflに確定したので自分で証明した感じは全然ないんですが
#rewriteは使わないで完結してそう
##これ見てもどうも...
#refl,sym,cong,trans自体は反射律,対称律,?,推移律ってのはまぁ分かるんですが
#例えばこの資料の93ページ目のcongの定義は何でこうなるのかさっぱりです
#rewriteが分からないというより
#reflやcongなどを使った証明が分かってないのかもしれないけど
#cong f refl = reflってどう理解すればいいんでしょう？
#↑Q1
#Q2. plus-id-example n m eq rewrite eq = reflはどう理解すればいいんでしょう？
#A1. cong : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y なので，x ≡ y から f x ≡ f y を示す'合流'です．
#"xとyが同じ(=ライプニッツ等値)であれば，辺々になにやっても(=何を適用しても)同じ"ということですね．
##"rewriting the goal and the context by the given equation"なので，plus-id-exampleの場合goalがn + n ≡ n + nに書き替えられてこれは明らかにreflです．
#eqをcase展開してやってドットパターン出すのでももちろんよいのですが，Basics-Jはドットパターン禁止でやってたので．
#congでは合同を証明したいんですよね？
#なのにcong f refl= reflというのがどうも理解に苦しみます。x==yならばf x==f yが当たり前(refl)だとして良いのが何処までrefl使えるの？みたいな。
#rewriteでゴール書き換えるというのは何でも好きにゴール変えて言い訳ではないでよね？当然元の証明となんがしか繋がってないとダメだと思うんですが。
#agdaはどのように証明をチェックしてるんでしょう？仕組みというか評価規則のようなものというか
#rewriteの"元の証明"との繋がりは Leibniz Equality で保証されていますよね？
#cong f refl = refl って，元々 cong f {x} {y} eq = {eq} からC-cC-cして cong f {.y} {y} refl = { } となり，ゴールもf y ≡ f y とかになってるという認識はだいじょぶですか？
#ここからimplicit param省略してf y ≡ f yの型持ったreflさしこむとcong f refl = refl ですよね？
#congはなるほどです。eqになり得るのがreflしかなくて、そうすると依存関係からxとyがおなじになるしかなくて、ゴールもf y==f yになると。
#rewriteはちょっと書き換えるの意味というかルールがまるで分かってないので…
#plus-id-example n m eqを実装するって問題をeqを実装するって問題に置き換えたってことですか？
#rewriteは基本的には今示そうとしているもの全体にかかるsubstみたいなもんです．
#rewriteって証明でいうと何をしていることに当たるんでしょう？
#rewrite eqは今の命題全体に含まれるeqの左辺をeqの右辺に置き替える
#するとゴールを書き換えてるわけではないんでしょうか？
#ゴールも書き替えてます
#でも意味が分からないながらもplus-id-exampleでrewriteやると右辺のholeの型は変わったな。
#rewriteしたことによって自動でreflが出てくるような型にtargetが変わったということを指してゴールを置き換えたってことだと思ったんだけど。
#ですよね。
#ゴールを書き換えるってのは証明すべき命題をすりかえるってことですよね？きっと。
#すりかえるし，"それをしてもいい等値性"が Leibniz Equality です．
#plus-id-exampleの例だと
#第三引数のeqをreflで置き換えていいのは分かりました。それしかその型を満たす項がないからということで。
#でもそれをしたからといってゴールの型が変わるのがまだ理解できてません。
#plus-id-example .m m refl となったらゴールは m + m ≡ m + m ですよね？型変わってますか？
#あれ？なんか勘違いしてたみたいです。
#rewrite eq = reflはこの場合eqの型から合理的で、
#それを与えることでn == mが依存関係から出てきて、それによって元の命題はn+n == m+mからn+n==n+nに決まって証明できたことになる。という流れでしゃうか。
#ああ，これそういうカンチガイか
#なんか元の命題からしてそらそうだろって思えてしまってどうやれば証明したことになるのか方向が分からん…
#rewrite eq = refl って別にeqがreflという意味ではないです
#plus-id-example n m eq rewrite eq で一度切って下さい．
#ここまでで eq : n ≡ m によって， n が m に置きかえられる．
#=のあとは普通に証明するのと同じです．ただしもういろんなものの中のnがmになっている
#rewriteってのはその命題を受け入れる？成り立つと仮定したら？ってことですかね？
#仮定されてるEqualityで書き換えるのがrewrite
#たとえば，複数個のEqualityでrewriteするような例は次のようなカンジ
#sample : (a b n m : ℕ) → a ≡ b → n ≡ m → a + n ≡ b + m
sample a b n m a≡b n≡m
rewrite a≡b -- aをbに置き替え
| n≡m -- nをmに置き替え
= { }0 -- 上記2つの置き替えで ?0 : b + m ≡ b + m なので refl でいい#なるほど、すると全体としては仮定したものを別途証明する必要が出てきますね？
#plus-id-exampleを証明するのが元のゴールだったんだけど、ある仮定を入れることで証明しておいて、あとはその仮定を証明すればいい。という戦略に見えますがあってますか？
#ちがいます．仮定はもうあるのです．a≡bやn≡mはgivenですよね．
#plus-id-exampleだとeqか
#むむ？
#plus-id-exampleの場合だと、n==mならばn+n==m+mである。
#というのが命題ですね？
#ですね
#で型が与えられてはいるけど、その項が書けて初めて証明できたことになる、という理解でいいですか？
#はい
#この場合、n==mになる項はreflしかないので
#plus-id-example .m m refl = ?
#のパターンしかマッチするのがなくて右辺は自動的にreflになる
#この流れだと
#仮定したわけじゃなくてn==mの証明としてreflを与えてる感じがするんですが、
#=の左にあるものは全て右にくるものを示すための仮定です
#rewriteを使った場合って、n==mの証明があるかどうかは知らないけど、仮にあれば、命題はm==mならばm+m==m+mである。となる。
#ぬぬぬ
#plus-id-exampleの例で、
#pplus-id-example .m m refl = reflってのと
#plus-id-example n m eq rewrite eq = refl
#ってのとでは
#それぞれどういう風に証明していると読めますか？
#まず前者ですが，
#nとmが等しいときはmの反射率で証明終了．nとmが異なるときは矛盾を引き出して証明終了．
#s/mの反射率/m+mの反射率/
#後者は，nをmに書き換えた後，m+mの反射率で証明終了
#おお
#rewriteってのはその仮定を使うことでこうを
#使うことで項を書き換えるのか
#その仮定を使う感じですね
#そうですね
#前者は色々なケースが考えられる中で今の場合はたまたま.m m reflのパターンしか
#(eqの型から)ありえなかったけど、
#とにかく前者はしらみ潰しに場合分けして考えていく戦略で
#後者はn==mの証明(実装)は知らんが、
#それでもその与えられた仮定を使えば命題となってたn==mが成り立つはずなので、
#それを使ってみろとagdaに指示してる。
#そうですね
#ようやく分かりましたが、rewriteって_==_な型の引数にしか使えないのですか？
#仮定されているEqualityで置き換えるという話でしたが
#気になったのはrewriteって組み込みの構文ぽいのに、_==_ってライブラリで定義されたものなので、
#Leibniz Equality と等価な定義のEqualityで，かつBUILTIN EQUALITY指定してれば使えるんじゃないかと思いますが，やってみたことないです．
#そのあたりはどうなってんのかなと。
#じゃあ今のようなパターンでだいたいことは足りてるってことですね。
#丁寧にありがとうございました。
#あと、右辺にreflって書いてるときの気分がいまひとつ分からなかったんですが、「反射律により成り立つ」みたいな感じなんですね。
#なんかずっと反射率って書いてますね自分．変換ミス
#分かるとまんまやんけって感じなんですが…ここもピンときてなかったです。
#ありがとうございました。
#とりあえずchallengeがまるでついていけないので、ひとまず公開してくれたsfのコードを入力しながら勉強してます。
#おお、congの定義もさっき分かったって書いたけど、今ようやく自然に読めます。
#感動
haskell-ja > Archives > 2013/06/02