FC2ブログ

30分でできる日記

ピタゴラス数

のもつ有名な性質のひとつである

a^2 + b^2 = c^2 ならば、aかbは3の倍数である

という命題をcoqで証明しようとしてみたのだが、結局証明仕切れなかった。
StandardLibraryを見る限りではcoqには剰余に関する命題はライブラリ化されていないようだったので、剰余に関する単純な補題をウンウン唸って証明したりているうちに夜になってしまったようだ。

"<="とかに関してはArith.Plus内に


Lemma plus_le_reg_l : forall n m p, p + n <= p + m -> n <= m.
Lemma plus_le_compat_l : forall n m p, n <= m -> p + n <= p + m.


と、両方用意されているのに、"="に関しては


Lemma plus_reg_l : forall n m p, p + n = p + m -> n = m.


がArith.Plusライブラリに有るのに

forall n m p, n = m -> p + n = p + m.


が見つからなくてなんでだろうと思っていたが、実際に証明してみたら


Lemma hogehoge :
forall n m p : nat,
n = m -> p + n = p + m.
Proof.
auto with arith.
Save.


と、autoで一発だったので何か納得した。

スポンサーサイト



  1. 2006/05/31(水) 23:17:57|
  2. プログラミング|
  3. トラックバック:0|
  4. コメント:1

XML

の授業のノートをコピーしたいとかいうことで地下にノートごと置いて帰ってしまったが、家に帰ってから課題の内容が分からないことに気付いてしょんぼり。というか、ここにしっかりとしたレジュメがあるんだから、私の誤字だらけのノートなんかいらなかったのではなかろうか。

まあ、とりあえずTD前処理つきBUアルゴリズムは実装できたように見えるんですがOCamlのオブジェクト指向がえらい使いづらいことを知りました。大して木のパターンマッチとかもしなかったし、普通にJavaかなんかで書けばよかったと後悔。

  1. 2006/05/30(火) 21:07:59|
  2. 大学|
  3. トラックバック:0|
  4. コメント:0

coq

を弄っていたわけですが、


Coq < Variables n : nat.


とやると


Warning: Keywords Variables/Hypotheses/Parameters expect more than one assumption
n is assumed


と警告してくるのに、


Coq < Variable n m : nat.


とやっても


n is assumed
m is assumed


と、何も言ってこないのには何か深い含蓄があるのでしょうか。。
あと、


Hypothesis h : p -> q -> r.
Hypothesis n : nat.


としても


Variable h : p -> q -> r.
Variable n : nat.


としても、効果が同じような気がするのは、やっぱり私の目が節穴だからなんですかね?よく分かりません。

  1. 2006/05/28(日) 21:11:09|
  2. 大学|
  3. トラックバック:0|
  4. コメント:0

演習さん

二期はとりあえず定理証明器なるものを弄ってみることに決定。

…で、昨日辺りからとりあえずCoqのTutorialを呼んでいるわけですが、なんだかよく分かんないコマンドが氾濫していて、一ヶ月ではとても使いこなせそうにない感じがしてきた。

それにしても、Googleで"Coq"を日本語ページに絞って検索するとコエンザイムQ10(CoQ10)のページばっかりヒットして困る。

  1. 2006/05/27(土) 19:52:46|
  2. 大学|
  3. トラックバック:0|
  4. コメント:0

うーむ

何となくPKUをやっていたらこんな時間になってしまった。次期演習IIIで何するか何も考えてないのに、こんな事してて良かったのだろうか…

しかし解く問題の先々でazouno氏やnkjm氏を見かけるのは、なんだかアレな感じだった。

  1. 2006/05/25(木) 23:18:36|
  2. 未分類|
  3. トラックバック:0|
  4. コメント:2

ふう

一昨日辺りから始まった発作がようやくおさまった模様(全クリはしてないが)。論文読みとか問題解きとかいろいろやりたいことはあるが、とりあえず疲れたので休みたい。。

  1. 2006/05/24(水) 18:21:08|
  2. 未分類|
  3. トラックバック:0|
  4. コメント:0

今日

の午前授業が休講だと気付いてしまった瞬間コントーラーを握り締めてしまった自分が悲しい。早く全クリしないと…

  1. 2006/05/23(火) 01:51:40|
  2. 未分類|
  3. トラックバック:0|
  4. コメント:0

あうあう

飯を炊いている合間にと、ちょっとゲームをやっていたわけですが、一段落してから炊飯器のところにいったら表示が「保温 5時間」になっていて困った。


  1. 2006/05/23(火) 00:56:06|
  2. 未分類|
  3. トラックバック:0|
  4. コメント:0

某課題...その後

いろいろあったが、とりあえず終了。
(空間方向の)境界条件が断熱的な時に正弦波だけでフーリエ級数を記述できないような初期条件を与えたときにどうやって解析解を求めりゃいいのかとか、そもそも一般的な境界条件に対してどうやって解析解を求めりゃいいのか、とかが分からないままだが、どこ見ても示し合わせたかのように正弦波だけで展開できるような初期条件&断熱条件の場合の例しかに取り上げていないように見えたような気がしないこともないので放置することに決定。

結局ZK関連の勉強は何もできないで週末は終了っぽい。次期にまわる研究室で何やるかもまだ決めていない。どうしたもんか。

  1. 2006/05/21(日) 21:11:07|
  2. 大学|
  3. トラックバック:0|
  4. コメント:0

某課題

調子に乗って拡散方程式をやり始めたら、見事に嵌って金土が潰れてしまった。私みたいな馬鹿はおとなしく簡単にPoisson方程式でも解いてりゃ良かった。まだ終わりそうもないので日曜も嵌る予定。

というわけなので、寝ぼけてたらすいません。。 > azouno氏

  1. 2006/05/20(土) 23:51:17|
  2. 大学|
  3. トラックバック:0|
  4. コメント:0

花って

今日母が実家からこっちに遊びに来るとかいうことなので、母の日用に花屋に花を買いにいってみたわけですが、花って普通に高いんですね…知らなかった。朝顔とかだと100円で売ってるんですが、普段見かけないようなものとかだと数束で数千円で売られていて少しびびった。

実家の法事とかで花の類がいるときは庭に咲いている花を適当に摘んで持っていったりして、花屋で買うことなんて一度もなかったわけですが、それで知らず知らずのうちにかなりの倹約をしていたことになるらしい。

  1. 2006/05/19(金) 22:50:43|
  2. 未分類|
  3. トラックバック:0|
  4. コメント:1

1981

timeが10000MS超えているのにacceptするのはどうかと思う。

  1. 2006/05/18(木) 00:16:26|
  2. プログラミング|
  3. トラックバック:0|
  4. コメント:0

演習III終了

とりあえず一期目は終了(とはいっても最終発表が三期の後にあるようだが)。何というか、いろいろとためになる経験になった。一期ではZKIPをやらせてもらったわけだが、どうも私はこういうガチガチの理論を調べていると細かくて複雑な理論に目が行きがちになってしまう。しかし研究としてこういったトピックを扱おうとするならば、その複雑な理論が結局どんな分野に応用できるのか、どんな実践を見据えているのか、とかいう俯瞰的な視点を持つことを同時に注意して、そこからモチベーションを獲得していかないと賛同も得られないし、自分自身もやってられなくなるということを強く感じた。

考えてみると、ZKがどういうものかは、まあ分かったのだが、具体的にどんな面白いことができそうかと考えるとあんまりはっきりと浮かんでこない。ゲームやP*Uもしたいが、最近のZK研究の動向とか、具体的にどんな分野への応用が実現しているのかとかも機を見計らって調べてみないといけない、というか調べてみたい。

  1. 2006/05/17(水) 22:26:11|
  2. 大学|
  3. トラックバック:0|
  4. コメント:0

分からないなりにいろいろやってはみたがWindows上だと接続できないまま。Linuxからだと接続可能だったので、結局NTFS用のドライバを落としてきてLinuxからWindows領域をマウントして、Windows上で書いていたプログラムコードをLinuxに持ってきてsubmitすることに。

で、めでたくacceptされた模様。carpetの敷き方に制約をつけたら一気に枝刈りができたようで、今までヒープ領域を食い尽くしていたのが、BFSの各段階で確保しているノードがほとんど1桁にまで落ちたのは壮観だった。

  1. 2006/05/16(火) 23:08:04|
  2. プログラミング|
  3. トラックバック:0|
  4. コメント:0

あう

昨日は眠かったので日記を書かなかったら、なんだか某氏にえらい怒られた。しかし大して日記のネタなんか無いわけで、無理して変な記事を書くとその某氏に「コメントしづらいです」とか書かれるわけで。どうしたもんか。

それはそうと、早くcarpetの問題をsubmitしたいのになぜかノートPCからネットワークにアクセスできないのはなんかの嫌がらせとしか思えません。

  1. 2006/05/16(火) 21:48:27|
  2. 未分類|
  3. トラックバック:0|
  4. コメント:0

演習III

の論文を読んでいた際、参考論文としてNIZKの論文を落とそうと思ったら見事にThe ACM Digital Libraryがひっかかってしまった。上の方から聞いたとおり、学内ネットワークでCS図書室の電子雑誌ページから行けば簡単に見れる模様。いい加減ここにある論文の読み方も覚えなくては…

  1. 2006/05/14(日) 19:57:12|
  2. 大学|
  3. トラックバック:0|
  4. コメント:1

TOEFL終了

朝の9時から茅場町まで行って来ました。
結果は177~233だそうで、予想通り微妙。3~4時間もちかちかするディスプレイ見続けるなんて、ゲーム以外では無理です。目が痛い。

  1. 2006/05/13(土) 13:33:39|
  2. 大学|
  3. トラックバック:0|
  4. コメント:2

TOEFL

無理。日本人は日本語だけ使えりゃいいと思います。

  1. 2006/05/12(金) 19:42:11|
  2. 大学|
  3. トラックバック:0|
  4. コメント:4

test

何だか知らないうちに日記ができていた模様。

  1. 2006/05/12(金) 15:17:36|
  2. 未分類|
  3. トラックバック:2|
  4. コメント:13

| ホーム |