Coq入門 - 4
進捗あまりない。
update · 702639b · totem3/coq-prac · GitHub
全然わからんのでもうImportしたのを使って証明せずに進めているｗ
できるところはそこまでにでてきた定理を使って証明して、まぁなんとなく感覚はわかってきたようなきていないような。
こうなってくると、今後まともにやっていくうえで大事なのはSearchを使いこなすことのような気がしてくるんだけど、不等号系が全然SearchRewriteとか使っても出てこない
このあたりがよくわからない。次使いこなすべきはSearchかなと思った
n <= m -> ~ m < nとかFalseの証明がでてきたけど、これがやっぱりわからない。
Searchを使いこなせるようになるのと、矛盾を示せるようになりたい
Coq入門 - 3
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について学ぼうと思う
ここがとても詳しいので、ここを読む。
emacsのauto-completeでCoqの補完が効いてなかった
題名の通り。
効いてなかった。
よくわからんのでスルーしていたが、ストレスフルなので治すことにした。
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+なんとかってやっぱちょっと長いしねー
Coq入門 - 2.1
進捗ありません。
疑問メモ
矛盾を示すのが難しい
forall n:nat, S n <= 0 と forall n:nat, S n > 0 があれば矛盾を示すのは簡単に見える
けど、どうやるのかわからない
forall n: nat, S n <= 0 はPropということでいいんだよな・・
CheckしてみるとPropとなるからやはりPropのはずだ
forall n : nat, S n > 0
: Prop
と思ったけど、これはforall n:natが付いた時で、仮定に
H : S n <= 0
とあるとこのS n <= 0はそういう型ということになのか
何かしらPropに対する操作をしようとすると
The term "H" has type "S n <= 0" which should be Set, Prop or Type.
というエラーがでる。
ということはなんか矛盾を示そうってのがそもそもなんか違うのかな
追記
ここにちゃんと↓こう書いてあった
Coq では "False_ind : forall (P : Prop), False -> P" という定理を使います。 ... ~ P は P -> False の別の書き方だったことを思い出せば、lt_n_O はサブゴールに apply できることに気付きます。n に 0 を代入すると 0 < 0 -> False となるので、H を lt_n_O に渡せば False が証明されます。
False -> Pということになるのか。
全然意味わからないままFalse_indを使っていた
かつ~はP -> Falseなのか！
ってことは・・・
~ S n <= 0というのがいればいいのか！ということがわかった
わかったらできた！（しょうがないからnle_succ_0は使った^^;)
何をImportすれば何が使えるようになるのか・・・
Moduleが全然わからん・・・
動きを調べたいからle_elimとか使いたいんだけど、何をImportすればいいんだろうか・・
追記
Moduleがファイル名とファイルの中のModuleを意味することがあるらしい。
How do I import modules in Coq? - Stack Overflow
あとNOrderをImportしても使えなかったのは、Abstractなやつだったからっぽい。
Searchを使いこなせばなんとかなりそう
hoge; fuga.について
hoge; fuga.
と
hoge. fuga.
だと意味が違うのか！！
難しい
Coq入門 - 2
こういうのをやることにした。
ただCoqの標準ライブラリからLemmaとTheoremを取り出してきただけ。
こんな初歩的なものなら簡単に証明できるだろ＼(^o^)／
と思っていたら、いきなりできない・・・ｗ
Lemma le_n_0_eq n : n <= 0 -> 0 = n.
こんな当たり前そうなものすら証明できない。
つらい・・・
こうなるじゃろ？
Lemma le_n_0_eq n : n <= 0 -> 0 = n. intros. symmetry. |
1 subgoals, subgoal 1 (ID 7) n : nat H : n <= 0 ============================ n = 0 |
で、induction nで行けると思うじゃろ？
こうなるじゃろ？
Lemma le_n_0_eq n : n <= 0 -> 0 = n. intros. symmetry. induction n. reflexivity. |
1 subgoals, subgoal 1 (ID 18) n : nat H : S n <= 0 IHn : n <= 0 -> n = 0 ============================ S n = 0 |
S n = 0
なんておかしい！こりゃ矛盾じゃ(´ω｀)
簡単じゃの(´ω｀)
・・・
・・・
・・・
・・・
で、できない(；´Д｀)
わからぬ・・・(；´Д｀)
基本がわからぬ・・・・(；´Д｀)
apply False_indしてみたところで、示せぬ・・・
ぐぬぬ・・・
とりあえずinductionしてみるけど、示し方が分からない。。。。
Lemma le_n_0_eq n : n <= 0 -> 0 = n. intros. symmetry. induction n. reflexivity. apply False_ind. induction n. |
2 subgoals, subgoal 1 (ID 28) H : 1 <= 0 IHn : 0 <= 0 -> 0 = 0 ============================ False subgoal 2 (ID 34) is: False |
分からない・・・
粘ったけど分からない・・・・
うぅ。。
仕方なくCoq本体見てみるも、証明が鮮やかだったり色んな他の補題や定理を使って証明しているのであまり練習にならない。。
むむむ・・・・
出直す・・・
Coq入門 - 1
Agda入門にまんまと失敗して、Coqを入門してみることにした。
このチュートリアルをやっている。
色々調べてみると結構他にも入門はあって、先に調べるべきだったと思ったりした。
で、このチュートリアルは、とりあえず手を動かしてみるものとしてはありだと思う。
ただ、体系的な解説ではないのでなんとなく理解が深まっている感がしなかったり（個人的に）、徐々に辛くなってくる（気がする）
とりあえず僕は証明駆動開発の前で死んでいる。ちゃんと理解して読み込んで進んでいないからかもしれない。
割と挫折気味なので、簡単な定理でも証明しまくって経験値を積んでやろうかなと思ってきた。
とりあえず交換法則でも証明するか！
ということでやってみたのがこれ
なんかひどい出来・・・
でもこれでなんとなく証明の感覚がつかめた気がする
簡単な定理を証明するために標準ライブラリの関数を使ってしまっているのが残念なので、これをまた証明してImportを消すという遊びをしながら証明に慣れたい。
数学的素養は全くなくて、高校数学でも証明はとても苦手だったのでまぁ苦手なわけでとりあえず慣れよう。うん。
もっとシンプルに証明できるはずだし。
