coq

Coq入門 - 4.1

coq

https://coq.inria.fr/を見ていたら、Documentationのところにこんなものがあった。 https://cel.archives-ouvertes.fr/file/index/docid/459139/filename/coq-hurry.pdf ここにSearchのことが少し書いてあって、SearchRewriteで望むものが出てこない理由が…

Coq入門 - 4

coq

進捗あまりない。 update · 702639b · totem3/coq-prac · GitHub 全然わからんのでもうImportしたのを使って証明せずに進めているw できるところはそこまでにでてきた定理を使って証明して、まぁなんとなく感覚はわかってきたようなきていないような。 こう…

Coq入門 - 3

coq

Coq入門 - 2.1 - エンジニアですよ! に追記したが、Lemma le_n_0_eqが証明できた あと補完が効くようになったらなぜか.を押すだけでC-c C-n相当の部分まで進むようになった。 False_indやFalseの証明の仕方が少しわかった。 しかし、その後も証明ははかどら…

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

題名の通り。 効いてなかった。 よくわからんのでスルーしていたが、ストレスフルなので治すことにした。 Auto Complete Modeユーザーマニュアル auto-completeの情報は↑に素晴らしくまとまっていて、簡単に対応はわかった。 ダウンロードしたauto-complete…

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と…

Coq入門 - 2

coq

totem3/coq-prac こういうのをやることにした。 ただCoqの標準ライブラリからLemmaとTheoremを取り出してきただけ。 こんな初歩的なものなら簡単に証明できるだろ\(^o^)/ と思っていたら、いきなりできない・・・w Lemma le_n_0_eq n : n <= 0 -> 0 = n. …

Coq入門 - 1

coq

Agda入門にまんまと失敗して、Coqを入門してみることにした。 プログラミング Coq このチュートリアルをやっている。 色々調べてみると結構他にも入門はあって、先に調べるべきだったと思ったりした。 で、このチュートリアルは、とりあえず手を動かしてみる…

coq環境作って使う emacs + ProofGeneral

そもそもはProofGeneralが使いたいがためにEmacsを使い始めたが、とりあえずAgdaをやめてCoqをいじるようになった今、vimscripts/coq_IDEというやつでもいいかもしれないと思い始めているが・・・ Macでの導入は簡単。 homebrewを使う.もう何でもこれに頼っ…

agdaに挑戦して即死した話

agdaに挑戦し、即死した話 agdaは公式のチュートリアル(http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Othertutorials)に日本語の記事があったので、それをやることにした http://ocvs.cfv.jp/tr-data/PS2008-014.pdf こいつだ。 その前にまずagda…