2020-01-09

東京のレンタルサイクルが好きだ

知見

東京の好きなところがある．短時間レンタルサイクルが充実していることだ．

東京の都心は，思っているより遥かに狭い．普段は鉄道や地下鉄でワープのように移動する．しかし，自転車で移動すると意外と狭い事がわかって楽しい．

東京にはものすごい量の自転車レンタルポートがある．

f:id:wass80:20200109032827p:plain

ポートマップ・駐輪 | 東京・港区自転車シェアリング（シェアサイクル）

3コンビニに1つぐらいの感覚である．全てのポート自転車を借りられるし，どこのポートで乗り捨てても良い．とても便利だ．

東京の道路は自転車に優しい．京都と違って，車道幅か歩道幅のどちらかは十分にある．しかし，勾配のある坂を上り下りさせられるのが欠点だ．

だが，このレンタルポートで借りられる自転車は電動自転車である．それなりの厳しい坂でも，すいすい登ることが出来る．

借りられる自転車の実装は悪くない．ハードは優秀．自転車番号をWebから入力．案内される4桁のPINを入力して解錠．返却にはポートでロックするだけ．おそらくGPSで位置を取得しているのだろう，ポート内であれば，正常に返却される．

Web側のUIは「駐輪場検索」「自転車番号」の2つある．駐輪場検索は検索性が悪く使い物にならない．位置特定して最寄りを出してほしい． f:id:wass80:20200109034126p:plain

150円/30分という値段も，地下鉄並みで良いと思う．これからも活用していきたい．

ところで，京都でも似たようなサービスが始まった．

京都エリア | PiPPA ピッパ

こちらも一度使ってみた．

東京に比べてポート数が少ないことが利便性を下げている．これは仕方ない．アプリも使い勝手が悪く，ハードの認識もうまく行かない個体が多かった． Bluetoothで認証させるのがうまく行かないのだろうか．これも仕方ないとする．

肝心の自転車があまりにダメすぎだった．電気自転車でないことは良い．ハードの認証を駆動させるためにバッテリーが乗っている．ひたすらに重い漕ぎ心地を考えると，そのバッテリーを常時充電しているようである．あまりにひどい．ハードがだめだと，他の改善点が治ってもどうしようもないので悲しんでいる．

京都観光もレンタルサイクルがおすすめなのですが，このサービスはおすすめしません．電動自転車をレンタルサイクルショップで借りましょう．

2019-09-07

定理証明コンテストに参加した [WIP]

競プロ

TODO多めのまま公開します。別に書いてた下書きが消えたので。

定理証明のコンテストシステムを作って、今日の夕方に第1回のコンテストを開催していた。https://t.co/8vi0dWszRW
— あしぃ (@asi1024) 2019年8月18日

これです。

定理証明コンテストとは,

定理証明支援系を用いて与えられた定理に対して証明を与えるコンテストです。

現在コンテストサイトに実装されている支援系はCoqです。

Coqで解く問題の見た目はこんなかんじです。

Definition task := forall n m, n * S m = n + n * m.

Theorem solution: task.
Proof.
  unfold task.
  (* FILL IN HERE *)
Qed.

これはn×(m+1)とn+(n×m)が任意の自然数n,mについて等しいことを示せというものです。

FILL IN HEREの部分にCoqの言葉で証明を与えます。

この問題を通そう

環境準備

Coqのインストールをしたのち，Coqをインタラクティブに使うツールを用意します。

ツールにはEmacs+ProofGeneralが最も標準的です。 WindowsではCoqIDEを使う方法もあります。

vscodeとその拡張vscoqを使う方法も存在したのですが, 現在バグだらけで使い物になりません。昔のvscodeのバージョンを用いると使えるらしいですが, その方法をおすすめすることはできません。

Emacs+Spacemacs+ProofGeneral導入記事は後で書くことにします。TODO

~~ここでは他の選択肢として，macでvscode+vscoqを用いる方法を説明します。~~

初めに brew install coq でcoqを入れます。そしてここが肝心ですが，vscodeの拡張であるvscoqはすでに更新がされておらず，最新のvscodeでは正常に動作しません。なので2年前ぐらいのvscodeをダウンロードして利用しましょう。

Visual Studio Code January 2018

vscodeでvscoq拡張をインストールします。

~~そうして*.vファイルを開くと，次の証明画面が出ます。~~

TODO

定義

というわけでこの命題を示しましょう。

forall n m, n * S m = n + n * m.

定理の証明にはまず定義を観察することが大事です。

ドキュメントに定義があります。

Standard Library | The Coq Proof Assistant

https://coq.inria.fr/library/Coq.Init.Datatypes.html#lab1084

また, Coq上でも定義を見ることができます。 TODO

初めに，自然数の定義が次のように帰納的定義がされています

Inductive nat : Set :=
  | O : nat
  | S : nat -> nat.

natという集合は，次の2つのコンストラクタから生み出されるものである。

コンストラクタ"O"は無引数でnatである。
コンストラクタ"S"はnatを引数に取ることでnatである。

と読みます。

例えばOやS (S O)なんかがnatで有ることがわかります。

そして, これが我々の良く知る自然数であるところの0や2に対応しています。

実際に，0や2もcoqで書くことができ，これはcoqではそれぞれOとS (S O)のエイリアスです。

また，+ の定義はaddという関数の糖衣構文で

Fixpoint add n m :=
  match n with
  | 0 => m
  | S p => S (p + m)
  end

where "n + m" := (add n m) : nat_scope.

掛け算の定義はmulという関数の糖衣構文で

Fixpoint mul n m :=
  match n with
  | 0 => 0
  | S p => m + p * m
  end

where "n * m" := (mul n m) : nat_scope.

と再帰的に定義されています。

matchは関数型言語ではおなじみのパターンマッチです。

その項のコストラクタによって場合分けを行い, その先の項を返します。

match 項 with
  | コンストラクタ1 引数1 => 項1
  | コンストラクタ2 引数2 => 項2
end

計算の例を示すと，

2+1を計算する例は

S (S O) + S O
= add (S (S O)) (S O)
= match (S (S O)) with
    | 0 => (S O)
    | S p => S (p + (S O))
  end
= S(S O + S O)
...
= S(S(O + S O))
...
= S(S(S(O))

ここで，S (S (S O)) + S Oは(S (S (S O))) + (S O)と読むことに注意してください。演算子のほうが関数適用っぽいものより優先度が弱いです。

2*3を計算する例は,

S (S O) * S (S (S O))
= mult (S (S O)) (S (S O))
= S (S (S O)) + S O * S (S (S O))
= S (S (S O)) + S (S (S O)) + O * S (S (S O))
= S (S (S O)) + S (S (S O)) + O
...
= S (S (S (S (S (S O)))))

という感じです。

Coqは便利で，具体的な例の計算ならやってくれます。

Theorem ex_2_plus_1_eq_3: S (S O) + S O = S (S (S O)).
Proof.
  simpl.  (* S (S O) + S O の部分を計算してくれる *)
  reflexivity. (* 両辺が同じ項の=となっているゴールを達成する *)
Qed.

これで2 + 1が3であることを形式的に示すことができました!

証明tactic

ex_2_plus_1_eq_3の例では, 実際に証明を行っています。 coqでは定理の証明を次の形で書きます。

Threom 名前: 命題.
Proof.
  証明tacticの列
Qed.

Proof.のあとに続くのは証明のtacticというものです。これは, 証明の状態を変化させます。

証明の状態とは, 証明するべきものである｢ゴール｣の列です。ゴールとは次の形で表されます。

仮定の列 |- 結論

｢仮定の列から結論を導く｣ことを要求するものがゴールです。

始めに Theorem で示したい命題を与えると,

|- 命題

このように, 仮定の列が空で, 命題が結論となったゴールが1つだけ状態から始まります。このゴールに対してtacticを適用することで, ゴールを変えたり, 達成したり, 増やしたりします。そして, これらゴールをすべて達成すると, 証明を完遂したことになります。

Coqのインタラクティブツールで普通右側に表示されている状態は, この状態を表しています。

tacticをStep実行してみましょう

Theorem ex_2_plus_1_eq_3: S (S O) + S O = S (S (S O)).
Proof.
  simpl.
  reflexivity.
Qed.

例交えてやる。　TODO

taciticの一覧はここにあります TODO

証明

さて, 初めに示した命題の証明を行いたいと思います。

Definition task := forall n m, n * S m = n + n * m.

Theorem solution: task.
Proof.
  unfold task.
  (* FILL IN HERE *)
Qed.

TODO

自動証明tactic

実はCoqのtacticは力強く, この程度の命題であれば自動で解いてくれる強いtaciticがあります。

自動証明tacticはゴールに対してtacticを適用するかを定義することで作られています。

例えばこの例では, ringというtacticを用いれば自動で行ってくれます。他にも, auto, eauto, omegaといったtacticがあります。

しかしこれらは, 証明してくれる命題の範囲がそれほど広くないです。それぞれのtacticの証明戦略を理解した上で, その証明を自分でもできるときに限って使うのが良いです。

僕が示せなかった証明を振り返る

長くなってきたので後編へ移ります。

Coqの勉強法はこれが一番有名らしいです。

わたしはこれやった https://t.co/lzg6cOnIPy
— そすうぽよ@技術書典く54D (@_primenumber) 2019年8月21日

また京大の五十嵐先生の講義テキストも便利です。 Computation and Logic: Winter Semester 2018

最後に宣伝なのですが, 証明コンテストTopProverは出れば出るだけ得するレートの付き方をするらしいです。是非参加して証明力を高めましょう。

2019-06-29

ズボラな一文字aliasコマンド集

知見開発

京都はクソ湿度が高くて気力が出ないです。そんなズボラな状態でもコマンドは叩けるようにようにしておきたいものです。

alias集

l='ls -CF'

ただ，zshの設定で空コマンドでEnterするとlsになっている。

v='vim'

必須

s='less'

LESSに環境変数をつけていない人はつけましょう。

このオプションをつけていれば lessを高機能 catとして使えます。

export LESS='-j10 --no-init --quit-if-one-screen -i -M -R -W -z-4 -x4'

g='git'

定番の1文字

git周りalias:

alias gap='git add -p'
alias gc='git commit -v'
alias gcp='git commit -p -v
alias gb='git checkout -b'
alias gs='git stash'
alias gg='git grep'

a='git add'

gaよりもaで良いのではと考えてこうなっている。

c='git commit -m'

実際はこのような設定

c-func(){git commit -m "$*"}
alias c='noglob c-func'

$ a hoge.txt
$ c Add !$

ダブルクオートも打たなくて済むのでズボラ度が高くておすすめ

o='git checkout'

便利

f='git fetch'

変な副作用がないので fで良い。

j='cd `git rev-parse --show-toplevel`'

git管理されているトップレベルに戻る。

d='date +%Y%m%d'

$(d)の形で使う。

alias dt='date +%Y%m%dT%H%M%S'

とともに，ファイルの名前付けに使うと便利。

m='make'

Makefileはめちゃくちゃ便利。どこにでもある

t='tmux -2'

最近はtmuxを使わなくなってしまった。

b='bundle'

alias b='bundle'
alias bi='bundle install --path vendor/bundle'
alias be='bundle exec'

の3点セットで使う。

n='npm'

こちらの3点セット

alias n='npm'
alias ni='npm install'
alias nr='npm run'

2019-06-13

サイコロで行く京都市バス桃鉄風すごろく大会

旅行開発

こんにちは。

京都市バスの地図を見た時，考えることがあると思います。

f:id:wass80:20190607140003p:plain

サイコロを振ってすごろくをすると楽しいのではないかと。

というわけで，京都市バスの1日乗車券を用いて，リアルすごろくを行いました。(去年の夏)

ルール

目的地バス停を決定する。
- あんまり遠くに行くとめんどくさいので，桂川より内側，JR東海道本線より内側だけにした。
参加者はバス停に向かう。遠くのバス停に歩いても良い。
6面ダイスを2こ振る。ダイスを降る前に時刻表を確認してはならない。
一番最初に来たバスに乗って出た目の数だけ停留所を進む。
目的地バス停に降り立つとポイントを獲得。通過する場合でも途中で降りることができる。
17:00になるまで，新しい目的地を決定しこれを繰り返す。

参加者の一人のnonylene氏の詳細な記事はこれです。めっちゃ丁寧なまとめなので雰囲気はこっちを読むと面白いです。

nonylene.hateblo.jp

すごろくスタート 10:00

僕, nonylene氏, tron氏, utgw氏の4人が百万遍に集まった。

作ったアプリケーションでランダムにバス停を決定する。

f:id:wass80:20190607142242p:plain

最初のバス停は「木辻南町」になった。

f:id:wass80:20190607145603p:plain

全員が同じバス停に向かい，サイコロを降った。

このためだけに便利なアプリを作った。

f:id:wass80:20190607153249p:plain

上から順番に

現在地点のバス停を入力する。 (GPSから自動入力可能)
どの乗り場から乗るかを入力する。
サイコロを降るボタンを押す。
最初にやってきたバスに乗る。
乗ってきたバスを入力する。
出目の数だけ進む。
降りた場所を入力する。(GPSから自動入力可能)

これによって全員の行動が逐次slackに送られてきます。

f:id:wass80:20190607153627p:plain

僕は最初のサイコロで3を出し，最初にやってきた102系統で「烏丸今出川」まで乗った。

f:id:wass80:20190607160153p:plain

続いて11を出し，203系統で「円町」まで直行。「木辻南町」へのバスの乗り場が異なる最高のバス停に到着した。

「木辻南町」へは丸太町通の93系統に乗ることでも向かうことができるが，どのバスに乗るかを決めることができないこのルールにおいて，バスの乗り場は決められても乗りたいバスに乗ることは困難となる。 93系統は3本/時であり，4系統以上あるバス停から93系統に乗れる可能性は低い。

今回は「円町」に到着したので，どのバスに乗っても「木辻南町」に向かう西行き乗り場に向かった。バス停に着いて，必要となる3以上の9の目が出たのでバスに乗って1番乗りでゴールした。

f:id:wass80:20190607161041p:plain

やってきたはいいが，木辻南町には何の目的もないので，次の目的地を設定する。

f:id:wass80:20190607162142p:plain

次の目的地は「新間ノ町二条」だ

地獄の四条大宮東行乗り場

サイコロを振ってたどり着いたは「四条大宮」だ。ここは大きいターミナルであり，多くのバスが発着する。つまりこのルールの上では，かなりの難敵となり襲いかかってくる。

f:id:wass80:20190607164233p:plain — http://www.arukumachi-kyoto.jp/info/wp-content/uploads/2015/09/shijoomiya-20150906.pdf

東行1番乗り場は8つの異なる行き先を持つバスが発着する。直ちに京都駅へ向かうバス，5駅先の四条河原町から南北に，7駅先の祇園から南北にとバスが分かれる。もし7より大きい数をダイスで降ってしまうと，行き先は全く選べないだろう。

東行1番乗り場で出した目は11．やってきたバスは207系統。目的地と反対方向である。

f:id:wass80:20190607164126p:plain

バスから降りて即ダッシュ

参加者の人々は同じバスからそれぞれ別の停留所で降りて目的地にダッシュしたらしい。

f:id:wass80:20190607165205p:plain

同じバスから異なるバス停で順々に降りて直ちにダッシュした人々が同じバス停へ向かう。

f:id:wass80:20190607165117p:plain

ダッシュはutgw氏の勝利だったらしい。この時まだ僕は207系統に乗っていた。

f:id:wass80:20190607165329p:plain

ランチタイム

目的地は御室仁和寺になった。五条坂からめちゃくちゃ遠い。

f:id:wass80:20190607165837p:plain

御室仁和寺に行くバスがあったが，これはJRバスなので1日乗車券で乗れない。眼の前でJRバスが通り過ぎていく。

f:id:wass80:20190607170101p:plain

とりあえずサイコロを振って辿り着く先が「今出川大宮」だった。

ここで予め設定していたイベントが発火した。

f:id:wass80:20190607165916p:plain

ここでnonylene氏と奇遇したので，是空というラーメン屋で一緒に食べた。

f:id:wass80:20190607170206p:plain

ラーメンを食べた後，何回かバスに乗ってあがいていたが，tron氏に圧倒的に負けた。

tron氏のバス停写真。

f:id:wass80:20190607170322p:plain

仁和寺に来たが，特に用事はないので次の目的地へ向かう。

休憩フェイズ

気持ちがわかってきて，こういう系統がたくさんあるバス停を見ると絶望するようになる。

f:id:wass80:20190607170625p:plain

2回ぐらい目的地が更新されて休憩になった。

f:id:wass80:20190607170609p:plain

近くの神社仏閣に行くことになった。梅津大社や，西院春日神社に人々は向かったらしい。

f:id:wass80:20190607171138p:plain

f:id:wass80:20190607171314p:plain

僕は特に観光スポットでもない寺社を眺めることになった。 f:id:wass80:20190607171420p:plain

終了

17:00になったので，最後の目的地を百万遍として終了になった。

僕は百万遍からかなり離れていたので，最後の目的地へのサイコロ移動はギブアップした。疲れたので。

17:29にutgw氏が最初にゴール。合計2回の目的地到達。
17:39にtron氏がゴール。合計2回の目的地到達。
17:48にnonylene氏がゴール。合計2回の目的地到達。
僕は3回目的地到達したので一応優勝らしい。

これで一日乗車券を酷使する会は終了となった。

感想

行動タイムラインがすごいことになる。これはnonylene氏のタイムライン。
行ったことがない場所に乗ったことがないバスで飛ばされるので良い。
日頃運動しないので，見ない町を歩くのが楽しいし健康。
600円ですごい旅行した気持ちになる。
機会があったらまたやっても良い。ドメイン特化のアプリケーションの使いやすさは最高なので。

経路

10:12 「百万遍」
10:16 ー102系統ー＞「烏丸今出川《地下鉄今出川駅》」
10:35 ー201系統ー＞「西ノ京円町《ＪＲ円町駅》」
10:44 ー93系統ー＞「木辻南町」
10:56 ー京都バス63系統ー＞「丸太町七本松」
11:10 ー52系統ー＞「四条大宮」
11:42 ー207系統ー＞「五条坂」
12:09 ー207系統ー＞「四条大宮」
12:36 ー201系統ー＞「今出川大宮」
13:30 ー203系統ー＞「北野中学前」
13:51 ー26系統ー＞「四条御前通」
14:19 ー80系統ー＞「中ノ橋五条」
14:53 ー特27系統ー＞「西大路三条」
16:14 ー3系統ー＞「四条大宮」
16:21 ー18系統ー＞「二条駅西口」
17:16 ー75系統ー＞「常磐野小学校前」

16回乗ったので3680を600円で乗ったことになり，およそ6倍の得。すごい。

2019-06-13

ググり方が難しいシェル(bash/zsh)周りの小ネタ集

開発

固まったsshから強制に抜ける

Enterしてから~.
~?でヘルプが出る

描画の壊れたターミナルを治す

stty sane コマンドで治る

書きかけのコマンドを保持する

Ctrl-Qでバッファをスタックする。
新しいプロンプトを出すと復帰する。

前回のコマンドの一部を書き換える

^hoge^hugaで前回のコマンドの一部を置換して実行できる。
前回のコマンド全ては!!
最後の引数は!$
前回の引数すべてを持ってくるのは!!1*

現在のカレントディレクトリから一部を書き換えてcd

cd hoge fugaをすると，例えば~/hoge-dir/dirから~/fuga-dir/dirに移動する。

標準エラーもパイプする

|&でパイプすれば良い。2>&1 |の省略形。
2>&1は「2の指す先(stderr)を1の指す先(stdout)にする」と読む。
3>&2 2>&1 1>&3だとstderrとstdoutがスワップします。

履歴検索

Ctrl-Rでコマンド履歴をインクリメンタルサーチする。
もしくは !v のようにコマンドの始め部分を入力する。

2019-05-10

debian6しか使えなくてapt-getもできなくてhttpsができない日の対策

知見開発

悲しいが，SSLを無効化するしかない…

~~wgetのSSL無効化~~というかこれは証明書の無視ですね。あとで気づいた。

$ echo "check_certificate = off" >> ~/.wgetrc

git clone https://~がコケるので，git@github.comに書き換える

url."git@github.com:".insteadOf https://github.com/

まあこれでもだめならOpenSSLをビルドするほうが健全ですね

2019-05-08

SpotlightはApplicationsにおいたSymbolic Linkのアプリを出さないので，AutomatorでShell Scriptを実行するアプリを作成すると良い

知見

Spacemacsをmacにインストールすると，Applicationsにシンボリックリンクを作れ，という指示が出る。

$ ln -s /usr/local/Cellar/emacs-plus/26.2/Emacs.app ~/Applications/Emacs.app

これはSpotlightに読み込まれない。手軽に起動できない。

回避するには，AutomatorでShell Scriptを実行するアプリケーションを作る。

f:id:wass80:20190508153836p:plain

$ open /usr/local/Cellar/emacs-plus/26.2/Emacs.app $@

そして，作ったアプリケーションをApplicationsに保存する。

参考: macos - Can I make a symlink (to a .app folder) in Applications directory show up in spotlight? - Ask Different

ついでに，IconがAutomatorだとキモいので置き換える。

「情報を見る」のウインドウのアイコンはCommand+C/Vでコピペできる。まじかよ。

f:id:wass80:20190508154007p:plain

参考: Can I change the application icon of an Automator script? - Ask Different

バージョン: macOS 10.13.6（17G5019)