emacs24 で ProofGeneral 使うときのメモ
ずっとtrunkのemacsを自分でビルドして使ってるわけなんですが、ProofGeneralを使おうとして、byte-compileしようとするとこけます。
で、エラーメッセージを読むと interactive-p を使うな、 called-interactively-p を使えとあるので
(interactive-p)
を探して
(called-interactively-p 'interactive)
に書きかえると動きます。
development releaseだったら何もしなくとも動くのかもしれない・・・
今日学んだこと
なんか実験で並列プログラミングとかいうのをやっていて、並列化する前に逐次実行のコードを速くしようとしてるんですけど、そういうことほとんどしたことないし、よくわからないですね。
とりあえず、ループの順番入れ替えるとかなんとかしてキャッシュミス減らして、むふーっていってます。
Cは投げ捨ててnasmとかで書くとよいのではないかなぁ、と思っとるんですがやる気次第。
double s = 0; for(i=0; i<k; ++i) s += a[i]; b[j] -= s;
と
double s = b[j]; for(i=0; i<k; ++i) s -= a[i]; b[j] = s;
だと、上のほうが速い。(ほんのちょっと)
なぜかはしりません。きっとそうではない環境とかもあるでしょう。
double s = 0; double *p = a; for(i=0; i<k; ++i) s += *p++; b[j] -= s;
のほうがもうちょっと速い。
あとループアンローリング???とかいうのすごいですね.....
明日、SIMDとか試す
SRM520 Div1 500
算数力が足りなくて、組合せが求められない。
以下のコードは、間違っています
#include <cmath> #include <ctime> #include <iostream> #include <string> #include <vector> #include <cstdlib> #include <cstdio> #include <map> #include <queue> #include <algorithm> #include <cstring> using namespace std; typedef long long ll; ll dp[50][200001]; ll dp2[200001]; const ll mod = 1000000007; class SRMIntermissionPhase { public: int countWays( vector <int> points, vector <string> description ) { memset(dp, 0, sizeof(dp)); memset(dp2, 0, sizeof(dp2)); ll minp[50], maxp[50],cnty[50]; for(int i=0; i<50; ++i) minp[i] = maxp[i] = cnty[i] = 0; const int n = description.size(); for(int i=0; i<n; ++i) { for(int j=0; j<3; ++j) if(description[i][j]=='Y') { maxp[i] += points[j]; minp[i] += 1; cnty[i]++; } } for(int j=0; j<n; ++j) for(int i=minp[j]; i<=maxp[j]; ++i) { if(cnty[j] == 0) dp[j][0] = 1; if(cnty[j] == 1) dp[j][i] = 1; else if(cnty[j] == 2) { // 誰かここと if(description[j][0] == 'Y') { dp[j][i] = min((ll)i-1,(ll)points[0]); }else{ dp[j][i] = min((ll)i-1,(ll)points[1]); } }else if(cnty[j] == 3) { // ここを書いて!!!!!!!!!!! ll tt = min((ll)points[0],(ll)i-2); ll ts = max(i-points[1]-points[2],0); dp[j][i] = tt*(i-1); dp[j][i] -= tt*(tt+1)/2; dp[j][i] -= ts*(i-1); dp[j][i] += ts*(ts+1)/2; dp[j][i] %= mod; } } ll tmp = 0; for(int j=maxp[0]; j>=minp[0]; --j) { tmp += dp[0][j]; tmp %= mod; dp[0][j] = tmp; } for(int i=1; i<n; ++i) { for(int j=minp[i]; j<=maxp[i]; ++j) { dp[i][j] = dp[i-1][j+1] * dp[i][j]; dp[i][j] %= mod; } tmp = 0; for(int j=maxp[i]; j>=minp[i]; --j) { tmp += dp[i][j]; tmp %= mod; dp[i][j] = tmp; } } ll ans = dp[n-1][minp[n-1]]; return ans; } };
Anarchy Proof - PHP
テスト前なので、逃避にCoPL(http://www.sato.kuis.kyoto-u.ac.jp/~igarashi/CoPL/index.cgi)やら、Anarchy Proofやらばっかりやってます。
今回の問題は、いわゆる鳩ノ巣原理ですね。
自然数のリストxsがあって、length xs < sum xs ならxsのなかに1より大きい要素があるというのを示せばよい問題です。
xsについて帰納法+ xsがnilでないなら先頭の要素が0か1かそれ以上で場合わけしました。
例によって、autoとか使ってないので、長い……
あと、手元(Coq8.3だったかな?)にはlt_z_Snに相当する命題がlt_0_Snっていう名前であるんですけど、サブミットするとそんな命題ねーよって言われたので、自分で証明してます、なんで……
Require Import Definitions. Require Import Lists.List. Require Import Arith. Lemma lt_z_Sn : forall n : nat, 0 < S n. Proof. induction n. apply lt_n_Sn. assert (S n < S (S n)). apply lt_n_Sn. apply lt_trans with (m := S n); assumption. Qed. Theorem Pigeon_Hole_Principle : forall (xs : list nat), length xs < sum xs -> (exists x, 1<x /\ In x xs). Proof. intros. induction xs. contradict H. simpl; exact (lt_irrefl 0). destruct a. assert (S (length xs) < sum xs). simpl in H; assumption. assert (exists x : nat , 1 < x /\ In x xs). apply IHxs. assert (length xs < S (length xs)). apply lt_n_Sn. apply lt_trans with (m := S (length xs)); assumption. simpl. destruct H1. exists x. split. exact (proj1 H1). right; exact (proj2 H1). destruct a. simpl in H. assert (length xs < sum xs). apply lt_S_n; assumption. assert (exists x : nat , 1 < x /\ In x xs). apply IHxs; assumption. destruct H1. simpl. exists x. split. exact (proj1 H1). right; exact (proj2 H1). exists (S (S a)). split. apply lt_n_S; apply lt_z_Sn. simpl. left. reflexivity. Qed.
Anarchy Proof - Sum of Natural Numbers
最近全然Coqを触ってなかったので、久々にやってみました。
示さないといけないのは、0からnまでの和の2倍が n * (n + 1)に等しいっていうやつで、まぁ何も考えずにnについて帰納法で示せばよいです。ただ、autoとかringとかomegaとかを使うとなぜか負けた気分になるので、使わずに地道に頑張りました。
golfしないといけないのに、全くgolfしてない・・・
後半の方は、a + b + c + d = c + b + a + dみたいな等式を書き換えしてるだけなので、もうちょっと縮むかもしれないですね。
Require Import Definitions. Require Import Arith. Theorem Sum_of_nat: forall (n: nat), 2 * sum n = n * (n + 1). Proof. induction n. simpl; reflexivity. assert (sum (S n) = (S n) + sum n). induction n; simpl; reflexivity. assert (S n = 1 + n). induction n; simpl; reflexivity. rewrite H. rewrite H0. rewrite mult_plus_distr_r. rewrite mult_plus_distr_l. rewrite IHn. rewrite mult_plus_distr_l. rewrite mult_1_l. rewrite mult_1_r. assert (1 + n + 1 = n + 2). rewrite plus_assoc_reverse; rewrite plus_permute. simpl; reflexivity. rewrite H1; rewrite mult_plus_distr_l. rewrite mult_plus_distr_l. rewrite mult_comm with (m:=2). do 2 rewrite plus_comm with (m:=(2*n)). rewrite plus_comm with (n:=(n*n)). rewrite mult_1_r. do 2 rewrite plus_assoc_reverse. do 2 rewrite plus_permute with (m:=2*n). rewrite plus_permute with (n:=2). reflexivity. Qed.
ICPC国内予選
この前の金曜日に、国内予選がありました。
某所で参加記書くと言ったので、模擬国内のときみたいに書いてみたいと思います。
そういえば、今年はJavaチャレンジなかったですね。
ベントされてしまった(追記:アドベント空間てきなつもりだったのですけど、今のご時世だと原発的な意味になりそうですね・・・)
3日前ぐらい
監督の人からきたメールに、会場となる計算機室は飲食禁止です！と明記されてて、今年は飲み物飲んじゃいけないんじゃないかと戦々恐々とする。(実際はそんなことなかった！！
3時間くらい前
金曜日は実験で朝から計算機室にいるので、AOJで簡単な問題解いたり、ライブラリちゃんと印刷したかどうか確認したりする。
あと戦略?の確認とか。模擬のときと同じようにやりましょうとか間違いなく早解き合戦になるなぁとかそんな話。
30分くらい前
出る人たちが続々と計算機室に来だして、これからお祭りがはじまる！！！って感じでわくわくしはじめる。
とりあえず、レッドブル飲んでドーピングしてた。
開始~~~
A,Bを読んでやる係だったので、Aを読んで書き始める。
123456*2を計算するのがめんどくさかったので、適当に250000ぐらい配列を確保したりした。
A accepted (3:48)
Bをみると、stack使うだけなので、適当に書く。
自分は、stlのstack使わずにvectorのpop_backとか使って書きたい派なのだけど、横でなんでそんな意味ないことするの?とか言われてた。
たしかに意味ないなぁと思うなど。
B accepted (8:57)
Cを聞くとただの全探索ゲーだと言うので、はいそうですか、と書き始める。
最初、左上とつながってない点も答えに含んでしまって、sampleが合わなかったのだけれど、すぐに気づいてなおしたらあったので提出。
C accepted (28:14)
Dも色数の制限と同じ色の枚数の制限から、そんなに状態数多く無いだろうし全探索ゲーなんだろうと見当はついてたけど、円と円の交差判定を書きたくなかったので、チームメイトに任せる。
交差判定ができあがった後、ペアプロして適当に書き上げた。
なにかでちょっとだけはまったようなおぼろげな記憶があるのだけれど、忘れてしまった・・・
D accepted (58:05)
ここで、とりあえず残りの問題を全部読んだような記憶がある。
Gは問題の意味するところがよくわかんなくて、Fは幾何だけど頑張って場合分けすれば解けないこともない気合ゲーで、Eはなんだこれ?とかいうようなことを思ったような気がする。
しばらくFの場合分けをぼんやり考えてたりしたのだけど、東大のチームとか先輩のチームがぽんぽん5問目を解いてたのできっとEは簡単に違いない!!!!と思い、Eをまじめに考え始める。
で、ちょっと考えると長方形を状態にするメモ化再帰だということが分かって、これさえ分かってしまえば残りはすごく単純なのでがりがり書き始める。
累積和がうんぬんとか添字のずれががががが、とかあったりして結構てこずったような覚えがある。
E accepted (1:59:34)
この時点で6位だったの(そうだっだっけ? 忘れてしまった・・・) で、まぁアジア予選にはいけるだろうなーとか考えてた。
Gは何度か読んでもよく意味が分からないし、しょうがないのでFで必要そうな幾何のライブラリをがりがり打ち込んでもらったりする。
しかし、考えれば考えるほど場合分けの数が増えていって、こんなん書けるか−と思ってやる気がなくなっていった。
最後30分ぐらいは、チョコレートもさもさ食べながらボーッっとしてました。
終わった瞬間、某先輩がRewrite買いに走って出ていったのが、一番印象に残った記憶。
結果
全体で6位、学内で2位だったらしいです。
A,B,CでたぶんFirst Acceptらしいですね、よきかなよきかな。
でもそれを考えると、D,Eが遅すぎる感があります。タイピング力だけではだめだってこと。(実際全然タイピング速くないですが・・・
たぶん、夏合宿に行けるので楽しみ。ぱない人たちにぼこぼこにされてこようと思います。
