#sfjaでLists-J.agdaを写経しています.
#test-subset1/2の後で練習問題がありますが、ここで次のようなのを思いついたのですが証明の仕方が分かりません。
#練習問題はあくまでcountとaddを使ってなにか定理を考えろなんですが、そこからは道を外しています。
#nomember-after-remove-all : {n : nat} -> {xs : bag} -> count n (remove-all n xs) == 0
#xsでCase分けすると[]の時は自明になるんですが、帰納パターンでどう進めればいいんでしょう？
#とりあえず帰納法を使ってrewrite nomember-after-remove-all {n} {xs}をしたらヒントとして以下のようになります。
#?0 : count n (remove-all n (x :: xs) | beq-nat n x) == 0
#このゴールはどう読めばいいんでしょうか？
#nを含むbagとかnを含まないbagというのを表現する型を導入してremove-all nの結果がnを含まないbagであることを証明する、か
#よくよく見るとnotogawaさんのadd-count-commute-count-incの証明も理解できん。。。
#beq-nat n nは常にtrueしかなさそうだし、beq-nat-refl nはbeq-nat n nと同じことのような気がするし、一体これはなんなんですか？
#たまたま見つけたんだけど,
#同じLists-J.agdaのdictionary-invariant1も同じようにwith beq-nat k k | beq-nat-refl kを使ってるんで、イディオムっぽい気がする。
#nomember-after-remove-all : {n : nat} -> {xs : bag} -> count n (remove-all n xs) ≡ 0
nomember-after-remove-all {n} {[]} = refl
nomember-after-remove-all {n} {x ∷ xs} = bool-remember {b = beq-nat n x} lemma1 lemma2
where
bool-remember : ∀ {a} {P : Set a} {b : bool} → (b ≡ false → P) → (b ≡ true → P) → P
bool-remember {a} {P} {true} x y = y refl
bool-remember {a} {P} {false} x y = x refl
lemma1 : beq-nat n x ≡ false → count n (remove-all n (x ∷ xs)) ≡ 0
lemma1 p rewrite p | p = nomember-after-remove-all {n} {xs}
lemma2 : beq-nat n x ≡ true → count n (remove-all n (x ∷ xs)) ≡ 0
lemma2 p rewrite p | p = nomember-after-remove-all {n} {xs}#Coqで言うremember tactic相当が必要という感じでしょうか
#add-count-commute-count-incのほうはbeq-nat n nは人目には明らかにtrueですが，withだとtrueとfalse出てきちゃいます．
#なのでbeq-nat-refl nもwithパターンにおまけしてあげて，ありえないfalseのケースを潰してるといったところでしょうか
#それ以前にこれはどういう風な証明になってるんでしょう？
#命題は分かるんですが、どういう風に証明しようとしてて、それでbeq-natが出てきてるのかみたいなのが皆目わからないんです。
#えっと，countの定義がwithで分岐するので，まずその分岐条件と同じものを食わせてそれぞれ分岐先の定義でどうなるか考えてやろうってのが最初のbeq-nat n nのココロです
#add-count-commute-count-incのwithで与えた引数とcountの定義のwithの引数はどう結び付いてきますか？
#add-count-commute-count-incのほうでcount n (add n xs)を評価する(C-cC-n)とcount n (n ∷ xs) | beq-nat n n となりますよね？このbeq-nat n nです．
#ありゃ?本当だ.
#agdaの場合のnormalizeってのは良く分かってないけど
#ってことは,型のところのcount n (add n xs)はそのままだとcount n (n :: xs) | beq-nat n nまでしか評価されないけどwithでヒントを与えるとそれを使ってその先まで評価を進めることができるってことですね
#そういう効果があるというのはちょっと思ってもいなかったです
#count n (n :: xs) | beq-nat n nってのは何のことかと思ってました
#同様にnomember-after-remove-allの例ではwith beq-nat n xがremove-allとcountそれぞれで行われねばならないのですが，
#この2回でbeq-nat n xの結果が違うケース(1回目のwithでtrueにした経路で2回目のwithで今度はfalseになってしまうような)が弾けないので，
#beq-nat n xをtrue/falseのどっちにしたかを一度決めて，それを使い回せるようにしてるのがbool-rememberです
#lemma1/2のrewrite p | pは1回目のpがremove-allのほうを分岐させていて2回目のpがcountのほうを分岐させてますよね
#分岐させているというか"どちらの分岐の定義を見に行くかを確定させている"か
#nomember-after-remove-allの方はまだ全然頭の中が整理できていないです...
#ただ,同じようなゴールが示されてたので，なんとなく同じようなことをremove-allの引数にも与えられればいいんだろうなという気はしてました．
#どうやって与えればいいかが全然分からなかったので，コードをよく読ませてもらいます．
#またこの辺りで質問するかもです．
#ありがとうございました．
#型にも影響するあたりがagdaはhaskellとはまるで違うな
#そう思うとなんか奇妙だな > agda
#実装部分で書いた内容が命題の式変形に影響するという感じかな
#まぁ証明を書いていくことで証明すべきゴールが変わっていくことを思えば当然なのかもしれないけど
#あんまり今まで意識してなかったな．実装したもの使って型を書けるってのは分かってたつもりだけど
#型を構成する式の評価に口出ししてるんだな。型は変わらないしゴールの書き換えはまた別だ。
haskell-ja > Archives > 2013/06/11