No Such Blog or Diary
あー,証明から値を取り出せないんか
- 2012-10-17 (Wed)
- 一般
まあ,exists x とか書かれていたとして具体的にどれが出てくるかとか証明上は関係ないのだから何かを取り出そうとしないというのが自然な思考なのだけど,ときどき値が取り出せたらなぁと思わなくない.
とりあえず Prop の扱いにまだ慣れていないらしい.
閑話休題.
証明を対話的にやるのが面倒だから直接プログラム書いてしまえと思うようになってきた.が,まだ tactic と実際のコードとの対応とかが把握しきれていないのでなんとも難しい.
- Comments: 0
- TrackBack (Close): -
単位体積あたりの熱量が……
- 2012-10-16 (Tue)
- 一般
パンだと少なすぎる気がする.半分以上空気じゃん.ご飯が恋しい.
閑話休題.
Function で定義した関数は Qed で終わらず Defined で終わっておかないと Eval compute とかで試しに動かした時にとても残念なコトになると学習した.ここらはもう少し中のことを理解しないとダメなんだろうなぁ…… つか,Function って何やってるのよ?
- Comments: 0
- TrackBack (Close): -
あー、便利なものがあるではないか、ないではないか
- 2012-10-15 (Mon)
- 一般
assert → apply とかいうコンボを使いまくっていたら,specialize 使えよアホというコメントを貰った.確かにアホだ.
閑話休題.
Leibniz equality ではなく equivalence relation を使って物事を定式化しようとすると証明が色々ととても面倒.rewrite とかが動かないのが非常にストレスなわけで…… Equivalence relation 用の rewrite とかあったりするのか? なければ自前で用意すりゃいいんだろうけどああ面倒.
- Comments: 0
- TrackBack (Close): -
Weekend パス
- 2012-10-14 (Sun)
- 一般
土日乗り放題で 3.6ユーロ.通常1回1.4ユーロなので3回乗ったら元が取れる.30回の回数券だと35.2ユーロなので4回乗らないと元が取れんけど.
お出かけ+買い物+大学に行くというのを週末にするにはこっちのほうがお得.
閑話休題.
日曜日とそれ以外の日との時刻表の差が激しすぎる…… 日曜だと始発が2時間半以上遅くなるとか信じられん.
- Comments: 0
- TrackBack (Close): -
ベルサイユ宮殿(雨)へ行く
早朝3時から天気予報とにらめっこをし,雨のベルサイユ宮殿ってのも面白いかねとか結論づけて朝イチの電車でパリへ出発.オステルリッツ駅に6時ちょっと過ぎに到着.そこからRERのC線(VICK)に乗り換えて終着駅まで40分くらい.とりあえず,終着駅の名前が Versailles Rive-Gauche だと思っていたところに券売機の表示が Versailles Château で戸惑った.切符には Versailles RG って書いてあるんだけど.
んで,駅から歩いて5分くらいでルイ14世がお出迎え.ぶっちゃけ7時過ぎなのでまだ真っ暗.
メインゲートが閉じてて庭園へすら入れないので宮殿の周りを歩きまわる.宮殿南の池から宮殿を望む.7時半を過ぎてそろそろ明るくなってきた.
8時過ぎに戻ってきたらメインゲートが開いていた.とりあえず中へ.
今日は土曜日なので噴水ショーがありますよと.お陰で庭園に入るだけで8.5ユーロとか取られる.
8時半を過ぎた辺りでチケット売り場に列が出来たので並ぶ.晴れてれば日がさしてただろうけど,あいにくと天気予報のとおりにご機嫌ななめな空模様.
色々と中略.9時直前に結構な雨が振ってきたり,チケットを事前に用意していた人たちの列がものすごかったり,チケット購入列の長い列の先には空いている自動券売機が鎮座していたり.色々と絶望した.
- Comments: 0
- TrackBack (Close): -
PermutationA め……
- 2012-10-12 (Fri)
- 一般
なんで欲しい性質が証明されていないんだ…… Sorting にある Permutation の方はいろいろ揃ってるのに.くそぅ.
- Comments: 0
- TrackBack (Close): -