数遊び

日常

ある日の夜，寝ようとして布団に入った瞬間に，どういうわけか 676 という数字が浮かんできた。

見覚えのある数字だ。でもどこで見たのだろうか。平方数か何かだろうか。そういえば 24 の二乗はそんな感じの数だった気がする。そこで計算してみると 24^2 = 4 \times 12^2 = 4 \times 144 = 576，ちょっと違う。

試しに素因数分解でもしてみようと思う。676 = 700 - 20 - 4 で右辺に出てくるのは 4 の倍数だから，676 は 4 で割り切れる。そこで試しに割ってみると 676 = 4 * 169 となる。169 は知っている。13 の二乗である。

ということは 676 = (2 \times 13)^2 = 26^2 なのか。そういえばそうだったような気がする。

そうすると 576 と 676 はいずれも平方数なのだ。そんなことがあるだろうか？というのは，平方数は疎らにしか存在しないように思えるので，両者の間隔がちょうど 100 というきりのいい数になるということはそれほどありそうにない。*1

それではなぜ 26^2 - 24^2 = 100 なのか。計算してみればそうなる，というのは論理的に正しいが，論理的に正しい証明が必ずしも納得をもたらすわけではない。

そういえば，24 と 26 の間には 25 があり，100 は 25 の倍数である。たぶんここから何かわかるのではないか。

平方数が奇数の和であることを思い出そう。つまり n^2 = \sum_{k=1}^n (2k-1) である。そうすると 25^2 = 24^2 + 49 と 26^2 = 25^2 + 51 がわかるから（これは (x \pm 1)^2 = x^2 \pm 2x + 1 を使っても確かめられる），確かに 26^2 - 24^2 = 49 + 51 = 100 でなければならないとわかった。少し納得した。

こんなことを考えているから眠れない。

*1:もちろんありそうにないからといってありえないという根拠にはならないし，そもそもありそうにないという感覚はよくある認知バイアスの一例である。例えば 1 以上 1000 以下の整数をランダムに選ぶとき，100 というきりのいい数字が出る確率が，623 のようなきりのよくない数が出る確率に比べて低いわけではない。同様に，二つの平方数を持ってきて差を計算したらちょうど 100 になるという出来事が，単にそれがきりのいい数だというだけで他の数が出てくるのに比べてありそうにないことだと主張することはできない。しかし僕の頭はこのような判断を一瞬で下せるほどにはよく働かなかった。

掛け算の順序を区別するなら割り算は二つ必要

joke 日常

掛け算記号の左右の役割は異なるので順番を入れ換えてはいけないという立場がある。左側は「一単位あたりいくつ」を表し，右側は「何単位分あるか」を表すのであり，それらを逆に書いてはいけないのだという。例えば，2×3=6 と書いたらそれは「三人がそれぞれ二つずつみかんを食べた」という状況は表すが「二人がそれぞれ三つずつみかんを食べた」という状況は表さない，ということだと理解している。

その立場を貫こうとすると，掛け算記号の左側を求めるための割り算と右側を求めるための割り算の二つが別々のものとして導入されねばならないように思う。2×3 と 3×2 で意味が異なるのだったら，□×3=6 と 2×□=6 のそれぞれにおいて □ に入る値を求めようとするとき，両者において用いられるべき演算が同じである理由はない。□ はそれぞれ異なる役割を担う位置に置かれているのだから，それを求めるのにも異なる演算が用いられると考えるのは道理であるし，実は同じ演算で求まるのですと言われてもそう簡単に納得できるようには思えない。実際それらを区別する用語はあって，前者を等分除，後者を包含除と呼ぶ。

しかし，両者を概念として区別することはあっても，例えば異なる記号で表すなど，構文的に区別しているのを見たことはない。これはどうしてだろうか。掛け算の左右を区別するのと同じように，二つの割り算も構文的に区別するべきではないか。そうしないと混乱の元であるのに，横着をして両者をごっちゃにしてはいけない。

というわけだから，□×3=6 の □ を求めるための演算と，2×□=6 の □ を求めるための演算を区別するために，いま仮に前者であるところの等分除を／で表し，後者であるところの包含除を＼で表すことにすれば

□×3=6 ⇔ □=6／3

であり，また

2×□=6 ⇔ □=2＼6

のように書くことができる。こうすれば見た目にも別々の演算であることが明らかで，わかりやすいのではないか。

最後に参考文献をひとつ挙げておこう。

Residuated Lattices: An Algebraic Glimpse at Substructural Logics: An Algebraic Glimpse at Substructural Logics (Studies in Logic and the Foundations of Mathematics)

Residuated Lattices: An Algebraic Glimpse at Substructural Logics: An Algebraic Glimpse at Substructural Logics (Studies in Logic and the Foundations of Mathematics)

Coq 8.5 を入れてみた

先日 Coq 8.5 がリリースされたので入れてみた話。

coq 自体のコンパイルは問題なくできたけど，その後 ssreflect のコンパイルに失敗した。make すると

Error: The files /usr/local/lib/coq/parsing/pcoq.cmi
       and /usr/local/lib/coq/lib/compat.cmi make inconsistent assumptions
       over interface Compat

と言われる。問題の compat.cmi はタイムスタンプを見ると Coq の前のバージョンのものらしいことがわかる。どうもソースコードのディレクトリ構成が変わっているようで，新しい compat.cmi は別のディレクトリに存在している。それで Coq を make install したときに上書きされずに古いものが残って，何らかの理由でそれが間違って参照されているようだ。

試しに

sudo rm -fr /usr/local/lib/coq/

してから coq をインストールし直してみると，今度は ssreflect の make に成功した。

mathcomp もコンパイルし直さないといけない。試しに make -j16 とかやってみたら 20 分ちょっとでコンパイルが終わった。

風呂場でする遊び

日常

さっきシャワーを浴びながら考えていたことなど。

8 って 9 - 1 だから平方数（以下，平方数に 0 は含めないことにする）の差だなーということをまず思った。なんで 8 のことを考えていたかは省略する。というかよく覚えていない。

平方数の差はたくさんあるので，これだけだとそんなに面白くない。もうちょっと強い条件はなにか考えられないだろうか。

例えば平方数の差で表せる正の数の中で 8 はどれくらいの位置にいるだろうか。そういう数の中で一番小さいのは 3 である。その次は 5 である。その次ぐらいじゃないか？と思ったが，よく考えたら 7 = 16 - 9 だから違った。

しかし以上のことから，平方数の差で表せる正の数のうち平方数の差で表せる最小の数番目に小さい数は 7 であることがわかった。8 はその次。

7 までに現れる数はすべて奇数だったので，8 の特徴付けとして「平方数の差で表せる最小の正の偶数」というものが考えられることもわかる。

考えてみれば 3 以上の奇数は必ず平方数の差で表せるのだった。そして偶数が平方数の差になることは，それが 4 の倍数かつ 4 より大きいことと同値である。いずれも証明は難しくないので読者への演習問題とする。

ssreflect の proof script のインデント

ssreflect を使っているとき，proofgeneral のデフォルトのままだと（といっても何が本当にデフォルトなのか把握できていませんが，少なくともそんなにいじってないはずの手元の環境では）インデントがあんまりうまくいってない感じが強いので何とかできないかなと思っています。

今日ちょっと coq-smie-indent.el などを見てみたら，by のインデントの調整くらいはすぐにできそうな気がしたのでやってみました。

(defadvice coq-smie-rules (around ssr-by-tactical (kind token) activate)
  (if (and (eq kind :before) (equal token "by")
           (save-excursion
             (skip-chars-backward "\t\n\r ")
             (= (char-before (point))  ?.)))
      (smie-rule-parent)
    ad-do-it))

by はデフォルトではインデントを深くするので，例えば

have -> : 1 + 1 = 2
  by reflexivity.

みたいになります。これはいいのですが，ssreflect では by を先頭に書くこともあって，例えば手元にある適当なコードを貼り付けますが

case.
move => H; move : (eq_sigT_snd H).
by rewrite eq_axiomK.

のようにも書きます。こういうときはインデントを深くしてほしくないので，advice でむりやりそうなるようにしました。

あとは => が tactical （と呼ぶのが正しいのかどうかいまいちわからないけど他に適切そうな言葉を知らない）として使われるときには ; より結合力が弱いはずなんだけどそういう動作になってないようです。

例えば，また適当に手元にあったものを貼り付けますが

by move => H; move : H inv HPinv HVinv inv_env pweq; elim => // *;
  match goal with [H : _ |- _] => case : H => ? ? ?; subst; eauto end.

みたいなのはデフォルトの動作だと

by move => H; move : H inv HPinv HVinv inv_env pweq; elim => // *;
                                                            match goal with [H : _ |- _] => case : H => ? ? ?; subst; eauto end.

となってとても残念。

これも何とかできるとよいなと思うのですが，こっちはたぶん文法規則を書き直す必要があるのでもっと面倒そう。

議論の構造の proof script への反映のしかた

Coq の証明を書くときに，ただ tactics を一列に並べて書くと，まったく読めなかったり Coq のバージョンが上がって証明が通らなくなったときにどこでこけてるのかわからなくなったりして不都合なので，証明の構造を proof script のテキスト上にも反映させましょうという話はたぶん昔からあって，昔はインデントとかでそれをやっていたのですが最近は Coq の側でそういうことをサポートするための仕組みが入りました。具体的には bullet と brace ですが，そのあたりの話。Reference manual の 7.2.6 あたり。

bullet は場合分けして case 1, case 2, ... というときには自然に書けて，例えば簡単な例を挙げると

Goal forall n : nat, n = 0 \/ exists m, n = S m.
Proof.
  induction n as [ | n' IHn].
  - left; reflexivity.
  - right; exists n'; reflexivity.
Qed.

のようになります。

これはいいのだけど，subgoal が発生する別のパターンとして assert のような補題を宣言する tactic を使った場合があって，これも bullet を使って書くと

Variables A B C D : Prop.
Goal (A -> B) -> (B -> C) -> A -> C.
Proof.
  intros HAB HBC HA.
  assert (HB : B).
  - apply HAB.
    exact HA.
  - apply HBC.
    exact HB.
Qed.

みたいになります。

しかし，この証明の流れは場合分けとは違う構造をしているように感じるので，こう書くのはちょっと違和感があります。つまり，assert が生成する二つの subgoal は induction の場合と違って対等ではなく，もともとの goal の証明（後ろの subgoal）が主で assert された事実の証明はそのための補助的な議論という関係にあります。だから先ほどと同じように単に二つ同種のものであるかのように並べて書くのは直感に反する気がするわけです。

この手の tactic では先に来る subgoal の方が補助的なものとみてよいと思うので（特に ssreflect の have/suff は名前から判断するにそういう使い分けをさせる意図がありそう）例えば brace を使ってこう書いたらどうでしょうか。

Goal (A -> B) -> (B -> C) -> A -> C.
Proof.
  intros HAB HBC HA.
  assert (HB : B). {
    apply HAB.
    exact HA.
  }
  apply HBC.
  exact HB.
Qed.

場合によってはネストしてみたりとか。

Goal (A -> B) -> (B -> C) -> (C -> D) -> A -> D.
Proof.
  intros HAB HBC HCD HA.
  assert (HC : C). {
    assert (HB : B). {
      apply HAB.
      exact HA.
    }
    apply HBC.
    exact HB.
  }
  apply HCD.
  exact HC.
Qed.

個人的には，どちらかというと bullet よりもよさそうな気がしていますが，こういうのを見たことがないので，あんまり想定された書き方ではないのかもしれない。

一つの問題は，brace を閉じた次の行のインデントがおかしなことになるので手で直さなければならない点。あとピリオドがないと subgoal が閉じている感じがしないのですが，これは慣れの問題かもしれない。しかし慣れとか言い始めると，そもそも bullet に慣れればそれでよくなるだろうということにも。

emacs のカーソルの色が勝手に変わる

最近，emacs を使っているといつの間にかカーソルのデフォルト色が skk が on になっているときの色（正確には skk-cursor-hiragana--color）になっていた，ということが何度もあったので原因を調べてました。skk を off にしてもカーソルの色が on のときと同じになるのでわかりにくいのです。

結論としてはどうするのが正しいかよくわからないけど，とりあえずこうしたらごまかせてる気がする。

(setq anything-save-configuration-functions
      '(set-window-configuration . current-window-configuration))

あれこれ

変化しているのは frame-cursor-color ですが，どういう理由なのか見当がつかないので，とりあえず色が変わるタイミングがいつなのかを知るために，定期的にカーソル色をチェックして変わっていたら知らせるようにしてみました。

具体的にはこんな感じです。毎秒各フレームのカーソル色を調べて，black でなくなっていたらデバッガを起動する。デバッガを起動するのは確実に気付かせるための方法ですぐ思いついたのがそれだっただけで，深い意味はありません。

(run-with-timer 1 1 (lambda ()
                      (dolist (f (frame-list))
                        (unless (string= (frame-cursor-color f) "black")
                          (debug "frame cursor color has changed" f)))))

それで十日くらい様子を見ていたら，どうやら anything が終了するタイミングのようだとわかったので anything のコードを見てみました。

そうすると anything-current-frame/window-configuration で取得した frame parameter らしきものを後で元に戻しているので，このあたりだろうと推測してさらに追いかけてみると，どうやら（デフォルトでは） anything の開始時に frame parameter を取得して，終了時にそれを使って復元しているということがわかりました。さらに，復元時には modify-frame-parameter が呼ばれており，この関数には skk-cursor から require されている ccc.el で advice がかけられていて，どうもその advice が原因になっているのではないかということがわかりました。（なので，このあたりの処理を変更してやれば解消しそうだ，ということで冒頭のような設定をしたわけです）

ちなみに問題の advice は以下。

(defadvice modify-frame-parameters (after ccc-ad activate)
  (when (and (assq 'cursor-color (ad-get-arg 1))
             (null buffer-local-cursor-color))
    (set-frame-cursor-color (ad-get-arg 0)
                            (cdr (assq 'cursor-color (ad-get-arg 1)))))
;; 以下略

buffer-local-cursor-color が設定されていないならカーソルの色を変える，という処理があって，ここでカーソルの色が変わるようです。たぶんこれがうまく意図した通りに動いていない。

このコードはおそらく current buffer を表示しているウィンドウが所属しているフレームのカーソル色を変更しようとした場合にはうまく動くけれど，そうでない場合には意図しない挙動をするのではないかと思います。

かといって，直そうとするとどう直せばいいのかよくわかりません（そんなに真面目に考えてもいませんが……）。

emacs においてカーソル色はフレームの属性ですが（たぶん），バッファは別にフレームに属するものではなくて，複数のフレームで同じバッファを表示したりできます。だから「バッファのカーソル色」みたいなものを考えてそれをそれらしく動作させようとすると，ちょっと難しいのかもしれません。