coq
https://coq.inria.fr/を見ていたら、Documentationのところにこんなものがあった。 https://cel.archives-ouvertes.fr/file/index/docid/459139/filename/coq-hurry.pdf ここにSearchのことが少し書いてあって、SearchRewriteで望むものが出てこない理由が…
進捗あまりない。 update · 702639b · totem3/coq-prac · GitHub 全然わからんのでもうImportしたのを使って証明せずに進めているw できるところはそこまでにでてきた定理を使って証明して、まぁなんとなく感覚はわかってきたようなきていないような。 こう…
Coq入門 - 2.1 - エンジニアですよ! に追記したが、Lemma le_n_0_eqが証明できた あと補完が効くようになったらなぜか.を押すだけでC-c C-n相当の部分まで進むようになった。 False_indやFalseの証明の仕方が少しわかった。 しかし、その後も証明ははかどら…
題名の通り。 効いてなかった。 よくわからんのでスルーしていたが、ストレスフルなので治すことにした。 Auto Complete Modeユーザーマニュアル auto-completeの情報は↑に素晴らしくまとまっていて、簡単に対応はわかった。 ダウンロードしたauto-complete…
進捗ありません。 疑問メモ 矛盾を示すのが難しい forall n:nat, S n <= 0 と forall n:nat, S n > 0 があれば矛盾を示すのは簡単に見える けど、どうやるのかわからない forall n: nat, S n <= 0 はPropということでいいんだよな・・ CheckしてみるとPropと…
totem3/coq-prac こういうのをやることにした。 ただCoqの標準ライブラリからLemmaとTheoremを取り出してきただけ。 こんな初歩的なものなら簡単に証明できるだろ\(^o^)/ と思っていたら、いきなりできない・・・w Lemma le_n_0_eq n : n <= 0 -> 0 = n. …
Agda入門にまんまと失敗して、Coqを入門してみることにした。 プログラミング Coq このチュートリアルをやっている。 色々調べてみると結構他にも入門はあって、先に調べるべきだったと思ったりした。 で、このチュートリアルは、とりあえず手を動かしてみる…
そもそもはProofGeneralが使いたいがためにEmacsを使い始めたが、とりあえずAgdaをやめてCoqをいじるようになった今、vimscripts/coq_IDEというやつでもいいかもしれないと思い始めているが・・・ Macでの導入は簡単。 homebrewを使う.もう何でもこれに頼っ…
agdaに挑戦し、即死した話 agdaは公式のチュートリアル(http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Othertutorials)に日本語の記事があったので、それをやることにした http://ocvs.cfv.jp/tr-data/PS2008-014.pdf こいつだ。 その前にまずagda…