Coq入門 - 2.1

coq

進捗ありません。

疑問メモ

矛盾を示すのが難しい

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.

だと意味が違うのか！！

難しい