vagrantで立ち上げたvmがどこにあったかわからなくなっちゃう

vagrant

Macというのはダメな奴なので、ubuntuとかが欲しくなる。

というわけでとりあえず作業用にVMを立ち上げたりよくするんだけど、適当にVagrantfileを作って起動するものだから、しばらくするとどこで立ち上げたやつだかわからなくなる。 Vagrantfileどこだっけ・・みたいな

ちゃんと管理しとけな話なんだけどそういうことがちょいちょいあるので、全部VM見れるようなのはないんだろうか。

と思ったらあった

fgrehm/vagrant-global-status · GitHub

と思ったらもうDEPRECATEDだ

Centralized machine index by mitchellh · Pull Request #3225 · mitchellh/vagrant · GitHub

と思ったらもうvagrant本家に取り込まれてるじゃん

vagrant global-status - Command-Line Interface - Vagrant Documentation

vagrant global-status　でいいのね。いいじゃん。

--prune でゾンビを消すこともできるんだ。便利

Coq入門 - 4.1

coq

https://coq.inria.fr/を見ていたら、Documentationのところにこんなものがあった。

https://cel.archives-ouvertes.fr/file/index/docid/459139/filename/coq-hurry.pdf

ここにSearchのことが少し書いてあって、SearchRewriteで望むものが出てこない理由がわかった。

The command SearchRewrite is similar, but it only looks for rewriting theorems, that is, theorems where the proved predicate is an equality.

なるほど、rewriteっていうのは確かにそういうことか。

applyとは別ね。

applyしか使ってなくてよく分かっていなかった。

このドキュメントを読む感じだとSearchやSearchPatternを使うべきっぽいが、emacsのcoq mode(かproof-general?)のコマンドにはそれらはない。

あるのは

  • SearchRewrite
  • SearchAbout
  • SearchConstant
  • Searchregexp
  • SearchIsos

のようだ。

RewriteとAboutは解説があるが、他は・・・？

特にemacsコマンドにドキュメントは書かれていないようだ

ただ、SearchIsosがC-c C-a C-oにProofGeneralでバインドされていて、使う頻度が高そう。

使ってみるとエコーエリア？に

SearchPattern (parenthesis mandatory), ex: (?X1 + _ = _ + ?X1) (default nil):

なんかSearchPatternと書いてあるし、クエリの例も求めているものっぽい。

使ってみると望み通りっぽい結果が出てきている。

これを使って進めてみよう。というメモ

Coq入門 - 4

coq

進捗あまりない。

update · 702639b · totem3/coq-prac · GitHub

全然わからんのでもうImportしたのを使って証明せずに進めているｗ

できるところはそこまでにでてきた定理を使って証明して、まぁなんとなく感覚はわかってきたようなきていないような。

こうなってくると、今後まともにやっていくうえで大事なのはSearchを使いこなすことのような気がしてくるんだけど、不等号系が全然SearchRewriteとか使っても出てこない

このあたりがよくわからない。次使いこなすべきはSearchかなと思った

n <= m -> ~ m < nとかFalseの証明がでてきたけど、これがやっぱりわからない。

Searchを使いこなせるようになるのと、矛盾を示せるようになりたい

Coq入門 - 3

coq

Coq入門 - 2.1 - エンジニアですよ！ に追記したが、Lemma le_n_0_eqが証明できた

あと補完が効くようになったらなぜか.を押すだけでC-c C-n相当の部分まで進むようになった。

False_indやFalseの証明の仕方が少しわかった。

しかし、その後も証明ははかどらない。

ムリ

Coqの使い方とかtacticがどうこう、というより単に証明するだけの頭脳が私にないような気がしてきた

もしくは自然数の証明は難しいのではないのか？

そんなことはないか

ペアノの公理は数学ガールで読んだことがあるというくらいの知識はあるんだがｗ

高校でも大学受験でも証明はすごい苦手だったなぁ

さて戻って、証明の続きをしてる。

全然証明進まないし、答え（標準ライブラリのコード）を見ても全然わからないんで飛ばす。

ArithとかImportしてるんで証明は進む。intuitionだけで進むｗ

intuitionだけで進まなくなったle_elim_relを証明してみようと思って取り組んでみる

さっぱりわからーん。

inductionとdestructしか使えるものがないので全然進まない

2日ほど悩んでライブラリを読んでみると、なんだろうね

auto with arithとかやってるので自動で証明できるくらい些細な事なんだろうな。

わからんけどね。

でもelimっていうのもあるので、使ってみたら証明できた。

autoを使っていないところ以外はまるっきりライブラリ通り。

introsで名前を渡すところとか、できる気がしない・・・

introsで名前を特に渡さずにやると、進まなくなる。

具体的には、この部分。

Lemma le_elim_rel :
 forall P:nat -> nat -> Prop,
   (forall p, P 0 p) ->
   (forall p (q:nat), p <= q -> P p q -> P (S p) (S q)) ->
   forall n m, n <= m -> P n m.
  intros P H0 HS.
  induction n; trivial.
  intros m Le.
  elim Le.
  apply HS.
  intuition.
 
2 subgoals, subgoal 1 (ID 97)
  
  P : nat -> nat -> Prop
  H0 : forall p : nat, P 0 p
  HS : forall p q : nat, p <= q -> P p q -> P (S p) (S q)
  n : nat
  IHn : forall m : nat, n <= m -> P n m
  m : nat
  Le : S n <= m
  ============================
   P n n

ここで、名前を付けずに進めていると、 IHn : forall m : nat, n <= m -> P n mこの部分がforall m : natが付いてないものになってしまい、P n nにapplyできなくて進まない。

証明ができない！ こんなときにもgeneralizeしないと進まないことあるよ、みたいに書いてあるからやってみたけどそれでも進まん。

まぁとりあえずintrosするときには名前を付けると何が違うのかと、elimについて学ぼうと思う

Coq タクティクリファレンス: 帰納法と場合分け

ここがとても詳しいので、ここを読む。

emacsのauto-completeでCoqの補完が効いてなかった

emacs coq

題名の通り。

効いてなかった。

よくわからんのでスルーしていたが、ストレスフルなので治すことにした。

Auto Complete Modeユーザーマニュアル

auto-completeの情報は↑に素晴らしくまとまっていて、簡単に対応はわかった。

ダウンロードしたauto-completeのディレクトリを見てみると、coq-modeという辞書ファイルはデフォルトで用意されていたので、辞書が読み込めていないのが原因だろうと。

ということで辞書関連にあたりを付けてマニュアルを見てみると、ac-dictionary-directoriesというのがある

Coqのファイルを開いているバッファでC-h vでac-dictionary-directoriesの値が何になっているか見てみると、nilになってる。

これがいかんのだ。きっと。

特に設定はしていないんだがac-user-dictionary-filesが~/.dictになっているが、ファイルを指定するところのはずなのでここには追加しない。

値おかしい気がするが無視する。

で、自分の場合は~/.emacs.d/elpa/auto-complete-20141103.105/dict/にデフォルトの辞書ファイルが置いてあったので、

ac-dictionary-directoriesに"~/.emacs.d/elpa/auto-complete-20141103.105/dict/"を追加する

以下の設定をinit.elに追加する。

(add-to-list 'ac-dictionary-directories "~/.emacs.d/elpa/auto-complete-20141103.105/dict/")

で、キャッシュを削除して設定を反映するためM-x ac-clear-dictionary-cacheを実行する。

これで補完が効くようになった(๑╹ڡ╹๑)

Coqの場合はC-c C-a C-tでcoq-insert-tacticとかそういうの使うのがいいのかもしれんけど、C-c C-a+なんとかってやっぱちょっと長いしねー