#ああ、なるほど、確かに非対称ですね。それがどのように影響しているか少し考えてみます。 > andb-true-elim1/2
#mult-commを自分なりに証明したんだけど、whereが連なって正直ダセェ
#あとローカルに定義した関数名が読めないのでなんか良い名前があってもよさげだし。
#部分的にrewrite使ってるのもどうなんだ？
#rewriteってどう変形されたのか良く分からんから証明としてはどうなんだ？って気になってきた。
#少し簡単になった。
#思ったけどこれも結構数学的に筋のいい小さな証明を作ってると複雑なものも証明しやすくなるということかな
#stdlibに含まれているのかもしれないけど。
#複雑なものをそのまま長大な証明で示そうとするとAgdaさんstack overflowとか泣きを入れてきたりするのでその点でも
haskell-ja > Archives > 2013/06/05