coq-hurry P10 練習問題

10ページの練習問題2問をやってみる
1問目　Exercise on sorting
 Define a function that takes a list as input and returns true when it has less than 2 elements or when the first element is smaller than or equal to the second one. Then define a function that takes a list as input and returns true exactly when this list is sorted.
 入力としてリストをとる関数を定義し、戻り値はリストの要素が２未満か最初の要素が２番目の要素以下のときTrueとなる関数を定義せよ。それからリストが完全にソート済みならTrueとなる関数を定義せよ。

最初、なかなかうまくいかない。
Fixpoint check_fs2 l := match l with nil => true | a::nil => true | a1::a2::tl => if leb a1 a2 then check_fs2 (a2::tl) else false end.
このように一つの関数でできそうな気がしたが、なぜかエラーとなる。まだ、coqの使い方が
よくわかっていない。

こういうときは、少し時間を置くことにしている。しばらくして、再挑戦したらできた。
問題で説明しているように、２つの関数でやってみた。最初の関数は、２つの要素の比較だけ行い、再帰はさせないようにした。もうひとつの関数で再帰を使ったらうまくいった。
もう少しスマートな方法がありそうだが、、、、。

Fixpoint check_fs l := match l with nil => true | a::nil => true | a1::a2::tl => if leb a1 a2 then true else false end.
Fixpoint check_sort l := match l with nil => true | a::tl => if check_fs (a::tl) then check_sort tl else false end.
これで、なんとかうまくいった。

２問目　Exercise on counting
 Knowing that the Coq system provides a function beq_nat to compare two natural numbers,
define a function count_list that takes a natural number and a list and returns the nubmer of times the natural number occurs in the list.

これについては
Fixpoint count_list n l s:= match l with nil => s | a::tl => if beq_nat n a then count_list n tl s+1 else count_list n tl s end.
としてみた。ただ、３つめの引数はムダなので、できればなくしたい。
その方法がよくわからない。

ネットで検索するとすでに、解答されている方がいた。
Fixpoint count_list2 n l:= match l with nil => 0 | a::tl => if beq_nat n a then 1+count_list2 n tl else count_list2 n tl  end.
これでいいようだ。
　nil=>0のところを、nil=>sにしようとこだわりすぎたようだ。自身の戻り値に１をたすならば、戻り値に１が累積されていくということに気づかなかった。自分が考えた引数に１をたしていくやり方だと、最後の関数で表示せざるをえないので、nil=>sとなり、スマートな方法とはいえない。

今年は、豊作

　畑を借りているが、今年は思い切ってトマト１５株植えた。雨が少ないため、豊作。食べきれないほどとれる。買えば１個１００円近くするので、もとがとれたか。
　カラスの害が心配で、ネットをかぶせたのもよかったかも。。
　手入れは、最低限のわき芽とり、サンボルドーによる消毒ぐらいか。

　ナスは７株。ゴーヤ、つるなしいんげんなども１畝ずつ。きゅうりは、１株で十分だ。
　防草シートを使っているが、除草は　はっきりいって、かなり手抜きしている。

　

sambaでワード、エクセルが読み取り専用になる不具合

　sambaをちょっと特殊な使い方をしている。それぞれの共有フォルダにユーザーを割り当てて、パスワードがないとアクセスできないようにしているが、それと同時に、hosts allowを使って、特定のIPアドレスのクライアントからもアクセスできるようにしている。（同一フォルダを別名の共有フォルダとして）
　結果的に、これがよくなかったらしく、ときどき、別の人が作成したファイルを開けない現象が発生した。なぜか、最初は原因がつかめなかったけれど、要するに、さまざまなユーザーのファイルができるため、アクセス権限が一致しないことが原因のようだった。
force create mode
force directory mode
でなんとか、その場をしのいだ。
　でも、それでもまだ似たような現象が発生した。ls -llで確認すると、どうやら+の記号がついてる(aclが設定されてしまっている）とそうなるということが判明。。そうならないためには、
nt acl support = no
を付け加える必要があったようだ。これで、しばらく様子を見てみよう。　それから、
setfacl -R -b /ディレクトリ名
として、aclを削除しておくことも必要なようだ。

＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊
上記の方法で解決したと思ったものの、まだ、読み取り専用になる現象が発生する。
いろいろ調べると、可能性のあることとして、

dos filetimes = Yes
dos filetime resolution = Yes
の設定を追加したほうがいいらしいこと。

エクスプローラの[整理] > [レイアウト] > [詳細ウィンドウ]と[プレビューウィンドウ]のチェックを外したほうがいいらしいこと

＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊
これでも、まだ　だめ？なようなので、さらに調べると
oplocks = No
blocking locks = No
の記述をしたほうがいいという情報もあったので、試してみた。

今のところ、読み取り専用になる現象は発生してないようだ。

mdbファイルの破損

　マイクロソフトaccessのmdbファイルが壊れた。よくあることで、これまでは、最適化で、ほとんど修正できていましたが、今回は手こずりました。
　テーブル（auto　incrementのインデックス有）のところどころの行がなぜか、表示されたりされなかったりしました。そのため、mdbファイルを操作しているクライアントソフトも、一部動作しません。欠番の行に挿入はできない仕様のようです。
　結局、いったんデータをエクセルにエクスポートしてから、全レコードを削除し、エクセルデータから再度、インポートしたところ、うまく復活できました。
　なぜこういうことになったか、原因はわかりませんが、やはり、データベースはMysqlとか、実績のあるものに、変えていく必要があるのかもしれません。

javaで、renameToを使うとき気を付けること

renameToを使ってServletを作っていた時のことです。
windowsでは、うまくファイルの移動ができていたのに、
Linuxで動かしたら、うまくいかないという現象に悩まされました。
権限の問題？だろうかといろいろ試行錯誤しても、結局うまくいかず。
例によってネットの情報を探していたら解決策がありました。

http://kaede.jp/2014/04/05170305.html
この情報で救われました。
ｍｏｖｅＦｉｌｅだと、Ｌｉｎｕｘでもだいじょうぶであることが判明。
なんとか解決しました。
Javaもなかなか難しいものです。

wdCalendarを試してみた

GoogleカレンダーのクローンタイプのソフトでwdCalendarというものがあったので
試してみた。認証も不要で、施設、備品貸し出し簿などに使うと便利そうである。

こちらのリンクがとても参考になりました。
http://web.chaperone.jp/w/index.php?jQuery%2FwdCalendar
ただ、若干、手直しが必要でした。

apache2のerror.logを参考に、
dbconfig.phpの１１行目で　：を;に修正
また、mysqlで使うために　mysqｌの設定に書き換えました。（コメントを参照すればOk）
そして、これでOkかと思いきや、、削除ができません。
なかなか、原因がつかめずにいましたが、、
どうやら、function removeCalendar　という関数の中のDeleteのためのqueryの記述が
なぜか違っていたようです。

function removeCalendar($id){
  $ret = array();
  try{
    $db = new DBConnection();
    $dbh= $db->getConnection();
    $sql = "delete from ".$db->getTbl()." where `id`=" . $id;
　　　　　　　if(mysql_query($sql)==false){→これを→   if($dbh->query($sql)==false){
　　　　と直したらうまくいきました。

cokkie 全角を扱うには

Javaで全角のクッキーを扱うには少し手間がかかる。

servletでも、JSPでも
 request.setCharacterEncoding("UTF-8");を入れないとだめだようだ。

あとは
Cookie cookie = new Cookie("filtermoji",URLEncoder.encode(filtermoji, "UTF-8"));
といった感じだ。


デコードは
 sfiltermoji = URLDecoder.decode(filtermoji.getValue(),"UTF-8");
となる