定理証明コンテストに参加した [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は出れば出るだけ得するレートの付き方をするらしいです。 是非参加して証明力を高めましょう。

ズボラな一文字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'

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

こんにちは。

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

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

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

ルール

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

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

nonylene.hateblo.jp

すごろくスタート 10:00

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

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

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

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

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

上から順番に

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

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

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

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

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

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

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

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

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

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

http://www.arukumachi-kyoto.jp/info/wp-content/uploads/2015/09/shijoomiya-20150906.pdf

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

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

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

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

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

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

ランチタイム

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

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

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

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

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

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

tron氏のバス停写真。

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

休憩フェイズ

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

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

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

僕は特に観光スポットでもない寺社を眺めることになった。

終了

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倍の得。すごい。

ググり方が難しいシェル(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 のようにコマンドの始め部分を入力する。

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をビルドするほうが健全ですね

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を実行するアプリケーションを作る。

$ 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でコピペできる。まじかよ。

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

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

mRubyの動くLED時計をESP32で作る [後編]

wass80.hateblo.jp

の後編です。

mRubyで時計のプログラムを書けるようにする

といっても，もくもくとAPIを実装するだけです。

用意したAPIはこれだけあります。

github.com

こういうプログラムをHTTPで書き込んで時計で実行できるようになりました。

i = 0

# ラインアート
lines = []
aline = [20, 10, 3, 8, 2, 3, 2, -1]

# 次の時間の線を生成する
def succ_line l
    x0, y0, x1, y1, dx0, dy0, dx1, dy1 = l[0], l[1], l[2], l[3], l[4], l[5], l[6], l[7]
    x0 += dx0; y0 += dy0; x1 += dx1; y1 += dy1
    (dx0 *= -1; x0 = 0) if x0 < 0
    (dy0 *= -1; y0 = 0) if y0 < 0
    (dx1 *= -1; x1 = 0) if x1 < 0
    (dy1 *= -1; y1 = 0) if y1 < 0
    (dx0 *= -1; x0 = 31) if x0 > 31
    (dy0 *= -1; y0 = 31) if y0 > 31
    (dx1 *= -1; x1 = 31) if x1 > 31
    (dy1 *= -1; y1 = 31) if y1 > 31
    [x0, y0, x1, y1, dx0, dy0, dx1, dy1]
end
8.times {|t|
  lines << aline
  aline = succ_line(aline)
}

time_format = "%H:%M"
message = "Welcome to KMC! Please Enjoy Yourself!"
# Loopの開始
Task::loop do
  # 描画削除
  Led::clear 0
  # 色指定 R, G, B (0 ~ 7)
  Led::color 0, 1, 0 
  lines.each {|l|
    # 線描画 x1, y1, x2, y2
    # 座標は(0 ~ 31, 0 ~ 31)
    Led::line l[0], l[1], l[2], l[3]
  }
  lines.shift()
  lines << succ_line(lines[-1])

  # フォント指定(番号)
  Led::font 2
  Led::color 7, 3, 3
  
  # 時刻更新
  Time::update
  
  # 文字出力 x, y, 文字列
  # Time::str(strftime文字列)
  Led::text 1, 12, Time::str(time_format)

  Led::font 0
  Led::color 5, 0, 5
  # 流れる表示 時間, 遅さ, y, 文字列
  Led::show i.div(2), 23, message
  
  Led::font 5
  # cmdで入力された文字列
  w = Task::cmd()
  Led::color 0, 5, 5
  Led::show i.div(2), 1, w 

  # [注意] Led::flushを実行しないと画面が更新されません。
  Led::flush
 
  i += 1
end

これは，[前編]の動画のプログラムです。 ラインアートを背景で動かしています。

mRuby拡張により配列や文字列を使えるので，普通のrubyプログラムのように書くことができます。

APIの実装

例えば Led::line の場合，

Cで実装されている部分はこのように，ブレゼンハムのアルゴリズムを持ってきます。

void b_line(int x0, int y0, int x1, int y1, int r, int g, int b) {
  mrb_int dx = abs(x1-x0), dy = abs(y1-y0),
          sx = (x0 < x1) ? 1 : -1, sy = (y0 < y1) ? 1 : -1,
          err = dx-dy;
 
  while (true){
    b_set(x0, y0, r, g, b);
    if (x0 == x1 && y0 == y1) break;
    mrb_int e2 = 2 * err;
    if (e2 > -dy) {
      err = err - dy;
      x0 = x0 + sx;
    }
    if (e2 < dx) {
      err = err + dx;
      y0 = y0 + sy;
    }
  }
}

mRubyの言葉に持ち上げます。

static mrb_value ledline(mrb_state* mrb, mrb_value self) { 
  mrb_int x0, y0, x1, y1;
  mrb_get_args(mrb, "iiii", &x0, &y0, &x1, &y1);
  b_line(x0, y0, x1, y1, p_r, p_g, p_b);
  return self;
}

そして Led::lineで呼べるように，環境に登録します

  struct RClass *Led = mrb_define_module(mrb, "Led");
  mrb_define_class_method(mrb, Led, "line", ledline, MRB_ARGS_REQ(4));

簡単ですね。

辛い点

• ESP32のメモリが足りないので，重いプログラムが動かない
  • slackから対局できるオセロ時計が作られたが，メモリ不足で最後まで対局できなかった。
• 日本語のエンコードにISO-2022-JPを選んでしまった。
  • 入れた日本語フォントがJISコードでの文字対応だったのでこのエンコードを選んだが，めんどくさいエンコードだった。
• 最初 Led::flush が Led::flash になっていた
• なぜ整数の割り算 3/2が小数1.5に評価されてしまうんだろう…。ここでRubyとの非互換性ができてしまった歴史的経緯が知りたい。

部員が作ってくれたプログラムたち

KMC部室にある時計の様子です。 pic.twitter.com/OVTERHy4Lg

— 月鈴那知 (@ten986) 2018年7月11日

この他にも様々プログラムを書いてもらえました。

現在のデフォルトの時計は，室内気温や天気の表示を行うものになっています。

室内気温の情報は昔に作ったこのシステムの情報を使っています。

wass80.hateblo.jp

感想

• ESP32を扱うのはサンプルコードが豊富なので割と簡単。
• はんだ付けとか実装のほうが難しい。
• 実際に動くものができるのは楽しいので良いですね。
• Exploitがめっちゃ簡単にできそうなコードをCだと書いてしまうので，安全なIoT開発手法はもっとほしい…
  • RustでESP32開発とかできたらいいんですが，まだLLVM backendがないんですよね。ほしい。